License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.6
URN: urn:nbn:de:0030-drops-77346
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7734/
Go to the corresponding LIPIcs Volume Portal

Akama, Yohji

The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

pdf-format:
LIPIcs-FSCD-2017-6.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{akama:LIPIcs:2017:7734,
  author =	{Yohji Akama},
  title =	{{The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7734},
  URN =		{urn:nbn:de:0030-drops-77346},
  doi =		{10.4230/LIPIcs.FSCD.2017.6},
  annote =	{Keywords: reducibility method, restricted reducibility theorem, sum type, typedirected expansion, strong normalization}
}

Keywords: reducibility method, restricted reducibility theorem, sum type, typedirected expansion, strong normalization
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI