×

Simulating expansions without expansions. (English) Zbl 0831.03004

Summary: We add extensional equalities for the functional and product types to the typed \(\lambda\)-calculus with, in addition to products and terminal objects, sums and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus decidable) rewriting system for the calculus that remains confluent when allowing unbounded recursion. To do this, we turn the extensional equalities into expansion rules, and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting taks than for the usual \(\lambda\)-calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non-extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence directly from our simulation technique without using the weak confluence property.

MSC:

03B40 Combinatory logic and lambda calculus
68Q42 Grammars and rewriting systems
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Curien, Springer-Verlag Lecture Notes in Computer Science 510 pp 291– (1991)
[2] Barendregt, The Lambda Calculus; Its syntax and Semantics (revised edition) (1984) · Zbl 0551.03007
[3] Akama, Springer-Verlag Lecture Notes in Computer Science 664 pp 1– (1993)
[4] DOI: 10.1305/ndjfl/1093636767 · Zbl 0624.03043
[5] DOI: 10.1016/0022-0000(87)90029-8 · Zbl 0619.68025
[6] Curry, Combinatory Logic (1958)
[7] Mints, Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V.A. Steklova AN SSSR 68 pp 83– (1977)
[8] Lambek, An introduction to higher order categorical logic (1986) · Zbl 0596.03002
[9] DOI: 10.1016/0304-3975(76)90009-8 · Zbl 0335.02016
[10] Klop, Mathematical Center Tracts 27 (1980)
[11] Girard, Proofs and Types (1990)
[12] DOI: 10.1305/ndjfl/1093883461 · Zbl 0476.03026
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.