Operational and Denotational Semantics

Topic

What has been provided thus far are the rules for reducing expressions-- this amounts to the operational semantics of the lambda calculus.

We can also provide a denotational semantics for it. That is, for every expression in the λ-calculus we can say what value it should denote. This can be done by producing a mathematical function Eval[[]] which will take expressions to values. We do this by cases for the three types of l-expression.

i) for a variable, say v, we need the notion of an environment, say env, which is a function which maps the names of variables to their values. In which case, our Eval function should be a function of two variables and the value of a variable is just its value in the environment

Eval[[ v, env]] = env[v].

ii) for an application, say (P Q), the value should be the value of the function applied to the value of the argument

Eval[[(P Q), env]] = (Eval[[P, env]] Eval[[Q, env]])

iii) for an abstraction, say λv.Q, the value of it should be a function. And one way of giving the value of a function is by saying what value that function has when applied to an arbitrary argument, say arg, and that will be the body of the abstraction evaluated in the environment extended to include v having the value arg.

Eval[[λv.Q, env]][arg] = Eval[[Q, env[v=arg]]]

where env[v=arg][v] = arg and env[v=arg][w] = env[w] for any variable w different from v.

And Scott and Stoy have the domain theory to show that this is OK. [You might want to check Dana Scott and Christopher Strachey [1971]. Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. PRG-6. 1971. and Joseph E. Stoy [1977], Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. Best of luck!]

The reduction of some expressions never terminates. These can be given a denotation ⊥

Eval[[<non terminating>, env]] = ⊥ (* pronounced 'bottom' *)

And this leads to another important definition.

A function f is strict iff f[⊥] = ⊥ and similarly for functions of several variables (for strict functions, if one of the arguments is undefined, the whole function is undefined).

The example which most springs to mind here is if-then-else with the 'condition' true, the 'then' with a value, but yet with the 'else' undefined

If[TRUE,1,⊥] to let this have the value 1 is to treat it in a non-strict way; to say that it is undefined and had the value ⊥ is to interpret it strictly.

And this notion is extended to languages, a language is strict iff all its functions are strict.