Strong normalization for the parameter-free polymorphic lambda calculus based on the Ω-rule

Ryota Akiyoshi, Kazushige Terui

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Following Aehlig [3], we consider a hierarchy Fp = {Fp n}n∈ℕ of parameter-free subsystems of System F, where each Fp n corresponds to IDn, the theory of n-times iterated inductive definitions (thus our Fp n corresponds to the n + 1th system of [3]). We here present two proofs of strong normalization for Fp n, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in IDn+1. This provides a tight upper bound on the complexity of the normalization theorem for System Fp n. The second one, based on the Gödel-Tait method, can be locally formalized in IDn. This provides a direct proof to the known result that the representable functions in Fp n are provably total in IDn. In both cases, Buchholz' Ω-rule plays a central role.

Original languageEnglish
Title of host publication1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume52
ISBN (Electronic)9783959770101
DOIs
Publication statusPublished - 2016 Jun 1
Event1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal
Duration: 2016 Jun 222016 Jun 26

Other

Other1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
CountryPortugal
CityPorto
Period16/6/2216/6/26

Keywords

  • Computability predicate
  • Infinitary proof theory
  • Polymorphic lambda calculus
  • Strong normalization

ASJC Scopus subject areas

  • Software

Cite this

Akiyoshi, R., & Terui, K. (2016). Strong normalization for the parameter-free polymorphic lambda calculus based on the Ω-rule. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 (Vol. 52). [5] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2016.5