diff --git a/.gitignore b/.gitignore index 253efe1..f955806 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,5 @@ /.stack-work -/stack.yaml.lock \ No newline at end of file +/stack.yaml.lock +*# +*~ +.#* \ No newline at end of file diff --git a/src/LCalc/Term.hs b/src/LCalc/Term.hs index 97e0cf3..d079581 100644 --- a/src/LCalc/Term.hs +++ b/src/LCalc/Term.hs @@ -1,14 +1,42 @@ {-# LANGUAGE OverloadedStrings #-} -module LCalc.Term where +module LCalc.Term ( alphaReduce + , betaReduce + , apply + , rename + , Term(..) + ) where -data Term = Variable String - | Abstraction String Term - | Application Term Term +data Term = Var String + | Lam String Term + | App Term Term instance Show Term where - show (Variable name) = name - show (Abstraction var term) = "(λ" ++ var ++ "." ++ show term ++ ")" - show (Application t1 t2) = "(" ++ show t1 ++ " " ++ show t2 ++ ")" + show (Var name) = name + show (Lam var term) = "(λ" ++ var ++ "." ++ show term ++ ")" + show (App t1 t2) = "(" ++ show t1 ++ " " ++ show t2 ++ ")" - +rename :: String -> String -> Term -> Term +rename old new (Lam name term) = Lam name $ rename old new term +rename old new (App t1 t2) = App + (rename old new t1) + (rename old new t2) +rename old new (Var name) = if old == name then Var new else Var name + +alphaReduce :: String -> Term -> Term +alphaReduce newname (Lam name term) = Lam newname + $ rename name newname term +alphaReduce _ t = t + +apply :: Term -> Term -> Term +apply (Lam x e) a = replace x e a +apply x1 + +replace :: String -> Term -> Term -> Term +replace v l@(Lam x b) a = if x == v then l else Lam x (replace v b a) +replace v (App x y) a = App (replace v x a) (replace v y a) +replace v o@(Var n) a = if v == n then a else o + +betaReduce :: Term -> Term +betaReduce (App t1 t2) = apply t1 t2 +betaReduce x = x diff --git a/src/Main.hs b/src/Main.hs index 7eb3e5a..3c99ad7 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -3,7 +3,7 @@ module Main (main) where import LCalc.Term t :: Term -t = Abstraction "x" (Application (Variable "x") (Variable "x")) +t = Lam "x" (App (Var "x") (Var "x")) main :: IO () main = putStrLn $ show t