Search Results

Documents authored by Terui, Kazushige

Document
DOI: 10.4230/LIPIcs.CSL.2018.37
MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics

Authors: Kazushige Terui

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various subsystems of second order arithmetic. Our goal is to understand it from an algebraic point of view. Among many proofs of cut elimination for higher order logics, Maehara and Okada's algebraic proofs are of particular interest, since the essence of their arguments can be algebraically described as the (Dedekind-)MacNeille completion together with Girard's reducibility candidates. Interestingly, it turns out that the Omega-rule, formulated as a rule of logical inference, finds its algebraic foundation in the MacNeille completion. In this paper, we consider a family of sequent calculi LIP = cup_{n >= -1} LIP_n for the parameter-free fragments of second order intuitionistic logic, that corresponds to the family ID_{<omega} = cup_{n <omega} ID_n of arithmetical theories of inductive definitions up to omega. In this setting, we observe a formal connection between the Omega-rule and the MacNeille completion, that leads to a way of interpreting second order quantifiers in a first order way in Heyting-valued semantics, called the Omega-interpretation. Based on this, we give a (partly) algebraic proof of cut elimination for LIP_n, in which quantification over reducibility candidates, that are genuinely second order, is replaced by the Omega-interpretation, that is essentially first order. As a consequence, our proof is locally formalizable in ID-theories.
Cite as

Kazushige Terui. MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.CSL.2018.37,
  author =	{Terui, Kazushige},
  title =	{{MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.37},
  URN =		{urn:nbn:de:0030-drops-97049},
  doi =		{10.4230/LIPIcs.CSL.2018.37},
  annote =	{Keywords: Algebraic cut elimination, Parameter-free second order logic, MacNeille completion, Omega-rule}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.5
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.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}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2013.41
Intersection Types for Normalization and Verification (Invited Talk)

Authors: Kazushige Terui

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
One of the basic principles in typed lambda calculi is that typable lambda terms are normalizable. Since the converse direction does not hold for simply typed lambda calculus, people have been studying its extensions. This gave birth to the intersection type systems, that exactly characterize various classes of lambda terms, such as strongly/weakly normalizable terms and solvable ones (see e.g. [van Bakel/TCS/1995] for a survey). More recently, a new trend has emerged: intersection types are not only useful for extending simple types but also for refining them [Salvati/JoLLI/2010]. One thus obtains finer information on simply typed terms by assigning intersection types. This in particular leads to the concept of normalization by typing, that turns out to be quite efficient in some situations [Terui/RTA/2012]. Moreover, intersection types are invariant under beta-equivalence, so that they constitute a denotational semantics in a natural way [Ehrhard/CSL/2012]. Finally, intersection types also work in an infinitary setting,where terms may represent infinite trees and types play the role of automata. This leads to a model checking framework for higher order recursion schemes via intersection types [Kobayashi/POPL/2009, Kobayashi+Luke Ong/LICS/2009]. The purpose of this talk is to outline the recent development of intersection types described above. In particular, we explain how an efficient evaluation algorithm is obtained by combining normalization by typing, beta-reduction and Krivine's abstract machine, to result in the following complexity characterization. Consider simply typed lambda terms of boolean type o -> o -> o and of order r. Then the problem of deciding whether a given term evaluates to "true" is complete for n-EXPTIME if r = 2n +2, and complete for n- EXPSPACE if r = 2n + 3 [Terui/RTA/2012].
Cite as

Kazushige Terui. Intersection Types for Normalization and Verification (Invited Talk). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 41-42, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.FSTTCS.2013.41,
  author =	{Terui, Kazushige},
  title =	{{Intersection Types for Normalization and Verification}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{41--42},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.41},
  URN =		{urn:nbn:de:0030-drops-44032},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.41},
  annote =	{Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.323
Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus

Authors: Kazushige Terui

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to "true"? A related problem is: given a term M of word type and of order r together with a finite automaton D, does D accept the word represented by the normal form of M? We prove that these problems are n-EXPTIME complete for r=2n+2, and n-EXPSPACE complete for r=2n+3. While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose. We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. The semantic evaluation can also be presented as intersection type checking.
Cite as

Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 323-338, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{terui:LIPIcs.RTA.2012.323,
  author =	{Terui, Kazushige},
  title =	{{Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{323--338},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.323},
  URN =		{urn:nbn:de:0030-drops-35012},
  doi =		{10.4230/LIPIcs.RTA.2012.323},
  annote =	{Keywords: simply typed lambda calculus, computational complexity, denotational semantics, intersection types}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact