substitution
authorTomáš Musil <tomik.musil@gmail.com>
Thu, 30 Oct 2014 01:57:46 +0000 (02:57 +0100)
committerTomáš Musil <tomik.musil@gmail.com>
Thu, 30 Oct 2014 01:57:46 +0000 (02:57 +0100)
Lambda.hs

index d9bdaee..dbb2fcf 100644 (file)
--- a/Lambda.hs
+++ b/Lambda.hs
@@ -37,8 +37,22 @@ parseApp = do
   t <- parseTerm
   char ' '
   r <- parseTerm
-  char '('
+  char ')'
   return $! App t r
 
 parseTerm :: Parser Term
 parseTerm = parseVar <|> parseLambda <|> parseApp
+
+-------------------------------------------------
+
+rename :: Term -> Term
+rename (Lambda x t) = Lambda n (substitute x n t)
+  where n = x ++ "r"
+
+substitute :: VarName -> VarName -> Term -> Term
+substitute a b (Var x) = if x == a then Var b else Var x
+substitute a b (Lambda x t) 
+  | x == a = Lambda x t
+  | x == b = substitute a b $ rename (Lambda x t)
+  | otherwise = Lambda x (substitute a b t)
+substitute a b (App t u) = App (substitute a b t) (substitute a b u)