Abstract
In 2001 Lee, Jones and BenAmram introduced the notion of sizechange termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is sizechange terminating if and only if it has a certain property which can be statically verified from the recursive definition of the program. Their proof of the sizechange termination theorem used Ramsey's Theorem for pairs, which is a purely classical result. In 2012 Vytiniotis, Coquand and Wahlsteldt intuitionistically proved a classical variant of the sizechange termination theorem by using the AlmostFull Theorem instead of Ramsey's Theorem for pairs. In this paper we provide an intuitionistic proof of another classical variant of the SCT theorem: our goal is to provide a statement and a proof very similar to the original ones. This can be done by using the Hclosure Theorem, which differs from Ramsey's Theorem for pairs only by a contrapositive step. As a side result we obtain another proof of the characterization of the functions computed by a tailrecursive SCT program, by relating the SCT Theorem with the Termination Theorem by Podelski and Rybalchenko. Finally, by investigating the relationship between them, we provide a property in the "language" of sizechange termination which is equivalent to Podelski and Rybalchenko's termination.
BibTeX  Entry
@InProceedings{steila:LIPIcs:2015:5502,
author = {Silvia Steila},
title = {{An Intuitionistic Analysis of Sizechange Termination}},
booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)},
pages = {288307},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897880},
ISSN = {18688969},
year = {2015},
volume = {39},
editor = {Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5502},
URN = {urn:nbn:de:0030drops55026},
doi = {10.4230/LIPIcs.TYPES.2014.288},
annote = {Keywords: Intuitionism, Ramsey's Theorem, Termination}
}
Keywords: 

Intuitionism, Ramsey's Theorem, Termination 
Collection: 

20th International Conference on Types for Proofs and Programs (TYPES 2014) 
Issue Date: 

2015 
Date of publication: 

12.10.2015 