↓これの続きでこざる。
cut-elimination.hatenablog.com
シーケント計算
シーケント計算は自然演繹ほど計算との対応が明確ではないとのことだった。しかしPROLOGの基礎になっていたり自動定理証明に使われるタブローの一般化でもあるという。これは知らなんだ。私はPROLOGの仕組みを知らないので調べねばね。タブローがシーケント計算の一部だというのは分りそうで分らない。。。
続いてシーケント計算が定義される。構造規則が思いの外重要であるとある。確かに構造規則が重要だからこそ構造規則を制限した線形論理が生れた訳だ。
前回までであまりピンときていなかった対称性が分ってきた。シーケント計算は左と右で対称性がある。ここでいう対称性とはカットが除去できるということで、論理が満すべき条件である。
今回はちゃんと図を描いたぞ！
Γ,A|-Δ Γ,B|-Δ --------(∧左1) --------(∧左2)---(1) Γ,A∧B|-Δ Γ,A∧B|-Δ Γ|-A,Δ Γ'|-B,Δ' ---------------(∧右)---(2) Γ,Γ'|-A∧B,Δ,Δ' Γ|-A,Δ --------(∧右1?)---(3) Γ|-A∧B,Δ A|-A B|-B ------(∧右1?) ------(∧左2) A|-A∧B A∧B|-B ---(4) ---------------------Cut A|-B
∧の規則は(1)と(2)のように定義される。線形論理の知識を先取りすると、左規則は加法的連言の規則で右規則は乗法的連言の規則になっている。これはありなのかなと思ったが、弱化を使えばカットが除去できるので別に良いのだろう。
対称性について自分なりに考えてみた。∧右規則が(3)のようだったら、場合によってはカットが除去できない。これは(4)を見ればわかる。よって(1)と(3)で定義される結合子は対称性を持たない。証明論的意味論ではトンクというダメな結合子の例がよく出てくる。これはそこから着想を得た。トンクは正規化定理を満さない。後で述べられている通り、正規な証明はカットの無い証明と対応する。ジラール先生が言っている対称性は証明論的意味論の結合子の正当化と近いんじゃないかと思う。しかしジラール先生は証明論的意味論に言及しているイメージがないのであまり評価していなさそう。
しかしこの後で非対称な解釈というのが出てきていて、これはよく分らなかった。"Basic Proof Theory"にこんな話が出てきた気がするがサボっているので分らない。
自然演繹との対応も述べられているのだが、ちょっと抽象的で分りにくかったなあ。もうちょっと考えてみたい。シーケント計算から自然演繹への翻訳は一意だが逆はそうではないとのこと。
強正規化定理
強正規化定理の詳しい証明。帰着可能性の概念を用いて証明しており、それを詳細に解説してあるのがありがたい。全ての項は帰着可能であり、帰着可能性は強正規化可能性を含意している、という証明である。これは後で述べるシステムFの強正規化定理の証明にも応用できるので詳しく述べているらしい。
型無ラムダ計算と違って型の構造帰納法が使えるから型付ラムダ計算は強正規化可能なのだということがよく分った気がする。
CR1〜4の条件と6.3.1と6.3.2からどのように帰着可能性定理が導かれているのかちゃんと説明されていない気がしてならない。私の考えでは項の複雑さとnステップの変換で帰着可能というnとの二重帰納法が使われているのではないかと思う。どうでしょう。
まとめ
けっこう難しくて先行き不安である。
