We present an effective proof (with explicit bounds) of the Podelski and Rybalchenko Termination Theorem. The sub-recursive bounds we obtain make use of bar recursion, in the form of the product of selection functions, as this is used to interpret the Weak Ramsey Theorem for pairs. The construction can be seen as calculating a modulus of well-foundedness for a given program given moduli of well-foundedness for the disjunctively well-founded finite set of covering relations. When the input moduli are in system T, this modulus is also definable in system T by a result of Schwichtenberg on bar recursion.
An analysis of the Podelski–Rybalchenko termination theorem via bar recursion
BERARDI, Stefano;STEILA, SILVIA
2019-01-01
Abstract
We present an effective proof (with explicit bounds) of the Podelski and Rybalchenko Termination Theorem. The sub-recursive bounds we obtain make use of bar recursion, in the form of the product of selection functions, as this is used to interpret the Weak Ramsey Theorem for pairs. The construction can be seen as calculating a modulus of well-foundedness for a given program given moduli of well-foundedness for the disjunctively well-founded finite set of covering relations. When the input moduli are in system T, this modulus is also definable in system T by a result of Schwichtenberg on bar recursion.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
Steila-Oliva-termination_theorem.pdf
Accesso aperto
Tipo di file:
PREPRINT (PRIMA BOZZA)
Dimensione
296.83 kB
Formato
Adobe PDF
|
296.83 kB | Adobe PDF | Visualizza/Apri |
berardi2015.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
258.85 kB
Formato
Adobe PDF
|
258.85 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.