git @ Cat's Eye Technologies Lariat / c75fce8
Implement `idBetaReducible` to support the `reduce` example. Chris Pressey 3 years ago
2 changed file(s) with 24 addition(s) and 13 deletion(s). Raw diff Collapse all Expand all
+3
-6
README.md less more
232232 is an abstraction term. Then we `resolve` the abstraction
233233 with the application term's second subterm.
234234
235 --
236 -- UNTESTED
237 --
238 let beta = fun(t) ->
235 let beta = fun(r) ->
239236 destruct(r,
240237 fun(n) -> var(n),
241238 fun(u, v) ->
247244 fun(t) -> t
248245 )
249246
250 ### Example 4 (untested)
247 ### Example 4
251248
252249 The next task would be to search through a lambda term,
253250 looking for a candidate application term to reduce, and
258255 -- UNTESTED
259256 --
260257 let reduce = fun(t) ->
261 if beta_reducible(t) then
258 if is_beta_reducible(t) then
262259 [true, beta(t)]
263260 else
264261 destruct(t,
+21
-7
impl/Haskell/LariatDemo.hs less more
7676 --
7777
7878 beta t = destruct t
79 (\n -> var n)
80 (\u v -> destruct u
81 (\_ -> app u v)
82 (\_ _ -> app u v)
83 (\u -> resolve u v)
84 )
85 (\u -> u)
79 (\n -> var n)
80 (\u v -> destruct u
81 (\_ -> app u v)
82 (\_ _ -> app u v)
83 (\u -> resolve u v)
84 )
85 (\u -> u)
8686
8787 testBeta1 = (show $ beta testApp) == "FreeVar \"n\""
8888 testBeta2 = (show $ beta testAbs) == "Abs (BoundVar 0)"
89 testBeta3 = (show $ beta (var "j")) == "FreeVar \"j\""
90
91 isBetaReducible t = destruct t
92 (\n -> False)
93 (\u v -> destruct u
94 (\_ -> False)
95 (\_ _ -> False)
96 (\u -> True)
97 )
98 (\u -> False)
99
100 testIsBeta1 = (isBetaReducible testApp) == True
101 testIsBeta2 = (isBetaReducible testAbs) == False
102 testIsBeta3 = (isBetaReducible (var "j")) == False