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))) | _ -> 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. *)