Reduction of higher type levels by means of an ordinal analysis of finite terms

DOI10.1016/0168-0072(85)90031-4zbMath0554.03024OpenAlexW2133262398MaRDI QIDQ759749

Jan Terlouw

Publication date: 1985

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://pure.rug.nl/ws/files/130207356/1_s2.0_0168007285900314_main.pdf

zbMATH Keywords

elimination of higher type levelsfinite termsordinal assignments

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Recursive functions and relations, subrecursive hierarchies (03D20) Higher-type and set recursion theory (03D65)

Related Items (2)

Combinatory logic with polymorphic types ⋮ Perpetual reductions in \(\lambda\)-calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Nested recursion
• Recursion on the countable functionals
• The lambda calculus, its syntax and semantics
• Functionals defined by recursion
• Ordinal analysis of terms of finite type
• On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising

This page was built for publication: Reduction of higher type levels by means of an ordinal analysis of finite terms