17
$\begingroup$

I actually have two questions:

  1. Who first used logical relations to relate semantics?

    I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim to have made an exhaustive search.

    I have found references to logical relations dating earlier (Tait, '67), but not for relating semantics.

  2. What is the best current introduction for logical relations?

I know of Mitchell's "Type Systems for Programming Languages" from the Handbook of TCS. What other expositions are there?

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ There's a chapter on Logical Relations in Mitchell's Foundations for Programming Languages. The bottom of the first page gives a brief historical overview, citing the main papers. I could type these up if you cannot get your hands on Mitchell's book. $\endgroup$
    – Dave Clarke
    Commented Jul 1, 2011 at 7:29
  • $\begingroup$ I can get my hands on it, thanks! I'll have a look when I get to the office. $\endgroup$
    – Ohad Kammar
    Commented Jul 1, 2011 at 8:22
  • $\begingroup$ OK, the book is much more elaborate than the handbook chapter, although they cover roughly the same material (minus Sconing, sadly). The historical notes are nearly identical, with the notable exception that the book mentions Plotkin's technical report NeelK gives below. $\endgroup$
    – Ohad Kammar
    Commented Jul 1, 2011 at 11:49

2 Answers 2

Reset to default
6
$\begingroup$

The second paragraph of Plotkin's 1973 Memo on Lambda-definability and Logical Relations says this:

"The definition of logical [relation] is derived from a corresponding one of M. Gordon for the typed λ-calculus."

This doesn't say explicitly that the term was coined by Gordon. But, given that the memo is titled "Lambda-definability and logical relations" as if "logical relation" is an already known idea, and the second para says "construct certain, so-called, logical relations," I think it very likely that Gordon coined the term and Plotkin used it hence. (Plotkin confirmed to me that whatever he wrote in the memo is correct.)

Gordon is credited again at the top of p. 12,

"M. Gordon proposed, as a possible remedy, that relations... should be extended - not just permutations."

The published version of the paper ("Lambda-definability in the full type hierarchy" in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism) has this remark. It also has a remark that could be construed as an explanation of the term "logical relation":

Because of the "logical" nature of the $\lambda$-definable elements, they should be invariant under permutations of $D$.

In my view, this is an extremely satisfying explanation of why logical relations are "logical". Lambda calculus is logical and, so, the functions defined using it will be uniform with respect to the base types. They can't "see" the permutations we might do to the values of the base types. Viewed in this way, what Gordon and Plotkin meant by "logical" is essentially the same as what Reynolds calls "parametric".

However, the term "logical relation" doesn't appear in the published version of the paper. It is possible that the referees might have objected that the term was confusing and Plotkin might have decided it best to avoid the term. But, Statman went back to the old terminology and the term has come back into popular parlance.

Improve this answer
$\endgroup$
14
$\begingroup$

Plotkin used logical relations in his unpublished but nevertheless widely circulated and influential 1973 paper "Lambda Definability and Logical Relations". I have a copy of this note on my webpage.

I used to think that this is where the name came from, but when I asked Rick Statman about this, he told me that Mike Gordon coined the term logical relation to describe Tait's method, and that he and Gordon Plotkin picked it up from him. I think this is how it entered programming language jargon, though you could make sure by asking Plotkin.

Improve this answer
$\endgroup$
8
  • 1
    $\begingroup$ This almost sounds like juicy TCS gossip. $\endgroup$
    – Dave Clarke
    Commented Jul 1, 2011 at 9:46
  • 5
    $\begingroup$ Don't ask Gordon, just coerce him to participate on this site, like I did with Dana. $\endgroup$
    – Andrej Bauer
    Commented Jul 1, 2011 at 22:07
  • 1
    $\begingroup$ OK, I asked both Gordon Plotkin and Mike Gordon. Both agree that Gordon Plotkin coined the term 'logical relations', and each claimed the idea to use relations came from the other. $\endgroup$
    – Ohad Kammar
    Commented Mar 5, 2013 at 15:09
  • 1
    $\begingroup$ Gandy's thesis is now freely available online: repository.cam.ac.uk/handle/1810/245090 $\endgroup$
    – Ohad Kammar
    Commented Dec 19, 2013 at 13:40
  • 2
    $\begingroup$ @OhadKammar: Plotkin's "Lambda-definability in the full type hierarchy" gives precise credit to Howard by saying that the idea of using relations rather than permutations "was also used by Howard for defining his hereditarily majorisable functionals [Tro]". The citation is to a book, but the only chapter from Howard is the appendix, "Hereditarily majorisable functionals of finite type": download.springer.com/static/pdf/314/… (from link.springer.com/book/10.1007%2FBFb0066739). $\endgroup$
    – Blaisorblade
    Commented Aug 24, 2014 at 6:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.