LIPIcs.FSCD.2016.5.pdf
- Filesize: 0.56 MB
- 15 pages
Document
Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.
Authors
-
Part of:
Volume:
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2016-06-17
Cite As Get BibTex
Ryota Akiyoshi and Kazushige Terui. Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.5
Abstract
Following Aehlig, we consider a hierarchy F^p= { F^p_n }_{n in Nat} 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
Aehlig). 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 ID_n+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 Godel-Tait method, can be locally
formalized in ID_n. This provides a direct proof to the known
result that the representable functions in F^p_n are provably
total in ID_n. In both cases, Buchholz' Omega-rule plays a
central role.
Subject Classification
Keywords
- Polymorphic Lambda Calculus
- Strong Normalization
- Computability Predicate
- Infinitary Proof Theory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads