-
Notifications
You must be signed in to change notification settings - Fork 0
/
LambdaCalc.hs
82 lines (72 loc) · 2.62 KB
/
LambdaCalc.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
-- Copyright © 2014 Garrison Jensen
-- License
-- This code and text are dedicated to the public domain.
-- You can copy, modify, distribute and perform the work,
-- even for commercial purposes, all without asking permission.
-- For more information, please refer to <http://unlicense.org/>
-- or the accompanying LICENSE file.
--
module LambdaCalc
( eval,
Expr(Var, Lam, App),
VarName(VC)
) where
type VColor = Int
data VarName = VC VColor String deriving (Eq, Show)
data Expr
= Var VarName
| Lam VarName Expr
| App Expr Expr
deriving (Eq)
instance Show Expr where
show (Var (VC _ s)) = s
show (Lam (VC _ s) e) = "λ" ++ s ++ "." ++ show e
show (App e1 e2) = "(" ++ show e1 ++ ")(" ++ show e2 ++ ")"
eval :: Expr -> Expr
eval expr = eval' expr []
eval' :: Expr -> [Expr] -> Expr
eval' v@(Var n) [] = v
eval' v@(Var n) stack = unwind v stack
eval' (Lam v e) [] = etaRed $ Lam v (eval e)
eval' (Lam v e) (x:stack) = eval' (betaRed e v x) stack
eval' (App e1 e2) stack = eval' e1 (e2:stack)
unwind :: Expr -> [Expr] -> Expr
unwind = foldl (\ expr x -> App expr $ eval x)
-- (λx.Mx) ==> M
etaRed :: Expr -> Expr
etaRed (Lam v (App e (Var v')))
| v == v' && (let (o,n) = occurs e v in not o) = e
etaRed expr = expr
-- (λx.Mx)N ==> M[x := N]
betaRed :: Expr -> VarName -> Expr -> Expr
betaRed expr v (Var v') | v == v' = expr
betaRed t@(Var v) n e
| v == n = e
| otherwise = t
betaRed (App e1 e2) v e = App (betaRed e1 v e) (betaRed e2 v e)
betaRed t@(Lam x _) v _ | v == x = t
betaRed (Lam x body) v e = Lam x' (betaRed body' v e)
where
(f,xIne) = occurs e x
(x',body') =
if f then
let uniXinE = colorpplus' (colorpplus x xIne) v
(bf,xOccurBody) = occurs body uniXinE
uniX = if bf
then colorpplus uniXinE xOccurBody
else uniXinE
in (uniX,betaRed body x (Var x'))
else (x,body)
colorpplus (VC c n) (VC c' _) = VC (max c c' + 1) n
colorpplus' v1@(VC _ n) v2@(VC _ n') =
if n==n' then colorpplus v1 v2 else v1
occurs :: Expr -> VarName -> (Bool, VarName)
occurs (Var v@(VC c name)) v'@(VC c' name')
| name /= name' = (False, v)
| c == c' = (True, v)
| otherwise = (False,v')
occurs (App t1 t2) v = let (f1,v1@(VC c1 _)) = occurs t1 v
(f2,v2@(VC c2 _)) = occurs t2 v
in (f1 || f2, if c1 > c2 then v1 else v2)
occurs (Lam x body) v | x == v = (False,v)
| otherwise = occurs body v