code/ski_evaluator.ml

   1 type term = I | S | K | App of (term * term)
   2
   3 let skomega = App (App (App (S,I), I), App (App (S,I), I))
   4 let test = App (App (K,I), skomega)
   5
   6 let reduce_if_redex (t:term):term = match t with
   7   | App(I,a) -> a
   8   | App(App(K,a),b) -> a
   9   | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
  10   | _ -> t
  11
  12 let is_redex (t:term):bool = not (t = reduce_if_redex t)
  13
  14 let rec reduce_try2 (t:term):term = match t with
  15   | I -> I
  16   | K -> K
  17   | S -> S
  18   | App (a, b) ->
  19       let t' = App (reduce_try2 a, reduce_try2 b) in
  20       if (is_redex t') then let t'' = reduce_if_redex t'
  21                             in reduce_try2 t''
  22                        else t'
  23
  24 let rec reduce_try3 (t:term):term = match t with
  25   | I -> I
  26   | K -> K
  27   | S -> S
  28   | App (a, b) ->
  29       let t' = App (reduce_try3 a, b) in
  30       if (is_redex t') then let t'' = reduce_if_redex t'
  31                             in reduce_try3 t''
  32                        else t'
  33
  34 (* To make this closer to the untyped lambda interpreter, we'd need to:
  35
  36 1.  Change the method by which we detect/report if a term is reducible, as
  37     follows:
  38
  39         (* Since there's no Stuck variant, and we don't return anything with
  40            the Already...  variant, this type is isomorphic to `None | Some
  41            term`, and we could just use that. However, we'll use this custom
  42            type to emphasize the parallels with the untyped interpreter. *)
  43         type reduceOutcome = AlreadyReduced | ReducedTo of term
  44
  45         let reduce_if_redex (t : term) : reduceOutcome = match t with
  46           | App(I,a) -> ReducedTo a
  47           | App(App(K,a),b) -> ReducedTo a
  48           | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
  49           | _ -> AlreadyReduced
  50
  51         let rec reduce_try4 (t : term) : term = match t with
  52           | I -> I
  53           | K -> K
  54           | S -> S
  55           | App(a, b) ->
  56               let t' = App(reduce_try4 a, reduce_try4 b) in
  57               (match reduce_if_redex t' with
  58                 | ReducedTo t'' -> reduce_try4 t''
  59                 | AlreadyReduced -> t')
  60
  61 2.  Shift the responsibilities between the looping function `reduce` and the
  62     reducing function, so that the latter now calls itself recursively trying
  63     to find a suitable redex, until it can perform one reduction.
  64
  65         type reduceOutcome = AlreadyReduced | ReducedTo of term
  66
  67         let rec reduce_once (t : term) : reduceOutcome = match t with
  68           | App(a, b) -> (match reduce_once a with
  69               | ReducedTo a' -> ReducedTo (App(a',b))
  70               | AlreadyReduced -> (match reduce_once b with
  71                   | ReducedTo b' -> ReducedTo (App(a,b'))
  72                   | AlreadyReduced ->
  73                       (* here we have the old functionality of reduce_if_redex *)
  74                       (match t with
  75                         | App(I,a) -> ReducedTo a
  76                         | App(App(K,a),b) -> ReducedTo a
  77                         | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
  78                         | _ -> AlreadyReduced)))
  79           | _ -> AlreadyReduced
  80
  81         let rec reduce_try5 (t : term) : term = match reduce_once t with
  82           | ReducedTo t'-> reduce_try5 t'
  83           | AlreadyReduced -> t
  84
  85 3.  Finally, the untyped interpreter only performs reductions in (possibly
  86     embedded) _head_ positions.  By contrast, the (eager) combinatory
  87     interpeters above wlll reduce `K (I I)` to `K I`. To make these
  88     interpreters also (eagerly) reduce only head redexes, let's bring back an
  89     `is_redex` function:
  90
  91         type reduceOutcome = AlreadyReduced | ReducedTo of term
  92
  93         let is_redex (t : term) : bool = match t with
  94           | App(I,_) -> true
  95           | App(App(K,_),_) -> true
  96           | App(App(App(S,_),_),_) -> true
  97           | _ -> false
  98
  99         let rec reduce_head_once (t : term) : reduceOutcome = match t with
 100           | App(a, b) -> (match reduce_head_once a with
 101               | ReducedTo a' -> ReducedTo (App(a',b))
 102               (* now we only try to reduce b when App(a,b) is a redex *)
 103               | AlreadyReduced when is_redex t -> (match reduce_head_once b with
 104                   | ReducedTo b' -> ReducedTo (App(a,b'))
 105                   | AlreadyReduced ->
 106                       (* old functionality of reduce_if_redex *)
 107                       (match t with
 108                         | App(I,a) -> ReducedTo a
 109                         | App(App(K,a),b) -> ReducedTo a
 110                         | App(App(App(S,a),b),c) -> ReducedTo (App(App(a,c),App(b,c)))
 111                         | _ -> AlreadyReduced))
 112               (* else leave b as it is *)
 113               | _ -> AlreadyReduced)
 114           | _ -> AlreadyReduced
 115
 116         let rec reduce_try6 (t : term) : term = match reduce_head_once t with
 117           | ReducedTo t'-> reduce_try6 t'
 118           | AlreadyReduced -> t
 119
 120 4.  In the untyped interpreter, there is no separate `is_redex` function. That
 121     check is embedded into the pattern-matching in the `reduce_head_once`
 122     function.  Otherwise, the code now structurally parallels the
 123     VA/substitute-and-repeat strategy of the untyped interpreter. The remaining
 124     differences have to do with the shift from combinatory logic to the lambda
 125     calculus, tracking free variables, the complexities of substitution, and so
 126     on.
 127
 128 *)