A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
type: Item
instance of: scholarly article
title: A proof of strongly uniform termination for Gödel's \(T\) by methods from local predicativity
zbMATH Open document ID: 0889.03049
author: Andreas Weiermann
published in: Archive for Mathematical Logic
publication date: 1997-12-10T00:00:00Z
review text: After reviewing the historical development of the subject, the author reconsiders the Howard-Schütte assignment of finite sequences of ordinals to terms in Gödel's \(T\). In its original form, this method yields decreasing ordinals only when the conversion \(I(t+1)ab \mapsto a(Itab)\) is restricted to numerals \(t\). This restriction is overcome by using an `essentially less than' relation \(\ll\) and a collapsing function \({\mathcal D}\) (as in the paper of \textit{W. Buchholz, A. Cichon} and \textit{A. Weiermann} [``A uniform approach to fundamental sequences and hierarchies'', Math. Log. Q. 40, 273-286 (1994; Zbl 0812.03023)]) such that \(a\) reduces to \(b\) implies that \([b]_0 \ll [a]_0\) and hence \({\mathcal D}(b) < {\mathcal D}(a)\). The collapse can be thought of as providing time to wait until the numerical argument \(t\) of the iterator \(Itab\) is reduced to a numeral. For simplicity of presentation the author has chosen a form of \(T\) with combinators and iterators. A treatment allowing for arbitrary typed \(\lambda\)-terms and the recursor is promised for a subsequent paper. The paper also sketches -- as the author puts it -- an `affirmative contribution' to a problem of Girard, who had assigned an ordinal \(|t|\) less than the Bachmann-Howard ordinal to every term \(t\) of \(T\) and asked `what is the relation of the ordinals \(|t|\) to the structure of computation of \(t\)?' Moreover, the author conjectures that the method of the present paper can be applied to general investigations on proving termination for higher order rewrite systems by using ordinal notations, referring to a paper of \textit{J. van de Pol} and \textit{H. Schwichtenberg} [``Strict functionals for termination proofs'', in: M. Dezani-Ciancaglini and G. Plotkin (editors), Typed Lambda Calculi and Applications, Lect. Notes Comput. Sci. 902, 350-364 (1995)] for related work.
Mathematics Subject Classification ID: 03F10
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03D20
zbMATH DE Number: 1095972
zbMATH Keywords: collapsing function
zbMATH Keywords: termination proofs
zbMATH Keywords: ordinal assignment
zbMATH Keywords: essentially less than
reviewed by: Helmut Schwichtenberg
MaRDI profile type: Publication
full work available at URL: s001530050075
OpenAlex ID: W2027585565
DOI: 10.1007/S001530050075
Recommended article: Derivation lengths classification of Gödel's T extending Howard's assignment
Recommended article: Reduction of higher type levels by means of an ordinal analysis of finite terms
Recommended article: Automated Deduction – CADE-19
Recommended article: Q4202962
Recommended article: Complexity of Gödel’s T in λ-Formulation
Recommended article: Total termination of term rewriting
Recommended article: Q4218926
Recommended article: Q4850555
Recommended article: An ordinal calculus for proving termination in term rewriting
description: scientific article; zbMATH DE number 1095972