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

Document

0

Metadata

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

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail