The Community for Technology Leaders
RSS Icon
Subscribe
Copenhagen, Denmark
July 22, 2002 to July 25, 2002
ISBN: 0-7695-1483-9
pp: 147
Marcelo Fiore , University of Cambridge
Roberto Di Cosmo , Université Paris 7 and INRIA-Roquencourt
Vincent Balat , Université Paris 7
ABSTRACT
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.
INDEX TERMS
null
CITATION
Marcelo Fiore, Roberto Di Cosmo, Vincent Balat, "Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types", LICS, 2002, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science 2002, pp. 147, doi:10.1109/LICS.2002.1029824
32 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool