blob: c733617854376335dcd26b902e6fe9fd0b83ecad (
plain)
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
module LambdaCalc where
import Data.Char (isSpace)
data Term = Variable String
| Abstraction Term Term
| Application Term Term
deriving (Eq)
instance Show Term where
show (Variable s) = s
show (Abstraction varName body) = '\x03BB':show varName ++ '.':show body
show (Application x y) = x' ++ ' ':y'
where
x' = if isAbstraction x then '(':show x ++ ")" else show x
y' = if isVariable y then show y else '(':show y ++ ")"
var :: String -> Term
var "" = error "cannot name a variable with an empty string"
var s
| any ( \c -> isSpace c || c `elem` "().\x03BB") s = error "name has forbidden characters"
| otherwise = Variable s
lambda :: String -> Term -> Term
lambda s t = Abstraction (var s) t
apply :: Term -> Term -> Term
apply = Application
infixl 6 <+>
(<+>) :: Term -> Term -> Term
(<+>) = apply
-- same as apply or <+>, but also beta reduces the result
infixl 6 <++>
(<++>) :: Term -> Term -> Term
x <++> y = betaReduce $ x <+> y
isVariable :: Term -> Bool
isVariable (Variable _) = True
isVariable _ = False
isAbstraction :: Term -> Bool
isAbstraction (Abstraction _ _) = True
isAbstraction _ = False
isApplication :: Term -> Bool
isApplication (Application _ _) = True
isApplication _ = False
isNormal :: Term -> Bool
isNormal (Variable _) = True
isNormal (Abstraction _ b) = isNormal b
isNormal (Application x y) = not (isAbstraction x) && isNormal x && isNormal y
betaStep :: Term -> Term
betaStep (Variable v) = Variable v
betaStep (Abstraction v body) = Abstraction v $ betaStep body
betaStep (Application x y)
| isAbstraction x = deAbstract x y
| otherwise = Application (betaStep x) (betaStep y)
betaPath :: Term -> [Term]
betaPath e
| isNormal e = [e]
| otherwise = e:betaPath (betaStep e)
betaReduce :: Term -> Term
betaReduce = last . betaPath
deAbstract :: Term -> Term -> Term
deAbstract (Abstraction v body) arg = go body
where
go v'@(Variable _)
| v == v' = arg
| otherwise = v'
go a@(Abstraction v' body')
| v == v' = a
| otherwise = Abstraction v' $ go body'
go (Application x y) = Application (go x) (go y)
deAbstract _ _ = error "deAbstract: first argument must an abstraction"
{- Common combinators -}
combI :: Term
combI = lambda "x" $ var "x"
identity :: Term
identity = combI
combK :: Term
combK = lambda "a" $ lambda "b" $ var "a"
constant :: Term
constant = combK
combKI :: Term
combKI = lambda "a" $ lambda "b" $ var "b"
combB :: Term
combB = lambda "f" $ lambda "g" $ lambda "a" body
where
body = var "f" <+> (var "g" <+> var "a")
compose :: Term
compose = combB
combC :: Term
combC = lambda "f" $ lambda "a" $ lambda "b" $ var "f" <+> var "b" <+> var "a"
{- Boolean values and operations -}
-- assumes valid input
fromBool :: Term -> Bool
fromBool e = case e <++> var "_TRUE" <++> var "_FALSE" of
Variable "_TRUE" -> True
Variable "_FALSE" -> False
_ -> error "could not recognize lambda expression as boolean"
bTrue :: Term
bTrue = lambda "x" $ lambda "y" $ var "x"
bFalse :: Term
bFalse = lambda "x" $ lambda "y" $ var "y"
bNot :: Term
bNot = lambda "b" $ var "b" <++> bFalse <++> bTrue
bOr :: Term
bOr = lambda "p" $ lambda "q" body
where
body = var "p" <++> var "p" <++> var "q"
bAnd :: Term
bAnd = lambda "p" $ lambda "q" body
where
body = var "p" <++> var "q" <++> var "p"
bEq :: Term
bEq = lambda "p" $ lambda "q" body
where
body = var "p" <++> var "q" <++> (bNot <++> var "q")
bXor :: Term
bXor = lambda "p" $ lambda "q" body
where
body = var "p" <++> (bNot <++> var "q") <++> var "q"
bImplies :: Term
bImplies = lambda "p" $ lambda "q" body
where
body = var "p" <++> var "q" <++> bTrue
bConverse :: Term
bConverse = combC <++> bImplies
|
