Informatics Report Series


Report   

EDI-INF-RR-0588


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:The Girard-Reynolds Isomorphism
Authors: Philip Wadler
Date: 2003
Publication Title:Information and Computation
Publication Type:Journal Article
Volume No:186(2) Page Nos:260-284
Abstract:
The second-order polymorphic lambda calculus, F2, was independently discovered by Girard and Reynolds. 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: for a suitable notion of logical relation, every term in F2 takes related arguments into related results. 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. The Girard projection discards all first-order quantifiers, so it seems unreasonable to expect that the Girard projection followed by the Reynolds embedding should also be the identity. However, we show that in the presence of Reynolds's parametricity property that this is indeed the case, for propositions corresponding to inductive definitions of naturals or other algebraic types.
Links To Paper
ACM Digital Portal
Bibtex format
@Article{EDI-INF-RR-0588,
author = { Philip Wadler },
title = {The Girard-Reynolds Isomorphism},
journal = {Information and Computation},
year = 2003,
volume = {186(2)},
pages = {260-284},
url = {http://portal.acm.org/citation.cfm?id=957696&dl=ACM&coll=portal},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh