A confluent reduction for the \(\lambda\)-calculus with surjective pairing and terminal object. (English) Zbl 0769.68056

Curien, Pierre-Louis; Di Cosmo, Roberto

Automata, languages and programming, Proc. 18th Int. Colloq., Madrid/Spain 1991, Lect. Notes Comput. Sci. 510, 291-302 (1991).

Summary: [For the entire collection see Zbl 0753.00027.]
We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The \(\lambda\)- calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing and terminal object via a confluent rewriting system, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with polymorphic types. Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed \(\lambda\)-calculus with subtyping.

MSC:

68Q42	Grammars and rewriting systems
03B40	Combinatory logic and lambda calculus
18D15	Closed categories (closed monoidal and Cartesian closed categories, etc.)
03B25	Decidability of theories and sets of sentences

Keywords:

full equational theory underlying cartesian closed categories; polymorphic extensions; \(\lambda\)-calculus extended with surjective pairing; terminal object; confluent rewriting system; decidability; polymorphic types

Citations:

Zbl 0753.00027