redukce

[fp.git] / Lambda.hs

diff --git a/Lambda.hs b/Lambda.hs
index d9bdaee..578c00f 100644 (file)
--- a/Lambda.hs
+++ b/Lambda.hs
@@ -37,8 +37,35 @@ parseApp = do
   t <- parseTerm
   char ' '
   r <- parseTerm
   t <- parseTerm
   char ' '
   r <- parseTerm

-  char '('
+  char ')'

   return $! App t r
 
 parseTerm :: Parser Term
 parseTerm = parseVar <|> parseLambda <|> parseApp
   return $! App t r
 
 parseTerm :: Parser Term
 parseTerm = parseVar <|> parseLambda <|> parseApp

+
+-------------------------------------------------
+
+isFreeIn :: VarName -> Term -> Bool
+isFreeIn x (Var v) = x == v
+isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
+isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
+
+rename :: Term -> Term
+rename (Lambda x t) = Lambda n (substitute x (Var n) t)
+  where n = rnm x 
+        rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
+
+substitute :: VarName -> Term -> Term -> Term
+substitute a b (Var x) = if x == a then b else Var x
+substitute a b (Lambda x t) 
+  | x == a = Lambda x t
+  | x `isFreeIn` 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)
+
+reduce :: Term -> Term
+reduce (Var x) = Var x
+reduce (Lambda x t) = Lambda x (reduce t)
+reduce (App t u) = app (reduce t) u
+  where app (Lambda x v) w = reduce $ substitute x w v
+        app a b = App a (reduce b)