<p>Plotkin used logical relations in his unpublished but nevertheless widely circulated and influential 1973 paper "Lambda Definability and Logical Relations". I have a <a href="http://www.cs.cmu.edu/~neelk/plotkin-logical-relations.pdf">copy of this note</a> on my webpage.</p>

<p>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. </p>

CC BY-SA 3.0
2011-07-01T09:46:34.197Z
This almost sounds like juicy TCS gossip.
Dave Clarke
CC BY-SA 3.0
2011-07-01T12:06:56.037Z
Naively looking at the publication year, Reynolds beats Plotkin by one year. I guess I'll have to ask Plotkin about this (or Reynolds?).  I guess we should also mention Robert Milne's thesis ( http://www.comlab.ox.ac.uk/files/3286/PRGX13.pdf ) to which both Reynolds and Plotkin refer. Milne also uses some form of logical relations, and both Reynolds and Plotkin give him credit for independent discovery.
Ohad Kammar
CC BY-SA 3.0
2011-07-01T22:07:55.630Z
Don't ask Gordon, just coerce him to participate on this site, like I did with Dana.
Andrej Bauer
CC BY-SA 3.0
2013-03-05T15:09:31.740Z
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.
Ohad Kammar
CC BY-SA 3.0
2013-03-05T15:11:41.813Z
More interestingly, Gordon Plotkin told me you can trace the origins back to the work of Howard [citation needed], and that Martin Hyland mentioned the technique is also present in Robin Gandy's thesis (does anyone have access to it?). The latter fact suggests that Turing himself was aware of the technique.
Ohad Kammar
CC BY-SA 3.0
2013-12-19T13:40:57.417Z
Gandy's thesis is now freely available online: https://www.repository.cam.ac.uk/handle/1810/245090
Ohad Kammar
CC BY-SA 3.0
2014-08-24T06:36:55.417Z
@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":

http://download.springer.com/static/pdf/314/bbm%253A978-3-540-37806-8%252F1.pdf?auth66=1409034928_06273f7ce684454f044792ab1813d6a7&ext=.pdf
(from http://link.springer.com/book/10.1007%2FBFb0066739).
Blaisorblade
CC BY-SA 3.0
2014-08-24T06:40:29.127Z
Howard's appendix is even freely available :-).
Blaisorblade
CC BY-SA 3.0
2011-07-01T09:44:46.457Z
2011-07-01T10:29:28.167Z
2011-07-01T10:29:28.167Z
Neel Krishnaswami
<p>The second paragraph of Plotkin's <a href="http://www.cs.cmu.edu/~neelk/plotkin-logical-relations.pdf" rel="nofollow">1973 Memo on Lambda-definability and Logical Relations</a> says this: </p>

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

<p>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, <em>so-called</em>, 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.) </p>

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

<blockquote>
  <p>"M. Gordon proposed, as a possible remedy, that relations... should be
  extended - not just permutations."</p>
</blockquote>

<p>The published version of the paper ("Lambda-definability in the full type hierarchy" in <a href="http://www.amazon.co.uk/To-H-B-Curry-Combinatory-Calculus-Formalism/dp/0123490502/ref=sr_1_1?ie=UTF8&amp;qid=1390096478&amp;sr=8-1&amp;keywords=hindley%20seldin%20curry" rel="nofollow">To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism</a>) has this remark.  It also has a remark that could be construed as an explanation of the term "logical relation":</p>

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

<p>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".</p>

<p>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.</p>

CC BY-SA 3.0
2014-01-19T02:21:27.990Z
2014-02-06T16:38:18.400Z
2014-02-06T16:38:18.400Z
Uday Reddy
<p>I actually have two questions:</p>

<ol>
<li><p>Who first used logical relations to relate semantics?</p>

<p>I traced them back to Reynold's "<a href="http://repository.cmu.edu/cgi/viewcontent.cgi?article=2287&amp;context=compsci">On the Relation Between Direct and Continuation Semantics</a>", but I can't claim to have made an exhaustive search.</p>

<p>I have found references to logical relations dating earlier (Tait, '67), but not for relating semantics. </p></li>
<li><p>What is the best current introduction for logical relations? </p></li>
</ol>

<p>I know of Mitchell's "<a href="http://portal.acm.org/citation.cfm?id=114899">Type Systems for Programming Languages</a>" from the Handbook of TCS. What other expositions are there?</p>

CC BY-SA 3.0
2011-07-01T07:29:53.063Z
There's a chapter on Logical Relations in Mitchell's [Foundations for Programming Languages](http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=3460). 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.
Dave Clarke
CC BY-SA 3.0
2011-07-01T08:22:02.730Z
I can get my hands on it, thanks! I'll have a look when I get to the office.
Ohad Kammar
CC BY-SA 3.0
2011-07-01T11:49:50.297Z
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.
Ohad Kammar
<reference-request><pl.programming-languages><denotational-semantics><logical-relations>
What is the origin of logical relations?
Ohad Kammar
# What is the origin of logical relations?

(Asked by: username_0 on 2011-06-30)

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](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2287&context=compsci)", 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](http://portal.acm.org/citation.cfm?id=114899)" from the Handbook of TCS. What other expositions are there?

**Tags:** reference-request, pl.programming-languages, denotational-semantics, logical-relations
> **Comments:**
> **username_1**: There's a chapter on Logical Relations in Mitchell's [Foundations for Programming Languages](http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=3460). 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.  
> **username_0**: I can get my hands on it, thanks! I'll have a look when I get to the office.  
> **username_0**: 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.  

---

## 2 answers

### Answer by username_5 on 2014-01-19. Score: 6 | Accepted answer

The second paragraph of Plotkin's [1973 Memo on Lambda-definability and Logical Relations](http://www.cs.cmu.edu/~neelk/plotkin-logical-relations.pdf) 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](http://www.amazon.co.uk/To-H-B-Curry-Combinatory-Calculus-Formalism/dp/0123490502/ref=sr_1_1?ie=UTF8&qid=1390096478&sr=8-1&keywords=hindley%20seldin%20curry)) 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.


---

### Answer by username_2 on 2011-07-01. Score: 14

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](http://www.cs.cmu.edu/~neelk/plotkin-logical-relations.pdf) 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.

> **Comments:**
> **username_1**: This almost sounds like juicy TCS gossip.  
> **username_0**: Naively looking at the publication year, Reynolds beats Plotkin by one year. I guess I'll have to ask Plotkin about this (or Reynolds?).  I guess we should also mention Robert Milne's thesis ( http://www.comlab.ox.ac.uk/files/3286/PRGX13.pdf ) to which both Reynolds and Plotkin refer. Milne also uses some form of logical relations, and both Reynolds and Plotkin give him credit for independent discovery.  
> **username_3**: Don't ask Gordon, just coerce him to participate on this site, like I did with Dana.  
> **username_0**: 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.  
> **username_0**: More interestingly, Gordon Plotkin told me you can trace the origins back to the work of Howard [citation needed], and that Martin Hyland mentioned the technique is also present in Robin Gandy's thesis (does anyone have access to it?). The latter fact suggests that Turing himself was aware of the technique.  
> **username_0**: Gandy's thesis is now freely available online: https://www.repository.cam.ac.uk/handle/1810/245090  
> **username_4**: @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":  http://download.springer.com/static/pdf/314/bbm%253A978-3-540-37806-8%252F1.pdf?auth66=1409034928_06273f7ce684454f044792ab1813d6a7&ext=.pdf (from http://link.springer.com/book/10.1007%2FBFb0066739).  
> **username_4**: Howard's appendix is even freely available :-).  

---

