1 type term = I | S | K | App of (term * term)
3 let skomega = App (App (App (S,I), I), App (App (S,I), I))
4 let test = App (App (K,I), skomega)
6 let reduce_if_redex (t:term):term = match t with
9 | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
12 let is_redex (t:term):bool = not (t = reduce_if_redex t)
14 let rec reduce_try2 (t:term):term = match t with
19 let t' = App (reduce_try2 a, reduce_try2 b) in
20 if (is_redex t') then let t'' = reduce_if_redex t'
24 let rec reduce_try3 (t:term):term = match t with
29 let t' = App (reduce_try3 a, b) in
30 if (is_redex t') then let t'' = reduce_if_redex t'
34 (* To make this closer to the untyped lambda interpreter, we'd need to:
36 1. Change the method by which we detect/report if a term is reducible, as
39 (* Since there's no Stuck variant, and we don't return anything with
40 the Already... variant, this type is isomorphic to `None | Some
41 term`, and we could just use that. However, we'll use this custom
42 type to emphasize the parallels with the untyped interpreter. *)
43 type reduceOutcome = AlreadyReduced | ReducedTo of term
45 let reduce_if_redex (t : term) : reduceOutcome = match t with
46 | App(I,a) -> ReducedTo a
47 | App(App(K,a),b) -> ReducedTo a
48 | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
51 let rec reduce_try4 (t : term) : term = match t with
56 let t' = App(reduce_try4 a, reduce_try4 b) in
57 (match reduce_if_redex t' with
58 | ReducedTo t'' -> reduce_try4 t''
59 | AlreadyReduced -> t')
61 2. Shift the responsibilities between the looping function `reduce` and the
62 reducing function, so that the latter now calls itself recursively trying
63 to find a suitable redex, until it can perform one reduction.
65 type reduceOutcome = AlreadyReduced | ReducedTo of term
67 let rec reduce_once (t : term) : reduceOutcome = match t with
68 | App(a, b) -> (match reduce_once a with
69 | ReducedTo a' -> ReducedTo (App(a',b))
70 | AlreadyReduced -> (match reduce_once b with
71 | ReducedTo b' -> ReducedTo (App(a,b'))
73 (* here we have the old functionality of reduce_if_redex *)
75 | App(I,a) -> ReducedTo a
76 | App(App(K,a),b) -> ReducedTo a
77 | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
78 | _ -> AlreadyReduced)))
81 let rec reduce_try5 (t : term) : term = match reduce_once t with
82 | ReducedTo t'-> reduce_try5 t'
85 3. Finally, the untyped interpreter only performs reductions in (possibly
86 embedded) _head_ positions. By contrast, the (eager) combinatory
87 interpeters above wlll reduce `K (I I)` to `K I`. To make these
88 interpreters also (eagerly) reduce only head redexes, let's bring back an
91 type reduceOutcome = AlreadyReduced | ReducedTo of term
93 let is_redex (t : term) : bool = match t with
95 | App(App(K,_),_) -> true
96 | App(App(App(S,_),_),_) -> true
99 let rec reduce_head_once (t : term) : reduceOutcome = match t with
100 | App(a, b) -> (match reduce_head_once a with
101 | ReducedTo a' -> ReducedTo (App(a',b))
102 (* now we only try to reduce b when App(a,b) is a redex *)
103 | AlreadyReduced when is_redex t -> (match reduce_head_once b with
104 | ReducedTo b' -> ReducedTo (App(a,b'))
106 (* old functionality of reduce_if_redex *)
108 | App(I,a) -> ReducedTo a
109 | App(App(K,a),b) -> ReducedTo a
110 | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
111 | _ -> AlreadyReduced))
112 (* else leave b as it is *)
113 | _ -> AlreadyReduced)
114 | _ -> AlreadyReduced
116 let rec reduce_try6 (t : term) : term = match reduce_head_once t with
117 | ReducedTo t'-> reduce_try6 t'
118 | AlreadyReduced -> t
120 4. In the untyped interpreter, there is no separate `is_redex` function. That
121 check is embedded into the pattern-matching in the `reduce_head_once`
122 function. Otherwise, the code now structurally parallels the
123 VA/substitute-and-repeat strategy of the untyped interpreter. The remaining
124 differences have to do with the shift from combinatory logic to the lambda
125 calculus, tracking free variables, the complexities of substitution, and so