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