## 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].

### MSC:

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