|
@ -1,14 +1,42 @@ |
|
|
{-# LANGUAGE OverloadedStrings #-} |
|
|
{-# 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 |
|
|
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 |