Conservative extension by surjective pairing

• To: rdv@cs.vu.nl
• Subject: Conservative extension by surjective pairing
• From: meyer@theory.LCS.MIT.EDU
• Date: Thu, 3 Aug 89 13:44:00 EDT
• Cc: types@theory.LCS.MIT.EDU
• In-Reply-To: Roel de Vrijer's message of Wed, 26 Jul 89 18:47:36 MET DST <8907261847.aa29875@ski.cs.vu.nl>

I hae a question related to your LICS '89 paper which we just had
the pleasure of presenting in our research seminar.

You establish that surjective pairing axioms conservatively extend
lambda-beta conversion, and mention that this question is open for
lambda-beta-eta conversion.

Of course there are lots of other lambda-beta, indeed lambda-beta-eta,
theories where conservative extension HOLDS simply because the theory
consists of the valid equations in some lambda model in which surjective
pairing functions exist, e.g,, D_infinity.  Also, I have no doubt there
are other theories besides lambda-beta-eta where conservativity is OPEN.
Is there any theory for which conservative extension by surjective pairing
is know to FAIL?  If not, would you conjecture that surjective pairing
axioms yield a conservative extension of EVERY lambda-beta-theory?

Regards, A.

• Prev: call-by-value semantics, etc. (248 lines)
• Next: LICS '90: Call for Papers
• Index(es):
  • Main
  • Thread