Tennent’s Principle of Correspondence

19 February 2012

Over the years I’ve encountered several references to R.D. Tennent and his principle of correspondence. The first time was Marc Chung’s 2009 article How Closures Behave In Ruby. Going back and reading it now, Marc has removed the reference to the principle, but Google turns up a couple of pages about it. A question on programmers.stackexchange.com has an interesting exchange, which I will discuss later. But there didn’t appear to be a good source online for the actual statement of the principle… until now¹!

The Principle of Correspondence

Quoting from R. D. Tennent’s Principle’s of Programming Languages — published in 1981:

[…] the underlying semantic notions for both parameter and definition mechanisms are simply expression evaluation (of an actual parameter or the right-hand side of a definition) and identifier binding (of a formal parameter or the left-hand side of a definition.) […] For any parameter mechanism, an analogous definition mechanism is possible, and vice versa. This is known as the principle of correspondence.

R.D. Tennent, Principles of Programming Languages, §9.1 Definitions and Blocks, p.130.

On pp. 127–8 he gives two example blocks of PASCAL code,

var i : integer;
begin
  i := -j;
  write(i)
end

and

procedure p(i : integer);
  begin
    write(i)
  end;
begin
  p(-j)
end

and states that

It is evident that these two fragments are equivalent.

So, like, it’s about, like, `return`, right?

No. In short, a function’s parameter list is equivalent to the variable definitions for a block. On p. 133, Tennent states

The principle of correspondence establishes the relationship between parameters of abstracts and definitions.

This demonstrates a common misconception that the principle of correspondence is relevant to how languages handle returns in lambdas. This mis-attribution, according to answers on the previously mentioned question on programmers.stackexchange.com, is due to Neal Gafter’s 2006 article discussing adding closures to Java². In my mind, Gafter gets a bit of a free pass, as he hedges by referring to Tennent’s Correspondence and Abstraction Principles.

Yehuda Katz also falls prey to this in his otherwise excellent JavaScript Needs Blocks, when he states:

In short, Tennent’s Correspondence Principle says:

For a given expression expr, lambda expr should be equivalent.

Gafter and Katz’s contexts actually appear to be Tennent’s principle of qualification in §9.3 of Tennent’s book. This is to code blocks and function bodies what correspondence is to parameters & variable definitions. I’m splitting hairs here, but that’s what we programmers do.

An Example

To demonstrate a violation of the principle, Tennent points to PASCAL’s var:

There is no definition mechanism that is the exact analog of the var parameter mechanism.

PASCAL’s var is a mechanism whereby a variable can be passed to a function, rather than the variable’s value. This is similar to passing a pointer to a variable in C, but without needing to remember to dereference the variable. To explore, let’s start with a simple PASCAL procedure

procedure inc(var i : integer);
  begin
    i := i + 1
  end;

var x : integer;
begin
  x := 1;
  inc(x);
  writeln(x);
end

that, when run, will result in an output of 2. An equivalent in C

void inc(int *i) {
  *i = *i + 1;
}

int x = 1;
inc(&x);
printf("%d", x);

will also result in 2. In PASCAL I know of no way to write an equivalent block definition for the above code. In fact, according to Tennent, there is no equivalent. But in C we could rearrange as

int x = 1;
{
  int *i = &x;
  *i = *i + 1;
}
printf("%d", x);

and we can see that C’s parameter mechanisms have generally³ equivalent block definition counterparts, where PASCAL does not.

Interestingly, I believe these examples aren’t directly replicable in Ruby or Javascript - the two languages I use in anger – as you can’t pass l-values to a function, only r-values. The only ways that I can think of to approximate are by wrapping the variable in an object⁴; or by defining inc as a function with a free variable. This doesn’t mean that either language violates the principle of correspondence, as neither Ruby nor Javascript have a way to define a reference variable or to define a function that accepts one.

Ramifications of the principle

Tennent doesn’t pass judgment in his book, only stating that

[…] the principle of correspondence can be useful to a language designer by pointing out possible inconsistencies and deficiencies.

In Neal Gafter’s previously mentioned adding closures to Java², Neal has stronger words

Tennent’s principles are very powerful because violations of them tend to show up in the language as flaws, irregularities, unnecessary restrictions, unexpected interactions or complications, and so on.

Douglas Crockford wrote a quick overview – which sadly has disappeared from the face of the Internet, leaving only a possibly incomplete RSS-feed remnant. Crockford states

the Correspondence Principle is descriptive, not prescriptive. He uses it to analyze the (by now forgotten) Pascal programming language, showing a correspondence between variable definitions and procedure parameters.

Crockford also notes that

Tennent does not identify the lack of correspondence of return statements as a problem.

In fact I have not found any references to return statements in the book at all.