2026-07-20T05:05:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5502 2024-03-06T10:36:14Z ddc:004 open_access

An Intuitionistic Analysis of Size-change Termination Steila, Silvia Intuitionism Ramsey's Theorem Termination In 2001 Lee, Jones and Ben-Amram introduced the notion of size-change termination (SCT) for first order functional programs, a sufficient condition for termination. They proved that a program is size-change 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 size-change 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 size-change termination theorem by using the Almost-Full 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 H-closure 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 tail-recursive 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 size-change termination which is equivalent to Podelski and Rybalchenko's termination. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Silvia Steila 2015 Is Part Of LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2014.288 urn:nbn:de:0030-drops-55026 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.288 eng https://creativecommons.org/licenses/by/3.0/legalcode