The answer to the first question (Can we adjust the OCaml evaluator to
exhibit lazy behavior?) is quite simple:
- let rec reduce_lazy (t : term) : term = match t with
+ let rec reduce_try3 (t : term) : term = match t with
| I -> I
| K -> K
| S -> S
| App (a, b) ->
- let t' = App (reduce_lazy a, b) in
+ let t' = App (reduce_try3 a, b) in
if (is_redex t') then let t'' = reduce_if_redex t'
- in reduce_lazy t''
+ in reduce_try3 t''
else t'
There is only one small difference from `reduce_try2`: instead of setting `t'` to `App
subexpression at all. Ever! The only way to get evaluated is to
somehow get into functor position.
- # reduce3 (App(App(K,I),skomega));;
+ # reduce_try3 (App(App(K,I),skomega));;
- : term = I
- # reduce3 skomega;;
+ # reduce_try3 skomega;;
C-c C-cInterrupted.
The evaluator now has no trouble finding the normal form for `KIΩ`,