In this chapter we introduced programming languages and we explained the need for high-level programming languages. Programming languages are formally defined by a grammar of abstract syntax and a semantic specification over the syntax. Three different kinds of semantics were introduced and were used to give the semantics for the sample programming language TLLF: A denotational description defining the meaning of programs extensionally, and two small-step operational descriptions defining the meaning of programs intensionally.
In the following chapter we show that indeed the three semantics are equivalent.
We did not make a distinction between static semantics and dynamic semantics. Via the introduction of a type system the set of well-formed programs can be defined to be the set
of closed expressions that can be type-checked. The introduction of such a static semantics would rule out expressions that by repeated application of the one-step reduction function would eventually reach a stuck term. Furthermore, we silently ignored axiomatic frame-works, because they will not be used in the following chapters.
Chapter 5
λ -calculi, programming languages, and semantic artifacts
In the previous chapter we loosely argued that the three different semantics for the tiny programming language TLLF define the same semantics. No proposition like
EJeKTLLFmt_env=inVal(inBasicb) ⇐⇒ runTLLFe=b ⇐⇒ evalTLLFe=b[s]
was included. In this chapter we will see how such propositions are proved by applying well-known meaning-preserving transformations to the semantic artifacts.
Roadmap We begin in Section 5.1 with Plotkin’s classical work on relations between λ-calculi and programming languages [59]. We then introduce the ‘syntactic’ correspondence in Section 5.2 and the ‘functional’ correspondence in Section 5.3 investigated by Danvy et al. [2–5, 8–10]. We introduce in Section 5.2 theλ^ρ-calculus, we illustrate the syntactic cor-respondence starting from the reduction semantics for TLLF (which is a strategy in the λρ^-calculus), and we mechanically derive the abstract machine for TLLF. We illustrate the functional correspondence in Section 5.3 by starting from a definitional interpreter for TLLF (which is the denotational semantics for TLLF with a semantics for the metalanguage) and mechanically derive the abstract machine for TLLF.
5.1 Call by value, call by name, and the λ-calculus
Plotkin’s starting point is Landin’s definitional SECD machine for the programming lan-guage ISWIM which was introduced on page 49. Plotkin aims for a calculus of terms that corresponds to the core of ISWIM, i.e., applicative expressions (AE). We will be concrete and let the abstract syntax of AE coincide with the abstract syntax of TLLF found on page 46, i.e., pureλ-terms with literal integers andSas basic constants. We let Evalvdenote the defining function for AE according to the SECD machine. It is a partial function mapping closed AEs to values:1
Value v ::= λe|b
1As Plotkin defines the SECD machine it evaluates closed expressions to closures. Unloading the result off the terminal state consists in mapping a closure to the expression it represents via a function Real.
5.1.1 Call by value
When the SECD machine encounters an applicatione e0, it (1) evaluates the operand expres-sione0, (2) evaluations the operator expressione, and if that last expression yields a closure hλx.e00, ρiit (3) evaluatese00in the environmentρextended with a binding ofxto the value ofe0. Such a calling mechanism is said to be (right-to-left) call-by-value.
Correspondence with theλv-calculus In the following theorem, due to Plotkin, normalizev
denotes the normalization function from Section 3.3.3;edenotes a closed AE which is also a term in theλv-calculus:
Theorem 4 (Plotkin I) normalizeve=v⇐⇒ Evalve=v
In words, Plotkin has shown that considering a closed expression either (1) evaluation via the SECD machine and weak head normalization in theλv-calculus (following the standard reduction strategy7→v) both do not yield a value or (2) they both yield the same value. From Proposition 4 on page 43 it especially follows thate =βvδ b ⇐⇒ Evalve = b. The SECD machine evaluates a program to a basic constant if and only if the program can be proved equal to that basic constant in theλv-calculus. Abstractions will be equal in=βvδ. In general the abstractions are different because in theλv-calculus, reductions can be performed in the body of abstractions.
Soundness and Incompleteness of theλv-calculus Plotkin also introduces the notion of operational equivalence between expressions, which gives a more general notion of correctness of theλv-calculus with respect to the programming language represented by Evalv(i.e., the SECD machine). The above property only consider closed expressions, i.e., whole programs.
Operational equivalence (≈) is defined via the notion of contexts forλ-expressions as defined on page 9:
e≈e0 iff
EvalvC[e],EvalvC[e0]are both undefined, or EvalvC[e] =b ⇐⇒ EvalvC[e0] =b
for all closedC[e], C[e0]
In the definitioneande0 are not restricted to closedλ-expressions. If one of the evaluations yields a basic constantbthe other evaluation also yieldsb. If one of the evaluation yields an abstraction the other evaluation also yields an abstraction. Operational equivalence does not demand a relation between these two abstractions.2
The correctness of theλv-calculus wrt. evaluation via the SECD machine (i.e., Evalv) is summarized in the following theorem.
Theorem 5 (Plotkin II) e=βvδe0=⇒e≈e0
In other words, it is only possible to prove two terms equal in theλv-calculus if they are operationally equivalent in the SECD machine. Theλv-calculus is said to be sound wrt. the programming language defined by the SECD machine.
2If evaluation was defined to give, e.g., a symbol ‘abstraction’ when evaluation yields an abstraction the definition of operational equivalence simplifies to EvalvC[e] =EvalvC[e0]for all closedC[e], C[e0]. Felleisen and Flatt [31] follow that approach. They do not consider evaluation via the SECD machine.
The right-to-left direction does not hold: A counter example is two closed expressions that are not equal in theλv-calculus and that both make the SECD machine diverge. In any context with no free variables by construction evaluation yields the same value on the two resulting programs or evaluation is undefined for both programs. The two terms are hence operationally equivalent but by assumption they are not equal in theλv-calculus. The λv-calculus is said to be incomplete wrt. the programming language.
5.1.2 Call by name
Analogously with Evalv in the call-by-value case Plotkin defines Evaln to represent evalua-tion of expressions following call-by-name evaluaevalua-tion order. Evalnthen represents a call-by-name version of the SECD machine. Plotkin shows similar theorems that directly connect the call-by-name evaluation mechanism with weak head normalization in theλβδ-calculus
— theλ-calculus extended with theδ-rule to cope with the introduction of basic constants introduced in Section 2.8. Plotkin likewise proves that the λβδ-calculus is sound and in-complete wrt. the programming language defined by the call-by-name version of the SECD machine.