Infiniteness of proof $ left( alpha \\right) is polynomial-space complete
Sachio Hirokawa, 佐千男 廣川 · QIR (Kyushu University Institutional Repository) (Kyushu University) · 1994
The infiniteness problem is investigated for the set proof $ left (alpha \\right) $ of closed $ lamda -terms in \\beta-normal $ form which has a as their types. The set is identical to the set of normal form proofs for $ alpha $ in the natural deduction system for implicational fragment of intuitionistic logic. It is shown that the infiniteness is determined by checking Aterms with the depth at most $ 2 mid alpha mid^2 $. Thus the problem is solved in polynomial-space. The bound is obtained by an estimation of the length of an irredundant chain of sequents in type assignment system in sequent calculus formulation. Then the non-emptiness problem of $ proof left( alpha\\right) $, which is identical to the provability of $ alpha $, is deduced to the problem of infiniteness problem by a transformation of types. Since the provability is polynomial- space complete (Statman, Theoret. Comput. Sci. 9 (1979) 97-105), the infiniteness problem is polynomial-space complete.