2019年12月1日 （日） 13:00 - 18:00

首都大学東京 南大沢キャンパス 5号館 131教室

13:00 - 14:30 福田陽介 （京都大学）「様相λ計算に対する相互作用の幾何に基づくプログラム意味論」

本研究は，直観主義様相論理およびそれにCurry-Howard対応する様相λ計算に対して相互作用の幾何に基づく意味論を与えることを目的とし，[Pfenning&Davies 01]（および[Davies&Pfenning 01]）による直観主義様相論理S4と様相λ計算の形式化を線型論理の枠組みへ拡張することでこれを達成する．

相互作用の幾何（Geometry of Interaction, GoI）[Girard 89]は，元々，線型論理の証明論におけるCut除去の手続きを解析するためにGirardが考案した意味論である．その最たる特徴は表示的(denotational)かつ操作的(operational)な性質を兼ね備える点にあり，しばしば「syntax-freeな表示的意味論でありながら，計算の動的過程(dynamics)の本質をも捉える」と表現される(cf. [Abramsky&Jagadeesan 92])．また，GoI意味論は論理の文脈のみならずλ計算やプログラミング言語の文脈においても研究されており(cf. [Mackie 94, 95][Danos&Reginier 96][Ghica 07][Schöpp 14]等，他多数])，例えば，いわゆるトークン・パッシング流のGoI意味論の下ではλ項（プログラム）の計算がある種のグラフ・ネットワーク上のトークンの情報流(information flow)として定式化される．

本発表は二部構成で話を進める．前半は[Mackie 94, 95]に基づき，直観主義線型論理のシーケント計算，証明網(Proof-net)，トークン・パッシング流のGoI意味論を説明し，このGoI意味論がCurry-Howard対応を通じて線型λ計算の計算的解釈を与えることを概観する．後半では，上述の結果を直観主義様相論理に拡張し，様相λ計算に対するGoI意味論を与える．具体的には，Pfenningらによる直観主義S4の論理体系・計算体系を様相線型論理(modal linear logic)の枠組みへと拡張し，(1)「様相論理から様相線型論理へのGirard変換」; (2)「様相線型論理に対するGoI意味論」を与えることで目的を達成する．なお，本発表は由水輝氏との共同研究[F.&Yoshimizu 19]に基づく．

--------------------------------------

14:45 - 16:15 山形頼之 （産業技術総合研究所） 「等式系の無矛盾性証明と限定算術の分離問題」

Bussが定義した限定算術の階層S12⊆S22⊆S32⊆...の分離問題（⊆が=であるか⊂であるか）は、その計算量理論への含意から限定算術の研究におけるもっとも重要な問題の一つである。理論間の分離の手法としてよく用いられるのが、無矛盾性証明を分離したい体系内で行い、ゲーデルの第2不完全性定理に訴える方法である。しかし、限定算術はその証明能力の弱さのため、ほとんどの体系の無矛盾性を示すことができない。この状況のもとで、限定算術の分離問題に有効な無矛盾性証明の対象の候補として、各種等式系があげられる。本講演ではBuss Ignjatovic 1995, Takeuti 1991, Beckmann 2002, Yamagata 2018などを取り上げ、この分野の研究を紹介する。

--------------------------------------

16:30 - 18:00 松田直祐 （神奈川大学） 「公理型のオーダーと論理の関係」

中間論理とは，直観主義論理に古典論理で導出可能な論理式を公理として加えて得られる論理の総称である．論理式の間に，

A<=B <-> Aの中のいくつかの変数に論理式を代入することでBが得られる

と前順序を入れると，A<=Bならば，直観主義論理にAを加えて得られる論理は直観主義論理にBを加えて得られる論理より強くなる．つまり，<=の意味で小さい論理式は，公理としては強いものになるということである．このような観察から，以下のような問が考えられる：

Aが古典論理で（<=の意味で）極小な論理式ならば，

直観主義論理にAを加えて得られる論理は常に古典論理になるか？

この問題は，古森雄一氏により与えられたもので（講演者は勝手に「古森-鹿島の問題」と呼んでいる），長年の未解決問題であったが，中村誠希氏により否定的な解決が与えられた．しかしながら，中村氏の解答は古森-鹿島の問題の本来の意義をとらえるような解答とは言い難いものである．

本講演では，古森-鹿島の問題の意義を検討し，論理式のオーダーという概念を利用した問題の再定式化を紹介する．また，論理式のオーダーと論理の関係についてのいくつかの未解決問題を紹介する．

京王線相模原線「南大沢」駅改札口から徒歩約10分

五十嵐涼介

Email: igarashi[dot]r0922[at]gmail[dot]com