| Matthias Blume 2004-07-23, 8:56 pm |
|
(* I have taken the trouble of writing some code that attempts to
* demonstrate several things:
* - A Bill-style "denotational semantics" for an ISWIM-like language
* can be given.
* - A Bill-style semantics (at least my version thereof) is formally
* compositional as it is an instantiation of a generic induction
* schema on the syntax of expressions. The functions that instantiate
* the schema do not refer to each other's definitions recursively,
* neither directly nor indirectly, meaning they also do not refer to
* the definition of the overall valuation function.
* - But they do refer to a given operational semantics!
* - The so-defined Bill-style denotational semantics is actually
* EXACTLY THE SAME FUNCTION as that previously given operational
* semantics which was used in its definition!
* - Therefore, although the construction is formally not
* circular, it does not make any progress either -- nothing new
* has been defined. All we get is a clone of the pre-existing
* (and necessary to do the cloning!) operational semantics.
*
* - A different instantiation of the same induction schema gives
* a more traditional denotational semantics for the same language.
* Not only is this semantics arguably more concise (even when
* not counting the code that implements the operational
* semantics), it manages to do so without using the operational
* semantics at all. It is also more abstract as it assigns equal
* meaning to many observationally equivalent terms and, thus, would
* be more useful in practice.
*
* Some points about the code:
* - I wrote it in Standard ML because I wanted something that is
* notationally close to what one would write on paper when
* dealing with semantics. (Also, I don't have to invent my own
* rules for how to ascii-ify gr notation. BNF and domain
* equations can be rendered as type declarations.)
* - An advantage of this is that the code is immediately executable.
* (I compiled it using SML/NJ 110.46 and tested a few trivial examples.
* I have not proved it correct!)
* - A di vantage is that the treatment of domains is very implicit,
* relying on the interpretation of ML types. Bottom is "modeled" as
* non-termination. In fact, the "better" denotational semantics
* is not a free-standing denotational semantics but rather a
* compiler from ISWIM to ML values. But an actual denotational
* semantics on paper would look almost exactly like it.
* - The Bill-style semantics I give is not the same that Bill
* tried to give himself. According to Will Clinger, Bill's
* semantics was incorrect anyway. (I was too lazy to check this
* claim carefully.) Moreover, Bill's version relies on an otherwise
* gratuitous modification of the grammar of the language.
* In my version of the semantics I finesse the issue that Bill
* tried to finesse by making the denotation of a term a pair
* consisting of 1. what amounts to the suspended bigstep semantics
* of the term, and 2. what amounts to (a copy of) the term itself.
* - My operational semantics is a big-step semantics because it
* is far more natural (pun intended) to render as executable code.
* - Free variables are considered "stuck".
* - Needless to say, the operational semantics can diverge or get
* stuck (here modeled by an ML exception). Therefore, the
* operational semantics appears in suspended form within the
* Bill-style "denotation" of a term.
*
* Anyway, this entire message (excluding headers) can be compiled by
* your favorite SML compiler as all "prose" is in ML comments.
*)
(* ++++++++++++ THE LANGUAGE +++++++++++++ *)
(* use small ints as variables *)
type var = int
(* list of primitive (built-in) operations *)
datatype pop = PLUS | MINUS | TIMES (* ... *)
(* constants (here: integers) *)
type con = int
(* expressions (using datatype as BNF) *)
datatype exp = Var of var (* variable *)
| Con of con (* constant *)
| App of exp * exp (* application *)
| Lam of var * exp (* lambda *)
| POp of pop * exp * exp (* primitive operation *)
(* ---------- END Of THE LANGUAGE ------------ *)
(* ++++++++++++++ UTILITIES ++++++++++++++++++ *)
exception Stuck (* for reporting stuckness ("type error") *)
(* bind a value in a functional environment *)
fun bind (env, v: var, x) v' = if v = v' then x else env v'
(* apply a primitive operations to two constants *)
fun apply (PLUS, c1 : con, c2 : con) = c1 + c2
| apply (MINUS, c1, c2) = c1 - c2
| apply (TIMES, c1, c2) = c1 * c2
(* make a fresh variable (negative int);
* assume original exp has only non-negative variables;
* this is used by the capture-free substitution routine to
* satisfy the side-condition on the beta rule *)
val gensym : unit -> var =
let val next = ref 0
in fn () => let val n = !next - 1 in next := n; n end
end
(* ------------- END OF UTILITIES ---------------- *)
(* +++++++++++++ AN OPERATIONAL SEMANTICS +++++++++++++ *)
(* values (this is for clarity only, I could have used exp here
* without expressing the restriction in the type system) *)
datatype value = VCon of con (* constants *)
| VLam of var * exp (* head-normal forms *)
(* convert values back to expressions; would not be needed if
* values were taken to be a subset of expression *)
fun v2e (VCon c) = Con c
| v2e (VLam (v, e)) = Lam (v, e)
(* capture-free substitution *)
fun subst (e1, v, e2) =
let fun s (Var v, env) = env v
| s (Con c, _) = Con c
| s (App (e1, e2), env) = App (s (e1, env), s (e2, env))
| s (Lam (v, e), env) = let val v' = gensym ()
in Lam (v', s (e, bind (env, v, Var v')))
end
| s (POp (p, e1, e2), env) = POp (p, s (e1, env), s (e2, env))
in
s (e1, bind (Var, v, e2))
end
(* big-step semantics *)
fun bigstep0 (e as Var _) = raise Stuck
| bigstep0 (Con c) = VCon c
| bigstep0 (App (e1, e2)) =
(case (bigstep0 e1, bigstep0 e2)
of (VLam (v, b), x) => bigstep0 (subst (b, v, v2e x))
| _ => raise Stuck)
| bigstep0 (Lam (v, e)) = VLam (v, e)
| bigstep0 (POp (p, e1, e2)) =
(case (bigstep0 e1, bigstep0 e2)
of (VCon c1, VCon c2) => VCon (apply (p, c1, c2))
| _ => raise Stuck)
(* A trivial variation on the big-step semantics: I suspend the
* actual calculation of the value and pair the thunk with the original
* expression. This is used to make the comparison with bill_denotation
* more direct (see below). *)
fun bigstep e = (fn () => bigstep0 e, e)
(* ------------------ END OF OPERATIONAL SEMANTICS ------------------- *)
(* +++++++++++++++++ INDUCTION SCHEMA ON SYNTAX ++++++++++++++++++++++ *)
(* parameterized denotational semantics (i.e., just a generic induction
* on the structure of an expression) *)
fun param_den (vfun, cfun, afun, lfun, pfun) =
let fun den (Var v) = vfun v
| den (Con c) = cfun c
| den (App (e1, e2)) = afun (den e1, den e2)
| den (Lam (v, e)) = lfun (v, den e)
| den (POp (p, e1, e2)) = pfun (p, den e1, den e2)
in den
end
(* --------------- END Of INDUCTION SCHEMA ON SYNTAX ----------------- *)
(* ++++++++++++++ BILL RICHTER-STYLE "DENOTATIONAL" SEMANTICS ++++++++ *)
(* type of a Bill-style "denotation"; the value part is suspended to
* avoid premature non-termination or stuck-ness *)
type bill_den = (unit -> value) * exp
(* Bill-style "denotational" semantics, using param_den.
* The functions that parameterize param_den do not refer to each other
* or to bill_denotation (but see below). *)
val bill_denotation : exp -> bill_den =
let fun vfun v = (fn () => raise Stuck, Var v)
fun cfun c = (fn () => VCon c, Con c)
fun afun (d1: bill_den, d2: bill_den) =
(fn () =>
(case (#1 d1 (), #1 d2 ())
of (VLam (v, b), x) => #1 (bigstep (subst (b, v, v2e x))) ()
| _ => raise Stuck),
App (#2 d1, #2 d2))
fun lfun (v, d: bill_den) = (fn () => VLam (v, #2 d), Lam (v, #2 d))
fun pfun (p, d1: bill_den, d2: bill_den) =
(fn () => (case (#1 d1 (), #1 d2 ())
of (VCon c1, VCon c2) => VCon (apply (p, c1, c2))
| _ => raise Stuck),
POp (p, #2 d1, #2 d2))
in
param_den (vfun, cfun, afun, lfun, pfun)
end
(* claim: bill_denotation = bigstep (up to alpha)
* proof: easy by induction on structure of argument (don't you love
* structural induction?);
* ===> We have won absolutely NOTHING as bill_denotation and bigstep are
* the SAME FUNCTION. But bigstep was used to define bill_denotation!
* That's the mathematical joke that Will Clinger has been
* referring to.
* I could have used bigstep0 instead of bigstep -- which would have
* made the two functions slightly different from each other. The main
* complaint, though, still stands: bigstep0 can be recovered from
* bill_denotation and vice versa in a trivial manner, so nothing is won
* defining the latter if the former already was available.
* So the definition of bill_denotation, while not formally circular,
* is nevertheless morally circular: it refers to bigstep -- which
* turns out to be exactly the same thing under a different name. *)
(* --------- END OF BILL RICHTER-STYLE "DENOTATIONAL" SEMANTICS ------- *)
(* +++++++ A BETTER (I.E., TRADITIONAL) DENOTATIONAL SEMANTICS ++++++++ *)
datatype better_den_value = BVCon of con
| BVLam of (better_den_value -> better_den_value)
type env = var -> better_den_value
type better_den = env -> better_den_value
val better_denotation : exp -> better_den =
let fun vfun v env = env v
fun cfun c _ = BVCon c
fun afun (d1, d2) env =
case (d1 env, d2 env)
of (BVLam f, x) => f x
| _ => raise Stuck
fun lfun (v, d) env = BVLam (fn x => d (bind (env, v, x)))
fun pfun (p, d1, d2) env =
case (d1 env, d2 env)
of (BVCon c1, BVCon c2) => BVCon (apply (p, c1, c2))
| _ => raise Stuck
in
param_den (vfun, cfun, afun, lfun, pfun)
end
(* Properties: - no reference to operational semantics, so
* neither formally nor morally circular in its definition
* - more concise
* - far more abstract *)
(* Matthias Blume *)
|