X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fski_evaluator.ml;h=11e8dd4ebd85a4794317052a7c39f8eaa3387eb6;hp=10d130e08f9e9d3006a846bffacbdcb2b2cb4fae;hb=0cb89c90973c0c5c74d7c3cfd929ca95946d44e4;hpb=6eb94b1b0c2bd030c11a3da469e769faa5ada8d9 diff --git a/code/ski_evaluator.ml b/code/ski_evaluator.ml index 10d130e0..11e8dd4e 100644 --- a/code/ski_evaluator.ml +++ b/code/ski_evaluator.ml @@ -1,30 +1,128 @@ -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_eager (t:term):term = match t with - I -> I - | K -> K - | S -> S - | FA (a, b) -> - let t' = FA (reduce_eager a, reduce_eager b) in - if (is_redex t') then reduce_eager (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))) + | _ -> AlreadyReduced + + let rec reduce_try4 (t : term) : term = match t with + | I -> I + | K -> K + | S -> S + | App(a, b) -> + let t' = App(reduce_try3 a, reduce_try 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. + +*)