From: Tomáš Musil <tomik.musil@gmail.com>
Date: Thu, 30 Oct 2014 02:38:23 +0000 (+0100)
Subject: redukce
X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/c291e22383673d73f8e17e4de85bc68ad2f2c454

redukce
---

diff --git a/Lambda.hs b/Lambda.hs
index dbb2fcf..578c00f 100644
--- 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 (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
-  | 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)
+
+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)