+
+(* 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)))
+ | _ -> AlreadyReduced
+
+ 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''
+ | AlreadyReduced -> 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'))
+ | AlreadyReduced ->
+ (* 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)))
+ | _ -> AlreadyReduced)))
+ | _ -> AlreadyReduced
+
+ let rec reduce_try5 (t : term) : term = match reduce_once t with
+ | ReducedTo t'-> reduce_try5 t'
+ | AlreadyReduced -> 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 *)
+ | AlreadyReduced when is_redex t -> (match reduce_head_once b with
+ | ReducedTo b' -> ReducedTo (App(a,b'))
+ | AlreadyReduced ->
+ (* 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)))
+ | _ -> AlreadyReduced))
+ (* else leave b as it is *)
+ | _ -> AlreadyReduced)
+ | _ -> AlreadyReduced
+
+ let rec reduce_try6 (t : term) : term = match reduce_head_once t with
+ | ReducedTo t'-> reduce_try6 t'
+ | AlreadyReduced -> t
+
+4. In the untyped interpreter, there is no separate `is_redex` function. That
+ check is embedded into the pattern-matching in the `reduce_head_once`
+ function. Otherwise, the code now structurally parallels the
+ VA/substitute-and-repeat strategy of the untyped interpreter. The remaining
+ differences have to do with the shift from combinatory logic to the lambda
+ calculus, tracking free variables, the complexities of substitution, and so
+ on.
+
+*)