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

Ryota Akiyoshi, Kazushige Terui

研究成果: Conference contribution

1 引用 (Scopus)

抜粋

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.

元の言語English
ホスト出版物のタイトル1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
出版者Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
52
ISBN(電子版)9783959770101
DOI
出版物ステータスPublished - 2016 6 1
イベント1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal
継続期間: 2016 6 222016 6 26

Other

Other1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016
Portugal
Porto
期間16/6/2216/6/26

ASJC Scopus subject areas

  • Software

これを引用

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