2026-07-21T23:19:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7734 2024-03-06T10:41:01Z ddc:004 open_access

The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type Akama, Yohji reducibility method restricted reducibility theorem sum type typedirected expansion strong normalization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yohji Akama 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.6 urn:nbn:de:0030-drops-77346 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.6 eng https://creativecommons.org/licenses/by/3.0/legalcode