### 抜粋

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.

元の言語 | 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 22 → 2016 6 26 |

### Other

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

国 | Portugal |

市 | Porto |

期間 | 16/6/22 → 16/6/26 |

### ASJC Scopus subject areas

- Software

### これを引用

*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