Combinatory logic with polymorphic types

Autor:	William R. Stirton
Rok vydání:	2021
Předmět:	Philosophy Class (set theory) Pure mathematics Reduction (recursion theory) Transfinite induction Logic Recursive ordinal Computability Finitary Type (model theory) Combinatory logic Mathematics
Zdroj:	Archive for Mathematical Logic. 61:317-343
ISSN:	1432-0665 0933-5846
DOI:	10.1007/s00153-021-00792-5
Popis:	Sections 1 through 4 define, in the usual inductive style, various classes of object including one which is called the “combinatory terms of polymorphic type”. Section 5 defines a reduction relation on these terms. Section 6 shows that the weak normalizability of the combinatory terms of polymorphic type entails the weak normalizability of the lambda terms of polymorphic type. The entailment is not vacuous, because the combinatory terms of polymorphic type are indeed weakly normalizable, as is proven in Sect. 7 using Tait and Girard’s computability predicates. The remainder of the paper is devoted to arguing that interesting consequences would follow from the existence of an “ordinally informative” proof, i.e. one which uses transfinite induction over recursive ordinal numbers and otherwise finitary methods, of normalizability for as large a class of the terms as possible.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::dd97471301bcb4118135665b162abce8 https://doi.org/10.1007/s00153-021-00792-5 Zobrazit plný text záznamu Full text from SpringerLink