| 作成者 |
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
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.続きを見る
|
Mendeley出力
rifis-tr-92