The Girard-Reynolds isomorphism (second edition)

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Jean-Yves Girard and John Reynolds independently discovered the second-order polymorphic lambda calculus, F2. Girard additionally proved a Representation Theorem: every function on natural numbers that can be proved total in second-order intuitionistic predicate logic, P2, can be represented in F2. Reynolds additionally proved an Abstraction Theorem: every term in F2 satisfies a suitable notion of logical relation; and formulated a notion of parametricity satisfied by well-behaved models. We observe that the essence of Girard's result is a projection from P2 into F2, and that the essence of Reynolds's result is an embedding of F2 into P2, and that the Reynolds embedding followed by the Girard projection is the identity. We show that the inductive naturals are exactly those values of type natural that satisfy Reynolds's notion of parametricity, and as a consequence characterize situations in which the Girard projection followed by the Reynolds embedding is also the identity. An earlier version of this paper used a logic over untyped terms. This version uses a logic over typed term, similar to ones considered by Abadi and Plotkin and by Takeuti, which better clarifies the relationship between F2 and P2. This paper uses colour to enhance its presentation. If the link below is not blue, follow it for the colour version. http://homepages.inf.ed.ac.uk/wadler
Original languageEnglish
Pages (from-to)201 - 226
JournalTheoretical Computer Science
Volume375
Issue number1-3
DOIs
Publication statusPublished - 2007

Fingerprint

Dive into the research topics of 'The Girard-Reynolds isomorphism (second edition)'. Together they form a unique fingerprint.

Cite this