| 作成者 |
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
An implicational formula is said to be of degree two when it has tlze form $ alpha = left(a \frac{1}{1} \to...\to a \frac{1}{n_1} \to a^1 \right) \to ... \to left(a ^m_1 \to ... \to a^m_n_m \to a^m \r...ight) \to a $ with type variables $ a \frac{1}{1}, . . ., a \frac{1}{n_1},a~1,...,a^m_1,...,a^1_n_m,a^m and a left(n_1,...,n_m leq 0 \right) $ .Given a degree two formula $ alpha $, we construct, in polynormial time of the size of $ alpha $, a context free grammar $ G left(alpha \right) $ such that $ proof (alpha)= left{ N | N leftarrow lambda _x_1...x_m.M for some M in L (G(alpha)light} $ where proof $ (alpha)$ is the set of normal form proof of $ alpha $ in NJ (natural deduction system of intuitionistic logic) and $ L(G(alpha)) $ is the set of context free language generated by $ G(alpha) $. The set of provable formulas of degree two is characterized as the set of simple substitution instances of principal type-schemes of 'sorted' terms. $ A lambda -term lamda-term /lamda _x_1...x_m.M $ is sorted when M has no $ lamda $'s and is constructed from function symbols $ x_1, ... , x_m, $ of arity $ n_1,...n_m in $, in the sense of many sorted algebra.続きを見る
|
Mendeley出力
rifis-tr-49