DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2021.12

Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus

Authors: Yuta Takahashi

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract

So far, several typed lambda-calculus systems were combined with algebraic rewrite rules, and the termination (in other words, strong normalisation) problem of the combined systems was discussed. By the size-based approach, Blanqui formulated a termination criterion for simply typed lambda-calculus with algebraic rewrite rules which guarantees, in some specific cases, the termination of the rewrite relation induced by beta-reduction and algebraic rewrite rules on strictly or non-strictly positive inductive types. Using the inflationary fixed-point construction, we extend this termination criterion so that it is possible to show the termination of the rewrite relation induced by some rewrite rules on types which are called non-positive types. In addition, we note that a condition in Blanqui’s proof can be dropped, and this improves the criterion also for non-strictly positive inductive types.

Cite as

Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{takahashi:LIPIcs.TYPES.2021.12,
  author =	{Takahashi, Yuta},
  title =	{{Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.12},
  URN =		{urn:nbn:de:0030-drops-167811},
  doi =		{10.4230/LIPIcs.TYPES.2021.12},
  annote =	{Keywords: termination, higher-order rewriting, non-positive types, inductive types}
}

Search Results

Documents authored by Takahashi, Yuta

Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message