From c291e22383673d73f8e17e4de85bc68ad2f2c454 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Tom=C3=A1=C5=A1=20Musil?= Date: Thu, 30 Oct 2014 03:38:23 +0100 Subject: [PATCH] redukce --- Lambda.hs | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) 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) -- 2.4.2