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

Autor:	Takahashi, Yuta
Jazyk:	angličtina
Rok vydání:	2022
Předmět:	termination Theory of computation → Equational logic and rewriting non-positive types inductive types Theory of computation → Type theory higher-order rewriting
DOI:	10.4230/lipics.types.2021.12
Popis:	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. LIPIcs, Vol. 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021), pages 12:1-12:23
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::5f6d4737cd5c551ebdbb2df9a0da8175 Zobrazit plný text záznamu