Infiniteness of proof(α) is polynomial-space complete

Sachio Hirokawa

    Research output: Contribution to journalArticlepeer-review

    7 Citations (Scopus)


    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
    Issue number1-2
    Publication statusPublished - Oct 6 1998

    All Science Journal Classification (ASJC) codes

    • Theoretical Computer Science
    • Computer Science(all)


    Dive into the research topics of 'Infiniteness of proof(α) is polynomial-space complete'. Together they form a unique fingerprint.

    Cite this