曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

ジラール先生の"Proofs and Types"の1,2章を(ちょっと真剣に)読む

 私は現代最高のロジシャンはJean-Yves Girardだとガチで思っている。

 ジラール先生の論文や本は、理論的なものであっても個人の論理に対する考えが混入していることがよくあるように思う。時には本線のテクニカルな議論からやや離れたお話のようなことが書かれていることもある。そういうところはテクニカルなロジックの文脈ではあまり取り上げられないが、哲学的には面白そうなのである。そういうのも読んでみるための本記事である。

 ここで取り上げる"Proofs and Types"は、1986〜1987年にパリ第七大学で行われた講義を元にしている。まさに線形論理が誕生する前後の時代である。この時代背景には要注意。フランス語の講義録であったがテイラー&ラフォン両氏によって英訳され1989年に出版された。付録は訳者によるもので、他にも訳者による修正はあるらしい。

 近年のジラール先生の論文は哲学的な度合いを強めているように思える。"Transcendental Syntax"というシリーズなんか私には難しすぎて読めないのだが、それを読めるように、ジラール生の哲学的見解も知っておきたい。今後もシリーズ化していって先の章も読んで記事を書いていきたい所存であるが、今回のこの"P&T"1,2章は特にお話し度が強い。

Chapter 1 Sense, Denotation and Semantics

 いきなりこんなことが述べられている。

Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in the area obeys a kind of "wedding cake" paradigm: for instance language design is reminiscent of  Ptolemic astronomy - forever in need of further corrections. There are, however, some limited topics such as complexity theory and denotational semantics which are relatively free from this criticism.(p.1)

「ウェディング・ケーキ」パラダイムというのがよく分らないので誰か教えてください。しかしプトレマイオス天文学というのはよく分る喩えである。どんどん星の軌道を表す円が体系に付け加わっていった様を言っているのだろう。そして暗にコペルニクスガリレイのような革命がコンピュータ科学ではまだ起きていないということをも言っているようだ。しかし計算複雑性理論や表示的意味論は認めておられるようだ。

 続いて、フレーゲの意味(Bedeutung)と意義(Sinn)の議論が参照される。英語ではそれぞれ denotation と sense と書かれる。

 27 \times 37 = 999

という式では、= の左右は同じ denotation を持っているが、sense は違う。二つの denotation が同じであるということを示す有限の計算プロセスがある。sense が同じだったら計算する意味がない。フレーゲの議論を計算という観点から見るこうした考えがよくあるものなのかどうか私は知らない*1。しかしよくできている。

 文の denotation は真理値である。これはタルスキやブール代数でお馴染みである。ジラール先生はタルスキ意味論をつまらないものとして度々批判する。しかし denotation の概念は勿論 denotational semantics 表示的意味論という素晴しい理論も生んでいる。

 この辺りでジラール先生が多用する二元論図式が現れてくる。ロジック/コンピュータ科学には次のような二元論がある(sense は同じならば denotation も同じ、しかし逆は必ずしも成り立たない、ということから分る通りこれらは対称的でない)。

  1. sense、有限、動的、構文論、証明
  2. denotation、無限、静的、意味論、真理、代数、モデル

この本もこの二元論に立脚しているが、しかしこれらを統合する理論が求められるとジラール先生は言う。ジラール先生の線形論理以降の様々な創造もこうした意識に拠っていると思われるのである。

 sense というのは構文論的なものだというのは確かだが、しかし構文論そのものではないという。3ページ後半でやや抽象的に議論されているが、構文論のレベルでカット除去のような対称性があり、これが実は sense の対称性なのではないか、とのこと。ジラール先生は構文論の「深層の幾何学的不変量」を見つけるべきでここに sense があると述べている。対称性というのが何なのかは分らなかった。

 続いてタルスキの意味論のつまらなさが述べられた後、それと対比してハイティングの直観主義論理の解釈の優秀性が述べられる。タルスキの意味論が denotation に基くものだったのに対し、ハイティングのそれは証明に基いている。ハイティングの解釈として述べられているものは直観主義型理論を読んだ際に出てきたものと同じっぽい。存在命題の証明をペアとするのはハイティングの頃からそうだったのだろうか? 私は知らないし気になる。

 ハイティング解釈の技術的な問題もいろいろと指摘されている。これはゲーデルの指摘をなぞっているのかも。

Chapter 2 自然演繹

 自然演繹が初めから計算的内実を意識して導入される。ジラール先生は対称性を持ったシーケント計算の方を自然演繹よりも高く評価しているようだが、計算的内実が分りやすいという理由で自然演繹が先に導入される。

 自然演繹についてこう書いているのは興味深い。

 Natural deduction is a slightly paradoxical system: it is limited to the intuitionistic case (in the classical case it has no particularly good properties) but it is only satisfactory for the (\land, \Rightarrow, \forall) fragment of the language: we shall defer consideration of \lor and \exists until chapter 10. Yet disjunction and existence are the two most typically intuitionistic connectors!(p.8)

自然演繹の様々な良い性質が直観主義論理にあって古典論理にはないのは確かだが、"limited to the intuitionistic case"とまで言ってのけるのはおもしろい。正規化定理を何よりも重視しているからだろう。またカリー=ハワード対応を考えると結合子を連言と含意と全称量化に限るというのは頷けるが、しかし選言特性や存在特性といった証明論的性質も大事であるということが述べられているっぽい。

 またシーケント計算と違って対称性がないと述べたが、導入則と除去則の対称性はあるとのこと。

 その後は自然演繹の \land, \Rightarrow, \forall 断片が導入され、ラムダ計算やペア-射影関数との対応が述べられている。

感想

 ルディクスについてもちょっと調べていたのだが、

cut-elimination.hatenablog.com

ジラール先生の「証明をベースにロジックや計算を組み立てる」という方針はずっと一貫していることがわかる。二元論(構文論と意味論)の克服というのもルディクスのテーマだが、それも証明の考察の徹底によってもたらされると考えているのだろう。

 また有限性やダイナミクスの強調は線形論理からGoIへの発展を予感させる。というかこの頃からすでに構想はあったのだろうか。

*1:アウディ先生がホモトピー型理論の講義でそんなようなことを述べているような。