[Prev][Next][Index][Thread]
Remarks on type isomorphisms with the empty and sum type
The following paper (to be presented in LICS'02) is available on the Web
Remarks on Isomorphisms in
Typed Lambda Calculi with Empty and Sum Type
by Vincent Balat, Roberto Di Cosmo and Marcelo Fiore
Tarski asked whether the arithmetic identities taught in high school
are complete for showing all arithmetic equations valid for the
natural numbers. The answer to this question for the language of
arithmetic expressions using a constant for the number one and the
operations of product and exponentiation is affirmative, and the
complete equational theory also characterises isomorphism in the typed
lambda calculus, where the constant for one and the operations of
product and exponentiation respectively correspond to the unit type
and the product and arrow type constructors.
This paper studies isomorphisms in typed lambda calculi with empty and
sum types from this viewpoint. We close an open problem by
establishing that the theory of type isomorphisms in the presence of
product, arrow, and sum types (with or without the unit type) is not
finitely axiomatisable. Further, we observe that for type theories
with arrow, empty and sum types the correspondence between isomorphism
and arithmetic equality generally breaks down, but that it still holds
in some particular cases including that of type isomorphism with the
empty type and equality with zero.
The paper is available over the Web:
http://www.cl.cam.ac.uk/~mpf23/papers/Types/remarks.ps.gz
http://www.cl.cam.ac.uk/~mpf23/papers/Types/remarks.pdf