(* Tagless-final operational semantics
Using call-by-value untyped lambda-calculus with De Bruijn variables and
integers and integer operations as a sample, we demonstrate
several interpreters and eventually a reducer.
Following the familiar operational semantics of lambda-calculus, the
reducer normalizes terms by successive rewriting: finding a redex and reducing
it -- repeating until either gets stuck or produces a value. The reducer
is instrumented to count the number of reduction steps.
The reducer code is intentionally written to be close to the structured
operational semantics presentation, so that counted reduction steps
faithfully represent the complexity of reducing a term.
Tagless-final style is designed around a compositional mapping of terms
of the embedded DSL to values of some `repr' domain -- i.e., denotational
semantics. Operational semantics in the tagless-final style doesn't seem
possible all. After all, to see if a term can be reduced we have to
pattern-match on it to find a redex. Performing an application, i.e.,
substituting into the abstraction body involves more pattern-matching.
Tagless-final terms are not represented via a data type (AST); how do we
pattern-match on them? This code shows how to search for a redex
and substitute into tagless-final style. Operational semantics turns
out not only possible but also relatively straightforward and
even profitable.
*)
(*
#use "reducer.ml";;
*)
(* ------------------------------------------------------------------------
Part 1: Source language and familiar tagless-final interpreters
Our source language is a call-by-value untyped lambda-calculus
with integer constants, successor and branching.
We could have stayed pure and encoded integers as Church numerals --
but that skews the complexity measures: A Church numeral can't be
compared to zero in constant time, in an applicative calculus.
We add ifz, which combines zero testing with the decrement.
The form ifz may be regarded as a deconstructor on naturals.
(ifz n) is a function of two arguments, z-continuation and p-continuation.
If n is zero, z-continuation is applied to 0. If n is not zero, it is
decremented and the result is passed to the p-continuation.
We could have defined the predecessor and conditional separately.
However, when we define self-interpreter, we will have to represent the
branches of ifz as thunks, to delay their evaluation. Therefore, it
behooves us to encode the branches as functions (continuations)
to begin with.
*)
module type Lambda = sig
type repr
val int : int -> repr (* integer literal *)
val vz : repr (* variable of the De Bruijn index 0 *)
val vs : repr -> repr (* next De Bruijn index (weakening) *)
val lam : repr -> repr (* abstraction *)
val (/) : repr -> repr -> repr (* application *)
(* Constants *)
val inc : repr (* successor *)
val ifz : repr (* branch on zero *)
end
type lambda = {e: 'a. (module Lambda with type repr = 'a) -> 'a}
module LambdaSelf : (Lambda with type repr = lambda) = struct
type repr = lambda
let int x = {e = fun (type a) (module L : Lambda with type repr = a) ->
L.int x}
let vz = {e = fun (type a) (module L : Lambda with type repr = a) ->
L.vz}
let vs e = {e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.vs (e.e l)}
let lam e = {e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.lam (e.e l)}
let (/) e1 e2 =
{e = fun (type a) ((module L : Lambda with type repr = a) as l)->
L.(e1.e l / e2.e l)}
let inc = {e = fun (type a) (module L : Lambda with type repr = a) ->
L.inc}
let ifz = {e = fun (type a) (module L : Lambda with type repr = a) ->
L.ifz}
end
(* Sample terms *)
module Sample = struct
open LambdaSelf
let ci = lam vz
let ck = lam @@ lam @@ vs vz (* the K combinator *)
let c0 = lam @@ lam vz (* zeroth Church numeral *)
let c2 = lam @@ lam @@ vs vz / (vs vz / vz) (* second Church numeral *)
(* several redices; some should be CBV-reduced,
and some should not *)
let er = (lam @@ lam @@ vz / (inc / (int 1)) / vs vz) / (inc / (int 3))
let et3 = lam @@ inc / (inc / (vz / int 1)) (* higher-order, numeric *)
let et3a = et3 / (lam @@ inc / (inc / (inc / vz)))
end
module Fix = struct
open LambdaSelf
let delta : lambda = lam @@ vz / vz
let lomega : lambda = lam @@ delta / delta
(* fix-point combinator, ordinary *)
let fix : lambda = lam (delta / lam (vs vz / (delta / vz)))
(* fix-point combinator, applicative (eta-expanded) *)
(*fixa = lam @@ delta / (lam @@ lam @@ (vs (vs vz)) / (delta / vs vz) / vz) *)
(*fixa = lam @@ delta / (lam @@ (vs vz) / (lam @@ delta / vs vz / vz)) *)
let fixa : lambda =
lam (vz /
(lam @@ delta / (lam @@ vs (vs vz) / (lam (delta / vs vz / vz))) / vz))
end
module SampleF = struct
open LambdaSelf
open Fix
open Sample
let ft1 : lambda =
fix / (lam @@ lam @@ vz / (ck / int 5) / (vs vz / c2))
let ft2 : lambda = ft1 / c0
let ft1a : lambda =
fixa / (lam @@ lam @@ vz / (lam (ck / int 5))
/ (lam (vs (vs vz) / c2))
/ int 10)
let ft2a : lambda = ft1a / c0
end
(* The regular recursive addition function
The induction is on the second argument
We can even use OCaml's let expressions, to attach
meaningful names to De Bruijn indices
*)
let add : lambda = let open LambdaSelf in let open Fix in
lam @@ fixa / (lam @@ lam @@
let y = vz and self = vs vz and x = vs (vs vz) in
ifz / y / (lam @@ vs x) / (lam @@ inc / (vs self / vz)))
;;
(* Our second implementation of Lambda signature interprets Lambda terms
as strings, so we can show them.
Actually, not quite strings: we need a bit of _context_:
the precedence and the number of variables already bound in the context.
The latter number lets us generate unique variable names.
*)
module Show = struct
type varcount = int
type prec = int
type repr = varcount -> prec -> string
let paren = function
| true -> fun text -> "(" ^ text ^ ")"
| false -> fun text -> text
let int n = fun _ _ -> string_of_int n
let vz = fun v _ -> "x" ^ string_of_int v
let vs e = fun v p -> e (v-1) p
let lam e = fun v p ->
let v' = v + 1 in
let x = "x" ^ string_of_int v' in
let body = e v' 0 in
paren (p > 0) ("L" ^ x ^ ". " ^ body)
let (/) e1 e2 = fun v p -> paren (p>10) (e1 v 10 ^ " " ^ e2 v 11)
let inc = fun _ _ -> "S"
let ifz = fun _ _ -> "ifz"
end
let show : lambda -> string = fun {e} -> e (module Show) 0 0
let "Lx1. x1" = show Sample.ci
let _ = show Sample.ck
let _ = show Sample.c0
let "Lx1. Lx2. x1 (x1 x2)" = show Sample.c2
let _ = show Sample.et3
let "(Lx1. S (S (x1 1))) (Lx1. S (S (S x1)))" = show Sample.et3a
let "(Lx1. Lx2. x2 (S 1) x1) (S 3)" = show Sample.er
let _ = show LambdaSelf.(add / int 1 / int 4)
(*
- : string =
"(Lx1. (Lx2. x2 (Lx3. (Lx4. x4 x4) (Lx4. x2 (Lx5. (Lx6. x6 x6) x4 x5)) x3))
(Lx2. Lx3. ifz x3 (Lx4. x1) (Lx4. S (x2 x4)))) 1 4"
*)
(* Another interpreter -- evaluator *)
(* It maps each Lambda term to the corresponding OCaml value
Our calculus implicitly has two types: integers and functions.
It is untyped (that is, implicitly types). Therefore, the corresponding
OCaml value for a term is a sum, either an OCaml integer or an OCaml
function.
*)
module NativeEval = struct
[@@@warning "-8"] (* partial pattern-match is intentional *)
type v = (* the value domain *)
| I of int
| A of (v->v) (* generally, a partial function *)
type repr = v list -> v (* also a partial function *)
let int x = fun _ -> I x
let vz = fun (h::_) -> h
let vs e = fun (_::t) -> e t
let lam e = fun env -> A (fun x -> e (x::env))
let (/) e1 e2 = fun env ->
match e1 env with A f -> f (e2 env)
let inc = fun _ -> A (function I x -> I (x+1)) (* partial *)
let ifz = fun _ -> A (function (* partial *)
| I 0 -> A (function A f -> A (fun _ -> f (I 0)))
| I n when n > 0 -> A (fun _ -> A (function A f -> f (I (n-1)))))
end
let eval : lambda -> NativeEval.v = fun {e} -> e (module NativeEval) []
let NativeEval.I 6 = eval Sample.et3a
(* Diverges as expected: our calculus is call-by-value indeed
let _ = eval SampleF.ft1
*)
let NativeEval.A _ = eval SampleF.ft1a
let NativeEval.I 5 = eval SampleF.ft2a
let NativeEval.I 5 = eval LambdaSelf.(add / int 1 / int 4)
(* ------------------------------------------------------------------------
Part 2: Normalizing terms by evaluation (NBE)
Denotational semantics approach to normalization
NativeEval/eval maps a term to an OCaml value. But we want to map a term
to a term.
One may think of the code below as having two passes. The first pass is
NativeEval. It evaluates a lambda term to a NativeEval.v value.
The second pass is a read-out, performed by dyn. It converts
NativeEval.v (so to speak) to a lambda-term, specifically, a value
that have the same meaning as NativeEval.v
To force a NativeEval.A function to produce a term, we introduce the
T variant into NativeEval, to carry the term being reconstructed.
The first pass never deals with T alternatives.
The sign read-out is in process is that env contains the T variant,
at least in the first slot
The main complexity of the code below is to avoid any reductions under
lambda, even if they could be done (e.g., inc 1). NBE is in essence
a partial evaluator! We deliberately pessimize it so not to do
any specializations. We want it because: (1) we want to compare to
the reducer below; (2) doing redices under lambda is perilous:
consider evaluating Fix.lomega. The true evaluator should return
lomega as it is since it is a value. A partial evaluator may diverge.
*)
module NBE = struct
[@@@warning "-8"] (* partial pattern-match is intentional *)
type v = (* the value domain *)
| I of int
| A of (v->v)
| T of lambda
type repr = v list -> v
let rec dyn : v -> lambda = function
| I x -> LambdaSelf.int x
| T e -> e
| A f -> LambdaSelf.(lam (dyn (f (T vz))))
let int x = function
| T _::_ -> T (LambdaSelf.int x) (* readout in progress *)
| _ -> I x
let vz = fun (h::_) -> h (* Substitution under lam is OK *)
let vs e = fun (_::t) ->
match e t with
| T e -> T LambdaSelf.(vs e)
| e -> e
let lam e = function
| T _::_ as env -> (* readout in progress *)
T LambdaSelf.(lam (dyn (e (T vz::env))))
| env -> A (fun x -> e (x::env))
let (/) e1 e2 = function
| T _::_ as env ->
T LambdaSelf.(dyn (e1 env) / dyn (e2 env))
| env ->
match e1 env with A f -> f (e2 env)
let inc = function
| T _::_ -> T LambdaSelf.inc
| _ -> A (function
| I x -> I (x+1)
| T e -> T LambdaSelf.(inc / e))
let ifz = function
| T _::_ -> T LambdaSelf.ifz
| _ -> A (function
| I 0 -> A (function A f -> A (fun _ -> f (I 0)))
| I n when n > 0 -> A (fun _ -> A (function A f -> f (I (n-1))))
| T e -> T LambdaSelf.(ifz / e))
end
let neval : lambda -> (NBE.v list -> NBE.v) = fun {e} -> e (module NBE)
let nbe : lambda -> lambda = fun e -> NBE.dyn @@ neval e []
let nbeshow : lambda -> string = fun e -> show @@ nbe e
let true = nbeshow Sample.ci = show Sample.ci
let true = nbeshow Sample.ck = show Sample.ck
let true = nbeshow Sample.c2 = show Sample.c2
let "Lx1. x1 (S 1) 4" = nbeshow Sample.er
let "Lx1. x1 (S 1) 4" = nbeshow @@ nbe Sample.er
let "Lx1. S x1" = nbeshow LambdaSelf.inc (* eta-long indeed *)
let "Lx1. ifz x1" = nbeshow LambdaSelf.ifz
let true = nbeshow Sample.et3 = show Sample.et3
let "6" = nbeshow Sample.et3a
let true = nbeshow Fix.delta = show Fix.delta
(* we really don't reduce under lambda *)
let true = nbeshow Fix.lomega = show Fix.lomega
let true = nbeshow Fix.fix = show Fix.fix
let true = nbeshow Fix.fixa = show Fix.fixa
let _ = nbeshow SampleF.ft1a
let "5" = nbeshow SampleF.ft2a
let "5" = nbeshow LambdaSelf.(nbe SampleF.ft1a / Sample.c0)
let _ = nbeshow LambdaSelf.(add / int 1)
(*
- : string =
"Lx1. ifz x1 (Lx2. 1) (Lx2. S ((Lx3. (Lx4. x4 x4) (Lx4. (Lx5. Lx6. ifz x6 (Lx7. 1) (Lx7. S (x5 x7))) (Lx5. (Lx6. x6 x6) x4 x5)) x3) x2))"
*)
let "5" = nbeshow LambdaSelf.(add / int 1 / int 4)
let "5" = nbeshow LambdaSelf.(nbe (add / int 1) / int 4)
(* Testing that nbe and eval produce the same values *)
let true =
let e = LambdaSelf.(add / int 1) in
let A f1 = eval e in
let A f2 = eval (nbe e) in
List.for_all (fun n -> f1 (NativeEval.I n) = f2 (NativeEval.I n))
[0;1;2;3;4;100]
(* ------------------------------------------------------------------------
Part 3: Reducer -- normalizing terms by successive re-writing
In other words, implementing operational semantics.
If we just want to find the normal form of a term, there are faster
and better ways to obtain it, in the tagless-final style: use
normalization-by-evaluation.
This application was developed for the purpose of analyzing complexity
of self-evaluator. It is important to count the reductions properly,
and do it in the way that is obviously `right', that is, matches
the reduction semantics of the call-by-value calculus.
Recall, the reduction semantics is: decompose a non-value term
into the context and the redex, reduce the redex, substitute into
the context and continue. It is the eval-apply semantics that should be
familiar from abstract machines.
*)
(* First, we implement a classifier of expressions, as a tagless-final
interpreter. Given an expression, it tells us if it is a value or a
reducible expression. In the former case, it tells what sort of value
it is: an integer or an applicable value.
Classification is done bottom-up, and so we also have to deal with open
terms. The advantage is that we also build the substitution function at
the same time, should we need to substitute into the term eventually.
(We also detect constant functions and optimize their applications).
Note how `kind' below differs from an AST for our calculus.
The classifier and the reducer take advantage of the fact that in
call-by-value (and call-by-name, for that matter) only closed terms are
substituted.
*)
module Classifier = struct
[@@@warning "-8"] (* partial pattern-match is intentional *)
type repr = {term: lambda; (* term as it is *)
kind: kind} (* and its kind *)
and kind =
| App of repr * repr (* subject to reductions *)
(* Expressions of the kind Int and Applicable are values *)
| Int of int
| Applicable of (repr -> repr) (* can be applied to an argument *)
(* All other are closed. The first argument is the depth:
the number of lambdas needed to close the expression
*)
| Open of int * (repr list -> repr)
let int x = {term = LambdaSelf.int x;
kind = Int x}
let vz = {term = LambdaSelf.vz;
kind = Open (1,fun (h::_) -> h)}
let rec vs e = match e.kind with
| Open (n,e') ->
{term = LambdaSelf.vs e.term;
kind = Open (n+1,fun (_::t) -> vs (e' t))}
(* vs may end up being applied to a closed value after the substitution.
In that case, it does nothing.
*)
| _ -> e
let rec lam e =
{term = LambdaSelf.lam e.term;
kind = match e.kind with
| Open (1,t) -> Applicable (fun x -> t [x])
| Open (n,t) when n > 1 ->
Open (n-1,fun env -> lam (t (vz::env)))
| _ -> Applicable (fun x -> e) (* constant function *)
}
let[@warning "+8"] rec (/) e1 e2 =
{term = LambdaSelf.(e1.term / e2.term);
kind = match (e1.kind,e2.kind) with
| (Open(n1,t1),Open(n2,t2)) -> Open(max n1 n2, fun env -> t1 env / t2 env)
| (Open(n1,t1),_) -> Open(n1,fun env -> t1 env / e2)
| (_,Open(n2,t2)) -> Open(n2,fun env -> e1 / t2 env)
| _ -> App (e1,e2)
}
let inc = {term = LambdaSelf.inc;
kind = Applicable (function {kind = Int x} ->
int (x+1))}
let ifz = {term = LambdaSelf.ifz;
kind = Applicable (function
| {kind = Int 0} ->
lam @@ lam @@ (vs vz / int 0)
| {kind = Int n} when n > 0 ->
lam @@ lam @@ (vz / int (n-1))
)
}
end
(* Structural operational semantics reducer *)
(* It is not very efficient: too many checks for term's shape *)
let sos : lambda -> lambda = fun {e} ->
let open Classifier in
let rec step : repr -> repr = (* the --> reduction of SOS *)
fun e -> match e.kind with
| Applicable _ | Int _ -> e (* value *)
| Open _ -> assert false (* cannot happen *)
| App (e1,e2) -> match (e1.kind,e2.kind) with
| (Applicable f,Int _) | (Applicable f,Applicable _) ->
f e2 (* redex *)
| (App _,_) -> step e1 / e2
| (_,App _) -> e1 / step e2
| _ -> failwith "stuck"
in
let rec loop : repr -> repr = (* transitive closure of step *)
fun e -> match e.kind with
| Applicable _ | Int _ -> e (* value *)
| _ -> loop (step e)
in (loop (e (module Classifier))).term
let sosshow : lambda -> string = fun e -> show @@ sos e
let true = sosshow Sample.ci = show Sample.ci
let true = sosshow Sample.ck = show Sample.ck
let "Lx1. 1" = sosshow LambdaSelf.(Sample.ck / int 1)
let "1" = sosshow LambdaSelf.(Sample.ck / int 1 / int 2)
let true = sosshow Sample.c2 = show Sample.c2
let "Lx1. x1 (S 1) 4" = sosshow Sample.er
let "Lx1. x1 (S 1) 4" = sosshow @@ sos Sample.er
let "S" = sosshow LambdaSelf.inc (* not eta-long *)
let "ifz" = sosshow LambdaSelf.ifz
let true = sosshow Sample.et3 = show Sample.et3
let "6" = sosshow Sample.et3a
let true = sosshow Fix.delta = show Fix.delta
(* we really don't reduce under lambda *)
let true = sosshow Fix.lomega = show Fix.lomega
let true = sosshow Fix.fix = show Fix.fix
let true = sosshow Fix.fixa = show Fix.fixa
let "Lx1. x1" = sosshow LambdaSelf.(Fix.fixa / Sample.c0)
let true = sosshow SampleF.ft1a = nbeshow SampleF.ft1a
let "5" = sosshow SampleF.ft2a
let "5" = sosshow LambdaSelf.(sos SampleF.ft1a / Sample.c0)
let true = sosshow LambdaSelf.(add / int 1) = nbeshow LambdaSelf.(add / int 1)
let "5" = sosshow LambdaSelf.(add / int 1 / int 4)
(* Big-step, natural-semantics reducer *)
let reducer : lambda -> (lambda * int) = fun {e} ->
let open Classifier in
let rec loop n e = match e.kind with
| Applicable _
| Int _ -> (e,n) (* value *)
| Open _ -> assert false
| App (e1,e2) ->
let (v1,n1) = loop n e1 in
let (v2,n2) = loop n1 e2 in
begin match v1.kind with
| Applicable f -> loop (n2+1) (f v2)
| _ -> failwith "Applying not to a function"
end
in
let (v,n) = loop 0 @@ e (module Classifier) in
(v.term,n)
let redshow : lambda -> (string * int) = fun e ->
let (v,n) = reducer e in (show v,n)
let true = redshow Sample.ci = (show Sample.ci,0)
let true = redshow Sample.ck = (show Sample.ck,0)
let ("Lx1. 1", 1) = redshow LambdaSelf.(Sample.ck / int 1)
let ("1", 2) = redshow LambdaSelf.(Sample.ck / int 1 / int 2)
let true = redshow Sample.c2 = (show Sample.c2,0)
let ("Lx1. x1 (S 1) 4",2) = redshow Sample.er
let ("Lx1. x1 (S 1) 4",0) = redshow @@ fst @@ reducer Sample.er
let ("S",0) = redshow LambdaSelf.inc (* not eta-long *)
let ("ifz",0) = redshow LambdaSelf.ifz
let true = redshow Sample.et3 = (show Sample.et3,0)
let ("6",7) = redshow Sample.et3a
let true = redshow Fix.delta = (show Fix.delta,0)
(* we really don't reduce under lambda *)
let true = redshow Fix.lomega = (show Fix.lomega,0)
let true = redshow Fix.fix = (show Fix.fix,0)
let true = redshow Fix.fixa = (show Fix.fixa,0)
let ("Lx1. x1", 2) = redshow LambdaSelf.(Fix.fixa / Sample.c0)
let true = redshow SampleF.ft1a = (nbeshow SampleF.ft1a,2)
let ("5",18) = redshow SampleF.ft2a
let ("5",16) = redshow LambdaSelf.(fst (reducer SampleF.ft1a) / Sample.c0)
let true = redshow LambdaSelf.(add / int 1) =
(nbeshow LambdaSelf.(add / int 1),3)
(* let "5" = nbeshow LambdaSelf.(nbe (add / int 1) / int 4) *)
(* As expected, addition takes linear time: adding 1+n takes 8+10n reductions *)
let ("1", 8) = redshow LambdaSelf.(add / int 1 / int 0)
let ("2", 18) = redshow LambdaSelf.(add / int 1 / int 1)
let ("3", 28) = redshow LambdaSelf.(add / int 1 / int 2)
let ("4", 38) = redshow LambdaSelf.(add / int 1 / int 3)
let ("5", 48) = redshow LambdaSelf.(add / int 1 / int 4)
let ("9", 88) = redshow LambdaSelf.(add / int 1 / int 8)
let ("17",168) = redshow LambdaSelf.(add / int 1 / int 16)
;;