### Abstract

Following Aehlig [3], we consider a hierarchy F^{p} = {F^{p} _{n}}_{n∈ℕ} 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 [3]). 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 IDn+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 Gödel-Tait method, can be locally formalized in IDn. This provides a direct proof to the known result that the representable functions in F^{p} _{n} are provably total in IDn. In both cases, Buchholz' Ω-rule plays a central role.

Original language | English |
---|---|

Title of host publication | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 |

Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |

Volume | 52 |

ISBN (Electronic) | 9783959770101 |

DOIs | |

Publication status | Published - 2016 Jun 1 |

Event | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal Duration: 2016 Jun 22 → 2016 Jun 26 |

### Other

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

Country | Portugal |

City | Porto |

Period | 16/6/22 → 16/6/26 |

### Keywords

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

### ASJC Scopus subject areas

- Software

### Cite this

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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 -