-
Notifications
You must be signed in to change notification settings - Fork 1
/
ULC.hs
280 lines (217 loc) · 7.68 KB
/
ULC.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
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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
{-|
Module : ULC
Description : Deep-embedding of the untyped lambda calculus in Haskell.
Copyright : (c) Luke Geeson, 2018
License : GPL-3
Maintainer : [email protected]
Stability : stable
Portability : POSIX
The "ULC" module denotes the tree types of the untyped lambda calculus. This languages is implemented as a deep embedding into Haskell, with all the canonical helper functions it needs.
-}
module ULC where
-- Tool imports.
import qualified Data.Set as S
import qualified Data.Map.Lazy as M
import qualified Data.Maybe as Maybe
-- | Untyped lambda calculus ADT.
-- Variables are strings of lower case characters.
-- Abstractions take a variable name "x" and a subterm.
data Term
= Var VarName
| Abs VarName Term
| App Term Term
deriving Ord
-- | Type Synonym for variable names in a term.
type VarName = String
-- | Alpha equivalence of lambda terms is the Eq instance Terms.
-- Concretely we use the "termEquality" function to represent this
instance Eq Term where
a == b = termEquality (a, b) (M.empty, M.empty) 0
-- | Checks for equality of terms using a map (term, id) for each variable.
-- Each abstraction inserts into the map and increments the id.
-- Variable occurrence checks for occurrences in t1 and t2 using the logic:
-- * if both variables bound, check that s is same in both maps
-- * if neither is bound, check literal equality
-- * if bound t1 XOR bound t2 == True then False
-- application recursively checks both the LHS and RHS of applications.
termEquality :: (Term, Term)
-> (M.Map String Int, M.Map String Int)
-> Int
-> Bool
termEquality (Var x, Var y) (m1, m2) _
= let testEq = do a <- M.lookup x m1
b <- M.lookup y m2
return $ a == b
in Maybe.fromMaybe (x == y) testEq
termEquality (Abs x t1, Abs y t2) (m1, m2) s
= let newm1 = M.insert x s m1
newm2 = M.insert y s m2
in termEquality (t1, t2) (newm1, newm2) (s+1)
termEquality (App a1 b1, App a2 b2) c s
= termEquality (a1, a2) c s && termEquality (b1, b2) c s
termEquality _ _ _ = False
-- | Show instance for ULC terms.
instance Show Term where
show (Var x)
= x
show (App t1 t2)
= paren (isAbs t1) (show t1)
++ " "
++ paren (isAbs t2 || isApp t2) (show t2)
show (Abs x t1)
= "\x03bb"
++ x
++ "."
++ show t1
-- | Helper function encloses the input string in (parens) if the
-- first parameter is true.
paren :: Bool -> String -> String
paren True x = "(" ++ x ++ ")"
paren False x = x
-- | Helper function returns true if the term is an abstraction.
isAbs :: Term -> Bool
isAbs (Abs _ _) = True
isAbs _ = False
-- | Helper function returns true if the term is an application.
isApp :: Term -> Bool
isApp (App _ _) = True
isApp _ = False
-- | Function returns a set of bound variables of a term.
bound :: Term -> S.Set VarName
bound (Var _) = S.empty
bound (Abs n t) = S.insert n $ bound t
bound (App t1 t2) = S.union (bound t1) (bound t2)
-- | Function returns a set of free variables of a term.
free :: Term -> S.Set VarName
free (Var n) = S.singleton n
free (Abs n t) = S.delete n (free t)
free (App t1 t2) = S.union (free t1) (free t2)
-- | Function tests to see if a term is closed (has no free vars).
closed :: Term -> Bool
closed = S.null . free
-- | Function returns the set of subterms of a term.
sub :: Term -> S.Set Term
sub t@(Var _) = S.singleton t
sub t@(Abs _ t') = S.insert t $ sub t'
sub t@(App t1 t2) = S.insert t $ S.union (sub t1) (sub t2)
-- | Function determines if a variable is bound in a term.
notfree :: VarName -> Term -> Bool
notfree x = not . S.member x . free
-- | Function returns the set of variables in a term.
vars :: Term -> S.Set VarName
vars (Var x) = S.singleton x
vars (App t1 t2) = S.union (vars t1) (vars t2)
vars (Abs x t1) = S.insert x $ vars t1
-- | Function generates a fresh variable name for a term.
newlabel :: Term -> VarName
newlabel x = head . dropWhile (`elem` vars x)
$ iterate genVar $ S.foldr biggest "" $ vars x
-- | Function generates fresh variable names from a given variable.
genVar :: VarName -> VarName
genVar [] = "a"
genVar ('z':xs) = 'a':genVar xs
genVar ( x :xs) = succ x:xs
-- | Function is the length-observing maximum function
-- that falls back on lexicographic ordering
biggest :: VarName -> VarName -> VarName
biggest xs ys = if length xs > length ys
then xs
else max xs ys
-- | Function renames a term.
--rename t (x,y) renames free occurrences of x in t to y
rename :: Term -> (VarName, VarName) -> Term
rename (Var a) (x,y) = if a == x
then Var y
else Var a
rename t@(Abs a t') (x,y) = if a == x
then t
else Abs a $ rename t' (x, y)
rename (App t1 t2) (x,y) = App (rename t1 (x,y)) (rename t2 (x,y))
-- | Function substitutes one term for another in a term
-- does capture avoiding substitution (Berendregt)
substitute :: Term -> (Term, Term) -> Term
substitute t1@(Var c1) (Var c2, t2)
= if c1 == c2
then t2
else t1
substitute (App t1 t2) c
= App (substitute t1 c) (substitute t2 c)
substitute (Abs y s) c@(Var x, t)
| y == x = Abs y s
| y `notfree` t = Abs y $ substitute s c
| otherwise = Abs z $ substitute (rename s (y,z)) c
where z = foldr1 biggest [newlabel s, newlabel t, newlabel (Var x)]
substitute s _ = s
-- | Eta reduction on a term. May fail if the term is not of the form:
-- (\x.M) y
eta :: Term -> Maybe Term
eta (Abs x (App t (Var y)))
| x == y && x `notfree` t = Just t
| otherwise = Nothing
eta _ = Nothing
-- | Function determines whether a term is a normal form.
-- A term is a normal form if has no subterms of the form (\x.s) t
isNormalForm :: Term -> Bool
isNormalForm
= let testnf t = case t of
(App (Abs _ _) _) -> True
_ -> False
in not . any testnf . sub
-- | One-step reduction relation on terms.
reduce1 :: Term -> Maybe Term
reduce1 (Var _)
= Nothing
reduce1 (Abs x s)
= Abs x <$> reduce1 s
reduce1 (App (Abs x t1) t2)
= return $ substitute t1 (Var x, t2) --beta conversion
reduce1 (App t1 t2)
= let reduceLeft = do t' <- reduce1 t1
return $ App t' t2
reduceRight = App t1 <$> reduce1 t2
in if Maybe.isJust reduceLeft
then reduceLeft
else reduceRight
-- | Multi-step reduction relation.
-- NOT GUARANTEED TO TERMINATE
reduce :: Term -> Term
reduce t = maybe t reduce (reduce1 t)
-- | Multi-step reduction relation that accumulates all reduction steps.
-- useful for logging how a term reduces.
reductions :: Term -> [Term]
reductions t = case reduce1 t of
Just t' -> t' : reductions t'
_ -> []
--common combinators
-- | Identity Combinator
i :: Term
i = Abs "a" (Var "a")
-- | True
true :: Term
true = Abs "a" (Abs "b" (Var "a"))
-- | False
false :: Term
false = Abs "a" (Abs "b" (Var "b"))
-- | Zero, Church Style
zero = false
-- | Canonical self-applying \x.x x
--used as the basis for recursion
xx = Abs "x" (App (Var "x") (Var "x"))
-- | Canonical infinitely reducing term.
omega = App xx xx
-- | If statement
_if c t = App (App c t)
-- | Test of is_zero encoded
_isZero n = _if n false true
-- | The sucessor of numbers church style
_succ = Abs "x" $ Abs "y"
$ Abs "z" $ App (Var "y")
$ App (App (Var "x") (Var "y")) (Var "z")
-- | Applies succ to some term
appsucc = App _succ
-- | Function from Haskell Int to Church Numeral
toChurch :: Int -> Term
toChurch n = Abs "x" (Abs "f" (toChurch' n))
where
toChurch' 0 = Var "x"
toChurch' n = App (Var "x") (toChurch' (n-1))