Skip to content

Instantly share code, notes, and snippets.

@ashley-woodard

ashley-woodard/ULC.hs

Forked from lukeg101/ULC.hs
Created May 22, 2018 04:14
Show Gist options
  • Save ashley-woodard/bedbfcd50ab1fc81c76fab7d01b9dd1e to your computer and use it in GitHub Desktop.
Save ashley-woodard/bedbfcd50ab1fc81c76fab7d01b9dd1e to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. @lukeg101 lukeg101 revised this gist Mar 21, 2018. 1 changed file with 8 additions and 1 deletion.
    9 changes: 8 additions & 1 deletion ULC.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -149,6 +149,7 @@ _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
    @@ -157,4 +158,10 @@ toChurch n = Abs 0 (Abs 1 (toChurch' n))

    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)
    test3 = App (App (toChurch 3) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)






  2. @lukeg101 lukeg101 renamed this gist Mar 21, 2018. 1 changed file with 0 additions and 0 deletions.
    0 untyped.hs → ULC.hs
    View file
    File renamed without changes.
  3. @lukeg101 lukeg101 revised this gist Mar 21, 2018. 1 changed file with 43 additions and 18 deletions.
    61 changes: 43 additions & 18 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,14 +1,41 @@
    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 (Eq, Ord)

    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
    @@ -17,35 +44,35 @@ instance Show Term where

    --bound variables of a term
    bound :: Term -> Set Int
    bound (Var n) = empty
    bound (Abs n t) = insert n $ bound t
    bound (App t1 t2) = union (bound t1) (bound t2)
    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) = singleton n
    free (Abs n t) = delete n (free t)
    free (App t1 t2) = union (free t1) (free t2)
    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) = singleton t
    sub t@(Abs c t') = insert t $ sub t'
    sub t@(App t1 t2) = insert t $ union (sub t1) (sub t2)
    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 . member x . free
    notfree x = not . S.member x . free

    --set of variables in a term
    vars :: Term -> Set Int
    vars (Var x) = singleton x
    vars (App t1 t2) = union (vars t1) (vars t2)
    vars (Abs x t1) = insert x $ vars t1
    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
    @@ -130,6 +157,4 @@ toChurch n = Abs 0 (Abs 1 (toChurch' n))

    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)


    test3 = App (App (toChurch 3) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)
  4. @lukeg101 lukeg101 revised this gist Mar 12, 2018. 1 changed file with 0 additions and 4 deletions.
    4 changes: 0 additions & 4 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -133,7 +133,3 @@ 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)






  5. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 9 additions and 6 deletions.
    15 changes: 9 additions & 6 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,5 @@
    module ULC where

    import Data.Set as S

    --untyped lambda calculus - variables are numbers now as it's easier for renaming
    @@ -88,7 +90,8 @@ 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 (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
    @@ -101,10 +104,6 @@ reduce t = case reduce1 t of
    Just t' -> reduce t'
    Nothing -> t

    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)

    ---multi-step reduction relation that accumulates all reduction steps
    reductions :: Term -> [Term]
    reductions t = case reduce1 t of
    @@ -128,7 +127,11 @@ 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)




  6. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 29 additions and 23 deletions.
    52 changes: 29 additions & 23 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,4 +1,3 @@
    import Data.List
    import Data.Set as S

    --untyped lambda calculus - variables are numbers now as it's easier for renaming
    @@ -8,41 +7,45 @@ data Term
    | App Term Term
    deriving (Eq, Ord)

    --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 ++ ")"
    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)
    bound (Var n) = empty
    bound (Abs n t) = insert n $ bound t
    bound (App t1 t2) = union (bound t1) (bound t2)

    --free variables of a term
    free :: Term -> Set Int
    free (Var n) = singleton n
    free (Abs n t) = (free t) S.\\ (singleton n)
    free (App t1 t2) = S.union (free t1) (free t2)
    free (Var n) = singleton n
    free (Abs n t) = delete n (free t)
    free (App t1 t2) = 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) = 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)
    sub t@(Var x) = singleton t
    sub t@(Abs c t') = insert t $ sub t'
    sub t@(App t1 t2) = insert t $ union (sub t1) (sub t2)

    --element is bound in a term
    notfree :: Int -> Term -> Bool
    notfree x = not . elem x . free
    notfree x = not . member x . free

    --set of variables in a term
    vars :: Term -> Set Int
    vars (Var x) = singleton x
    vars (App t1 t2) = S.union (vars t1) (vars t2)
    vars (Abs x t1) = S.insert x $ vars t1
    vars (Var x) = singleton x
    vars (App t1 t2) = union (vars t1) (vars t2)
    vars (Abs x t1) = insert x $ vars t1

    --generates a fresh variable name for a term
    newlabel :: Term -> Int
    newlabel = (+1) . maximum . vars

    @@ -55,8 +58,10 @@ 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 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
    @@ -71,10 +76,11 @@ eta (Abs x (App t (Var y)))

    --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
    isNormalForm = not . any testnf . sub
    where
    testnf t = case t of
    (App (Abs _ _) _) -> True
    _ -> False

    --one-step reduction relation
    reduce1 :: Term -> Maybe Term
  7. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 5 additions and 5 deletions.
    10 changes: 5 additions & 5 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -22,7 +22,7 @@ bound (App t1 t2) = S.union (bound t1) (bound t2)
    --free variables of a term
    free :: Term -> Set Int
    free (Var n) = singleton n
    free (Abs n t) = S.filter (/= n) $ free t
    free (Abs n t) = (free t) S.\\ (singleton n)
    free (App t1 t2) = S.union (free t1) (free t2)

    --test to see if a term is closed (has no free vars)
    @@ -38,10 +38,10 @@ sub t@(App t1 t2) = S.insert t $ S.union (sub t1) (sub t2)
    notfree :: Int -> Term -> Bool
    notfree x = not . elem x . free

    vars :: Term -> [Int]
    vars (Var x) = [x]
    vars (App t1 t2) = vars t1 ++ vars t2
    vars (Abs x t1) = x: vars t1
    vars :: Term -> Set Int
    vars (Var x) = singleton x
    vars (App t1 t2) = S.union (vars t1) (vars t2)
    vars (Abs x t1) = S.insert x $ vars t1

    newlabel :: Term -> Int
    newlabel = (+1) . maximum . vars
  8. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 24 additions and 22 deletions.
    46 changes: 24 additions & 22 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,37 +1,39 @@
    import Data.List
    import Data.Set as S

    --untyped lambda calculus - variables are numbers now as it's easier for renaming
    data Term
    = Var Int
    | Abs Int Term
    | App Term Term
    deriving (Eq, Ord)

    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 -> [Int]
    bound (Var n) = []
    bound (Abs n t) = n:bound t
    bound (App t1 t2) = bound t1 ++ bound t2
    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 -> [Int]
    free (Var n) = [n]
    free (Abs n t) = filter (/= n) $ free t
    free (App t1 t2) = free t1 ++ free t2
    free :: Term -> Set Int
    free (Var n) = singleton n
    free (Abs n t) = S.filter (/= 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 = null . free
    closed = S.null . free

    --subterms of a term
    sub :: Term -> [Term]
    sub t@(Var x) = [t]
    sub t@(Abs c t') = t:sub t'
    sub t@(App t1 t2) = t:sub t1 ++ sub t2
    sub :: Term -> Set Term
    sub t@(Var x) = 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)

    notfree :: Int -> Term -> Bool
    notfree x = not . elem x . free
    @@ -88,19 +90,20 @@ reduce1 t@(App t1 t2) = case reduce1 t1 of
    _ -> Nothing

    --multi-step reduction relation - NOT GUARANTEED TO TERMINATE
    reduceM :: Term -> Term
    reduceM t = case reduce1 t of
    Just t' -> reduceM t'
    reduce :: Term -> Term
    reduce t = case reduce1 t of
    Just t' -> reduce t'
    Nothing -> t

    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)

    ---multi-step reduction relation that accumulates all reduction steps
    reduceM_ :: Term -> [Term] -> [Term]
    reduceM_ t l = case reduce1 t of
    Just t' -> reduceM_ t' (t:l)
    _ -> reverse (t:l)
    reductions :: Term -> [Term]
    reductions t = case reduce1 t of
    Just t' -> t' : reductions t'
    _ -> []

    --common combinators
    i = Abs 1 (Var 1)
    @@ -120,8 +123,7 @@ toChurch n = Abs 0 (Abs 1 (toChurch' n))
    toChurch' 0 = Var 1
    toChurch' n = App (Var 0) (toChurch' (n-1))

    myTest :: Term
    myTest = App (App (toChurch 3) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)




  9. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 4 additions and 4 deletions.
    8 changes: 4 additions & 4 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -46,7 +46,7 @@ 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) = Var y
    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))

    @@ -56,9 +56,9 @@ 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 /= x && y `notfree` t = Abs y $ substitute s c
    | otherwise = Abs z $ substitute s (Var x, (rename t (y, z)))
    | 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
  10. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -56,9 +56,9 @@ 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 == x = (Abs y s)
    | y /= x && y `notfree` t = Abs y $ substitute s c
    | otherwise = Abs y $ substitute s (Var x, (rename t (y, z)))
    | otherwise = Abs z $ substitute s (Var x, (rename t (y, z)))
    where z = max (newlabel s) (newlabel t)

    --eta reduction
  11. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 3 additions and 3 deletions.
    6 changes: 3 additions & 3 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -55,9 +55,9 @@ rename (App t1 t2) (x,y) = App (rename t1 (x,y)) (rename t2 (x,y))
    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)
    substitute (Abs y s) c@(Var x, t)
    | y == x = Abs y s
    | y /= x && y `notfree` t = Abs y $ substitute s c
    | y == x = (Abs y s)
    | otherwise = Abs y $ substitute s (Var x, (rename t (y, z)))
    where z = max (newlabel s) (newlabel t)

    @@ -121,7 +121,7 @@ toChurch n = Abs 0 (Abs 1 (toChurch' n))
    toChurch' n = App (Var 0) (toChurch' (n-1))

    myTest :: Term
    myTest = App (App (toChurch 1) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)
    myTest = App (App (toChurch 3) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)



  12. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 9 additions and 0 deletions.
    9 changes: 9 additions & 0 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -57,6 +57,7 @@ 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 && y `notfree` t = Abs y $ substitute s c
    | y == x = (Abs y s)
    | otherwise = Abs y $ substitute s (Var x, (rename t (y, z)))
    where z = max (newlabel s) (newlabel t)

    @@ -113,6 +114,14 @@ _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

    toChurch :: Int -> Term
    toChurch n = Abs 0 (Abs 1 (toChurch' n))
    where
    toChurch' 0 = Var 1
    toChurch' n = App (Var 0) (toChurch' (n-1))

    myTest :: Term
    myTest = App (App (toChurch 1) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)



  13. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 6 additions and 2 deletions.
    8 changes: 6 additions & 2 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -76,11 +76,15 @@ isNormalForm = not . any testnf . sub where
    --one-step reduction relation
    reduce1 :: Term -> Maybe Term
    reduce1 t@(Var x) = Nothing
    reduce1 t@(Abs x s) = 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
    _ -> Nothing
    _ -> case reduce1 t2 of
    Just t' -> Just $ App t1 t'
    _ -> Nothing

    --multi-step reduction relation - NOT GUARANTEED TO TERMINATE
    reduceM :: Term -> Term
  14. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -106,8 +106,8 @@ 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 = \n -> Abs 1 $ Abs 2 $ App (Var 1) $ App (App n (Var 1)) (Var 2)
    _succ = Abs 0 $ Abs 1 $ Abs 2 $ App (Var 1) $ App (App (Var 0) (Var 1)) (Var 2)
    appsucc = App _succ



  15. @lukeg101 lukeg101 revised this gist Mar 8, 2018. 1 changed file with 13 additions and 7 deletions.
    20 changes: 13 additions & 7 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -33,13 +33,6 @@ sub t@(Var x) = [t]
    sub t@(Abs c t') = t:sub t'
    sub t@(App t1 t2) = t:sub t1 ++ sub t2

    --common combinators
    i = Abs 1 (Var 1)
    true = Abs 1 (Abs 2 (Var 1))
    false = Abs 1(Abs 2 (Var 2))
    xx = Abs 1 (App (Var 1) (Var 1))
    omega = App xx xx

    notfree :: Int -> Term -> Bool
    notfree x = not . elem x . free

    @@ -104,6 +97,19 @@ reduceM_ t l = case reduce1 t of
    Just t' -> reduceM_ t' (t:l)
    _ -> reverse (t:l)

    --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 = \n -> Abs 1 $ Abs 2 $ App (Var 1) $ App (App n (Var 1)) (Var 2)






  16. @lukeg101 lukeg101 created this gist Mar 8, 2018.
    109 changes: 109 additions & 0 deletions untyped.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,109 @@
    import Data.List

    --untyped lambda calculus - variables are numbers now as it's easier for renaming
    data Term
    = Var Int
    | Abs Int Term
    | App Term Term

    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 -> [Int]
    bound (Var n) = []
    bound (Abs n t) = n:bound t
    bound (App t1 t2) = bound t1 ++ bound t2

    --free variables of a term
    free :: Term -> [Int]
    free (Var n) = [n]
    free (Abs n t) = filter (/= n) $ free t
    free (App t1 t2) = free t1 ++ free t2

    --test to see if a term is closed (has no free vars)
    closed :: Term -> Bool
    closed = null . free

    --subterms of a term
    sub :: Term -> [Term]
    sub t@(Var x) = [t]
    sub t@(Abs c t') = t:sub t'
    sub t@(App t1 t2) = t:sub t1 ++ sub t2

    --common combinators
    i = Abs 1 (Var 1)
    true = Abs 1 (Abs 2 (Var 1))
    false = Abs 1(Abs 2 (Var 2))
    xx = Abs 1 (App (Var 1) (Var 1))
    omega = App xx xx

    notfree :: Int -> Term -> Bool
    notfree x = not . elem x . free

    vars :: Term -> [Int]
    vars (Var x) = [x]
    vars (App t1 t2) = vars t1 ++ vars t2
    vars (Abs x t1) = x: vars t1

    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) = Var y
    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 && y `notfree` t = Abs y $ substitute s c
    | otherwise = Abs y $ substitute s (Var x, (rename t (y, z)))
    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) = 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
    _ -> Nothing

    --multi-step reduction relation - NOT GUARANTEED TO TERMINATE
    reduceM :: Term -> Term
    reduceM t = case reduce1 t of
    Just t' -> reduceM t'
    Nothing -> t

    test1 = App i (Abs 1 (App (Var 1) (Var 1)))
    test2 = App (App (Abs 1 (Abs 2 (Var 2))) (Var 2)) (Var 4)

    ---multi-step reduction relation that accumulates all reduction steps
    reduceM_ :: Term -> [Term] -> [Term]
    reduceM_ t l = case reduce1 t of
    Just t' -> reduceM_ t' (t:l)
    _ -> reverse (t:l)