On Mints’ reduction for ccc-calculus. (English) Zbl 0786.03006

Bezem, Marc (ed.) et al., Typed Lambda calculi and applications. International conference, TLCA ’93, March 16-18, 1993, Utrecht, the Netherlands. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 664, 1-12 (1993).
Summary: We present a divide-and-conquer lemma to infer the \(\text{SN}+\text{CR}\) (Strong Normalization and Church-Rosser) property of a reduction system from that property of its subsystems. Then we apply the lemma to show the property of Mints’ reduction for ccc-calculus with restricted \(\eta\)- expansion and restricted \(\pi\)-expansion. In the course of the proof, we obtain some relations of the two restricted expansions against traditional reductions. Among others, we get a simple characterization of the restricted \(\eta\)-expansion in terms of traditional \(\beta\)- and \(\eta\)-reductions, and a similar characterization for the restricted \(\pi\)-expansion.
For the entire collection see [Zbl 0866.00038].


03B22 Abstract deductive systems
03B40 Combinatory logic and lambda calculus