Infiniteness of proof(α) is polynomial-space complete

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

It is shown that the infiniteness problem of proof (α) is polynomial-space complete. The set proof (α) is the set of closed λ-terms in β-normal form which has α as their types. The set is identical to the set of normal form proofs of α in the natural deduction system for implicational fragment of intuitionistic logic. A transformation of a type is defined by F(α)=(((6→α)→α)→b)→b and applied as a deduction of the non-emptiness problem to the infiniteness problem. The non-emptiness is identical to the provability of α, which is polynomial-space complete (Statman, 1979). Therefore, the infiniteness problem is polynomial-space hard. To show the polynomial completeness, an algorithm is shown which searches λ-terms of given type α. It is proved that the infiniteness is determined within the depth of 2|α|3, where the size |α| is the total number of occurrences of symbols in α. Thus, the problem is solved in polynomial space. Hence, the infiniteness problem is polynomial-space complete. The bound is obtained by an estimation of the length of an irredundant chain of sequents in type-assignment system in sequent calculus formulation.

Original languageEnglish
Pages (from-to)331-339
Number of pages9
JournalTheoretical Computer Science
Volume206
Issue number1-2
DOIs
Publication statusPublished - Oct 6 1998

Fingerprint

Polynomials
Polynomial
Normal Form
Natural Deduction
Sequent Calculus
Intuitionistic Logic
Deduction
Term
Completeness
Fragment
Assignment
Closed
Formulation

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Infiniteness of proof(α) is polynomial-space complete. / Hirokawa, Sachio.

In: Theoretical Computer Science, Vol. 206, No. 1-2, 06.10.1998, p. 331-339.

Research output: Contribution to journalArticle

@article{59e01dc22b064d6da31769feb25fb3d7,
title = "Infiniteness of proof(α) is polynomial-space complete",
abstract = "It is shown that the infiniteness problem of proof (α) is polynomial-space complete. The set proof (α) is the set of closed λ-terms in β-normal form which has α as their types. The set is identical to the set of normal form proofs of α in the natural deduction system for implicational fragment of intuitionistic logic. A transformation of a type is defined by F(α)=(((6→α)→α)→b)→b and applied as a deduction of the non-emptiness problem to the infiniteness problem. The non-emptiness is identical to the provability of α, which is polynomial-space complete (Statman, 1979). Therefore, the infiniteness problem is polynomial-space hard. To show the polynomial completeness, an algorithm is shown which searches λ-terms of given type α. It is proved that the infiniteness is determined within the depth of 2|α|3, where the size |α| is the total number of occurrences of symbols in α. Thus, the problem is solved in polynomial space. Hence, the infiniteness problem is polynomial-space complete. The bound is obtained by an estimation of the length of an irredundant chain of sequents in type-assignment system in sequent calculus formulation.",
author = "Sachio Hirokawa",
year = "1998",
month = "10",
day = "6",
doi = "10.1016/S0304-3975(97)00168-0",
language = "English",
volume = "206",
pages = "331--339",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

T1 - Infiniteness of proof(α) is polynomial-space complete

AU - Hirokawa, Sachio

PY - 1998/10/6

Y1 - 1998/10/6

N2 - It is shown that the infiniteness problem of proof (α) is polynomial-space complete. The set proof (α) is the set of closed λ-terms in β-normal form which has α as their types. The set is identical to the set of normal form proofs of α in the natural deduction system for implicational fragment of intuitionistic logic. A transformation of a type is defined by F(α)=(((6→α)→α)→b)→b and applied as a deduction of the non-emptiness problem to the infiniteness problem. The non-emptiness is identical to the provability of α, which is polynomial-space complete (Statman, 1979). Therefore, the infiniteness problem is polynomial-space hard. To show the polynomial completeness, an algorithm is shown which searches λ-terms of given type α. It is proved that the infiniteness is determined within the depth of 2|α|3, where the size |α| is the total number of occurrences of symbols in α. Thus, the problem is solved in polynomial space. Hence, the infiniteness problem is polynomial-space complete. The bound is obtained by an estimation of the length of an irredundant chain of sequents in type-assignment system in sequent calculus formulation.

AB - It is shown that the infiniteness problem of proof (α) is polynomial-space complete. The set proof (α) is the set of closed λ-terms in β-normal form which has α as their types. The set is identical to the set of normal form proofs of α in the natural deduction system for implicational fragment of intuitionistic logic. A transformation of a type is defined by F(α)=(((6→α)→α)→b)→b and applied as a deduction of the non-emptiness problem to the infiniteness problem. The non-emptiness is identical to the provability of α, which is polynomial-space complete (Statman, 1979). Therefore, the infiniteness problem is polynomial-space hard. To show the polynomial completeness, an algorithm is shown which searches λ-terms of given type α. It is proved that the infiniteness is determined within the depth of 2|α|3, where the size |α| is the total number of occurrences of symbols in α. Thus, the problem is solved in polynomial space. Hence, the infiniteness problem is polynomial-space complete. The bound is obtained by an estimation of the length of an irredundant chain of sequents in type-assignment system in sequent calculus formulation.

UR - http://www.scopus.com/inward/record.url?scp=0345767008&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0345767008&partnerID=8YFLogxK

U2 - 10.1016/S0304-3975(97)00168-0

DO - 10.1016/S0304-3975(97)00168-0

M3 - Article

VL - 206

SP - 331

EP - 339

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -