Introduction to Full Abstraction

Operational Models and Testing

An operational model of computation consists of:

1. A collection of programs, usually defined by an abstract grammar. Let P, Q and R range over programs.
2. A reduction relation P → Q defining when program P can evolve at runtime to become program Q.

For example, for arithmetic expressions we could define:

1. Programs are arithmetic expressions, including constants, variables, arithmetic operations, and a variable binder (let x = e in f).
2. Reduction is given by left-to-right arithmetic evaluation.

For example:

(1 + 2) + 3 → 3 + 3 → 6
let x = 1 + 2 in x + 3 → let x = 3 in x + 3 → 3 + 3 → 6

A theory of testing is given by extending an operational model in two ways:

1. A collection of tests, usually given by a program with a single hole ⋅. Let T range over tests.
2. A definition of how a test T can be applied to a program P to produce a new program T[P].
3. A definition of when a program is a success state.

We can then define when a program passes a test as:

P may pass T whenever T[P] →* Q for some success state Q

For example, for a language of arithmetic expressions:

1. A test is an arithmetic expression containing a single hole ⋅.
2. Applying a test T[e] consists of replacing the hole ⋅ by the expression e.
3. The only success state is the integer constant 0.

For example, a possible test is given by the context (let x = 1 + 2 in ⋅). The expression (x + 3) fails this test:

let x = 1 + 2 in x + 3 → let x = 3 in x + 3 → 3 + 3 → 6 (an unsuccessful state)

The expression (x - 3) passes this test:

let x = 1 + 2 in x - 3 → let x = 3 in x - 3 → 3 - 3 → 0 (a successful state)

Finally, this allows us to define when one program Q is an operational improvement on another program P:

P ≤ Q whenever ∀ T . P may pass T ⇒ Q may pass T

This order is called the may testing order, and it is routine to verify that it is a pre-order (that is P ≤ P and if P ≤ Q ≤ R then P ≤ R).

For example, let us introduce a new arithmetic expression Ω which never terminates:

Ω → Ω

Since this expression never reaches a successful state, it is the least program in the may-testing order (so any program is an improvement on Ω):

Ω ≤ P

Also, since order of arguments to addition does not matter, we can show that addition is commutative:

(x + y) ≤ (y + x)

As a sanity check, we can verify that x ≠ x + 1 since we have a test which distinguishes them:

(x + 1) must fail (let x = 0 in ⋅)
(x) may pass (let x = 0 in ⋅)

The theory of testing in the form described above originated from Morris (1968) and was developed further by Hennessy (1998). It is quite a robust theory, and has been applied to many languages, including models of functional programming such as the λ-calculus (Abramsky, 1989) and PCF (Plotkin, 1977; Abramsky, Jagadeesan and Malacaria, 2000; Hyland and Ong, 2000), concurrent languages such as the π-calculus (Fiore, Moggi and Sangiorgi 1996; Hennessy, 2002), and object-oriented languages such as the σ-calculus (Jeffrey and Rathke, 2002). The aim of the Full Abstraction Factory project is to scale up the techniques used in theories of testing to languages closer to industrial practice such as Java or C#.

Denotational Models and Full Abstraction

The theory of may testing is quite elegant, but suffers from a serious problem: it often simple to prove that one program does not improve on another (we find a test which one passes and the other does not) but very hard to prove that one program does improve on another (we need to show that for every test one passes, so does the other).

An alternative to operational models are denotational models, which consist of:

1. A set E of elements. Let a, b and c range over elements.
2. For each program P, a denotation [[P]] ⊆ E.

(For purists, we are assuming a prime algebraic domain, and identifying a member of the domain with its prime compact approximants.)

For example, a denotational model for arithmetic expressions can be given as:

1. Elements are of the form (σ,k) where σ is a variable assignment of the form (x₁=k₁,...,x_n=k_n) for variables x_i and constants k_i.
2. The denotation of an expression [[e]] is given as the set of all elements (σ,k) where evaluating e with variable assignment σ yields result k.

For example, the denotation of (x + y) is given by:

[[x + y]] = { (σ, j + k) | (x=j) ∈ σ and (y=k) ∈ σ }

and the denotation of Ω is given by:

[[Ω]] = Ø

Such a denotational semantics gives another definition of improvement: Q is a denotational improvement on P whenever [[P]] ⊆ [[Q]].

The characteristics of denotational models are rather different from operational models. Checking whether one program denotationally improves another is often overkill (it is often just as easy to find a test which distinguishes them). But it is much simpler to prove denotational improvement than operational improvement. For example:

[[x + y]] = { (σ, j + k) | (x=j) ∈ σ and (y=k) ∈ σ } = { (σ, j + k) | (y=j) ∈ σ and (x=k) ∈ σ } = [[y + x]]

and:

[[Ω]] = Ø ⊆ [[P]]

We would like to take advantage of the different characteristics of operational and denotational models: we use operational models when we want to show improvement fails (that is, when we are bug hunting) and we use denotational models when we want to show improvement succeeds (that is, when we are verifying software).

This is the full abstraction problem (Milner, 1977):

A denotational model is fully abstract for an operational model if [[P]] ⊆ [[Q]] precisely when P ≤ Q

Full abstraction helps in software verification and validation in two ways:

1. As noted above, it is often much simpler to verify improvement denotationally than operationally. Moreover it is often possible to build tools which will automatically check denotational improvement for finite systems, and full abstraction guarantees that such tools provide a sound methodology.
2. If a proof of denotational improvement fails, it will often do so by generating a counterexample: that is an element a which is in the denotation of one program but not the other. Using the Definability result discussed below, we can use this element to automatically generate a failing test case: this test can then be added to a unit test suite.

Proofs of full abstraction often follow a standard outline, and are usually straightforward for simple languages such as integer arithmetic:

Proposition (Denotational Precongruence). If [[P]] ⊆ [[Q]] then [[T[P]]] ⊆ [[T[Q]]].

Proposition (Computational Adequacy). There exists an element a such that, for any P, a ∈ [[P]] if and only if P →* Q for some success state Q.

Theorem (Soundness of Denotational Model for Operational Model). If [[P]] ⊆ [[Q]] then P ≤ Q.

Proof. For any test T, if P may pass T then T[P] →* P′ for some success state P′, so (Computational Adequacy) a ∈ [[T[P]]] and (Denotational Precongruence) a ∈ [[T[Q]]] so (Computational Adequacy) T[Q] →* Q′ for some success state Q′ and so Q may pass T.

Proposition (Definability). For any element a, there exists a test T such that, for any P, a ∈ [[P]] if and only if P may pass T.

Theorem (Completeness of Denotational Model for Operational Model). If P ≤ Q then [[P]] ⊆ [[Q]].

Proof. For any element a, if a ∈ [[P]] then (Definability) P may pass T and so Q may pass T, and so (Definability) a ∈ [[Q]].

Scaling Up Full Abstraction

Full abstraction results are often simple to prove for simple languages such as integer arithmetic, but quickly become complex for languages with richer feature sets. The reason for this is that programming language design is a balancing act between expressivity and testing power. Adding features to a programming language makes the programming language more expressive, and so Definability (and hence Completeness) is simpler to prove. However, it also increases the expressive power of tests, and so Denotational Precongruence (and hence Soundness) is harder to prove.

Full abstraction results for languages with powerful features such as first-class functions are often surprisingly difficult to achieve. For example, there is no fully abstract semantics for the language PCF (which contains integers, booleans and first-class functions) for which equivalence of finite programs is decidable.

The goal of the Full Abstraction Factory is to design programming languages which include real-world features such as object-orientation and concurrency, but where the balance of features is chosen to make it possible to find tractable fully abstract models. Moreover, we hope to provide a fully abstract treatment of larger-scale computing entities (such as component-based object systems) then has previously been attempted.

References

Abramsky, S. The lazy lambda calculus, in Turner, D. (Ed.), Declarative Programming, Addison-Wesley, 1989.

Abramsky, S., Jagadeesan, R. and Malacaria, P. Full abstraction for PCF, in Information and Computation 163, pp. 409-470, 2000.

Fiore, M., Moggi, E., and Sangiorgi, D. A fully-abstract model for the π-calculus, in Proc. IEEE Conf. Logic in Computer Science, pp. 43-54, 1996.

Hennessy, M. Algebraic Theory of Processes, MIT Press, 1988.

Hennessy, M. A fully abstract denotational semantics for the π-calculus, in Theoretical Computer Science 278(1), pp. 53-89, 2002.

Hyland, J. M. E, and Ong, C.-H. L. On full abstraction for PCF: I, II and III, in Information and Computation 163, pp. 285-408, 2000.

Jeffrey, A. S. A., and Rathke, J. A fully abstract may testing semantics for concurrent objects, in Proc. IEEE Logic In Computer Science, pp. 101-112, 2002.

Milner, R. Fully abstract semantics of typed λ-calculi, in Theoretical Computer Science 4, pp. 1-22, 1977.

Morris, J.-H. Lambda Calculus Models of Programming Languages, Ph.D. Dissertation, M.I.T., 1968.

Plotkin, G. LCF considered as a programming langauge, in Theoretical Computer Science 5, pp. 223-256, 1977.