Provable isomorphisms of types. (English) Zbl 0763.03011

Summary: A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. Using the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC’s. Using the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having “invertible” proofs between the two terms. Work of M. Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.


03B40 Combinatory logic and lambda calculus
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
68P10 Searching and sorting
Full Text: DOI


[1] Barendregt, The Lambda Calculus; Its syntax and Semantics (revised edition) (1984) · Zbl 0551.03007
[2] Asperti, Categories, Types, and Structures (1991)
[3] DOI: 10.1007/BF02023009 · Zbl 0537.03009 · doi:10.1007/BF02023009
[4] DOI: 10.1007/BF01084396 · Zbl 0509.18002 · doi:10.1007/BF01084396
[5] Rittri, Lecture Notes in Computer Science 449 (1990)
[6] Rittri, Journal of Functional Programming 1 (1989)
[7] Curien, ICALP pp 291– (1991)
[8] Martini, Strong equivalence in positive propositional logic: provable realizability and type assignment (1991)
[9] DOI: 10.1007/BFb0075313 · doi:10.1007/BFb0075313
[10] Martin, Notices of the Am. Math. Soc. 19 pp 778– (1972)
[11] DOI: 10.1016/0304-3975(76)90085-2 · Zbl 0368.02028 · doi:10.1016/0304-3975(76)90085-2
[12] Lambek, An introduction to higher order categorical logic (1986) · Zbl 0596.03002
[13] DOI: 10.1305/ndjfl/1093883461 · Zbl 0476.03026 · doi:10.1305/ndjfl/1093883461
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.