1 Search Results for "Akiyoshi, Ryota"


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

Authors: Ryota Akiyoshi and Kazushige Terui

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)


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

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)


Copy BibTex To Clipboard

@InProceedings{akiyoshi_et_al:LIPIcs.FSCD.2016.5,
  author =	{Akiyoshi, Ryota and Terui, Kazushige},
  title =	{{Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.5},
  URN =		{urn:nbn:de:0030-drops-59718},
  doi =		{10.4230/LIPIcs.FSCD.2016.5},
  annote =	{Keywords: Polymorphic Lambda Calculus, Strong Normalization, Computability Predicate, Infinitary Proof Theory}
}
  • Refine by Author
  • 1 Akiyoshi, Ryota
  • 1 Terui, Kazushige

  • Refine by Classification

  • Refine by Keyword
  • 1 Computability Predicate
  • 1 Infinitary Proof Theory
  • 1 Polymorphic Lambda Calculus
  • 1 Strong Normalization

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail