redukce

diff --git a/Lambda.hs b/Lambda.hs
index dbb2fcf..578c00f 100644 (file)
--- a/Lambda.hs
+++ b/Lambda.hs
@@ -45,14 +45,27 @@ 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 :: Term -> Term

-rename (Lambda x t) = Lambda n (substitute x n t)
-  where n = x ++ "r"
+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 -> VarName -> Term -> Term
-substitute a b (Var x) = if x == a then Var b else Var x
+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
 substitute a b (Lambda x t) 
   | x == a = Lambda x t

-  | x == b = substitute a b $ rename (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)
   | 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)