TY - GEN
T1 - The confluent terminating context-free substitutive rewriting system for the lambda-calculus with surjective pairing & terminal type
AU - Akama, Yohji
PY - 2017/9/1
Y1 - 2017/9/1
N2 - For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo, inspired by Knuth-Bendix completion, introduced a confluent rewriting system of the naive rewriting system. Their system is a confluent (CR) rewriting system stable under contexts. They left the strong normalization (SN) of their rewriting system open. By Girard's reducibility method with restricting reducibility theorem, we prove SN of their rewriting, and SN of the extensions by polymorphism and (terminal types caused by parametric polymorphism). We extend their system by sum types and eta-like reductions, and prove the SN. We compare their system to type-directed expansions.
AB - For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo, inspired by Knuth-Bendix completion, introduced a confluent rewriting system of the naive rewriting system. Their system is a confluent (CR) rewriting system stable under contexts. They left the strong normalization (SN) of their rewriting system open. By Girard's reducibility method with restricting reducibility theorem, we prove SN of their rewriting, and SN of the extensions by polymorphism and (terminal types caused by parametric polymorphism). We extend their system by sum types and eta-like reductions, and prove the SN. We compare their system to type-directed expansions.
KW - Reducibility method
KW - Restricted reducibility theorem
KW - Strong normalization
KW - Sum type
KW - Typedirected expansion
UR - http://www.scopus.com/inward/record.url?scp=85030533532&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85030533532&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2017.6
DO - 10.4230/LIPIcs.FSCD.2017.6
M3 - Conference contribution
AN - SCOPUS:85030533532
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
A2 - Miller, Dale
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
Y2 - 3 September 2017 through 9 September 2017
ER -