Last active
May 22, 2018 04:14
-
-
Save lukeg101/9090f20f4a7b09f401df9390a0e357c9 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module ULC where | |
import Data.Set as S | |
import Data.Map.Lazy as M | |
--untyped lambda calculus - variables are numbers now as it's easier for renaming | |
data Term | |
= Var Int | |
| Abs Int Term | |
| App Term Term | |
deriving Ord | |
-- alpha equivalence of lambda terms as Eq instance for Lambda Terms | |
instance Eq Term where | |
a == b = checker (a, b) (M.empty, M.empty) 0 | |
-- checks for equality of terms, has a map (term, id) for each variable | |
-- each abstraction adds to the map and increments the id | |
-- variable occurrence checks for ocurrences in t1 and t2 using the logic: | |
-- if both bound, check that s is same in both maps | |
-- if neither is bound, check literal equality | |
-- if bound t1 XOR bound t2 == true then False | |
-- application recursively checks both the LHS and RHS | |
checker :: (Term, Term) -> (Map Int Int, Map Int Int) -> Int -> Bool | |
checker (Var x, Var y) (m1, m2) s = case M.lookup x m1 of | |
Just a -> case M.lookup y m2 of | |
Just b -> a == b | |
_ -> False | |
_ -> x == y | |
checker (Abs x t1, Abs y t2) (m1, m2) s = | |
checker (t1, t2) (m1', m2') (s+1) | |
where | |
m1' = M.insert x s m1 | |
m2' = M.insert y s m2 | |
checker (App a1 b1, App a2 b2) c s = | |
checker (a1, a2) c s && checker (b1, b2) c s | |
checker _ _ _ = False | |
--Show instance TODO brackets convention | |
instance Show Term where | |
show (Var x) = show x | |
show (App t1 t2) = '(':show t1 ++ ' ':show t2 ++ ")" | |
show (Abs x t1) = '(':"\x03bb" ++ show x++ "." ++ show t1 ++ ")" | |
--bound variables of a term | |
bound :: Term -> Set Int | |
bound (Var n) = S.empty | |
bound (Abs n t) = S.insert n $ bound t | |
bound (App t1 t2) = S.union (bound t1) (bound t2) | |
--free variables of a term | |
free :: Term -> Set Int | |
free (Var n) = S.singleton n | |
free (Abs n t) = S.delete n (free t) | |
free (App t1 t2) = S.union (free t1) (free t2) | |
--test to see if a term is closed (has no free vars) | |
closed :: Term -> Bool | |
closed = S.null . free | |
--subterms of a term | |
sub :: Term -> Set Term | |
sub t@(Var x) = S.singleton t | |
sub t@(Abs c t') = S.insert t $ sub t' | |
sub t@(App t1 t2) = S.insert t $ S.union (sub t1) (sub t2) | |
--element is bound in a term | |
notfree :: Int -> Term -> Bool | |
notfree x = not . S.member x . free | |
--set of variables in a term | |
vars :: Term -> Set Int | |
vars (Var x) = S.singleton x | |
vars (App t1 t2) = S.union (vars t1) (vars t2) | |
vars (Abs x t1) = S.insert x $ vars t1 | |
--generates a fresh variable name for a term | |
newlabel :: Term -> Int | |
newlabel = (+1) . maximum . vars | |
--rename t (x,y): renames free occurences of x in t to y | |
rename :: Term -> (Int, Int) -> Term | |
rename (Var a) (x,y) = if a == x then Var y else Var a | |
rename t@(Abs a t') (x,y) = if a == x then t else Abs a $ rename t' (x, y) | |
rename (App t1 t2) (x,y) = App (rename t1 (x,y)) (rename t2 (x,y)) | |
--substitute one term for another in a term | |
--does capture avoiding substitution | |
substitute :: Term -> (Term, Term) -> Term | |
substitute t1@(Var c1) (Var c2, t2) | |
= if c1 == c2 then t2 else t1 | |
substitute (App t1 t2) c | |
= App (substitute t1 c) (substitute t2 c) | |
substitute (Abs y s) c@(Var x, t) | |
| y == x = Abs y s | |
| y `notfree` t = Abs y $ substitute s c | |
| otherwise = Abs z $ substitute (rename s (y,z)) c | |
where z = max (newlabel s) (newlabel t) | |
--eta reduction | |
eta :: Term -> Maybe Term | |
eta (Abs x (App t (Var y))) | |
| x == y && x `notfree` t = Just t | |
| otherwise = Nothing | |
--term is normal form if has no subterms of the form (\x.s) t | |
isNormalForm :: Term -> Bool | |
isNormalForm = not . any testnf . sub | |
where | |
testnf t = case t of | |
(App (Abs _ _) _) -> True | |
_ -> False | |
--one-step reduction relation | |
reduce1 :: Term -> Maybe Term | |
reduce1 t@(Var x) = Nothing | |
reduce1 t@(Abs x s) = case reduce1 s of | |
Just s' -> Just $ Abs x s' | |
Nothing -> Nothing | |
reduce1 t@(App (Abs x t1) t2) | |
= Just $ substitute t1 (Var x, t2) --beta conversion | |
reduce1 t@(App t1 t2) = case reduce1 t1 of | |
Just t' -> Just $ App t' t2 | |
_ -> case reduce1 t2 of | |
Just t' -> Just $ App t1 t' | |
_ -> Nothing | |
--multi-step reduction relation - NOT GUARANTEED TO TERMINATE | |
reduce :: Term -> Term | |
reduce t = case reduce1 t of | |
Just t' -> reduce t' | |
Nothing -> t | |
---multi-step reduction relation that accumulates all reduction steps | |
reductions :: Term -> [Term] | |
reductions t = case reduce1 t of | |
Just t' -> t' : reductions t' | |
_ -> [] | |
--common combinators | |
i = Abs 1 (Var 1) | |
true = Abs 1 (Abs 2 (Var 1)) | |
false = Abs 1 (Abs 2 (Var 2)) | |
zero = false | |
xx = Abs 1 (App (Var 1) (Var 1)) | |
omega = App xx xx | |
_if = \c t f -> App (App c t) f | |
_isZero = \n -> _if n false true | |
_succ = Abs 0 $ Abs 1 $ Abs 2 $ App (Var 1) $ App (App (Var 0) (Var 1)) (Var 2) | |
appsucc = App _succ | |
-- function from Haskell Int to Church Numeral | |
toChurch :: Int -> Term | |
toChurch n = Abs 0 (Abs 1 (toChurch' n)) | |
where | |
toChurch' 0 = Var 1 | |
toChurch' n = App (Var 0) (toChurch' (n-1)) | |
test1 = App i (Abs 1 (App (Var 1) (Var 1))) | |
test2 = App (App (Abs 1 (Abs 2 (Var 2))) (Var 2)) (Var 4) | |
test3 = App (App (toChurch 3) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment