Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2021.12
URN: urn:nbn:de:0030-drops-167811
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16781/
Takahashi, Yuta
Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus
| pdf-format: |
|
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.
BibTeX - Entry
@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/opus/volltexte/2022/16781},
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}
}
| Keywords: | termination, higher-order rewriting, non-positive types, inductive types | |
| Seminar: | 27th International Conference on Types for Proofs and Programs (TYPES 2021) | |
| Issue date: | 2022 | |
| Date of publication: | 04.08.2022 |
