| Creator |
|
| Language |
|
| Publisher |
|
|
|
| Date |
|
| Source Title |
|
| Vol |
|
| Publication Type |
|
| Access Rights |
|
| Related DOI |
|
|
|
| Related URI |
|
|
|
| Relation |
|
|
|
| Abstract |
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.show more
|
Export Mendeley
rifis-tr-92