Is extensionality equational in the absence of xi?

• To: types@cis.upenn.edu
• Subject: Is extensionality equational in the absence of xi?
• From: Philip Wadler <wadler@research.bell-labs.com>
• Date: Wed, 14 Mar 2001 17:30:57 -0500

The theory (lambda) has the following derivation rules:

	(I)	(\x.M)N  =  M[x:=N]		(beta)
	(II.1)	M = M				(reflexivity)
	(II.2)	M = N => N = M			(symmetry)
	(II.3)	L = M, M = N => L = N		(transitivity)
	(II.4)	M = N => ML = NL		(congruence)
	(II.5)	M = N => LM = ZL		(congruence)
	(II.6)	M = N => \x.M = \x.N		(xi)

In the presence of these rules, then extensionality

		Mx = Nx => M = N		(ext)

is equivalent to (eta)

		\x.Mx = M			(eta)

Define (lambda-) to be (lambda) without rule (xi).  It is easy
to check that (lambda-)+(ext) is closed under (xi).

Question: Is it possible to extend (lambda-) by a finite set of
equations A such that (lambda-)+A is closed under (ext)?

We cannot solve this trivially by taking A=(ext) or A=(eta)+(xi),
because A must be a set of equations of the form M=N, which rules
out conditional equations like (ext) and (xi).

For combinatory logic CL there is such a set of equations, called
A_beta_eta, see Barendregt 7.3.15.  Further, CL+A_beta_eta is provably
equivalent to (lambda)+(ext), but this proof relies on (xi).

Cheers,  -- P



	

• Prev: CfP: Babel01 Workshop on Multi-Language Infrastructure and Interoperability
• Next: TACS 2001 -- call for papers
• Index(es):
  • Main
  • Thread