Barenbaum, Pablo ;
Sottile, Cristian
Two Decreasing Measures for Simply Typed 位Terms
Abstract
This paper defines two decreasing measures for terms of the simply typed 位calculus, called the 饾挷measure and the 饾挴^{饾惁}measure. A decreasing measure is a function that maps each typable 位term to an element of a wellfounded ordering, in such a way that contracting any 尾redex decreases the value of the function, entailing strong normalization. Both measures are defined constructively, relying on an auxiliary calculus, a nonerasing variant of the 位calculus. In this system, dubbed the 位^{饾惁}calculus, each 尾step creates a "wrapper" containing a copy of the argument that cannot be erased and cannot interact with the context in any other way. Both measures rely crucially on the observation, known to Turing and Prawitz, that contracting a redex cannot create redexes of higher degree, where the degree of a redex is defined as the height of the type of its 位abstraction. The 饾挷measure maps each 位term to a natural number, and it is obtained by evaluating the term in the 位^{饾惁}calculus and counting the number of remaining wrappers. The 饾挴^{饾惁}measure maps each 位term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree.
BibTeX  Entry
@InProceedings{barenbaum_et_al:LIPIcs.FSCD.2023.11,
author = {Barenbaum, Pablo and Sottile, Cristian},
title = {{Two Decreasing Measures for Simply Typed \lambdaTerms}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {11:111:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772778},
ISSN = {18688969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17995},
URN = {urn:nbn:de:0030drops179956},
doi = {10.4230/LIPIcs.FSCD.2023.11},
annote = {Keywords: Lambda Calculus, Rewriting, Termination, Strong Normalization, Simple Types}
}
28.06.2023
Keywords: 

Lambda Calculus, Rewriting, Termination, Strong Normalization, Simple Types 
Seminar: 

8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Issue date: 

2023 
Date of publication: 

28.06.2023 