A Provably Correct Translation of the λ-Calculus into a Mathematical Model of C++

Rose H. Abdul Rauf^{∗}, Ulrich Berger, Anton Setzer^{†}^{‡}

November 9, 2006

Abstract We introduce a translation of the simply typed λ-calculus into C++, and give a mathematical proof of the correctness of this translation. For this purpose we develop a suitable fragment of C++ together with a denotational semantics. We then introduce a formal translation of the λ-calculus into this fragment, and show that this translation is correct with respect to the denotational semantics and complete. We introduce a mathematical model for the evaluation of programs of this fragment, and show that the evaluation computes the correct result with respect to this semantics.

1 Introduction

C++ is a general purpose language that supports object-oriented programming as well as procedural and generic programming, but unfortunately not directly functional programming. We have developed a parser-translator program that translates typed λ-terms into C++ statements so as to integrate functional concepts. The translated code uses the object-oriented approach of programming that involves the creation of classes for the λ-term. By using inheritance, we achieve that the translation of a λ-abstraction is an element of a function type.

In this article, we do not only present this translation, but give as well a mathematical proof that it is correct. For this purpose we introduce a suitable fragment of C++ with a precise denotational semantics. We give a formal translation of λ-terms into this fragment and show that it preserves this semantics. We will show as well completeness, i.e. essentially all programs in this fragment of C++ can be obtained by translating terms of the λ-calculus. We develop a mathematical model for the evaluation of programs in this model, and show that this evaluation is correct with respect to the denotational semantics. This shows that our translation results in C++ programs which are evaluated correctly in our mathematical model of C++.

We hope that our model of a fragment of C++ which includes a formal model of the heap, will have applications which go beyond the translation of the typed λ-calculus. We expect that extensions of this model can be used to verify formally the correctness of more complex C++ programs, including programs with side effects.

∗Faculty of Information System and Quantitative Science, University of Technology MARA, 40450 Shah Alam, Selangor D.E., Malaysia. Email: hafsah@tmsk.uitm.edu.my

†Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK. Email: {u.berger,a.g.setzer}@swansea.ac.uk

‡Supported by EPSRC grant GR/S30450/01.

Organisation of the paper. In Sect. 2 we introduce the typed λ-calculus together with a standard denotational semantics. In Sect. 3, we present our parser-translator program, which translates λ-terms into the full language of C++. We discuss how the translated code is executed including a description of the memory allocation. Since it is not feasible (at least for our group) to prove the correctness of our translation with respect to the full operational semantics of the very complex language C++, we develop in Sect. 4 a small fragment of C++ into which we can translate the typed λ-calculus. We introduce as well the evaluation of applicative terms in this language. In Sect. 5 we give a formal translation of the typed λ-calculus into this fragment. We introduce a denotational semantics of the fragment of C++ and show correctness and completeness of the formal translation: The translation respects the denotational semantics, and essentially all applicative terms can be obtained by translating suitable typed λ-terms (completeness). In Sect. 6 we show that the evaluation of λ-terms is correct with respect to the denotational semantics. This proof makes use of a Kripke-style logical relation. We conclude with an overall result, namely that if we translate a λ-term into the fragment of C++ and evaluate it, we obtain the correct result with respect to the denotational semantics.

Related work. Several researchers [Kis98], [Läu95] have discovered that C++ can be used for functional programming by representing higher order functions using classes. Our representation is based on similar ideas. There are other approaches that have made C++ a language that can be used for functional programming such as the FC++ library [MS00] (a very elaborate approach) as well as FACT! [Str] (extensive use of templates and overloading) and [Kis98] (creating macros that allow creation of single macro-closure in C++). What is different in our paper is that we develop a mathematical model of a fragment of C++, and that we formally prove the correctness of our translation.

The approach of using denotational semantics and logical relations for proving program correctness has been used before by Plotkin [Plo77], Reynolds [Rey83] and many others. The method of logical relations can be traced back at least to Tait [Tai67] and has been used for various purposes (e.g. Jung and Tiuryn [JT93], Statman [Sta85] and Plotkin [Plo80]). To our knowledge the verification of the implementation of the λ-calculus in C++ (and related object-oriented languages) using logical relations is new.

There are other fragments of object-oriented languages in the literature which are used to prove the correctness of programs. A well-known example is Featherweight Java ([IPW99]). The model for this language avoids the use of a heap, since methods do not modify instance variables. In contrast, our model of C++ does make use of a heap and is therefore closer to the actual implementation of C++. Although our fragment of C++ does not allow for methods with side effects, it could easily be extended this way and then used to verify programs in C++ with side effects.

Acknowledgements: We would like to thank the referees of earlier versions of this paper for valuable comments.

1.1 General Notations

Notation 1.1 (Finite maps) By X →_{fin} Y we denote the set of finite maps from the set X to the set Y, that is, the set of functions f: dom(f) → Y where dom(f) is a finite subset of X. If f ∈ X →_{fin} Y and (x, y) ∈ X × Y, then f[x ↦ y] denotes the finite function with domain dom(f) ∪ x that sends x to y and any other x′ ∈ domf to f(x′). A list x_{1} : y_{1}, …, x_{n} : y_{n}, where the x_{i} are distinct elements of X and the y_{i} are in Y, denotes an element of X →_{fin} Y in the obvious way. Furthermore, f, x : y := f[x ↦ y].

In this article we observe a strict naming convention: Once a group of letters has been used to range over a certain entity (e.g. A, B (but not C) range over types), letters in that group (possibly with sub- or superscripts) will always denote instances of that entity. There will be only two exceptions: x, y, z may denote elements of unspecified sets X, Y, Z as well as variables (Definition 2.2), and f ranges over unspecified functions as well as basic C++ functions 2.1. For the reader’s convenience there is a complete table of notations in Sect. 8 at the end of this article

2 The Typed λ-Calculus

We introduce a version of the typed λ-calculus based on base types, which are native C++-types, and basic functions, which are native C++-functions.

Assumption 2.1 (a) We fix a set basetype of base types ρ, σ, . . .. One specific base type is the type of integers int.

(b) We fix a set F of names for basic functions f : (ρ_{1}, …, ρ_{k}) → σ.

(c) We view functions of arity 0 as constants and denote them by the letter n.

(d) Let [[ρ]] denote the set of elements of base type ρ. In case of int, [[int]] is the set of integers.

(e) Let [[f]] : [[ρ_{1}]] × … × [[ρ_{k}]] → [[σ]] be the function denoted by f ∈ F. Especially we assume that a constant (0-ary function) n, which stands for the integer n, is interpreted by itself (i.e. by n).

Any native C++ type can be used as a base type, and any native C++ functions without side effects (including constants) can be used as basic functions ^{1}.

Definition 2.2 (Simply typed λ-calculus with basic functions)

(a) We fix a set Var of variables x, y, z, . . ..

1The translation given below makes sense as well fore functions with side effects, including those which affect instance variables of the classes used. However, in this case we would go beyond the simply typed λ-calculus, and could not use the simple denotational semantics of the λ-calculus in order to express the correctness of the translation.

(b) The sets of types, contexts and λ-terms are defined as follows:

Types:  Type ∋ A, B, E, F ::= ρ | A → B
Contexts: Context ∋ Γ, Δ  ::= Var →_{fin} Type
λ-terms: Term ∋ r, s, t  := x | f[r_{1}, …, r_{k}] | r s | λx^{A}.r

(c) The relation Γ ⊢ r : A is inductively defined by the following standard typing rules:

Γ, x : A ⊢ x : A  \frac{Γ, x : A ⊢ r : B}{Γ ⊢ λx^{A}r : A → B}  \frac{Γ ⊢ r : A → B  Γ ⊢ s : A}{Γ ⊢ r s : B}

\frac{Γ ⊢ r_{1} : σ_{1} … Γ ⊢ r_{k} : σ_{k}}{Γ ⊢ f[r_{1}, …, r_{k}] : ρ} (f : (ρ_{1}, …, ρ_{k}) → σ)

Note that we do not have any product types and that native C++-functions are not necessarily objects – they can even be constants such as integers– therefore the rule for f[r_{1}, …, r_{k}] is not subsumed by the rule for r s.

The simply type λ-calculus has a well-known operational semantics defined by β-reduction, (λx^{A}r)s →_{β} r[s/x], and function reduction, f[n_{1}, …, n_{k}] →_{f} [[f]](n_{1}, …, n_{k}). But there is also an equivalent denotational semantics which, for our purposes, will be more convenient to work with. Since our calculus does not allow for recursive definitions, it is possible to interpret types and terms in a naive set-theoretic hierarchy D of functionals of finite types over the base types:

Definition 2.3 For A ∈ Type we define the set D(A) of functionals of finite types over A by induction on A:

D(ρ) := [[ρ]]
D(A → B) := the set of functions from D(A) to D(B)
D := ⋃_{A∈Type} D(A)

Semantic values (elements of D(A)) are denoted by d.

Definition 2.4 (a) A functional environment is a mapping ξ : Var → D. FEnv denotes the set of all functional environments.

(b) If Γ is a context, then ξ : Γ means ∀x ∈ dom(Γ).ξ(x) ∈ D(Γ(x)).

Definition 2.5 (Denotational semantics of the simply typed λ-calculus) For every typed λ-term Γ ⊢ r : A and every functional environment ξ : Γ the denotational value [[r]]ξ ∈ D(A) is defined by

[[x]]ξ = ξ(x)
[[f[r_{1}, …, r_{k}]]]ξ = [[f]]([[r_{1}]]ξ, …, [[r_{k}]]ξ)
[[r s]]ξ = [[r]]ξ([[s]]ξ)
[[λx^{A}.r]]ξ = λλd ∈ D(A).[[r]]ξ[x ↦ d]

3 Translation of Typed λ-Terms into C++

In this section we describe how to translate simply typed λ-terms into C++ using the object-oriented concepts of classes and inheritance.

The translation generates new identifiers, which we need to disambiguate; in order for this to work, we restrict ourselves to the translation of finitely many λ-terms and types at a time. We first define an identifier name(A) : String for finitely many A : Type. Here String is the set of strings.

• If ρ is a native C++-type, name(ρ) is a C++ identifier obtained from ρ. This is ρ, if ρ is already an identifier, and the result of removing blanks and modifying symbols not allowed in identifiers (e.g. replacing ∗ by x), in case ρ is a compound type like long int or ∗ ρ. ^{2}

• name(A → B) :=“C”∗name(A)∗“ ”∗name(B)∗“D”, where ∗ means concatenation. Here C stands for an open bracket, D for a closing bracket, and for the arrow in this identifier. By using these symbols we obtain valid C++-identifiers.^{3}

For instance name(int → int) =“Cint intD”, name((int → int) → int) = “CCint intD intD”. In the following, we write CA BD instead of name(A → B) and CA BD aux instead of name(A → B)∗” aux” (that type will be introduced below), similarly for other types.

For every A ∈ Type we introduce a series of class definitions, after which name(A) is a valid C++ type (assuming class definitions for any native C++ type used):

• For native C++-types the sequence of class definitions is empty.

• The sequence of class definitions for A → B consists of the class definitions of A, the class definitions of B not contained in the class definitions of A and additionally

      class CA_BD_aux{
        public: virtual B operator () (A x)=0;};
      typedef CA_BD_aux * CA_BD;

So, CA BD aux is a class with one virtual method used as application,^{4} which maps an element of type A to an element of type B. CA BD is a pointer to an element of this class. The body of this method will then be the body of the function to be invoked when applied to its arguments.

Now we define for every λ-term r a sequence of C++-class definitions and a C++-term r^{C++}, s.t. if r : A, then r^{C++} is of type name(A). ^{5} • If x is a variable, then the class definitions for introducing x are empty

2This modification might result in name clashes, in which case one adds some string like n for some integer n in order to disambiguate the names. Since we are translating only finitely many λ-types at any time, this way of avoiding name clashes is always possible.

3Again, we might need to disambiguate the identifiers as it was done for native C++ types.

4In C++, if an object o has a method B operator () (A x), invocation of this method is written like application, i.e. as o(s). Note however that Java objects correspond in C++ to pointers to C++-objects. A pointer o' to an object o has first to be dereferenced, written as (* o'), and therefore o' applied to s is written as (* o')(s). Note that, when creating an object using new, we obtain a pointer to an object.

5Strictly speaking, r^{C++} depends on the choice of identifiers for λ-types and C++-classes representing λ-terms. When defining the parse function P in Sect. 6, this will be made explicit

and x^{C++} := x.

• Let t = λx^{A}.r be of type A → B. Assume the free variables of t are of type x_{1} : A_{1}, …, x_{k} : A_{k} and that t is a new identifier. Assume name(A_{i}) = Ai, xi is the C++-representation for x_{i}, name(A) = A, name(B) = B, and r^{C++} = r. The class definition for t consists of the class definition for r together with

class t : CA_BD_aux{
  public:
    A1 x1;
    ...
    An xk;
    t(A1 x1,A2 x2, ... , Ak xk){
         this->x1 = x1;
         ...
         this->xk = xk;}
    virtual B operator () (A x){
          return r;};};

t^{C++} := new t(x1, ..., xk).

Therefore the class definition of t has instance variables xi of type Ai. The constructors has one argument for each variable xi and sets the instance variable xi to the value of that argument. The class has one method operator() with one argument x of type A. When invoked, the body of this method r, which is the translation of the body of the λ-term, is evaluated in the environment mapping x to the value of the argument of the method, and xi to the value of this instance variable. Note that no other variables are visible in the body of this method, since this environment might differ between when an object of this class was created and when it is used. That is the reason why one needs to copy first, when creating an object of such a class, the environment into some instance variables.^{6}

When applying an object of this class to an element, the body of the λterm is invoked. The λ-term is translated into the statement which creates a new object with the instance variables set to the value they have in the current environment.

• Assume t = r s. Then the class definitions of t consist of the class definitions for r, and the class definitions for s (where the class definitions corresponding to λ-abstractions occurring in both r and s need only to be introduced once).^{7} Furthermore t^{C++} := (∗(r^{C++}))(s^{C++}).

by having the dependency of this function on the context Γ and the class environment C. Since in our abstract setting λ-types are represented by themselves, P does not depend on the choice of identifiers for those types.

6In C++ there are no inner classes as they occur in Java, which allow references to the current environment.

7A λ-abstraction is represented as a new instance of its corresponding class. Even if the classes for two occurrences of the same λ-abstraction coincide, for each occurrence a new instance is created. Therefore there is no problem, if a variable occurs as the same name, but with different referential meaning in two identical λ-expressions.

So t is interpreted as the result of applying the translation of r to the translation of s.

• Assume t = f[r_{1}, …, r_{k}]. Then the class definitions for t are the class definitions for r_{i} (again class definitions for λ-terms occurring more than once need only to be introduced once). Furthermore, t^{C++} := f(r_{1}^{C++}, ...,r_{k}^{C++}). So t is interpreted as the result of applying the native C++ function f to the translations of r_{i}.

Note that a λ-abstraction is interpreted as a function of its free variables in the form (newt(x_{1}, …, x_{k})). Hence, the evaluation of a λ-abstraction in an environment for the free variables is similar to a “closure” in implementations of functional programming languages.

We have developed a program which parses λ-terms and translates them into the full language of C++. Our intention is to upgrade this to an extension of the language of C++ by λ-types and -terms together with a parser program which translates this extended language into native C++. For this purpose we introduce a syntax for representing λ-types and -terms in C++. We use functional style notation rather than overloading existing C++-notation, since we belief that this will improve readability and acceptability of our approach by functional programmers. In our extended language, we write A –> B for the function type A → B, r^^s for the application of r to s^{8}, and \A x.B s for λx^{A}.s if s : B. (If s is a term starting with λ, B will be omitted). For instance, the term

t = (λf^{int→int}λx^{int}.f (f x)) (λx^{int}. x + 2) 3

is written in our extended C++ syntax as

(\ int->int f. \ int x. int f^^(f^^x))^^(\ int x. int x+2)^^3

As an example, we show how the translation program transforms the term t above into native C++ code. We begin with the class definitions for the λ-types:

class Cint_intD_aux
{ public : virtual int operator() (int x) = 0; };
typedef Cint_intD_aux*  Cint_intD;
class CCint_intD_Cint_intDD_aux
{  public : virtual Cint_intD operator()
                             (Cint_intD x) = 0; };
typedef CCint_intD_Cint_intDD_aux*
        CCint_intD_Cint_intDD;

The class definition for t_{1} := λx^{int}.f (f x) is

class t1 : public Cint_intD_aux{
 public :Cint_intD f;
 t1( Cint_intD f)  {   this-> f = f;};
 virtual int operator () (int x)
 { return (*(f))((*(f))(x)); };
};

8Note that we cannot r(s) here, since this notation will not translate into application, but into (∗ r)(s).

and t_{1}^{C++} = new t1(f). The class definitions for t_{0} := λf^{int→int}λx^{int}.f(fx) and t_{2} := λx^{int}.2 + x (using identifiers t0, t2) are as follows:

class t0 : public CCint_intD_Cint_intDD_aux{
 public :
 t0( ) { };
 virtual Cint_intD operator () (Cint_intD f)
 { return new  t1( f); }
};
 class t2 : public Cint_intD_aux{
 public :
 t2( ) { };
 virtual int operator () (int x)
 { return x + 2; };
};

Finally

t^{C++} := (∗((∗( new t0( )))( new t2( ))))(3);

When evaluating the expression t^{C++}, first the application of t0 to t2 is evaluated. To this end, instances l0, l2 of the classes t0 and t2 are created first. Then the operator() method of l0 is called. This call creates an instance l1 of t1, with the instance variable f set to l2. The result of applying t0 to t2 is l1.

The next step in the evaluation of t^{C++} is to evaluate 3, and then to call the operator() method of l1. This will first make a call to the operator method of f, which is bound to l2, and apply it to 3. This will evaluate to 5. Then it will call the operator method of f again, which is still bound to l2, and apply it to the result 5. The result returned is 7.

We see that the evaluation of the expression above follows the call-by-value evaluation strategy.^{9} Note that l0, l1, l2 were created on the heap, but have not been deleted afterwards. The deletion of l0, l1 and l2 relies on the use of a garbage collected version of C++, alternatively we could use smart pointers in order to enforce their deletion.

4 Modelling a Fragment of C++

In this section we construct a mathematical model of a fragment of C++ that contains the code created by the translation of λ-terms described in the previous section. We model the execution of C++ code by functions eval and apply, similar to the modelling of the λ-calculus in [ASS85]. However, in order to model the C++ implementation as truthfully as possible, we differ from [ASS85] by making the pointer structures for the classes and objects explicit and letting the functions eval and apply modify these pointer structures via side effects.

When we investigate what was needed from C++ in order to translate simply typed λ-terms, we see that the classes obtained have instance variables, one constructor, and one method corresponding to the operator() method. The constructor has one argument for each instance variable and sets the instance variables to these arguments. No other code is performed. The method has one argument, and the body consists of a simplified C++ expression. Here simplified C++ expressions are the C++ expressions occurring in the translation process, which were all translations of λ-terms. Simplified C++-expressions are variables, native C++ functions applied to simplified C++ expressions, the application of one simplified C++ expression to another simplified C++ expression (which corresponds to the method call in case the first applicative term is an object), and the construct new applied to a constructor and simplified C++ expressions.

9Note that this computation causes some overhead, since for every subterm of the form λx.r a new object is created, which is in many cases used only once, and can be thrown away afterwards. One could optimise this, however at the price of having a much more complicated translation, and therefore a much more complex correctness proof of the translation.

We develop a language which formulates this fragment of C++. In this language, a class is be given by a context representing its instance variables, the abstracted variable of the method and its type, and an applicative term. Applicative terms (which correspond to the simplified C++ expressions above) are variables, native C++ functions applied to applicative terms (where C++ functions with no arguments are constants), the application of one applicative term to another applicative term (which corresponds to the method call in case the first applicative term is an object), or a constructor applied to applicative terms (which corresponds to the new-construct).

This fragment could easily be extended in order to cover modification of instance variables and method calls in the body of a method, the possibility of having several methods, and other C++ constructs.

Definition 4.1 (Applicative terms, classes, class environments)

Let Constr be an infinite set of constructors (i.e. class names), denoted by c.

Applicative terms:  App ∋ a, b ::= x | f[a_{1}, …, a_{k}] | a b | c(a_{1}, …, a_{k})
Classes: Class ::= (Γ; x : A; b)
Class environments: CEnv ∋ C ::= Constr →_{fin} Class

Applicative terms (∈ App) correspond to the C++ constructs x, f[a_{1}, ..., a_{k}], (∗ (a))(b) and newc(a_{1}, …, a_{k}). A class (Γ; x : A; b) ∈ Class, where Γ = x_{1} : A_{1}, …, x_{n} : A_{n}, corresponds to a C++ class definition of the form

class c : CA_BD_aux{
  public: A1 x1;
          ...
          An xk;
  c(A1 x1,A2 x2, ... , Ak xk){
                this->x1 = x1;
                ...
                this->xk = xk;}
  virtual B operator () (A x){
               return b;};};

Note that the type B is omitted in (Γ; x : A; b) since it can be derived, and the class name c is associated with the class through the class environment CEnv.

Definition 4.2 We define the free variables FV(a) of an applicative term a ∈ App as follows: FV(x) = {x}, FV(f[a_{1}, …, a_{k}]) := FV(a_{1}) ∪ ⋯ ∪ FV(a_{k}), FV(a b) := FV(a) ∪ FV(b), FV(c(a_{1}, …, a_{k})) := FV(a_{1}) ∪ ⋯ ∪ FV(a_{k}).

When a constructor call of a class is evaluated, its arguments are first evaluated. Then, memory for the instance variables of this class is allocated on the heap, and these instance variables are set to the evaluated arguments. The address to this memory location is the result returned by evaluating this constructor call. The only other possible result of the evaluation of an applicative term is a number, so values are addresses or numbers.

Note as well that on the heap we store elements of the form c(v⃗), which can be represented as elements of Constr×Val^{∗} (here Val is the set of values). Therefore we can model the heap as a finite function from addresses to Constr × Val^{∗}.

Definition 4.3 (Values, closures, heaps, and value environments)

Let Addr be an infinite set of addresses denoted by h.

Let n range over C++ constants, that is, elements of basic C++ types;

Values: Val ∋ v, w ::= n | h
Closures:  Constr × Val^{∗} ::= (c, v_{1}, …, v_{k})
Heaps: Heap ∋ H ::= Addr →_{fin} (Constr × Val^{∗})
Value environments VEnv ∋ η  ::= Var →_{fin} Val

Note that n denotes both constants and elements of basic C++-types. Since constants are to be interpreted by themselves, this doesn’t cause any confusion.

The functions eval and apply defined below have side effects on the heap. This fact can be conveniently expressed using monads.

Definition 4.4 (State monad)

The partial state monad for a given sets X (of states) is the functor M_{X}: Set → Set (the object part of which is)

M_{X}(Y) := X →^{∼} Y × X

where X →^{∼} Y × X is the set of partial functions from X to Y × X.

Elements of M_{X}(Y) are called actions and can be viewed as elements of Y that may depend on a current state x ∈ X and also may change the current state. So, an element of M_{X}(Y) is a partial function which, depending on the current state returns a result and a new state (or fails). Monads are a category-theoretic concept whose computational significance was discovered by Moggi [Mog91].

We need to work with partial instead of total functions because the operations eval and apply defined below do not yield defined results in general. We will however prove that for inputs that can be typed the results will always be defined.

Notation 4.5 (do, return, mapM, read, add) We use the following standard monadic notation (roughly following Haskell syntax): Suppose e_{1} : M_{X}(Y_{1}), …, e_{k+1} : M_{X}(Y_{k+1}) are actions where e_{i} may depend on y_{1} : Y_{1}, …, y_{i−1} : Y_{i−1}. Then

do{y_{1} ← e_{1} ; …; y_{k} ← e_{k} ; e_{k+1}} : M_{X}(Y_{k+1})

is the action that maps any state y_{0} : Y to (y_{k+1}, x_{k+1}) where (y_{i}, x_{i}) ≃ e_{i} x_{i−1}, for i = 1, …, k+1 (≃ denotes the usual “partial equality”). The intuitive idea is that the do-expression is computed by evaluating e_{0}, …, e_{k+1} in sequence, where e_{i} can make use of the result y_{j} returned by e_{j} (j < i). The result returned is that of e_{k+1}, and the computation of each e_{i} might change the state.

We also allow let-expressions with pattern matching within a do-construct (with the obvious meaning). We adopt the convention that computations are “strict”, i.e. the result of a computation is undefined if one of its parts is. Furthermore, we use the standard monadic notations

return : Y → M_{X}(Y)  return y x = (y, x)
mapM : (Z → M_{X}(Y)) → Z^{∗} → M_{X}(Y^{∗}) mapM f z⃗ = do{y_{1} ← f z_{1} ; …
…; y_{k} ← f z_{k} ; return (y⃗)}

as well as

read : X → M_{X→_{fin}Y} (Y), read x m ≃ (m x, m)
add : Y → M_{X→_{fin}Y} (X), add y m ≃ (x, m[x ↦ y]) where x = fresh(m)

Here, fresh is a function with the property that if m : X →_{fin} Y, then fresh(m) ∈ X \ dom(m) ^{10}.

Definition 4.6 We define functions

eval :  CEnv → VEnv → App → M_{Heap}(Val)
apply :  CEnv → Val → Val → M_{Heap}(Val)

by mutual recursion as follows (in Sect.6 we will omit the argument C, since it will be a global parameter):

eval C η x = return (η x)
eval C η f[a⃗] = do{n⃗ ← mapM (eval C η) a⃗ ; return [[f]](n⃗)}
eval C η (a b) = do{(v, w) ← mapM(eval C η) (a, b) ; apply C v w}
eval C η c(a⃗) = do{v⃗ ← mapM (eval C η) a⃗ ; add (c, v⃗)}
apply C h v = do{(c, w⃗) ← read h ; let (y⃗ : B⃗; x : A; a) = C c in eval C [y⃗, x ↦ w⃗, v] a}
apply C n v = ∅

where ∅ is the undefined action, i.e. the partial function with empty domain^{11}.

Lemma 4.7 (1) If eval C η a H = (v, H′), then H ⊆ H′.

(2) If apply C v w H = (v′, H′), then H ⊆ H′.

Proof. Straightforward simultaneous induction on the definitions of eval and apply, i.e. by “fixed point induction” [Win93]. q.e.d.

Due to the complexity of C++ it would be a major task, which would require much more man power than was available in our research group, to formally prove that our mathematical model, given by eval and apply, coincides with the operational semantics of C++.^{12} (Note that other models of fragments of object-oriented languages in the literature face the same problem and their correctness w.r.t. real languages is therefore usually not shown.) However, when going through the definitions we observe that the evaluation function eval is indeed defined in accordance with the expected behaviour of C++:

10In our applications X will be a space of addresses which we assume to be infinite, i.e. we assume that the allocation of a new address is always possible.

11It would be more appropriate to let apply C n v result in a finite error, but, for simplicity, we identify errors with non-termination.

• A variable is evaluated by returning its value in the current environment η.

• The application of a native C++ function to arguments a_{1}, …, a_{k} is carried out by first evaluating a_{1}, …, a_{k} in sequence, and then applying the function f to those arguments.

• Note that constants are special cases of functions with arity 0, and therefore constants are evaluated by themselves.

• (a b) corresponds in C++ to the construct (∗ (a))(b). First a and b are evaluated. Because of type correctness, a must be an element of the type of pointers to a class, and the value of a will therefore be an address on the heap. On the heap the information about the class used and the values of the instance variables of that class are stored. Then (∗ (a))(b) is computed by evaluating the body of the method of the class in the environment where the instance variables have the values as stored on the heap, and the abstracted variable has the result of evaluating b. This is what is computed by eval η (a b) (which makes use of the auxiliary function apply).

• The expression c(a⃗), which stands for the C++ expression newc(a_{0}, …, a_{k}), is evaluated by first computing a_{0}, …, a_{k} in sequence. Then new storage on the heap is allocated. Note that in our simplified setting, the constructor of c simply assigns to the instance variables the values of a_{0}, …, a_{k}. Consequently, the intended behaviour of C++ is that it stores on the heap the information about the class used and the result of evaluating a_{0}, …, a_{k}, which is what is carried out by eval.

5 Formal Translation of Typed λ-Terms and its Correctness

Despite of the fact that we could describe only informally the connection of our mathematical model with the actual implementation of C++, we will be able to prove formally that the model as well as the translation of λ-terms described in Section 3 are correct in the following sense: As we did for λ-terms, we will define for C++ terms, a ∈ App, a typing relation, Γ ⊢ a : A, and a denotational semantics, [[ a]]^{H}ξ ∈ D(A). Similarly, we will define for values, v ∈ Val, a relation H ⊢ v : A and a semantics [[ v]]^{H} ∈ D(A) (all these definitions will depend on a class environment C ∈ CEnv). Our main results will be the correctness of the translation function, P (see below), and the evaluation function, eval, with respect to these typing relations and denotational semantics (Theorems 5.6 and 6.9).

12The formalisation of the semantics of Java in [SSB01] was a major project, and still this book excludes some features of Java like inner classes. Note that C++ is much more complex than Java.

In this section we carry out the first step, namely the introduction of the parsing relation and a proof that it is correct and complete. In the next section we will show that the evaluation of applicative terms is correct as well and obtain the correctness of our implementation.

Definition of the Parse Function P

We are going to define a formal analogue to the translation of λ-terms described in Section 3. We use the monadic notation from Section 4.

Definition 5.1 (Definition of the Parse Function P) We define a function

P :  Context → Term → M_{CEnv}(App)

by recursion on terms as follows:

P Γ x = return x, if x is a variable
P Γ f[r⃗] = do{a⃗ ← mapM (P Γ) r⃗ ; return f[a⃗]}
P Γ (r s) = do{(a, b) ← mapM (P Γ) (r, s) ; return (a b)}
P Γ (λx^{A}.r) = do{a ← P (Γ, x : A) r ; c ← add(Γ; x : A; a) ; return c(dom(Γ))}

Hence, the translation has a side effect on the class environment.

Lemma 5.2 P Γ r is total and if P Γ r C = (a, C′), then C ⊆ C′.

Proof. Induction on the term r. q.e.d.

Typing and denotational semantics of applicative terms

Definition 5.3 (Typing of Applicative Terms) We define inductively a typing relation C; Γ ⊢ a : A (where we sometimes write Γ ⊢ a : A instead, if C is a global fixed parameter):

C; Γ, x : A ⊢ x : A

\begin{matrix}f ∈ F, f : (ρ_{1}, …, ρ_{k}) → σ \\ C; Γ ⊢ a_{i} : A_{i} (i = 1, …, k) \end{matrix} ; C; Γ ⊢ f[a_{1}, …, a_{k}] : B

\begin{matrix}C; Γ ⊢ a : A → B & C; Γ ⊢ b : A \\ C; Γ ⊢ a b : B \end{matrix}

{C(c) = (Δ; x : A; a) Δ = x_{1} : A_{1}, …, x_{k} : A_{k} \atop C; Δ, x : A ⊢ a : B} ; C; Γ ⊢ a_{i} : A_{i} (i = 1, …, k) ; C; Γ ⊢ c(a_{1}, …, a_{k}) : A → B

Definition 5.4 (Denotational semantics of applicative terms) If C; Γ ⊢ a : A, then for every functional environment ξ ∈ FEnv such that ξ : Γ we define [[ a]]^{C}ξ ∈ D(A) (we write [[ a]]ξ if C is a fixed global parameter):

[[ x]]^{C}ξ := ξ(x)
[[ f[a_{1}, …, a_{k}] ]]^{C}ξ := [[ f ]]([[ a_{1} ]]^{C}ξ, …, [[ a_{k}]]^{C}ξ)
[[ a b]]^{C}ξ := [[ a]]^{C}ξ([[ b]]^{C}ξ)
[[ c(a_{1}, …, a_{k}) ]]^{C}ξ := λλd ∈ D(A).[[ a]]^{C}ξ′[x ↦ d]

where in the last clause it is assumed that we have C(c) = (Δ; x : A; a) with C; Δ, x : A ⊢ a : B, Δ = x_{1} : A_{1}, …, x_{k} : A_{k} and C; Γ ⊢ a_{i} : A_{i} (i = 1, …, k), and ξ′ is defined by ξ′(x_{i}) := [[ a_{i}]]^{C}ξ for i = 1, …, k.

Lemma 5.5 (a) If C ⊆ C′, Γ ⊆ Γ′, C; Γ ⊢ a : A, then C′; Γ′ ⊢ A.

(b) If C; Γ ⊢ a : A, C; Γ ⊢ a : A′, then A = A′.

(c) If C ⊆ C′, Γ ⊆ Γ′, ξ ⊆ ξ′, C; Γ ⊢ a : A, and ξ : Γ, ξ′ : Γ′, then [[ a]]^{C}ξ = [[ a]]^{C′}ξ′.

Proof: Straightforward.

Correctness of the Parse Function P

Theorem 5.6 If r is a λ-term, Γ ⊢ r : A, then P Γ r C ≃ (a, C′) for some C′, a s.t. C′; Γ ⊢ a : A and for all ξ : Γ we have [[ r]]ξ = [[ a]]^{C′}ξ.

Proof: Induction on the derivation of Γ ⊢ r : A. The only interesting case is r = λx^{B}.r′, where we have Γ, x : B ⊢ r′ : A. Assume Γ = x_{1} : A_{1}, …, x_{k} : A_{k} and let x⃗ := x_{1}, …, x_{k}. By induction hypothesis P (Γ, x : B) r′ C = (a′, C_{1}) for some C_{1}, a′ s.t. C_{1}; Γ, x : B ⊢ a′ : A, and for d ∈ D(A) we have [[ r′]]ξ[x ↦ d] = [[ a′]]^{C_{1}}ξ[x ↦ d]. Then P Γ r C = (c(x⃗), C_{2}), where C_{2} := C_{1}[c ↦ (Γ; x : B; a′)], for some fresh c. C_{2}; Γ ⊢ x_{i} : A_{i}, and by monotonicity C_{2}; Γ, x : B ⊢ a′ : A, therefore C_{2}; Γ ⊢ c(x⃗) : B → A. Furthermore, [[ x_{i}]]^{C_{2}}ξ = ξ(x_{i}), therefore ξ′ ⊆ ξ for the ξ′ as in the definition of [[ c(x⃗) ]]^{C_{2}}ξ. Therefore [[ c(x⃗) ]]^{C_{2}}ξ = λλd.[[ a]]^{C_{2}}ξ′[x ↦ d] = λλd.[[ a]]^{C}ξ[x ↦ d] = λλd.[[ r′]]ξ[x ↦ d] = [[ r]]ξ. q.e.d.

Completeness of the Parse Function P

In addition to the correctness of the translation function P we show the opposite direction, namely completeness: the translated versions of typed λ-terms are already essentially all typed elements of App. The only restriction is that constructors are only applied to variables, and that they are applied to all variables in the context, independently of whether the variables occur in the body of the class or not.

Definition 5.7 Let C; Γ ⊢′ a : A be defined by the same rules as for C; Γ ⊢ a : A, except for the rule of deriving C; Γ ⊢ c(a_{1}, …, a_{k}) : A → B, which is replaced by the following:

{C(c) = (Γ; x : A; a) Γ = x_{1} : A_{1}, …, x_{k} : A_{k} \atop C; Γ, x : A ⊢′ a : B} ; C; Γ ⊢′ c(x_{1}, …, x_{k}) : A → B

Remark 5.8 In Theorem 5.6 we have as well C′; Γ ⊢′ a : A.

We have no control over the choice of class names (constructors) introduced by the parse function. So a class term will in general only be reached by the parse function up to renaming of class names. Furthermore, if in a λ-term there exist the same λ-term twice as a subterm, the parse function will assign different class names to each occurrence of it. (One could improve the parse function so that this doesn’t take place.) Therefore, if we want to obtain an element a of App by parsing a λ-term r, it might be that in the parsed λ-term a′ there are two different constructors which correspond to the same constructor in a. So we obtain an element of App by parsing a λ-term only up to renaming and possibly identification of class names. The following definition of a class homomorphism makes this explicit:

Definition 5.9 (a) Let θ : Constr →_{fin} Constr. Then θ(a) is defined if each constructor occurring in a is an element of dom(θ). If θ(a) is defined, then θ(a) is the result of replacing each occurrence of c ∈ Constr in a by θ(c). Furthermore, for (Γ; x : B; a) ∈ Class we define θ(Γ; x : B; a) :≃ (Γ; x : B; θ(a)).

(b) Let C, C′ ∈ CEnv. θ : dom(C′) → dom(C) is a CEnv-homomorphism, if ∀c ∈ dom(C′).θ(C′(c)) = C(θ(c)).

Theorem 5.10 (Completeness of the Parse Function P) Assume C; Γ ⊢′ a : A, and C′ ∈ CEnv. Then there exists a λ-term r, a CEnv-homomorphism θ : C′′ → C, and an a′ ∈ App s.t. the following holds

\begin{aligned}Γ & ⊢ & r : A , \\ P Γ r C′ & = & (a′, C′ ∪ C′′) , \\ C′ ∪ C′′; Γ & ⊢ & a′ : A , \\ θ(a′) & = & a . \end{aligned}

Proof: Induction on C; Γ ⊢′ a : A.

Case Γ = x_{1} : A_{1}, …, x_{k} : A_{k}, a = c(x_{1}, …, x_{k}), A = A′ → B′, C(c) = (Γ; x : A′; a′), C; Γ, x : A′ ⊢ a′ : B′. Assuming C′ we find by induction hypothesis C_{0}, a CEnv-homomorphism θ′ : C_{0} → C, a λ-term r′, a′′ ∈ App s.t. P (Γ, x : A′) r′ C′ = (a′′, C′ ∪ C_{0}) and θ′(a′′) = a′. Then P Γ (λx^{B}.r′) C′ = (c_{0}(x_{1}, …, x_{k}), C′ ∪ C_{0}[c_{0} ↦ (Γ; x : B; a′′)]) for some fresh c_{0}. Let a′ := c_{0}(x_{1}, …, x_{k}), C′′ := C_{0}[c_{0} ↦ (Γ; x : B; a′′)], θ := θ′[c_{0} ↦ c], r := λx^{B}.r′.

The other cases are straightforward. q.e.d.

6 Correctness of the Evaluation of Applicative Terms

In this Section, except for the main theorem 6.10 at the end, the class environment C will not change. We will therefore omit this parameter in all notations (including apply, eval).

Typing, Semantics, and Semantic Typing of Values

Definition 6.1 (Typing of Values) The typing relation H ⊢ v : A is defined inductively by the following rules:

If ρ is a native C++ type and n ∈ [[ ρ]], then

H ⊢ n : ρ

If h ∈ Addr, H(h) = (c, v_{1}, …, v_{k}), C(c) = (Δ; x : A; a)

Δ = x_{1} : A_{1}, …, x_{k} : A_{k} then

\begin{matrix}Δ, x : A ⊢ a : B \\ H ⊢ v_{i} : A_{i} (i = 1, …, k) \end{matrix} ; H ⊢ h : A → B

Definition 6.2 (Denotational Semantics of Values) (a) Assuming H ⊢ v : A we define the denotational semantics of v, [[ v]]^{H} ∈ D(A), by recursion on the derivation of H ⊢ v : A:

[[ n]]^{H} := n
[[ h]]^{H} := λλd ∈ D(A).[[ a]]ξ[x ↦ d]

where H(h) = (c, v_{1}, …, v_{k}), C(c) = (Δ; x : A; a), Δ = x_{1} : A_{1}, …, x_{k} : A_{k}, Δ, x : A ⊢ a : B, H ⊢ v_{i} : A_{i} and ξ(x_{i}) := [[ v_{i}]]^{H} (i = 1, …, k).

If C needs to be mentioned we write [[ v]]^{C,H} instead of [[ v]]^{H}.

(b) If η ∈ FEnv, η : Γ, we define [[ η]]^{H} ∈ VEnv by [[ η]]^{H} := λλx ∈ dom(η).[[ η(x) ]]^{H}.

Lemma 6.3 (a) If H ⊢ v : A and H ⊆ H′, then H′ ⊢ v : A and [[ v]]^{H} = [[ v]]^{H′}.

(b) If H ⊢ v : A and H ⊢ v : A′, then A = A′.

The next definition is motivated by the following consideration: We want to show that eval η a H is defined, whenever we have Γ ⊢ a : A, and if the result is (v, H′), then [[ a]] = [[ v]]^{H′} (more precisely we have a dependency on an environment η). The problem is that [[ a b]] = [[ a]]([[ b]]), whereas eval η (a b) H :≃ apply v w H′′ where v, w are obtained by applying eval to a and b, and H′′ is the heap obtained when evaluating a and b. Even so in the proof of the correctness of eval we might know by induction hypothesis (for some suitable heap H′′′) that [[ a]] = [[ v]]^{H′′′} and [[ b]] = [[ w]]^{H′′′}, we will not be able to conclude that [[ a]]([[ b]]) = [[ v′]]^{H′′′}, if apply v w H′′ ≃ (v′, H′′′), unless we know for a already that it respects apply. If a = c(a_{1}, …, a_{n}), this is no problem, but a might be a variable or an application term a′ b′.

So, when proving the correctness for an applicative term of type A → B, we need to show that it respects apply as well. We can achieve this if we know that apply is only applied to terms which respect apply themselves. We also need to assume that all variables have this property as well. The correct condition is expressed by using the following Kripke-style logical relation H ⊧ v ∼ d : A between a C++ value v ∈ Val and a denotational value (d ∈ D(A)). This relation, which depends on a class environment C, a heap H, and the type A, can be viewed as a semantic analogue of the (proof-theoretic) typing relation.

Definition 6.4 (a) We define a relation H ⊧ v ∼ d : A by recursion on the type A.

In order to increase readability we will use the following abbreviations: ⊧ apply v w H ∼ d : A is shorthand for

∃v′, H′ (apply v w H ≃ (v′, H′) ∧ H′ ⊧ v′ ∼ d : A).

Similarly, ⊧ eval η a H ∼ d : A stands for

∃v′, H′ (eval η a H ≃ (v′, H′) ∧ H′ ⊧ v′ ∼ d : A).

(Note that ⊧ apply v w H ∼ d : A implies apply v w H is defined):

H ⊧ v ∼ n : ρ :⟺ v = n ∈ [[ ρ]]
H ⊧ v ∼ f : A → B :⟺ H ⊢ v : A → B ∧ [[ v]]^{H} = f

∧∀H′ ⊇ H, ∀(w, d) ∈ Val × D(A).

\begin{matrix}H′ ⊧ w ∼ d : A \\ ⟹⊧ apply v w H′ ∼ f(d) : B \end{matrix}

(b) We also define

H ⊧ η ∼ ξ : Γ :⟺ dom(Γ) ⊆ dom(η) ∩ dom(ξ)∧ ∀x ∈ dom(Γ)H ⊧ η(x) ∼ ξ(x) : Γ(x)

Lemma 6.5 If H ⊧ v ∼ d : A and H ⊆ H′ then H′ ⊧ v ∼ d : A.

Proof. Easy by the definition and Lemma 6.3 (a). q.e.d.

Lemma 6.6 If H ⊧ v ∼ d : A, then H ⊢ v : A. Hence, if H ⊧ η ∼ ξ : Γ, then H ⊢ η : Γ.

Proof. Clear, by definition. q.e.d.

Proof of Correctness of eval

The main result below corresponds to the usual “Fundamental Lemma” or “Adequacy Theorem” for logical relations:

Lemma 6.7 Assume Γ ⊢ a : A. Then for all η, ξ we have

H ⊧ η ∼ ξ : Γ ⟹⊧ eval η a H ∼ [[a]]ξ : A .

Proof. The proof is by induction on the typing judgement Γ ⊢ a : A. In the proof we will use the properties (1) and (2) of Lemma 4.7 and Lemma 6.5. We refer to the latter one as “monotonicity”. We now consider the four possible cases of how Γ ⊢ a : A can be derived.

Γ, x : A ⊢ x : A. Assume ξ : (Γ, x : A) and H ⊧ η ∼ ξ : (Γ, x : A). We need to show ⊧ eval η x H ∼ [[x]]ξ : A. We have eval η x H = (η(x), H) and [[x]]ξ = ξ(x) ∈ D(A). Furthermore, H ⊧ η ∼ ξ : (Γ, x : A) entails H ⊧ η(x) ∼ ξ(x) : A, and therefore the assertion follows.

Γ ⊢ c(a⃗) : A → B, derived from C(c) = (Δ; x : A; a), where Δ = y⃗ : A⃗, Γ ⊢ a⃗ : A⃗, and Γ, x : A ⊢ a : B. Assume ξ : Γ and H ⊧ η ∼ ξ : Γ.

We need to show ⊧ eval η c(a⃗) H ∼ [[ c(a⃗) ]]ξ : A → B. By induction hypothesis for Γ ⊢ a_{i} : A_{i} and monotonicity we get that mapM (eval η) a⃗ H = (v⃗, H_{1}) for some H_{1}, v⃗ s.t. H_{1} ⊧ v_{i} ∼ [[ a_{i}]]ξ : A_{i} Therefore eval η c(a⃗) H = (h, H′), where H′ = H_{1}[h ↦ (c, v⃗)]) with h = fresh(H_{1}). We need to show H′ ⊧ h ∼ [[ c(a⃗) ]]ξ : A → B, which is a conjunction of three statements (i), (ii), (iii):

(i) We need to show H′ ⊢ h : A → B, which follows, since H′(h) = (c, v⃗), C(c) = (Δ; x : A; a), Γ, x : A ⊢ a : B and H′ ⊢ v_{i} : A_{i}, where the last statement follows by H_{1} ⊧ v_{i} ∼ [[ a_{i}]]ξ : A_{i}.

(ii) We need to show [[ h]]^{H′} = [[ c(a⃗) ]]ξ:

\begin{aligned}[[ h]]^{H′} & = & λλd ∈ D(A).[[ a]][[ η_{0} ]]^{H′}[x ↦ d] , \\ [[ c(a⃗) ]]ξ & = & λλd ∈ D(A).[[ a]]ξ_{0}[x ↦ d] \end{aligned}

where η_{0} := [y⃗ ↦ v⃗], [[ η_{0} ]]^{H′} := λλy ∈ dom(η_{0}).[[ η_{0}(y) ]]^{H′}, and

ξ_{0} = [y⃗ ↦ [[ a⃗]]ξ]. By H_{1} ⊧ v_{i} ∼ [[ a_{i}]]ξ : A_{i} and monotonicity we have H′ ⊧ η_{0} ∼ ξ_{0} : Δ. Therefore [[ η_{0}(y_{i}) ]]^{H′} = ξ_{0}(y_{i}) and we are done.

(iii) Assume H′′ ⊇ H′ and H′′ ⊧ w ∼ d : A. We need to show

⊧ apply h w H′′ ∼ ([[ c(a⃗) ]]ξ)(d) : B .

First,

apply h w H′′ ≃ eval η_{0}[x ↦ w] a H′′ ,
([[ c(a⃗) ]]ξ)(d) = [[ a]]ξ_{0}[x ↦ d] .

By H′ ⊧ η_{0} ∼ ξ_{0} : Δ, H′′ ⊧ w ∼ d : A, and monotonicity we obtain H′′ ⊧ η_{0}[x ↦ w] ∼ ξ_{0}[x ↦ d] : (Δ, x : A). Using the induction hypothesis we obtain ⊧ eval η_{0}[x ↦ w] a H′′ ∼ [[a]]ξ_{0}[x ↦ d] : B.

Γ ⊢ a b : B, derived from Γ ⊢ a : A → B and Γ ⊢ b : A. Assume ξ : Γ and H ⊧ η ∼ ξ : Γ. We need to show ⊧ eval η (a b) H ∼ [[a b]]ξ : A. By induction hypothesis and (1), eval η a H = (v, H_{1}) for some H_{1} ⊇ H with H_{1} ⊧ v ∼ [[a]]ξ : A → B and, using monotonicity, eval η b H_{1} = (w, H_{2}) for some H_{2} ⊇ H_{1} with H_{2} ⊧ w ∼ [[b]]ξ : A. By the definition of H_{1} ⊧ v ∼ [[ a]]ξ : A → B we obtain ⊧ apply v w H_{2} ∼ [[a]]ξ([[b]]ξ) : B and we are done, since eval η (a b) H ≃ apply v w H_{2} and [[a b]]ξ = [[a]]ξ([[b]]ξ).

Γ ⊢ f[a_{1}, …, a_{k}] : B, derived from Γ ⊢ a_{i} : A_{i}, i = 1, …, k, where f : (A_{1}, …, A_{n}) → B. Assume ξ : Γ and H ⊧ η ∼ ξ : Γ. We need to show ⊧ eval η f[a⃗] H ∼ [[f[a⃗]]]ξ : B. By induction hypothesis and (1), eval η a_{1} H = (n_{1}, H_{1}) for some n_{1} ∈ [[ A_{1} ]] and H_{1} ⊇ H with H_{1} ⊧ n_{1} ∼ [[a_{1}]]ξ : A_{1}, especially n_{1} = [[a_{1}]]ξ. Similarly, using monotonicity and (1), for i = 1, …, k − 1 we have eval η a_{i+1} H_{i} = (n_{i+1}, H_{i+1}) for some n_{i+1} ∈ [[ A_{i}]] and H_{i+1} ⊇ H_{i} with n_{i+1} = [[a_{i+1}]]ξ. It follows eval η f[a⃗] H = ([[f]](n⃗), H_{k}) = ([[f[a⃗]]]ξ, H_{k}). q.e.d.

Lemma 6.8 If H ⊢ v : A then H ⊧ v ∼ [[ v]]^{H} : A.

Proof. Induction on H ⊢ v : A.

The case A ∈ basetype is trivial.

Case H ⊢ h : A → B, derived from H(h) = (c, v⃗), C(c) = (x⃗ : A⃗; x : B; a), x⃗ : A⃗, x : A ⊢ a : B, H ⊢ v⃗ : A⃗. We need to show that for H′ ⊇ H, w, d s.t. H′ ⊧ w ∼ d : A we have ⊧ apply h w H′ ∼ [[ h]]^{H}(d) : B, so assume H′, w, d as stated.

Let η := [x⃗ ↦ v⃗], ξ := [[ η]]^{H}. Then [[ h]]^{H}(d) = [[ h]]^{H′}(d) = [[ a]]ξ[x ↦ d]. By induction hypothesis H ⊧ v_{i} ∼ [[ v_{i}]]^{H} : A_{i}, and by H′ ⊧ w ∼ d : A we get therefore H′ ⊧ η[x ↦ w] ∼ ξ[x ↦ d] : Γ. Furthermore, apply h w H′ ≃ eval (η[x ↦ w]) a H′. By Lemma 6.7 ⊧ eval (η[x ↦ w]) a H′ ∼ [[a]]ξ[x ↦ d] : B, which proves the assertion

Theorem 6.9 (Correctness of eval) If Γ ⊢ a : A, H ⊢ η : Γ, then there exists H′, v s.t. eval η a H ≃ (v, H′), H′ ⊢ v : A and [[ a]]([[ η]]^{H′}) = [[ v]]^{H′}.

Proof: Immediate by Lemma 6.7 and 6.8.

Main Theorem

Theorem 6.10 (Overall Correctness) Assume ⊢ r : A and let C ∈ CEnv. Then P ∅ r C = (a, C′) for some C′ ⊇ C. Furthermore, for any heap H, any environment η and any C′′ ⊇ C′ we have

eval C′′ η a H = (v, H′)

for some H′, v s.t. [[ r]]∅ = [[ v]]^{C,H′}.

Especially, in case A = int we have that r →_{β} n for some n, and therefore [[ r]]∅ = n and

eval C′′ η a H = (n, H′) .

Proof. By Theorem 5.6 and 6.9.

Remark. The proof of Theorem 6.7 is rather “low level” since it mentions and manipulates the class environment and the heap explicitely. It would be desirable, in particular with regard to a formalisation in a proof assistant, to lift the proof to the same abstract monadic level at which the functions P, eval and apply are defined. A framework for carrying this out might be provided by suitable versions of Moggi’s Computational λ–Calculus, Pitts’ Evaluation Logic [Pit91] and special logical relations for monads [GLN02].

7 Conclusion

In this paper we showed how to introduce functional concepts into C++ in a provably correct way. The modelling and the correctness proof used monadic concepts as well as denotational semantics and logical relations.

This work lends itself to a number of extensions, for example, the integration of recursive higher-order functions, polymorphic and dependent type systems, the integration lazy evaluation and infinite structures as well as the combination of larger parts of C++ with the λ-calculus. The accurate description of these extensions would require more sophisticated, e.g. domain-theoretic constructions. We believe that if our approach is extended to cover full C++, we obtain a language in which the worlds of functional and object-oriented programming are merged, and that we will see many examples, where the combination of both language concepts (e.g. the use of λ-terms with side-effects) will result in interesting new programming techniques.

The remarkable fact that it is possible to have a denotational semantics at a description level where pointers are manipulated explicitely entails that the wellknown benefits of denotational semantics, extensionality and compositionality, are still available at that level. This has already paid off in this paper where we were able to give a short and concise correctness proof for our C++ fragment using the denotational semantics (instead of a complicated operational argument). More benefits are to be expected when it comes to verifying programs written in this C++ fragment or in one of the future extensions mentioned above.

8 List of Identifiers and Notations

In the following we list the notations used in this article, together with the place where they are introduced. 2.1 (a).

Finite functions  X →_{fin} Y  Def. 1.1
Extension of fin. fns.  g[x ↦ y] or f, x : y  Def. 1.1
Explicitly given fin. fns.  x_{1} : y_{1}, …, x_{k} : y_{k}  Def. 1.1
Base types  basetype ∋ ρ, σ  Ass. 2.1 (a)
Base type int  int  Ass. 2.1 (a)
Basic functions  F ∋ f  Ass. 2.1 (b)
Denot. sem. of base type  [[ ρ]]  Ass. 2.1 (d)
Denot. sem. of basic fn.  [[ f ]]  Ass. 2.1 (e)
Constants (of any base type) n  Ass. 2.1 (c)
Variables  Var ∋ x, y, z  Def. 2.2 (a)
Types  Type ∋ A, B  Def. 2.2 (b)
Contexts  Context ∋ Γ, Δ  Def. 2.2 (b)
Extension of Contexts  Γ, x : A  Def. 2.2 (b)
λ-terms  Term ∋ r, s, t  Def. 2.2 (b)
Typed λ-terms  Γ ⊢ r : A  Def. 2.2 (b)
Functionals of type A  D(A) ∋ d  Def. 2.3
Functional environment  FEnv ∋ ξ  Def. 2.4 (a)
Typed contexts  ξ : Γ  Def. 2.4 (b)
Denot. sem. of λ-terms  [[ r]]ξ  Def. 2.5
Name of a type  name(A)  Sect. 3
Translation of λ-terms  t^{C++}  Sect. 3
Constructors or classnames Constr ∋ c  Def. 4.1
Applicative terms  App ∋ a, b  Def. 4.1
Classes  Class ∋ (Γ; x : A; b)  Def. 4.1
Class environments  CEnv = Constr ∋ C  Def. 4.1
Free variables of a  FV(a)  Def. 4.2
Heap addresses  Addr ∋ h  Def. 4.3
C++ constants  n  Def. 4.3

Values  Val ∋ v, w  Def. 4.3
Closures  Constr × Val^{∗} ∋ (c, v_{1}, …, v_{k}) Def. 4.3
Heaps  Heap = Addr ∋ H  Def. 4.3
Value environments  VEnv ∋ η  Def. 4.3
State Monad  M_{X}(Y)  Def. 4.4
Monadic notations  do, return, mapM, read, add  Not. 4.5
Fresh element  fresh(X)  Not. 4.5
Eval and Apply  eval, apply  Def. 4.6
Parse function  P  Def. 5.1
Typed applicative terms  C; Γ ⊢ a : A  Def. 5.3
Denot. sem. of appl. terms  [[ a]]^{C}ξ or [[ a]]ξ  Def. 5.4
Variant of above  C; Γ ⊢′ a : A  Def. 5.7
CEnv-homomorphism  θ  Def. 5.9 (b)
θ applied to r  θ(r)  Def. 5.9 (a)
θ applied to a class  θ(Γ; x : B; a)  Def. 5.9 (a)
Typed values  H ⊢ v : A  Def. 6.1
Denot. sem. of values  [[ v]]^{H}, [[ v]]^{C,H}  Def. 6.2 (a)
Denot. sem. of value envs. [[ η]]^{H}  Def. 6.2 (b)
Semantic typing of values H ⊧ v ∼ d : A Def. 6.4
Special not. for the above  ⊧ apply v w H ∼ d : A
⊧ eval η a H ∼ d : A  Def. 6.4

References

[ASS85] H. Abelson, G. J. Sussman, and J. Sussman. Structure and interpretation of computer programs. MIT Press, 1985.

[GLN02] J. Goubault-Larrecq, S. Lasota, and D. Nowak. Logical relations for monadic types. In Julian C. Bradfield, editor, Proceedings of the 16th International Workshop on Computer Science Logic (CSL’02), volume 2471 of Lecture Notes in Computer Science, pages 553–568, Edinburgh, Scotland, UK, September 2002. Springer.

[IPW99] Atshushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Loren Meissner, editor, Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Applications (OOP-SLA‘99), volume 34(10), pages 132–146, N. Y., 1999.

[JT93] A. Jung and J. Tiuryn. A new characterization of lambda definability. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 245–257. Springer, 1993.

[Kis98] O. Kiselyov. Functional style in C++: Closures, late binding, and lambda abstractions. In ICFP ’98: Proceedings of the third ACM SIGPLAN International conference on Functional programming, page 337, New York, NY, USA, 1998. ACM Press.

[Läu95] K. Läufer. A framework for higher-order functions in C++. In COOTS, 1995.

[Mog91] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.

[MS00] B. McNamara and Y. Smaragdakis. Functional programming in C++. In ICFP ’00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pages 118–129, New York, NY, USA, 2000. ACM Press.

[Pit91] A. M. Pitts. Evaluation logic. In G. Birtwistle, editor, IVth Higher Order Workshop, Banff 1990, Workshops in Computing, pages 162– 189. Springer, 1991.

[Plo77] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[Plo80] G. D. Plotkin. Lambda definability in the full type hierarchy. In R. Hindley and J. Seldin, editors, To H.B. Curry: Essays in Combinatory Logic, lambda calculus and Formalisms, pages 363 – 373. Academic Press, 1980.

[Rey83] J. C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP’83, pages 513–523. North-Holland, 1983.

[SSB01] R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine – Definition, Verification, Validation. Springer, 2001.

[Sta85] R. Statman. Logical relations and the typed lambda-calculus. Information and Control, 65:85 – 97, 1985.

[Str] J. Striegnitz. FACT! – the functional side of C++.

http://www.fz-juelich.de/zam/FACT.

[Tai67] W. W. Tait. Intensional interpretation of functionals of finite type. Journal of Symbolic Logic, 32:198 – 212, 1967.

[Win93] G. Winskel. The formal semantics of programming languages: an introduction. MIT Press, Cambridge, MA, USA, 1993.