Remarks on isomorphisms in typed lambda calculi with empty and sum types

Proceedings - Symposium on Logic in Computer Science - Trang 147-156
M. Fiore1, R. Di Cosmo2, V. Balat3
1Computer Laboratory, University of Cambridge, UK
2PPS-Université Paris, INRIA-Roquencourt, France
3Université, Paris, France

Tóm tắt

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.

Từ khóa

#Equations #Digital arithmetic #Educational institutions #Computer languages #Calculus #Logic programming #Functional programming #Algebra #Laboratories #Libraries

Tài liệu tham khảo

10.1016/0168-0072(90)90049-8

fiore, 2002, Extensional normalisation for typed lambda calculus with sums via Grothendieck logical relations

10.1090/S0002-9939-1985-0781071-1

doner, 1969, An extended arithmetic of ordinal numbers, Fundamenta Mathematica, 65, 95, 10.4064/fm-65-1-95-127

10.1017/S0960129596002241

di cosmo, 1995, Isomorphisms of types From ?-calculus to information retrieval and language design, 10.1007/978-1-4612-2572-0

di cosmo, 1995, Second order isomorphic types. A proof theoretic study on second order ?-calculus with surjective pairing and terminal object, Information and Computation, 176, 10.1006/inco.1995.1085

10.1017/S0956796800000861

10.1017/S0956796800000861

lambek, 1986, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics, 7

lafont, 1987, Logiques cate?gories et machines

martin, 1972, Axiomatic bases for equational theories of natural numbers, Notices of the Am Math Soc, 19, 778

10.1109/LICS.1993.287600

rittri, 1990, Retrieving library identifiers by equational matching of types, Lecture Notes in Computer Science, 499, 10.1007/3-540-52885-7_117

rittri, 1990, Searching program libraries by type and proving compiler correctness by bisimulation

10.1017/S095679680000006X

runciman, 1991, Retrieving re-usable software components by polymorphic type, Journal of Functional Programming, 1, 191, 10.1017/S0956796800020049

10.1016/S0022-4049(99)00185-1

10.1007/BF01084396

barthes, 2001, Type isomorphisms and proof reuse in dependent type theory, LNCS, 2030, 57

10.1007/3-540-48168-0_18

delahaye, 1997, Recherche dans une bibliothe?que de preuves Coq en utilisant le type et modulo isomorphismes, PRC/GDR de programmation Po?le Preuves et Spe?cifications Alge?briques

10.1007/3-540-61756-6_95

10.1007/3-540-56944-8_71

10.1016/0022-4049(93)90035-R

10.2307/2324454

wilkie, 1981, On exponentiation - A solution to Tarski's high school algebra problem

10.1145/22145.22175

taylor, 1999, Practical foundations of mathematics, Cambridge Studies in Advanced Mathematics, 59

bruce, 1992, Provable isomorphisms of types, Mathematical Structures in Computer Science, 2, 231, 10.1017/S0960129500001444

10.1017/CBO9781139172707

10.1017/S0960129500000232

Thông tin
Thông tin xuất bản

Proceedings - Symposium on Logic in Computer Science

147-156

Thông tin tác giả