2026-07-25T00:30:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5971 2024-03-06T10:37:23Z ddc:004 open_access

Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule. Akiyoshi, Ryota Terui, Kazushige Polymorphic Lambda Calculus Strong Normalization Computability Predicate Infinitary Proof Theory Following Aehlig, we consider a hierarchy F^p= { F^p_n }_{n in Nat} of parameter-free subsystems of System F, where each F^p_n corresponds to ID_n, the theory of n-times iterated inductive definitions (thus our F^p_n corresponds to the n+1th system of Aehlig). We here present two proofs of strong normalization for F^p_n, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in ID_n+1. This provides a tight upper bound on the complexity of the normalization theorem for System F^p_n. The second one, based on the Godel-Tait method, can be locally formalized in ID_n. This provides a direct proof to the known result that the representable functions in F^p_n are provably total in ID_n. In both cases, Buchholz' Omega-rule plays a central role. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ryota Akiyoshi and Kazushige Terui 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.5 urn:nbn:de:0030-drops-59718 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.5 eng https://creativecommons.org/licenses/by/3.0/legalcode