ashley-woodard · May 22, 2018 04:14
diff --git a/untyped.hs b/untyped.hs
 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)

 --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)      = 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)    = 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')   = 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 . 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

 --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

 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
    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

 toChurch :: Int -> Term
 toChurch n = Abs 0 (Abs 1 (toChurch' n))
  where
    toChurch' 0 = Var 1
    toChurch' n = App (Var 0) (toChurch' (n-1))
	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)

	--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) = 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) = 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') = 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 . 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

	--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

	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
	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

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