Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.

Akiyoshi, Ryota; Terui, Kazushige

doi:10.4230/LIPIcs.FSCD.2016.5

Document

Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.

Authors Ryota Akiyoshi, Kazushige Terui

Part of: Volume: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Formal Structures for Computation and Deduction (FSCD)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2016-06-17

PDF

File

PDF

LIPIcs.FSCD.2016.5.pdf

Filesize: 0.56 MB
15 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSCD.2016.5
URN: urn:nbn:de:0030-drops-59718

Subject Classification

Keywords

Polymorphic Lambda Calculus
Strong Normalization
Computability Predicate
Infinitary Proof Theory

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

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

Author Details

Ryota Akiyoshi

Kazushige Terui

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail