Tennent’s Principle of Correspondence
Over the years I’ve encountered several references to R.D. Tennent and
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
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 now1!
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.
On pp. 127–8 he gives two example blocks of PASCAL code,
and states that
It is evident that these two fragments are equivalent.
So, like, it’s about, like,
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
lambdas. This mis-attribution, according to
on the previously
due to Neal Gafter’s 2006 article discussing
adding closures to Java2. In my
mind, Gafter gets a bit of a free pass, as he hedges by referring to
Tennent’s Correspondence and Abstraction Principles.
In short, Tennent’s Correspondence Principle says:
For a given expression
lambda exprshould 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.
To demonstrate a violation of the principle, Tennent points to
There is no definition mechanism that is the exact analog of the
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
that, when run, will result in an output of
2. An equivalent in C
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
and we can see that C’s parameter mechanisms have generally3 equivalent block definition counterparts, where PASCAL does not.
Interestingly, I believe these examples aren’t directly replicable in
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
object4; or by defining
inc as a function with a free
variable. This doesn’t mean that either language violates the
to define a reference variable or to define a function that accepts
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 Java2, 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
returnstatements as a problem.
In fact I have not found any references to
return statements in the
book at all.
Languishing at the bottom of the aforementioned
programmers.stackoverflow thread – and, let’s
be honest, at the bottom of this article too – is a an excellent
comment with links to
an excellent post about Tennent’s principles by Claus
Reinke; the Tennent paper that Claus is referring to,
Language design methods based on semantic principles
– unfortunately hidden behind a paywall; and to an intriguing looking
paper by Reinke,
On functional programming, language design, and persistence. From
Is there any reason to prefer functions as units of programming over other forms, such as predicates, relations, objects, processes, etc.?
Sadly, I haven’t had the time to read either of the Tennent or Reinke papers, so this is as much further reading for me as for you.