＜テクニカルレポート＞Balanced Formulas, Minimal Formulas and Their Proofs

作成者 著者識別子 作成者名 所属機関 所属機関名 Department of Computer Science, College of General Education, Kyushu University 九州大学教養部 英語 Research Institute of Fundamental Information Science, Kyushu University 九州大学理学部附属基礎情報学研究施設 1991-11-07 48 Accepted Manuscript open access RIFIS Technical Report || 48 || p1-12 http://www.i.kyushu-u.ac.jp/research/report.html According to the formulas-as-types notion, an implicational formula can be identified with a type of a $lambda$-term which represents a proof of the formula in implicational fragment of intuitionist...ic logic. A formula is balanced iff no type variable occurs more than twice in it. It is known that balanced formulas have unique proofs. In this paper, it is shown that closed $lamda$-terms in $\beta$-normal form having balanced types are BCK-$lamda$-terms in which each variable occurs at most once. A formula is BCK-minimal iff it is BCK-provable and it is not a non-trivial substitution instance of other BCK-provable formula. It is also shown that the set BCK-minimal formulas is identical to the set of principal type-schemes of BCK-$lamda$-terms in $\beta$-$eta$-normal form.続きを見る

本文ファイル

rifis-tr-48 pdf 652 KB 143

詳細

レコードID 3154 査読無 Proc. Intern. Conf. on Logical Foundations of Computer Science, Lecture Notes in Computer Science 620, 198-208,1992 テクニカルレポート 2009.04.22 2017.01.20