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

Strong normalization for the parameter-free polymorphic lambda calculus based on the Ω-rule. / Akiyoshi, Ryota; Terui, Kazushige.

1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Vol. 52 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016. 5.

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

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, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, 16/6/22. https://doi.org/10.4230/LIPIcs.FSCD.2016.5
Akiyoshi R, Terui K. 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. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2016. 5 https://doi.org/10.4230/LIPIcs.FSCD.2016.5
Akiyoshi, Ryota ; Terui, Kazushige. / 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. Vol. 52 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016.
@inproceedings{ef83c5507e8d47718412083a372f8426,
title = "Strong normalization for the parameter-free polymorphic lambda calculus based on the Ω-rule",
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{\"o}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.",
keywords = "Computability predicate, Infinitary proof theory, Polymorphic lambda calculus, Strong normalization",
author = "Ryota Akiyoshi and Kazushige Terui",
year = "2016",
month = "6",
day = "1",
doi = "10.4230/LIPIcs.FSCD.2016.5",
language = "English",
volume = "52",
booktitle = "1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

}

TY - GEN

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

AU - Akiyoshi, Ryota

AU - Terui, Kazushige

PY - 2016/6/1

Y1 - 2016/6/1

N2 - 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.

AB - 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.

KW - Computability predicate

KW - Infinitary proof theory

KW - Polymorphic lambda calculus

KW - Strong normalization

UR - http://www.scopus.com/inward/record.url?scp=84977568853&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84977568853&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSCD.2016.5

DO - 10.4230/LIPIcs.FSCD.2016.5

M3 - Conference contribution

VL - 52

BT - 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -