TY - GEN
T1 - On mints’ reduction for ccc-calculus
AU - Akama, Yohji
N1 - Funding Information:
* Supported by JSPS Fellowship for Japanese Junior Scientists 2 In this paper, the type forming operator D is right associative. And the type-superscripts of terms are often omitted. The term forming operators 1 and r have higher precedences than the application operator. As usual, we denote a-congruence by --. We refer to \[1\]a s the standard text.
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1993.
PY - 1993
Y1 - 1993
N2 - In this paper, we present a divide-and-conquer lemma to infer the SN+CR (Strongly 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 ν-expansion and restricted π-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 ν-expansion in terms of traditional β-and ν-reductions, and a similar characterization for the restricted π-expansion.
AB - In this paper, we present a divide-and-conquer lemma to infer the SN+CR (Strongly 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 ν-expansion and restricted π-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 ν-expansion in terms of traditional β-and ν-reductions, and a similar characterization for the restricted π-expansion.
UR - http://www.scopus.com/inward/record.url?scp=85028770923&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85028770923&partnerID=8YFLogxK
U2 - 10.1007/bfb0037094
DO - 10.1007/bfb0037094
M3 - Conference contribution
AN - SCOPUS:85028770923
SN - 9783540565178
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 12
BT - Typed Lambda Calculi and Applications - International Conference on Typed Lamda Calculi and Applications, TLCA 1993, Proceedings
A2 - Bezem, Marc
A2 - Groote, Jan Friso
PB - Springer Verlag
T2 - 1st International Conference on Typed Lamda Calculi and Applications, TLCA 1993
Y2 - 16 March 1993 through 18 March 1993
ER -