双側

古典の計算的解釈

福田 陽介 UuQbmF2 6mFm/V
京都大学大学院情報学研究科
証明論的意味論 US`QQ7@h?2Q`2iB+ a2KMiB+b- Sha- +7X (Ry)V は，文の意味をその文がどのように証明されるかを定めることによって与える，証明論に基づく意味論でありR ，モデル論的（表示的）な意味にěĜ少なくとも明示的にはěĜ依拠することなく言語の意味を説明する理論である．最も有名な .mKK2iiĜS`rBix 流の Sha (k- d) は「文の意味にプリミティブに寄与するのは主張行為のみ」という単側面説 UlMBHi2`HBbKVに基づいており，.mKK2ii はこの枠組みの下で直観主義論理は正当化できるが古典論理は正当化できないとして古典論理に対する批判に利用した (k)．
一方で，主張のみならず否認も文の意味に寄与するという考え方を双側面説 U"BHi@2`HBbK- +7X (R9)V と呼び，_mK}ii (3- N) はこの考えに基づき双側面古典論理 U"BHi2`H*HbbB+H GQ;B+- "*GV を提案した．"*G は通常の古典自然演 の（主張の）論理規則に加え，否認の論理規則，主張と否認の協調原理 U*Q@Q`/BMiBQM S`BM+BTH2bV により定義され，_mK}ii はこの "*G の議論により古典論理の正当化を与えた (3)．
しかし 62``2B` (j) や鈴木 (R8) が指摘するように _mK}ii の古典論理の正当化は協調原理に関する議論が不十分であり，Sha の観点からは正当化が達成できていない．
この問題に対して鈴木 (R8) は反証主義的双側面説を提案し，Sha の枠組みを拡張することで解決を与えたが，本研究では異なる観点から協調原理の問題に取り組む．
本発表では _mK}ii が提案した "*G に対して *m``vĜ>Qr`/ 対応 U+7X (Rj)V を通じた計算的解釈を与える．具体的には "*G の自然演 に対応する双側面型付き 計算を定め，その計算的構造が "*G の推論構造を捉えることを述べる．提案体系の最も特徴的な点は，以下の表 R に示す通り「主張と否認」の概念が計算機科学でよく知られた「式と継続」 (9) という概念に一致し，また，協調規則がそれらの間の型付け規則として表される点にある．加えて，通常の *m``vĜ>Qr`/ 対応の場合と同様に "*G の証明図は双側面 計算の項に一致するが，協調規則が関係する証明の正規化は式と継続との間の相互作用による計算として定式化できることを見る．
表 R, 双側面説に基づく形式体系の *m``vĜ>Qr`/ 対応
双側 古典
U"*GV
双側 型付き 計算
主張 +A否認 A
論理規則
協調規則

式の型 +A
継続の型 A式の型付け規則  継続の型付け規則
式と継続との間の型付け規則さらに本研究で提案する双側面 計算は全く異なる文脈で考案された GQpb らによる計算体系 (e) と本質的に同等であり，そのメタ数学的性質が q/H2` の双対計算
U.mH *H+mHmbV (Rk- R) への埋め込みを通じて示せることを述べる．こうして得られた結果から，提案体系が "*G の推論構造ěĜ特に協調原理ěĜに対して計算の観点から自然な解釈を与えることを議論する．また時間が許せば 6BHBMbFB の対称 計算 (9)の浅井らによる定式化 (Re- RR)，および，近年の関連研究との位置付けを概説する．
本発表は鈴木佑京 氏との共同研究に基づく．
R

その萌芽は :2Mix2M の博士論文 (8) にすでに現れ，彼は「論理結合子の意味は，当該結合子の導入規則によって定まり，除去規則はその定義からの帰結に過ぎない」という趣旨の記述を残している．

R

参考 献(R) .MB2H .Qm;?2`iv- aBHpB :?BH2xM- SB2``2 G2b+MM2- M/ aBHpB GBFp2+Xai`QM; LQ`KHBxiBQM Q7 i?2 .mH *HbbB+H a2[m2Mi *H+mHmbX AM S`Q+22/BM;b
Q7 AMi2`MiBQMH *QM72`2M+2 QM GQ;B+ 7Q` S`Q;`KKBM;- `iB}+BH AMi2HHB;2M+2M/ _2bQMBM; UGS_V- T;2b ReNĜR3j- kyy8X(k) JB+?2H .mKK2iiX h?2 GQ;B+H "bBb Q7 J2iT?vbB+bX >`p`/ lMBp2`bBiv
S`2bb- RNNRX(j) 62`MM/Q 62``2B`X h?2 *Q@Q`/BMiBQM S`BM+BTH2b,  S`Q#H2K 7Q` "BHi2`HBbKX
JBM/- RRdU9e3V,Ry8RĜRy8d- kyy3X(9) M/`x2D 6BHBMbFBX .2+H`iBp2 *QMiBMmiBQMb M/ *i2;Q`B+H .mHBivX Jbi2`Ƕb
i?2bBb- lMBp2`bBiv Q7 *QT2M?;2M- RN3NX(8) :2`?`/ :2Mix2MX lMi2`bm+?mM;2M Ƀ#2` /b HQ;Bb+?2 a+?HB2Ľ2MX AX Ji?2K@iBb+?2 w2Bib+?`B7i- jNURV,RdeĜkRy- RNj8X(e) qBHHBK GQpb M/ E`H *``vX ai`m+im`H LQ`KHBxiBQM 7Q` *HbbB+H Lim`H.2/m+iBQMX kyyeX JMmb+`BTiX(d) .; S`rBixX S`;KiBbi M/ o2`B}+iBQMBbi h?2Q`B2b Q7 J2MBM;X AM _M@
/HH 1X mtB2` M/ G2rBb 1/rBM >?M- 2/BiQ`b- h?2 S?BHQbQT?v Q7 JB+?2H.mKK2ii- T;2b 988Ĝ93RX PT2M *Qm`i- kyydX(3) AM _mK}iiX ǳu2bǴ M/ ǳLQǴX JBM/- RyNU9jeV,d3RĜ3kj- kyyyX(N) AM _mK}iiX *Q@Q`/BMiBQM T`BM+BTH2b,  `2THvX JBM/- RRdU9e3V,Ry8NĜRyejkyy3X(Ry) S2i2` a+?`Q2/2`@>2Bbi2`X S`QQ7@h?2Q`2iB+ a2KMiB+bX AM 1/r`/ LX wHi2/BiQ`- h?2 aiM7Q`/ 1M+v+HQT2/B Q7 S?BHQbQT?vX J2iT?vbB+b _2b2`+? G#aiM7Q`/ lMBp2`bBiv- bT`BM; kyR3 2/BiBQM- kyR3X(RR) uvQB l2/ M/ E2MB+?B bBX _2BMp2biB;iBQM Q7 avKK2i`B+ GK#/ *H+m@HmbX AM S`Q+22/BM;b Q7 i?2 9i? .AEl@Aah CQBMi qQ`Fb?QT QM 6QmM/iBQMb Q7
aQ7ir`2- kyRRX h2+?MB+H _2TQ`i kyRRfR- .AEl- lMBp2`bBiv Q7 *QT2M?;2MTTX RyĜkeX(Rk) S?BHBT q/H2`X *HH@#v@pHm2 Bb /mH iQ +HH@#v@MK2X AM S`Q+22/BM;b Q7 AMi2`@
MiBQMH *QM72`2M+2 QM 6mM+iBQMH S`Q;`KKBM; UA*6SV- kyyjX(Rj) S?BHBT q/H2`X S`QTQbBiBQMb b hvT2bX83URkV,d8Ĝ39- kyR8X(R9) 大西琢朗X 証的意*QKKmMB+iBQMb Q7 i?2 *J-と双側 説X S?. i?2bBb- 京都大学- kyRkX(R8) 鈴木佑京X 反証主義と双側面説X Jbi2`Ƕb i?2bBb- 東京大学- kyReX(Re) 阪上紗里 M/ 浅井健一X 対称keUkV,jĜRd- kyyNX計算の基礎理論X コンピュータソフトウェア-k