index 5e23ff9..727a84a 100644 (file)
-type term = I | S | K | FA of (term * term)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-let test = FA (FA (K,I), skomega)
-
-let reduce_one_step (t:term):term = match t with
-    FA(I,a) -> a
-  | FA(FA(K,a),b) -> a
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-  | _ -> t
-
-let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-let rec reduce (t:term):term = match t with
-    I -> I
-  | K -> K
-  | S -> S
-  | FA (a, b) ->
-      let t' = FA (reduce a, reduce b) in
-        if (is_redex t') then reduce (reduce_one_step t')
-                         else t'
-
-let rec reduce_lazy (t:term):term = match t with
-    I -> I
-  | K -> K
-  | S -> S
-  | FA (a, b) ->
-      let t' = FA (reduce_lazy a, b) in
-        if (is_redex t') then reduce_lazy (reduce_one_step t')
-                         else t'
+type term = I | S | K | App of (term * term)
+
+let skomega = App (App (App (S,I), I), App (App (S,I), I))
+let test = App (App (K,I), skomega)
+
+let reduce_if_redex (t:term):term = match t with
+  | App(I,a) -> a
+  | App(App(K,a),b) -> a
+  | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
+  | _ -> t
+
+let is_redex (t:term):bool = not (t = reduce_if_redex t)
+
+let rec reduce_try2 (t:term):term = match t with
+  | I -> I
+  | K -> K
+  | S -> S
+  | App (a, b) ->
+      let t' = App (reduce_try2 a, reduce_try2 b) in
+      if (is_redex t') then let t'' = reduce_if_redex t'
+                            in reduce_try2 t''
+                       else t'
+
+let rec reduce_try3 (t:term):term = match t with
+  | I -> I
+  | K -> K
+  | S -> S
+  | App (a, b) ->
+      let t' = App (reduce_try3 a, b) in
+      if (is_redex t') then let t'' = reduce_if_redex t'
+                            in reduce_try3 t''
+                       else t'
+
+(* To make this closer to the untyped lambda interpreter, we'd need to:
+
+1.  Change the method by which we detect/report if a term is reducible, as
+    follows:
+
+       (* Since there's no Stuck variant, and we don't return anything with
+          the Already...  variant, this type is isomorphic to `None | Some
+          term`, and we could just use that. However, we'll use this custom
+          type to emphasize the parallels with the untyped interpreter. *)
+        type reduceOutcome = AlreadyReduced | ReducedTo of term
+
+        let reduce_if_redex (t : term) : reduceOutcome = match t with
+         | App(I,a) -> ReducedTo a
+         | App(App(K,a),b) -> ReducedTo a
+         | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
+
+        let rec reduce_try4 (t : term) : term = match t with
+         | I -> I
+         | K -> K
+         | S -> S
+         | App(a, b) ->
+             let t' = App(reduce_try4 a, reduce_try4 b) in
+             (match reduce_if_redex t' with
+               | ReducedTo t'' -> reduce_try4 t''
+
+2.  Shift the responsibilities between the looping function `reduce` and the
+    reducing function, so that the latter now calls itself recursively trying
+    to find a suitable redex, until it can perform one reduction.
+
+        type reduceOutcome = AlreadyReduced | ReducedTo of term
+
+       let rec reduce_once (t : term) : reduceOutcome = match t with
+         | App(a, b) -> (match reduce_once a with
+             | ReducedTo a' -> ReducedTo (App(a',b))
+             | AlreadyReduced -> (match reduce_once b with
+                 | ReducedTo b' -> ReducedTo (App(a,b'))
+                     (* here we have the old functionality of reduce_if_redex *)
+                     (match t with
+                       | App(I,a) -> ReducedTo a
+                       | App(App(K,a),b) -> ReducedTo a
+                       | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
+
+        let rec reduce_try5 (t : term) : term = match reduce_once t with
+         | ReducedTo t'-> reduce_try5 t'
+
+3.  Finally, the untyped interpreter only performs reductions in (possibly
+    embedded) _head_ positions.  By contrast, the (eager) combinatory
+    interpeters above wlll reduce `K (I I)` to `K I`. To make these
+    interpreters also (eagerly) reduce only head redexes, let's bring back an
+    `is_redex` function:
+
+        type reduceOutcome = AlreadyReduced | ReducedTo of term
+
+        let is_redex (t : term) : bool = match t with
+         | App(I,_) -> true
+         | App(App(K,_),_) -> true
+         | App(App(App(S,_),_),_) -> true
+         | _ -> false
+
+       let rec reduce_head_once (t : term) : reduceOutcome = match t with
+         | App(a, b) -> (match reduce_head_once a with
+             | ReducedTo a' -> ReducedTo (App(a',b))
+             (* now we only try to reduce b when App(a,b) is a redex *)
+                 | ReducedTo b' -> ReducedTo (App(a,b'))
+                     (* old functionality of reduce_if_redex *)
+                     (match t with
+                       | App(I,a) -> ReducedTo a
+                       | App(App(K,a),b) -> ReducedTo a
+                       | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
+             (* else leave b as it is *)
+
+        let rec reduce_try6 (t : term) : term = match reduce_head_once t with
+         | ReducedTo t'-> reduce_try6 t'