<テクニカルレポート>
Degree-Two Formulas and Their Proofs

作成者
本文言語
出版者
発行日
雑誌名
出版タイプ
アクセス権
概要 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.続きを見る

本文情報を非表示

rifis-tr-49 pdf 602 KB 58  

詳細

レコードID
査読有無
関連情報
タイプ
登録日 2009.04.22
更新日 2017.01.20