檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2018-12-12 (水)

順序集合のカン拡張と特徴述語論理

| 19:10 | 順序集合のカン拡張と特徴述語論理を含むブックマーク

圏論における随伴系やモナドの概念を、順序集合に関して考えるとガロア接続や閉包作用素になります。同様に、圏論におけるカン拡張を順序集合に関して考えることができます。が、それだけだと実感に乏しく面白くもありません。カン拡張(右カン拡張と左カン拡張)を、述語論理の限量子と捉えてみます。

内容:

  1. 圏と順序集合
  2. 基本的な言葉と記法
  3. 劣拡張と最大劣拡張
  4. ミート完備な順序集合
  5. 最大劣拡張の構成
  6. 最小優拡張と書き方の約束
  7. 特徴述語論理
  8. おわりに

圏と順序集合

圏論に関する話を、順序集合に関する話にダウングレードすると、議論が容易になります。例えば、2つの関手が随伴対であることは、2つの単調写像がガロア接続を形成することと同じです。それについては:

モナドの順序的対応物に関しては:

「圏 → 順序集合」というダウングレードは簡単です。なぜなら、順序集合は特殊な圏とみなせるからです。Cがやせた圏〈thin category〉とは、次が成立することです。

  • A, B∈|C| に対して、ホムセット C(A, B) が空集合か単元集合のどちらか。

やせた圏は、プレ順序集合〈preordered set〉と同じです。さらに、やせた圏Cが次の性質を持てばとてもやせた圏〈very thin category〉です。

  • C(A, B) ≠ ¥emptyset かつ C(B, A) ≠ ¥emptyset ならば、A = B

とてもやせた圏は順序集合になります。より詳しくは次を参照:

何か圏論の一般的な概念があったとき、やせた圏/とてもやせた圏に制限すれば、それだけでプレ順序集合/順序集合に関する概念が出てきます。

基本的な言葉と記法

カン拡張に関しては、ここでは触れません。次の記事を参照してください。

圏の一般論と順序の理論の対応関係もいちいちは指摘しませんが、主要な用語の対応は次の表のとおりです。

圏の一般論 順序の理論
右拡張 劣拡張
右カン拡張 最大劣拡張
左拡張 優拡張
左カン拡張 最小優拡張

カン拡張における上下左右: 入門の前に整理すべきこと」で使った記号と、この記事内の記号との対応は:

圏の一般論 順序の理論
C, D, E 順序集合 A, B, C
関手 K:CD 単調写像 k:A→B
関手 F:CE 単調写像 f:A→C
関手 G, H:DE 単調写像 g, h:B→C
自然変換 α::F⇒G:CD 不等式 f ≦ g on A in B
右カン拡張 KF 最大劣拡張 kf
左カン拡張 KF 最小優拡張 kf

ここから先、A, B, C などは順序集合を表し、その順序は一律に'≦'で表します。f, g, h などは単調写像〈{monotone | monotonic} {map | mapping | function}〉を表します。順序集合AからBへの単調写像の全体を BA または [A, B] と書きます。AとBが順序集合のとき、次の文はすべて同じ意味です。

  • f:A→B は単調写像
  • f∈BA
  • f∈[A, B]

f, g∈[A, B] に対して、f ≦ g は次のように定義します。

  • f ≦ g :⇔ ∀a∈A.( f(a) ≦ g(a) )

a, b∈A に対して、a ≦ b であることを次のようにも書きます。

  • a ≦ b in A

f ≦ g in [A, B] のことを次のようにも書きます。

  • f ≦ g on A in B

圏のホムセットと同じ記法を順序集合に対しても使います。A(a, b) は次のような集合です。

  • A(a, b) := if a ≦ b then {(a, b)} else ¥emptyset

この定義より、

  • A(a, b) は、空集合か単元集合のどちらか。
  • A(a, b) ≠ ¥emptyset ⇔ a ≦ b

劣拡張と最大劣拡張

k:A→B と, f:A→C を2つの単調写像とします。g:B→C が、kに沿ったfの劣拡張〈lower extension of f along k〉だとは、次の不等式が成立することです。

  • 任意の a∈A に対して、g(k(a)) ≦ f(a)

A⊆B で、kが包含写像(埋め込み写像)の場合を考えると:

  • fは、Bの部分集合Aでしか定義されてない。
  • gは、B全体で定義されている。この意味で拡張
  • A上では、g ≦ f が成立しているので、gは順序的に〈下方 | lower〉である。

実際にはkは何でもいいのですが、上記の特殊な状況を考えると、劣拡張という呼び名が納得できるでしょう。ただし、kが包含写像でない場合は、「拡張」という呼び名は、国語辞書的にはまったく不適切になります。「概念が一般化されると呼び名が不適切になる」ことはよくあることなので、諦めましょう*1

(kに沿った)fの劣拡張の全体を LowExt(k, f) とすると、

  • LowExt(k, f)⊆[B, C]
  • [B, C] の順序をそのまま受け継いで LowExt(k, f) も順序集合。

順序集合 LowExt(k, f) に最大元が在ることは保証されませんが、もし最大元があれば、それを、fの最大劣拡張〈greatest lower extension〉と呼びます。gが、(kに沿った)fの最大劣拡張であるとは次のことです。

  1. g:B→C は、kに沿ったfの劣拡張である。
  2. h:B→C がkに沿ったfの劣拡張であるならば、h ≦ g on B in C 。

最大劣拡張が存在するなら一意です。g, g':B→C が、kに沿ったfの最大劣拡張とします。gが最大劣拡張でg'が劣拡張であることから g' ≦ g 、同様に g ≦ g' 、これらより g = g' です。

Cがタチの良い順序集合のとき、k:A→B と f:A→C を元にして最大劣拡張を構成することができます。Cに要求される性質(タチの良さ)と、最大劣拡張の具体的構成を次節以降で述べます。

ミート完備な順序集合

Aが順序集合で、X⊆A とします。このとき、次のような要素 a∈A が存在すれば、それをXのミート〈meet〉と呼びます

  1. ∀x∈X.( a ≦ x )
  2. b∈A が ∀x∈X.( a ≦ x ) を満たすならば、b ≦ a

一番目を満たすaは、Xの下界〈かかい | lower bound〉といいます。二番目の条件から、aは下界のなかで最大なものなので、ミートを最大下界〈greatest lower bound〉とか下限〈infimum〉とも呼びます。

AとXの選び方により、AにおけるXのミートは存在したりしなかったりですが、存在するなら一意に存在します(練習問題)。そのミートを、次のように書きます(どの書き方でもよい)。

  • A(X)
  • infA(X)
  • glbA(X)

ここでは、∧A(X) という書き方を使い、Aが分かっているときは単に ∧(X) とも書きます。Iがインデックス集合で、α:I→A が写像のとき、∧(αの像) を色々な書き方で表します。

¥bigwedge_{i ¥in I} ¥alpha_i

¥bigwedge (i ¥in I |¥: ¥alpha_i)

¥bigwedge (¥alpha_i |¥: i ¥in I)

¥bigwedge ¥{¥alpha_i |¥: i ¥in I¥}

書き方の相違はホントにどうでもいいことなので、主に ∧(i∈I | α(i)) を使います('∧'をデカくもしない)。

順序集合Aが、任意の X⊆ A に対してミートを持つとき、ミート完備〈meet complete〉と呼びます。Aがミート完備なら、Pow(A)をAのベキ集合として、写像

  • ∧:Pow(A)→A

がチャンと定義されている〈well-defined〉ことになります。

Aがミート完備なら、任意の写像(インデックス族) α:I→A に関して、∧(i∈I | α(i)) は ∧(αの像) と同じなのでやはりチャンと定義されています。

最大劣拡張の構成

k:A→B, f:A→C という単調写像がある状況で、kに沿ったfの最大劣拡張を構成しましょう。ただし、Cはミート完備であるという条件を付けます。

上記のような k, f が与えられているとして、g:B→C を次のように定義します。

  • b∈B に対して、g(b) := ∧(x∈k-1(b)| f(x))

ここで、k-1(b) は、k:A→B の逆像集合です(記法k-1逆写像を意味しないので注意)。k-1(b)はAの部分集合で、fをk-1(b)に制限した写像(インデックス族) k-1(b)→C に対するミートは、Cのミート完備性から一意に存在します。したがって、b|→g(b) はチャンと定義された写像です。

今定義した g:B→C が、kに沿ったfの最大劣拡張であることを示すには、次の2つのことを示すことになります。

  1. gは、kに沿ったfの劣拡張である。
  2. hがkに沿ったfの劣拡張ならば、h ≦ g 。

一番目を示しましょう。a∈A に対して、

  • g(k(a)) ≦ f(a)

が言えればOKです。gの定義から、x∈k-1(b) ⇒ g(b) ≦ f(x) ですが、b = k(a) と置けば、a∈k-1(b) なので、g(k(a)) = g(b) ≦ f(a) が成立します。これで一番目は示せました。

次にニ番目を示しましょう。b∈B に対して、

  • h(b) ≦ g(b)

が言えればOKです。gの定義 g(b) := ∧(x∈k-1(b)| f(x)) から、c∈C がなんであっても、

  • [ア] 任意の x∈k-1(b) に対して c ≦ f(x) ならば、c ≦ g(b)

b = k(a) となるaが存在するときを考えます。hがfの劣拡張であることから、

  • [イ] h(b) = h(k(a)) ≦ f(a)

上記の[ア]に、x←a, c←h(k(a)) と代入すれば、次が出ます。

  • [ウ] a∈k-1(b) だから、h(k(a)) ≦ f(a) ならば、h(k(a)) ≦ g(b)

[イ]より実際に h(k(a)) ≦ f(a) なので、[ウ]を考慮すれば、

  • h(b) = h(k(a)) ≦ g(b) in C

が成立します。

b = k(a) となるaが存在しないときは、g(b) = ∧(x∈¥emptyset| f(x)) = ∧(¥emptyset) = (Cの最大元) 。

  • h(b) ≦ (Cの最大元) in C

はbがなんでも成立するので、この場合も h(b) ≦ g(b) は言えます。

以上から、bがなんであっても h(b) ≦ g(b) となり、gは劣拡張のなかで最大であることが分かりました。

最小優拡張と書き方の約束

今までの議論の不等号の向きを逆にすると、最小優拡張を定義できます。Cに関する条件としてはジョイン完備性を考えます。ほとんど繰り返しですが、ジョイン完備性の定義は書いておきましょう。

X⊆A に対して、次のような要素 a∈A が存在すれば、それをXのジョイン〈join〉と呼びます

  1. ∀x∈X.( x ≦ a )
  2. b∈A が ∀x∈X.( x ≦ b ) を満たすならば、a ≦ b

一番目を満たすaは、Xの上界〈じょうかい | upper bound〉といいます。二番目の条件から、aは上界のなかで最小なものなので、ジョインを最小上界〈least upper bound〉とか上限〈supremum〉とも呼びます。Xのジョインが存在するなら一意的です。

順序集合Aが、任意の X⊆ A に対してジョインを持つとき、ジョイン完備〈join complete〉と呼びます。Aがジョイン完備なら、Pow(A)をAのベキ集合として、写像

  • ∨:Pow(A)→A

がチャンと定義されます。

k:A→B, f:A→C の状況で:

  • g:A→C が、kに沿ったfの優拡張〈upper extension of f along k〉だとは、任意の a∈A に対して、f(a) ≦ g(k(a)) が成立すること。
  • g:A→C が、(kに沿った)fの最小優拡張であるとは:
    1. g:B→C は、kに沿ったfの優拡張である。
    2. h:B→C がkに沿ったfの優拡張であるならば、g ≦ h on B in C 。

Cがジョイン完備なとき、gを次のように定義すると、gは、kに沿ったfの最小優拡張になります。

  • g(b) := ∨(x∈k-1(b) | f(x))

kに沿ったfの最大劣拡張と、kに沿ったfの最小優拡張を(それがあれば)次の書き方で表すことにします。

  • (kに沿ったfの最大劣拡張) = kf
  • (kに沿ったfの最小優拡張) = kf

kf は、右カン拡張 KF の順序集合バージョン、kf は、左カン拡張 KF の順序集合バージョンです。

特徴述語論理

k:A→B, f:A→C で、Cがミート完備かつジョイン完備である状況で考えます。順序集合 A, B, C を次のように解釈します。

  • Aは、個体の領域〈domain of individuals〉と考える。個体の領域を、述語論理では議論の領域〈domain of discourse〉と呼ぶこともある。
  • Bは、Aに属する個体を特徴づける値・量の領域と考える。
  • Cは、論理的真偽値の領域と考える。ただし、二値真偽値とは限らない。

Cが真偽値の領域なので、写像 f:A→C は、個体に真偽値を対応させる述語ということになります。Cがミート完備・ジョイン完備であることから、述語に対する ∧, ∨ や、論理定数 T, ⊥ を定義することができます。無限も許す∧演算として全称限量子∀、無限も許す∨演算として存在限量子∃も導入できます。

通常の述語論理でお目にかからないのは、領域Bと写像 k:A→B です。kはBの値によってAの個体を特徴付ける写像と考えます。分かりやすい例は、Bの要素が属性値であるときです。例えば、Aが人の集合で、B = N とします。k:A→B は、人に年齢を対応付ける写像とします。年齢は人を特徴付ける値のひとつです。

年齢とはまったく異なった例として、A⊆B であり、k:A→B は包含写像のときを考えます。この場合、kはAの各個体をより広い“場”であるB内に埋め込んでいます。別な場に置くことも特徴付けと(ちょっと無理矢理に)考えれば、kは特徴付けの写像と言ってもいいでしょう。以下では、k:A→B を特徴付け写像〈characterizer〉と呼びましょう。

個体領域Aと特徴付けのための領域Bも順序集合ですが、離散順序も順序なので、単なる集合 A, B と単なる写像 k:A→B であっても順序集合と単調写像だとみなせます。

これで、順序集合/単調写像に関する構造を述語論理として捉える状況設定が出来たので、kに沿ったfの最大劣拡張 kf 、kに沿ったfの最小優拡張 kf を限量子付き命題として解釈しましょう。次の記法を導入します。

  • (kf)(b) = (∀x∈A, k(x) = b.f(x))
  • (kf)(b) = (∃x∈A, k(x) = b.f(x))

これらの命題(述語)は、B上の命題(述語)になり、そのインフォーマルな内容的解釈は、

  • k(x) = b であるすべてのxに対して f(x) である。
  • k(x) = b であるxで、f(x) であるxが存在する。

B = 1 = {0} として、k:A→B を自明な写像とするとき、∀x∈A, k(x) = 0.f(x) と ∃x∈A, k(x) = 0.f(x) は、特徴付けなしの ∀x∈A.f(x) と ∃x∈A.f(x) に同じになります。一方で、特徴付けを含む論理式の意味は、次の(通常の)論理式と同じです。

  • ∀x∈A.(k(x) = b ⊃ f(x))
  • ∃x∈A.(k(x) = b ∧ f(x))

おわりに

特徴述語論理に関しては、限量子を定義しただけですが、これがカン拡張(の一側面)の論理的対応物なのではないかと思います。述語論理は、ハイパードクトリン(短い記述はココ)などにより定式化できます。特徴述語論理を完全に定式化すると、いったいどんな構造になるのでしょう。

カリー/ハワード/ランベックの教義によれば、「圏論、論理、型理論/プログラム論」のあいだには対応関係(類似性)があるはずです。特徴述語論理をあいだにはさむことによって、カン拡張に対応する型理論/プログラム論的概念が見つかるかも知れません。限量子が関係するなら、依存型っぽいナニカかも知れません(よく知らんけど)。

*1:最近、僕がよくこのテの注意書きをするのは、国語辞書的な解釈に拘る人が、どうも相当数いるらしいと気付いたからです。「拡張してないのに、なんで『拡張』なんだ?」とか気にするのはまったく不毛です。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181212

2018-12-10 (月)

野菜そば

| 12:09 | 野菜そばを含むブックマーク

次のメニューの英訳部分がどうも解せなかったのですが、

googleで出すことに成功。「そば」はちゃんと訳すので「傍」にしました。

「椎茸うま煮そば」は出せませんでした。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181210

2018-11-08 (木)

偉大なり、米田

| 13:20 | 偉大なり、米田を含むブックマーク

米田の補題は(名前は「補題」ですが)、圏論の中心的な概念です。その重要さはジョークのネタにされるほどです。

米田の補題の米田信夫さん(肖像のお写真はコチラ)は、エンド/コエンド〈end/coend〉とグロタンディーク構成〈Grothendieck construction〉の創始者でもあるんですよね。

エンド/コエンドに関しては、ロアギアン論文から引用します。強調(太字+下線)は檜山。

The original definition of a co/end for a functor T : Cop×CD, as a universal object ∫T(c, c) ∈ D satisfying a certain property was apparently given by N. Yoneda (who used an integral sign –see §1.2– to denote them for the first time, even if his notation for coends was reversed: today, ∫cT is an end for T, and ∫cT a coend, whereas Yoneda writes ∫cT for the coend, and ∫*cT for the end), and then refined by Mac Lane in his [ML70] with applications to the "tensor product" of two functors, that generalizes the well-known description of M¥otimesRN as a coequalizer for MR and RN right and left R-modules.

グロタンディーク構成に関しては、ハーパズ/プラーズマ論文から引用します。強調(太字+下線)は檜山。

According to [MM, §I.5], this construction was first used for diagrams of sets by Yoneda. It was later developed in full generality by Grothendieck in [Gro] and became a key tool in studying categories which "vary in families".

引用内に登場する文献への参照は:

  • [MM] S. MacLane, I. Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory, Springer (1992).
  • [Gro] A. Grothendieck, Reve^tements e'tales et groupe fondamental, Institut des Hautes Etudes Scientifiques (1964).

エンド/コエンドとグロタンディーク構成に関しても、マックレーン、グロタンディークよりも先に、米田さんがアイディアを出していたようです。偉大だ。

カブカブ 2018/11/14 14:51 刺激的な記事、いつも楽しく読ませていただいてます。この記事を見ていて昔、大学院のとき先生に教わったジョークを思い出しましたので、初めてコメントします。
Yoneda Lemma is important because Yo(u) ne(e)d a Lemma.
(早口で発音すると、それらしく聞こえる^^)

m-hiyamam-hiyama 2018/11/14 17:43 カブさん、
You need a ≒ 米田 、なるほど。
ありがとうございます。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181108

2018-11-01 (木)

論理/メタ論理の記法をどうするか 2: 悟りへの道

| 17:06 | 論理/メタ論理の記法をどうするか 2: 悟りへの道を含むブックマーク

論理/メタ論理の記法をどうするか」の続き。書き方(構文、記法)の話です。いきなり「どう書こうが同じだろ」「書き方なんて何だっていいじゃねーか」と言って済ますことが出来るなら楽なんだけど … そうもいかないのですよねー。

悩みと迷いとウンザリを繰り返せば、いずれは「どう書こうが同じだろ」「書き方なんて何だっていいじゃねーか」の境地=悟りに到れるかも。

内容:

  1. 含意記号について
  2. 変数宣言と仮定
  3. 定理・公理記述の変形とシーケント計算
  4. 定理・証明の変形の書き方
  5. リーズニングの図示
  6. リーズニングのテキスト表現

含意記号について

最近は、含意記号に二本棒矢印'⇒'を使うことが多いです。しかし、もともと僕は、'⇒'を使う習慣はなくて、'⊃'を使っていました。'⇒'も使うようになった理由は、'⊃'を知らない人が多くて違和感を持たれてしまうからです。

2006年の記事「論理記号のいろいろ」で引用した次の表を見てみると:

含意に'⇒'を使っている例ってないんですよね。僕がよく使っていた記法は、「竹内 1975」と同じです(竹内外史さんは、含意に'→'も使っています)。次の記事内(節の冒頭)では、使う記号を確認したりしています。

僕の本音としては、含意に'⇒'を使いたくない。二本棒矢印は、別な目的で使いたいのです。一本棒矢印も含意以外で使いたいこと多いし。論理ではいろいろな矢印が出てくるので、矢印記号が不足して困るんですよ。次の記事参照。

ところで、いま僕は「含意記号」といいましたが、「ならば」を意味する記号は条件記号〈conditional symbol〉と呼び含意記号〈implication symbol〉とは呼ばない人もいます*1 -- 含意〈implication〉と条件法〈conditional〉を別な意味で使うのです。条件法とは区別された含意を《含意》と書くことにして、「命題Aが命題Bを《含意する》」とは、

  • 条件命題 A⊃B が成立すること。

「へっ?」という感じもしますが、条件記号'⊃'は、単なる論理結合子〈論理演算子〉であって、《含意する》はメタ論理の概念なんです。

《含意》を上記のように解釈するとして、ある演繹システムSによる証明可能性を |-S と書くと、次の3つのメタ命題は同値です。

  • Sにおいて、AがBを《含意する》。
  • |-S A⊃B (Sにおいて、仮定なしに、条件命題 A⊃B を証明できる。)
  • A |-S B (Sにおいて、命題Aを仮定して、命題Bを証明できる。)

これは《含意》の構文的解釈(証明論的解釈)ですが、意味的解釈(モデル論的解釈)もできます。

たぶん、含意記号/含意命題と条件記号/条件命題を別物として扱う人は少数派だと思うので、僕は「含意」と「条件/条件法」を区別してません。上記のようなメタ論理的な概念が必要なら、メタ論理記号である '|-'(証明可能)、'|='(妥当)、'|⇒'(伴意)などを使ってその旨を表現します(前回記事も参照)。

変数宣言と仮定

定理・公理の記述として、変数(自由変数)の宣言の前には'For'、仮定の命題の前には'Given'、結論の命題の前には'Holds'を付けた書き方をしてみます。

For x∈R
For y∈R
Given x≧0
Given y≧0
  Holds x + y ≧ 0

こういう丁寧な書き方をしていた時期もあったのですが、めんどくさくなって、変数宣言も仮定も一律に'For'(または一律に'Given')になってしまいました。さらには、キーワード書くのもめんどうなんで、結局は次のような形:

  • x∈R, y∈R, x≧0, y≧0 → x + y ≧ 0

これって結局、シーケント〈sequent〉の構文です。シーケントを知らない人は、今言った形がシーケントだと思えばいいです。つまり、矢印'→'の左側に変数宣言と仮定命題を書いて、右側に結論命題を書いた形です。

シーケントの左右区切りとして出てくる矢印と、含意記号を区別する必要があるので、含意に'⇒'を使いたくなかったのです。記号の使い方の案は:

含意記号 シーケントの左右区切り記号
案1 ⊃  ⇒
案2 →  ⇒
案3 ⊃  →
案4 ⇒  →

案1と案2は竹内外史さんが使っていた記法です。案3は、'⇒'を別な目的で温存したいときに僕は使っています。案4は含意に'⇒'を使ってしまったときの用法です。ここではとりあえず、案3を使います。

シーケントの左右区切りに'|-'を使うこともけっこうあります。ですが、形式的シーケント計算内で'|-'を使うのはどうかな? という気もします。なぜなら、'|-'はメタ論理の「証明可能性」で使う記号ですから。形式的体系(人工的な記号操作のメカニズム)としてのシーケント計算のシーケントは、メタ論理的な意味も捨象されています。もちろん、“証明可能性の計算”をするときなら、シーケントの左右区切りに'|-'を使うのは適切です。

シーケントの左側には変数宣言と仮定の命題が並びます。変数宣言と仮定の命題の違いは見ればわかりますが、念の為、変数宣言は丸括弧で囲むことにします。

  • (x∈R), (y∈R), x≧0, y≧0 → x + y ≧ 0

複数の変数宣言を、まとめて丸括弧内に入れてもいいとします。

  • (x, y∈R), x≧0, y≧0 → x + y ≧ 0

定理・公理記述の変形とシーケント計算

以前に述べた証明のお膳立ての操作は、形式化すればシーケント計算に吸収されるでしょう。言い方を換えれば、シーケント計算(シーケントの変形)は、日常的に知らず知らずに使っているのです。

重要かつ典型的なシーケントの変形に次があります。

   Γ, A → B
  -------------↓↑
   Γ → A⊃B


   Γ, (x∈X) → A
  -----------------↓↑
   Γ → ∀x.A

ここで、Γ(大文字ガンマ)はその他諸々の変数宣言/仮定命題です。「↓↑」が付いているのは、上下両方向の変形が許されるからです。シーケントの矢印'→'は、証明可能性判断〈provability judgement〉の'|-'だと思っても、証明要求〈proof requirement〉の'|-?'だと思っても、どっちでも通用します。証明要求については、次の記事を参照:

シーケントの'→'を意味的帰結〈semantic consequence | entailment〉と解釈すれば、シーケント計算は、(形式化された)“事実の記述”の計算になります。意味的帰結については前回記事参照:

定理・証明の変形の書き方

この記事のタイトルは「記法をどうするか」です。内容にはあまり踏み込まず、記法(書き方)だけを問題にします。

前節の Γ, A → B などは、ひとつの定理の前提と結論の記述だとみなします。そして、矢印の部分に証明が詰め込まれていると考えましょう。詰め込まれている感じを出すために、Γ, A |→| B のように書き方を変えます。記号 '|→|' は、「この部分に証明が入る」という意味だと捉えてください -- ただし、あくまで気分だけの話です。

次に、「横の物を縦にする*2」ことにします。

 Γ, A
 ------
   ↓
  ----
   B

見栄えをよくするために、横棒('-'の並び)の長さを変えてますが、これは必須ではありません。'-'は4個とかに固定してもいいです。

前節の「変形する」の意味の横棒は、二重線('='の並び)に切り替えます。すると、前節と同じ絵図が次のように変わります。

   Γ, A
   ----
    ↓
   ----
    B
 =========↓↑
   Γ
   ----
    ↓
   ----
   A⊃B


   Γ, (x∈X)
   ----
    ↓
   ----
    A
 =========↓↑
   Γ
   ----
    ↓
   ----
   ∀x∈X.A

縦にスペースを取りすぎる気もします。二重線を縦棒にして左右に並べてみましょうか。

   Γ, A  ‖ Γ
   ----   ‖ ----
    ↓    ‖  ↓
   ----   ‖ ----
    B     ‖ A⊃B
         ←→


   Γ, (x∈X) ‖ Γ
   ----       ‖ ----
    ↓        ‖  ↓
   ----       ‖ ----
    A         ‖ ∀x∈X.A
             ←→

二重線の縦棒を並べるのはけっこうな手間だし、レイアウトが崩れてガタガタになったりするので、縦棒を横矢印にしてみます。

   Γ, A     Γ
   ----      ----
    ↓   ⇔   ↓
   ----      ----
    B        A⊃B


   Γ, (x∈X)     Γ
   ----           ----
    ↓        ⇔   ↓
   ----           ----
    A             ∀x∈X.A

以上のような描き方(図の記法)の変更をしても、内容的には何も変わってません。ですが、描画方向や使っている印が違っただけで、「難しい」「分からない」となってしまうことが多いのです。これは残念なことです。

縦の物を横にする、横の物を縦にする、印を置き換える、といった操作を躊躇なく自由に出来る能力はほんとに重要です。以下の記事は、圏論のストリング図の話として書いてますが、論理の横棒記法の図でも事情は同じです。図の描き換えの練習をしましょう。

リーズニングの図示

今は、シーケントの矢印に'→'を使っています。場合により、'→'が、'⇒', '|-', '|-?', '|⇒' なんかに変わるかも知れません。これらの区切り記号をシーケント区切り記号〈sequent delimiter〉と呼ぶことにします。シーケント区切り記号の変化に過敏に反応したり、惑わされないようにしましょう。

シーケントを変形する操作をリーズニング〈reasoning〉と呼びましょう*3。リーズニングを表す記号はリーズニング記号〈reasoning symbol〉ということにします。

リーズニングを図示する際には、次の選択をすることになります。

  1. シーケント区切り記号は、どれを使うか?
  2. シーケントの方向を、どの方向にするか?
  3. リーズニング記号は、どれを使うか?
  4. リーズニングの方向を、どの方向にするか?

幾つかの例を挙げてみます。


  1. シーケント区切り記号: |→|
  2. シーケントの方向: 左から右(→)
  3. リーズニング記号: '='の並び
  4. リーズニングの方向: 上から下(↓)
  Γ, A |→| B
 ===============↓
  Γ |→| A⊃B


  1. シーケント区切り記号: 縦に書いた |→|
  2. シーケントの方向: 上から下(↓)
  3. リーズニング記号: '='の並び
  4. リーズニングの方向: 上から下(↓)
  Γ A
  ----
   ↓
  ----
   B
 ======↓
  Γ
  ----
   ↓
  ----
   A⊃B


  1. シーケント区切り記号: →
  2. シーケントの方向: 左から右(→)
  3. リーズニング記号: ⇒
  4. リーズニングの方向: 左から右(→)
 Γ, A → B  ⇒  Γ → A⊃B


  1. シーケント区切り記号: ':'の縦並び
  2. シーケントの方向: 上から下(↓)
  3. リーズニング記号: ⇒
  4. リーズニングの方向: 左から右(→)
  Γ A     Γ
   :        :
   :   ⇒   :
   :        :
   B       A⊃B


横書きテキストだと、変数宣言や命題を並べる方向は左から右に限定されますが、絵(イラスト、ピクチャ)なら、その方向も自由になります。A, B, C → D というシーケントは次のように書くかもしれません。

  A
  B  → D
  C

他に:

  1. 変数宣言や命題に名前〈ラベル〉を付けるかも知れない。名前の付け方や付ける場所の選択肢・自由度がある。
  2. シーケントに名前〈ラベル〉を付けるかも知れない。名前の付け方や付ける場所の選択肢・自由度がある。
  3. リーズニングに名前〈ラベル〉を付けるかも知れない。名前の付け方や付ける場所の選択肢・自由度がある。

要するに、書き方・描き方には、ものすごいバリエーションがあるってことです。しかし、中身・内容は何も変わらない、一緒なんです。書き方・描き方のバリエーションに対応するには、自分でいろいろな書き方・描き方を試してみるのが一番です。

リーズニングのテキスト表現

最後に、リーズニングを横書きテキストだけで書き表すときの書き方について考えます。各種の矢印記号をどう選ぶか? がポイントです。含意記号の選び方が、シーケント区切り記号とリーズニング記号の選び方に影響します。

含意記号 シーケント区切り記号 リーズニング記号
案1  ⊃   →  ⇒
案2  →   ⇒  ▷
案3  ⇒   →  ▷

リーズニングに三角を選んだのは僕の恣意的選択です(これといって根拠などない)。

次のリーズニングを例題にしましょう。

before

For x∈R
For y∈R
Given x≧0
Given y≧0
  Holds x + y ≧ 0


after

For x∈R
For y∈R
Given x≧0
  Holds y≧0 ならば x + y ≧ 0

案1を使うと:

  • (x∈R), (y∈R), x≧0, y≧ → x + y ≧ 0 ⇒ (x∈R), (y∈R), x≧0 → y≧0 ⊃ x + y ≧ 0

案2を使うと:

  • (x∈R), (y∈R), x≧0, y≧ ⇒ x + y ≧ 0 ▷ (x∈R), (y∈R), x≧0 ⇒ y≧0 → x + y ≧ 0

案3を使うと:

  • (x∈R), (y∈R), x≧0, y≧ → x + y ≧ 0 ▷ (x∈R), (y∈R), x≧0 → y≧0 ⇒ x + y ≧ 0

どうでしょう? 「ややこしいな」「紛らわしいな」と思いましたか? その通りです。もし、「結局、どう書いても一緒じゃん」と思えたなら、それは「悟り」です。悟りは「拘り」を捨てることであり、「諦め」と似ています。諦めは「呆れた」とほぼ同じです。「もう呆れたよ、諦めたよ、拘ってもしょうがないね」 -- と、そう悟ってください。

*1:例えば、大竹出版『記号論理学』の著者・藤川吉美さん。

*2:「横の物を縦にもしない」はモノグサを表す言葉です。僕はモノグサですが、縦横の変更くらいはやります。

*3:リーズニングは、シーケント計算における推論/証明と事実上同じことです。ただし、バックワードリーズニングも認めます。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181101

2018-10-31 (水)

Googleは竹内外史になんでこの写真を付けるんだ?

| 16:27 | Googleは竹内外史になんでこの写真を付けるんだ?を含むブックマーク

竹内先生はこんな(↓)感じで、若い頃の写真だとしてもおかしい(実際、別人)。

*1

新垣結衣さんは、ちゃんとご本人の顔が出ている。

なんで、新垣結衣さんと比較するか? 2011年にこんなことがあったから。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181031

2018-10-24 (水)

アニメーションとしての証明

| 19:05 | アニメーションとしての証明を含むブックマーク

随分と以前から、「証明はアニメーションなんだ」と言ってます。このことを認識してないと、さほど難しくもないことが無闇と難しいモノになってしまうと思うんですよ。

この記事では具体的な事例を出してないので、モンヤリした話ですが、たぶん、具体的な事例を出す機会はあると思うので書いておきます。

アニメーションと、代替の表現手段

「証明はアニメーション」は、比喩とか例え話ではなくて、「実際にそうだよ」ってことです。なので、まず通常の「アニメーション」について語ります。が、僕がアニメ好きとか詳しいとか、では全くありません。非常に基本的な概念を確認するだけです。

現在の娯楽、あるいは芸術作品として公開されているアニメは、1秒に24フレーム(以上)らしいです。10秒で240フレームですね。素人作品で、多少粗い動きでもいいや、って事なら8フレーム/秒とかでもいいかも知れません。

いま、アニメを作りたい人がいたとします。しかし、作るための機材(ツール)もなく、技術も知識もないとします。でもなにか作りたい! さぁ、どうしましょう? いくつかの選択肢があります。

  1. パラパラ漫画にする。
  2. 紙芝居にする。
  3. マンガにする。
  4. 小説にする。

パラパラ漫画は、フィルム(デジタルなモノも含めてフィルムと呼ぶ)の代わりに、複数枚の紙を使いますが、原理はアニメーションと同じと言っていいでしょう。フレームレートは … よく分かりませんが、仮に10フレーム/秒としておきましょう。10秒で100枚の紙が必要です。

紙芝居は、表現手段としてパラパラ漫画とは違うものです。フレームレート(?)が10秒で1枚とかでしょう。絵の動きは最早なくて、代わりに「語り」を使います。

マンガもまた表現手段として別なものになります。パラパラ漫画として描いた絵達を、台紙に順番に貼り付けていったらマンガになるでしょうか? それはマンガではなくて、一連の動きのスナップショット群を一度に見せただけです。マンガにはマンガとしての語彙・文法があります(「記法バイアスと記法独立な把握: 順序随伴を例として // 語彙、文法、記法」参照)

小説になると、非常に異なった表現手段になるので、別な才能が必要になります。アニメーションで伝えたかったことが、はたして小説で伝わるのかも疑問です。

アニメーション作成ツールとしての証明支援系

「証明はアニメーションなんだ」の意味は、証明が、ある種の絵〈図形〉が変化していく様を見せるものだからです。ストーリーの分岐や合流もあります。人間は同時に複数のストーリーを追うのは難しいので、メイン・ストーリーのあいだにサイド・ストーリーを適宜挟むとかして分岐・合流を表すことになるでしょう。

この事を考えれば、証明作成支援ツール〈証明支援系〉は、アニメーション作成ツールと似たものになるでしょう。僕がGlobularを高く評価するのは、(現状の出来ばえはともかくとして)アニメーション作成ツールの方向に一歩進めた(おそらくは初めての)ソフトウェアだからです。(もし、Globularに興味が湧いたなら「Globularの使い方 (1)」をどうぞ。)

Globularは、フレーム群に相当する複数の絵(静止画)を作成するお絵描き機能を持っています。同時に、複数の絵達が関連して持つ構造も指定できます。再生〈リプレイ〉をどうするかを制御する機能は(今は)なくて、ユーザー側が好きに探索するようになっています。その意味では、ゲームの舞台(例えばダンジョン)だけを作成するツールのようでもあります。時間方向のストーリーが特になくても、舞台内を勝手に動き回って探索できれば、けっこう面白いです。

Globularは、背景としている原理も新しいのですが、伝統的な論理に基づく証明支援系であっても、要求される機能は同じです。フレームに相当する静止画の作成機能、フレームどうしの関連を指定する構造化の機能です。

ストーリーには分岐や合流がありますが、制作者側が再生手順を完全に決めるのではなくて、ユーザー(作品の視聴者)が対話的に選択できるようにするほうが望ましいでしょう。証明という作品は、受動視聴には向いてないので、早送り・巻き戻しのような、いやもっと高機能なナビゲーションが必須です。

劣悪な制作環境・視聴環境

アニメーション作品としての証明を制作する環境は、まったく整っていません。アニメーション作品としての証明を再生・視聴する環境もありません。これは、デジタルなツールだけの話ではなくて、紙媒体においても事情は同様です。

「いや、TeXで綺麗に組版できるじゃないか」 -- そういう話ではありません。アニメーションを諦めるにしても、代替表現手段もロクなもんがないのです。

アニメーションがダメなら、まずはパラパラ漫画でしょう。時間に沿った再生(パラパラすること)が難しいなら、台紙に貼って見せることになります*1。僕は、この「台紙に貼ったパラパラ漫画」はありだと思いますが、現実に使われている例は稀でしょう。労力と紙の面積を膨大に必要とするからです。動かないから、面白くないし。

となると、マンガですね。マンガには独自な語彙・文法があるわけですが、コマ運びや表現手法のクセが強くて難読だとしたらどうでしょう? コマを追えず、ひとつのコマでさえ意味不明となるでしょう。形式的証明記述の現状は、このようなものだと思います。

それで結局、落ち着くところは紙芝居や小説で表現することです。我々が教科書や論文でいつも見ている自然言語で書かれた非形式的証明記述です。絵は補助で「語り」、あるいは「語りだけ」でストーリーを読者に伝える方法です。

「語り」は「絵」に劣ります -- こう言うと奇妙に感じるかも知れませんが、Globularの“絵”に限らず、伝統的な、自然演繹の証明図にしろシーケント計算の証明図にしろ、それは形式化された絵であり、“語り=自然言語”に比べればずっと精密です。

証明において、形式化された絵(静止画)と、それらを編成・構造化したアニメーションを扱える環境がないことが、さほど難しくもないことまで、無闇と難しいモノにしてしまっている要因でしょう。…… という状況を解決できなくても、状況を知るだけでも「無意味な難しさ」に気付くことはあります。

*1:「台紙に貼ったパラパラ漫画」は、目線のほうを移動しながら、動いているところを想像する方式です。マンガのような語彙・文法(約束ごと)はなくて、単純に静止画を次々と追いかけるだけです。

そんなに難しいものそんなに難しいもの 2018/10/29 03:47 ほんとにイライラしますよね
コンピュータでみんなが自由に気軽に証明を書く時代はいつになったらくるんですか?だれか頭のいい人もっと直っ感的で使いやすいやつ作って
というか選択肢が無さすぎ、なんでもいいからもっといろんなサービスを用意してくれ

m-hiyamam-hiyama 2018/10/29 11:40 そんなに難しいものさん、
気分としては、「なんとかしてくれよ、もう」ですが、
> そんなに難しいもの
難しいです。証明支援系とそのインターフェイス開発は膨大な時間と労力がかかります。
Coq, Isabelle は30年間アクティブな開発が続いてますが、それでも満足できる状況にはないです。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181024

2018-10-19 (金)

クリーネ代数: 不等式的定義と等式的定義

| 12:04 | クリーネ代数: 不等式的定義と等式的定義を含むブックマーク

クリーネ代数 再論」で、クリーネ代数の定義を(いまさらに)述べたのですが、不等式と等式に関してちょっと微妙なところがあります。

最小な前不動点は不動点になる

クリーネ代数もコンウェイ半環も、最小不動点を扱う代数系だと言えます。最小不動点と最小前不動点に関して次のように書きました。

最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同じなので、次の2つの条件を満たすtは最小不動点となります。

「同じ」という言い方は誤解をまねくかな、と思って次のように修正しました。

最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同様に扱えるので、次の2つの条件を満たすtは最小不動点とみなせます。

しかし、修正後もまた別な誤解がされそう。文言の削除挿入ではうまく説明できそうにない。ので、この記事で説明します。

Kを順序半環、a∈K とします。集合 PreFix(a) を次のように定義します。

  • PreFix(a) := {x∈K | ax + 1 ≦ x }

PreFix(a)は、アフィン線形写像 f(x) = ax + 1 の前不動点〈pre-fixed point〉の集合です。PreFix(a)は空でないと仮定して、t∈PreFix(a) に関する次の条件を考えます。

  • x∈PreFix(a) ならば t ≦ x

この条件は、前不動点tが、他のfの前不動点より小さいことを意味します。このようなt(最小前不動点)があれば、それはfの不動点になります。

まず、f(t)がfの前不動点になることを見ます。f(t) ≦ t は成立しているので、両辺にfを適用して f(f(t)) ≦ f(t) 、これは「f(t)がfの前不動点」であることです。tに関する条件 ∀x∈K.(f(x) ≦ x ⇒ t ≦ x) から、

  • t ≦ f(t)

最初から

  • f(t) ≦ t

は成立しているので、上記ニ条件から

  • f(t) = t

よって、fの最小前不動点があれば、それはfの最小不動点です。

不等式と等式

クリーネ代数では、最小不動点の存在を最小前不動点の存在として定式化しています。クリーネスターa*は最小不動点を与えるので、

  • aa* + 1 = a*

を公理に入れるのは別に問題はない(冗長になるだけ)ですが、実際に使いたいのは、

  • ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)

という不等式条件のほうです。この不等式条件を使った証明法は不動点帰納法と呼ばれたりします。クリーネ代数の公理は、不等式による推論が出来るように選ばれているのです。

一方で、コンウェイ半環のスターも不動点を与えます。次の積スター等式で、b = 1 とすると、a*の不動点等式です。

  • (ab)* = 1 + a(ba)*b

大雑把に言えば、クリーネ流はアフィン不動点の不等式的な性質に注目し、コンウェイ流は等式的な性質に注目しています。この流儀の違いはどうも後々まで影響しそうで、「不等式でも等式でも同じ」とは言いにくいのです。

トレース付きデカルト圏のような不動点理論の圏論的な定式化は、等式的なので、クリーネ代数よりコンウェイ半環の圏化(亜化)と言えそうです。クリーネ代数の圏化では、順序/不等式を、どのように表現するかが鍵となるでしょう。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181019

2018-10-18 (木)

微分幾何の特殊な習慣をもう少し詮索

| 15:21 | 微分幾何の特殊な習慣をもう少し詮索を含むブックマーク

微分幾何の特殊な習慣 -- 知らんかった」で、「dsはdとsに分解しない。単なる習慣的記法。s単独で意味などない」と書いたのですが、書いた後で「ちょっと言い過ぎかな」と思いました。で、追記しときました。

長い期間、広く使われている記法には、なにかしらの意味はあるものです。“意味”が心理的なもの(メンタルモデル)かも知れませんが、適切な解釈のもとでの整合性は期待できるでしょう。

内容:

  1. dxはdとxに分けて考える
  2. 微小量にはdを付けるという習慣
  3. 長さの微小量はどう書くか?
  4. sは弧長パラメータ
  5. まとめ

dxはdとxに分けて考える

記事「微分幾何の特殊な習慣 -- 知らんかった」で、dsは、'd'と's'の二文字まとめて単一の記号で、分解したら無意味だと言いました。しかし、dfとかdxとかは、そもそも分解したら無意味だと思っている方もいるでしょう。そうじゃないです。“普通は”分解しても解釈できます。何が“普通”かの議論は大いにあるでしょうが。

外微分計算〈exterior calculus〉では、dfと書いたら、dとfに分解できます。fが関数で、dは微分(外微分作用素)です。dが作用素で、fが被作用項〈オペランド〉であることを強調して d(f) と書くとして、例えば2次元での話なら:

 d(f) ¥:=¥: ¥frac{¥partial f}{¥partial x}dx ¥;+¥; ¥frac{¥partial f}{¥partial y}dy

ここで出てきたdx, dyも、それぞれ関数xと関数yの微分です。xはどんな関数かというと、(a, b) |→ a という第一射影を取る関数です。yは第二射影ですね。dxとdyが、“1次微分形式=余接ベクトル場”の(加群としての)基底になります。

df/dx = g(x) という簡単な微分方程式は、df = g(x)dx と書いても同じです。より一般に、df, dx などが出現している等式は、なんらかの微分方程式だと解釈できます。

微小量にはdを付けるという習慣

気分を変えて、長さではなくて体積を話題にしましょう。体積をラテン文字・大文字'V'で表すことにします。文字'V'は体積を表すために固定(あるいは予約)するとしましょう。このとき、dVに意味を持たせることはできます。ただし、「関数Vを外微分したものがdV」という解釈はできません。

Vを関数と考えるなら、その域〈domain〉は何でしょうか? 「微分幾何の特殊な習慣 -- 知らんかった」で例に使ったような開集合 U⊆Rn を選んで、V:U→R と考えていいでしょうか? ちょっと無理がありますよね。

Vの引数になり得るのは、なにか“体積を持つ図形”でしょうから、

  • V:(“体積を持つ図形”の集合)→R

でしょう。図形をR3の部分集合だと考えれば、

  • (“体積を持つ図形”の集合)⊆Pow(R3)

ここで、Pow(R3)はR3のベキ集合 -- R3のすべての部分集合からなる集合です。

(“体積を持つ図形”の集合)を定義するのは難しいですが、うまく定義できたとすると、Vは(“体積を持つ図形”の集合)の上の測度になります。測度は積分として表示するのが自然でしょうから:

 V(A) = ¥int_{A} dV

ここで出現した被積分項dVは、「微小な体積」という解釈を持ちます。「R3に内在する(最初から在る)微小な体積を、図形Aの上で寄せ集めたら、Aの体積になる」と読めます。

この被積分項dVを、dとVに分解して「Vにdしたもの」と解釈するのは無理ですが、「マクロ量Vの微小バージョンdV」というメンタルモデルとしての意味はあります。

長さの微小量はどう書くか?

体積と同じことを長さに関して議論してみます。ラテン文字・大文字'V'はvolumeの'v'から取ったので、長さはlengthの'l'からラテン文字・大文字'L'を採用しましょう。

Lの引数になるのは、なにか“長さを持つ図形”でしょうから、

  • L:(“長さを持つ図形”の集合)→R

先ほどと同様に図形をR3の部分集合だと考えれば、

  • (“長さを持つ図形”の集合)⊆Pow(R3)

A∈(“長さを持つ図形”の集合) に対して、

 L(A) = ¥int_{A} dL

話のスジは、体積でも長さでも同じです。が、しかし、“長さを持つ図形”をR3の部分集合として測度論的に扱うのは面倒で計算もやりにくいですね。扱い方を変えましょう。

部分集合Aではなくて、関数 f:I→R3 を考えます。ここで、Iは実数の区間で、fはなめらか(いくらでも微分可能)とします。fの域である区間Iは、2つの実数a, bにより I = [a, b] と書けますが、位置をズラせば、I = [0, a] とできるので、区間の左端は常に0に取ると約束します。また、fの微分係数〈速度ベクトル〉はゼロベクトルにはならないことも仮定します。

以上の設定で、L(f) はどう表現できるでしょうか。

 L(f) = ¥int^{a}_{u = 0} |f’(u)|du

ここで、f'は関数fの微分係数〈導関数 | 速度ベクトル〉で、|-| はベクトルの長さ〈ノルム〉です。fを (f1, f2, f3) と成分表示するなら:

 L(f) = ¥int^{a}_{u = 0} ¥(¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

前節同様に、「マクロ量Lの微小バージョンdL」というメンタルモデルに従うと、

 L(f) = ¥int^{a}_{u = 0} dL

被積分項どうしを比較して、

 dL = ¥( ¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

fの存在を暗黙に前提するなら、LとdLの関係はとても自然なものだと思います。体積と長さだけでなくて、この記法は一般的に使用していいでしょう。次のようにルール化できます。

  • なんらかのマクロな量Xがあるとする。
  • その量Xは、Aなどを測って得られるとする。
  • 量Xの微小バージョンをdXと書く。
  • マクロ量 X(A) は、微小量 dX をAに関して積分して得られる。

sは弧長パラメータ

さて、最初に取り上げた微分幾何の's'に話を戻しましょう。長さを'L'とするか's'とするかは別にどうでもいいので、伝統に則り's'にしましょう。

 s(f) = ¥int^{a}_{u = 0} ¥(¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

 s(f) = ¥int^{a}_{u = 0} ds

 ds = ¥( ¥sqrt{¥({¥frac{df_1}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_2}{du}}¥)^2 ¥;+¥; ¥({¥frac{df_3}{du}}¥)^2 }¥)du

自然な記法であり、なんら問題ありません。

しかし、文字's'の出自は別なところにあります。弧長パラメータです。弧長パラメータは、“長さを持つ図形”の表示を正規化〈一意化〉する手段として使われます。異なる出自と異なる経緯でも、同じ記法に到達するのですが、「異なる経緯」を追ってみます。

なめらかな関数 f:I→R3 で“長さを持つ図形”を表そうとすると、かなりの任意性・恣意性・自由度があります。任意性を潰すために同値関係を入れましょう。

f:I→R3 と g:J→R3 が同値だとは、次のことだとします。

  • 区間のあいだの関数 h:I→J があり、hはなめらかで微分係数はいたるところ非ゼロな可逆関数とする。そんなhを使って、f = g¥circh と書けるとき、fとgは同値。

個々の関数ではなくて、同値類を使えばパラメータ付けの任意性は消えますが、同値類よりは、代表元である関数を選んで、それを使ったほうが分かりやすいです。

f:I→R3 に次の条件を課します。

  • 微分係数〈速度ベクトル〉f'の長さはいたるところで1。

この条件を満たすfは、先の同値類の代表元になります。この条件を満たすfに関しては:

 s(f) ¥:=¥: ¥int^{a}_{u = 0}|f’(u)|du ¥:=¥: a

長さs(f)が区間の右端aで与えられます。この等式左辺のsはマクロ量としての長さです。

「微分係数f'の長さはいたるところで1」であるfに関しては、実数区間を走るパラメータに's'を使うと約束します。この約束から、今までuと書いてきたところがsに変わるので:

 s(f) ¥:=¥: ¥int^{a}_{s = 0}|f’(s)|ds ¥:=¥: a

fに課した条件から |f'(s)| = 1 なので、

 s(f) ¥:=¥: ¥int^{a}_{s = 0} ds ¥:=¥: a

[追記]

すぐ上の等式  s(f) ¥:=¥: ¥int^{a}_{s = 0} ds ¥:=¥: a は、だまされた/バカにされたような気がするかも知れません。右辺側で暗黙に前提しているfを明示的に書いて、

 s(f) = ¥int_{f} ds

ならどうでしょう。fのマクロ量s(f)を測ることは、dsという微小量をfに関して積分して求めるのです。となると、積分操作は、f達がいる空間とds達がいる空間のあいだで行うことになります。これは、微分形式やチェーンの代数を出さないと、うまく表現ができない気がします。

[/追記]

まとめ

  • dX という書き方に対して、「dが外微分作用素、Xが被作用項」という解釈がある。
  • dX という書き方に対して、「Xがマクロな量、dXがその微小バージョン」という解釈がある。
  • 上記ニ種類の解釈がたまたま一致することもあるが、一般的には異なった解釈となる。
  • よって、解釈の選択肢を間違えると、意味不明になるかも知れない。
  • 実際に解釈の選択肢を間違えて混乱するヤツがいる(それは私だ)。

[追記]念の為に言うと、「外微分のd」と「微小量のd」が無関係だ、と主張しているわけではありません。「外微分のd」は「微小量のd」のなかで、線形代数でうまく定式化できる部分を取り出したものでしょう。「微小量のd」のほうが、より多様に、そしてときに曖昧に使われるので、「微小量のd」が「外微分のd」としては解釈できないこともあるよ、ということです。

教訓としては、

  • 外微分のdのように見えても、外微分では解釈できない場合もあるから注意せよ。

です。[/追記]

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181018

2018-10-17 (水)

微分幾何の特殊な習慣 -- 知らんかった

| 09:42 | 微分幾何の特殊な習慣 -- 知らんかったを含むブックマーク

「郷に入っては郷に従え」という諺がありますが、従うべき郷の習慣を知らないと、何がなんだかサッパリ分からなかったり、とんでもない誤解をしたりします。

内容:

  1. 微分幾何の習慣は知らない
  2. 特別な意味の文字
  3. dsって何だろう
  4. 接ベクトル場、余接ベクトル場
  5. 内積場、ノルム場
  6. 内積場/ノルム場の表示
  7. ノルム場がdsだった
  8. 習慣の由来は

微分幾何の習慣は知らない

添字をたくさん使うテンソル計算と、そんなテンソル計算を使う微分幾何は、早い段階で「やってられん!」と投げ出しました。そこらへんの事情は昔書いたことがあります。

後になって、ネルソンの本で少し勉強しました。

ネルソンの本はモダンですが、ネルソンが考案した記法で書かれていて、伝統的な微分幾何とはだいぶ違います*1

そんな事情で、伝統的な微分幾何では常識であっても、僕はまったく知らないことが多々あります。

特別な意味の文字

特定の文字が、固有名詞として特定の対象物を指すことは珍しくありません。ギリシャ文字・小文字'π'は円周率を表します。ラテン文字・小文字'e'はネイピア数ですね。もちろん、この約束が破られることもあります。正確に言えば、特定の分野や文脈において、特定の文字が、固有名詞として特定の対象物を指すことがある、です。

微分幾何にけるラテン文字・小文字's'、物理の相対論におけるギリシャ文字・小文字'τ'が、そのような特別な意味を持つ文字だったようです(知らなかった)。s, τは、「特定の対象物を指す」というより、「特別な使い方の習慣がある」ということです。ほんとに特別なんです。なかなか推測は出来ないので、知ってないとアウトだと思います。

以下では、ラテン文字・小文字's'の特別な使い方の習慣を話題にします。実は、's'については「そう言えば、そんな習慣あったな」くらいの記憶はあるのですが、'τ'についての習慣はまったく知らなかったので、ホントに何がなんだかサッパリ分からなかったです*2

dsって何だろう

多様体を持ち出すと面倒なので、関数やベクトル場を考える領域は、Rnの開部分集合Uに限定します。なんなら、n = 2 とか n = 3 に次元を固定してもいいです。

's'について特に何も知らないとして、ds と書かれていたら、どう解釈するでしょう? 僕は、dは微分(外微分)と思うので、sは関数 s:U→R で、それを微分してdsなんだ、と解釈します。dsは、U上の1次微分形式(の場)ですね。

ds2 ならどうでしょう? d(s2) とは考えにくいので、(ds)(ds) と解釈します。dsの併置(並べること)は、なんらかの掛け算でしょう。1次微分形式には自然な掛け算があります。αとβが1次微分形式だとして、

  • (αβ)(v) = α(v)β(v) (右辺の併置は実数値関数の普通の掛け算)

ここで、vはU上の接ベクトル場です。Uの一点pで考えるならば、

  • (αβ)p(vp) = αp(vpp(vp) (左辺の併置は実数の普通の掛け算)

ds2 とは、たぶんそんなもんだろう、と思いますよね。実際はまったく違うんですわ。

接ベクトル場、余接ベクトル場

Uの一点pでの接ベクトルの全体を TpU と書きます。U⊆Rn なので、TpU ¥stackrel{¥sim}{=} Rn です。点pごとに、TpU の要素(つまり接ベクトル)を割り当てる写像が接ベクトル場です。接ベクトル場vは、v:U→Rn と考えてかまいません(あくまで U⊆Rn, TpU ¥stackrel{¥sim}{=} Rn だからです)。点pでのvの値は、v(p)ではなくてvpと書くことにします(後で理由は分かるでしょう)。

TpU の標準双対空間を T*pU と書きます。

  • T*pU := (TpU)*

T*pU の要素を、点pにおける余接ベクトルといいます。点pごとに、T*pU の要素(つまり余接ベクトル)を割り当てる写像は余接ベクトル場です。余接ベクトル場αは、α:U→(Rn)* と考えてかまいません。しかし、(Rn)*Rnを同一視することはしません。点pでのαの値は、α(p)ではなくてαpと書くことにします。余接ベクトル場の一点での値αpは、TpU→R という線形写像です。

余接ベクトル場と1次微分形式はまったく同じ概念です。ここから先は、「余接ベクトル場」のほうを使います。

α:U→(Rn)* が余接ベクトル場、v:U→Rn が接ベクトル場のとき、

  • U∋p |→ αp(vp) ∈R

は、U上の実数値関数、つまりスカラー場になります。点引数pを下付きにしたのは、α(p)(v(p)) だとちょっと分かりにくいからです。

内積場、ノルム場

Uの点pごとに、接ベクトル空間TpUに内積が入っているとします。点pにおける内積を (-|-)p と書きます。ハイフン'-'は無名変数です。(-|-)p:TpU×TpU→R で、(-|-)p は内積の公理を満たす双線形写像です。

  • U∋p |→ [内積 (-|-)p:TpU×TpU→R]

これは、点pごとに内積を割り当てているので、内積場という言い方をしてもいいでしょう。普通は、内積場とは言わないで計量場ですけど。

v, w:U→Rn が2つの接ベクトル場のとき、

  • U∋p |→ (vp|wp)pR

はスカラー場です。内積場があれば、2つの接ベクトル場を内積してスカラー場を得ることができます。例えば、(vp|wp)p がpによらず恒等的に0なら、「vとwは直交する接ベクトル場だ」とか言えます。

接ベクトル場 v:U→Rn に対して、

  • U∋p |→ sqrt((vp|vp)p) ∈R

と定義すると、これは、各点pでの接ベクトルの長さを与えることになります。長さはノルムとも言うので、p |→ sqrt((vp|vp)p) という割り当てをノルム場と呼びましょう。点pでのノルムは |-|p と書きます。この記法を使ってノルム場を次のようにも書けます。

  • U∋p |→ [ノルム |-|p:TpU→R]

接ベクトル場 v:U→Rn に対するノルム |v| は、次のようなスカラー場(U上の実数値関数)になります。

  • U∋p |→ |vp|pR

内積場/ノルム場の表示

v:U→Rn をU上の接ベクトル場とします。成分表示して、

  • v = (v1, ..., vn)

とします。横ベクトル形式で書いてますが、実際は縦ベクトル形式なんだと思ってください。vの転置 vT が横ベクトル形式です。点pごとの値は、

  • vp = (vp 1, ..., vp n)

vp i と書くか、vi p と書くか悩みますが(どっちでもいい)、この形式にします。

U上の内積場 p |→ (-|-)p を具体的に定義するとき、点pごとにn×n行列を与えればいいですね。Gがそのような行列の場だとします。

  • G:U→Mat(n, n)

ここで、Mat(n, n)はn×n行列の空間です。この行列場Gを使って、

  • (vp|wp)p := (vpT)Gpwp

と内積の値を定義できます。n = 2 の場合をもっと具体的に書けば:

(¥begin{pmatrix}v_{p¥, 1} ¥¥ v_{p¥, 2}¥end{pmatrix} | ¥begin{pmatrix}w_{p¥, 1} ¥¥ w_{p¥, 2}¥end{pmatrix})_p ¥: :=¥: ¥begin{pmatrix}v_{p¥, 1} & v_{p¥, 2}¥end{pmatrix}¥begin{pmatrix}G_{p¥, 1 1} & G_{p¥, 1 2} ¥¥G_{p¥, 2 1} & G_{p¥, 2 2} ¥¥¥end{pmatrix}¥begin{pmatrix}w_{p¥, 1} ¥¥ w_{p¥, 2}¥end{pmatrix}

対応するノルム場は、

  • |vp|p := sqrt((vpT)Gpvp)

n = 2 の場合のノルム場は、

¥|¥begin{pmatrix}v_{p¥, 1} ¥¥ v_{p¥, 2}¥end{pmatrix}¥|_p ¥: :=¥: ¥sqrt{¥begin{pmatrix}v_{p¥, 1} & v_{p¥, 2}¥end{pmatrix}¥begin{pmatrix}G_{p¥, 1 1} & G_{p¥, 1 2} ¥¥G_{p¥, 2 1} & G_{p¥, 2 2} ¥¥¥end{pmatrix}¥begin{pmatrix}v_{p¥, 1} ¥¥ v_{p¥, 2}¥end{pmatrix}}

上記のルート内を展開して書いてみます。ここから先では、下付きpが煩雑なので省略します。点pごとではなくて、U全体に対して記述していると思ってください。

¥|¥begin{pmatrix}v_{1} ¥¥ v_{2}¥end{pmatrix}¥| ¥: :=¥: ¥sqrt{G_{1 1}v_1 v_1 + G_{1 2}v_1 v_2 +  G_{2 1}v_2 v_1 +  G_{2 2}v_2 v_2}

あるいは両辺を二乗して:

¥|¥begin{pmatrix}v_{1} ¥¥ v_{2}¥end{pmatrix}¥|^2 ¥: :=¥: G_{1 1}v_1 v_1 + G_{1 2}v_1 v_2 +  G_{2 1}v_2 v_1 +  G_{2 2}v_2 v_2

一般的な次元nでは:

| v |^2 ¥: :=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i

ここで、vは接ベクトル場、Gは行列場ですが、添字が付いた Gji, vj, vi 達はスカラー場です。

ノルム場がdsだった

前節のノルム場をNという1文字で表すことにします。

N(v) ¥: :=¥: sqrt{¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i}

ノルム場Nの二乗はN2とします。

N^2(v) ¥: :=¥: N(v)^2 ¥;=¥; ¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i

内積場やノルム場を、dxi を使って書く場合もあります(それが普通)。

N^2 ¥::=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i

これは、完全に合理的な記法です。なぜなら、dxiは余接ベクトル場で、ベクトル場vに対して dxi(v) = vi と成分を取り出す働きがあるからです*3

N^2(v) ¥:=¥: (¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i)(v) ¥:=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j(v) dx_i(v) ¥:=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}v_j v_i

辻褄が合ってますね。

辻褄が合わなくなるのはここからです。ノルム場Nを、dsと書く習慣があるのです。ノルム場の二乗N2ならds2です。

ds ¥::=¥: ¥sqrt{¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i}

ds^2 ¥::=¥: ¥sum_{1 ¥le i, j ¥le n}G_{j i}dx_j dx_i

dsをdとsに分解してはダメです。s自体に意味があるわけではなくて、'ds'を単一の記号とみなして、それはノルム場を表すために予約されていると解釈します。sは関数ではなく、dsは余接ベクトル場〈1次微分形式〉ではありません。ノルム場(またはその二乗)の定義式を見て、「sは何だろう?」「sはどこから来たのだろう?」「sの正体は?」とか考えるのはまったくのナンセンスです。だって、単なる習慣的記法だもの。

それ相応の文脈があれば誤解はないでしょうが、ノルム場の具体的な定義として、 ds = (なんか具体的な式) という等式がポンと出されると、「sを微分したのが (なんか具体的な式) なのね」てなことになります。で、ワケワカメ状態。

習慣の由来は

ノルム場をdsと書くようになった由来は、割と容易に想像がつきます。弧長パラメータという概念があり、その弧長パラメータをsと書く習慣があります。無限小な弧長だから「d(無限小) + s(弧長)」となったのでしょう。

「sという関数にdという作用素を適用した」のではなくて、「無限小弧長」を表す符丁だったんですね。ほぼ固有名詞みたいなもんです。

この特殊な用法でのdsを、「線素」とも呼ぶようです。「線素」という言葉は聞いたことがありますが、「線」が1次元のモノを意味し、「素」が無限小で、「線素=接ベクトル」だろうと僕は解釈していました。「線素=接ベクトルの長さ=無限小弧長」という意味もあるんですね。

理解を妨げたり、誤解を招く言葉や記法というのは、いたるところにあって落とし穴になるのですが、僕も落とし穴にマンマと落とされました。

  • dsはdとsに分解しない。単なる習慣的記法。s単独で意味などない

[追記]これ(↑)は言い過ぎかな。'd'と's'に分解した上で、それぞれ単独での意味は、探せば在りますね、解釈法を変えれば。'd'を微分(外微分作用素)と解釈している限りは's'に意味を持たせられない、ということです。[/追記]

[さらに追記]この記事の修正はしませんが、言い過ぎに対する補正をするために続きの記事を書きました。

[/さらに追記]

*1:普通のテンソル代数とは少し違った、ネルソン代数とでも呼ぶべき代数を定義して、それをベースにしています。見た目は伝統的微分幾何と似せる工夫をしているのですが解釈は違います。ちょっとトリッキーな印象を受けました。

*2:結論を言えば、's'に関する習慣と'τ'に関する習慣は同じものです。

*3:それに、dxiは関数xiの微分であるという点でも整合的記法です。

2018-10-15 (月)

論理/メタ論理の記法をどうするか

| 16:05 | 論理/メタ論理の記法をどうするかを含むブックマーク

最近割と、論理/メタ論理の話をする機会があるのですが、そのとき、どんな書き方をすればいいか悩みます。

内容:

  1. キーワード方式とターンスタイル方式
  2. 正しさを分類する
  3. 書き方の変種や修飾
  4. 意味的帰結の書き方

キーワード方式とターンスタイル方式

正確な記述と演繹のための非日本語記法」で次のような書き方をしました。

For x∈R, y∈R.
For x ≧0, y ≧0.
  IsCorrect x + y ≧ 0

少し前までは、次のような書き方をしてました。これ(↓)は、誰か(誰だか忘れた)の真似をしたものです。

Given x∈R, y∈R.
Given x ≧0, y ≧0.
  Holds x + y ≧ 0

キーワードの差(ForとGiven、IsCorrectとHolds)以外何の違いもありません。IsCorrectとHoldsは、ターンスタイル記号'|-'と同じ意味です。論理/メタ論理における標準的記法はターンスタイル記号です。

ターンスタイル記号より、上に紹介した書き方がいい点は:

  1. 英単語由来のキーワードのほうが、見慣れない記号'|-'より幾分か親しみやすい。
  2. 文脈(前提)を、何行かに分けてグルーピングして書ける。

「幾分か親しみやすい」は気分的なもので、たいした理由ではないです。「何行かに分けて書ける」もターンスタイル記法でもやれば出来ます。文脈をグルーピングしたいなら、区切り記号(例えばスラッシュ)を導入すればいいでしょう。

x∈R, y∈R / x ≧0, y ≧0 |- x + y ≧ 0

どう書こうが同じだろ、ってのが僕の感想ですが、“気分的な差”とか“視覚的な(見た目の)差”とかが実にバカにできなくて、「どう書くべきか」の判断は難しくなります。

正しさを分類する

前節のキーワード 'IsCorrect', 'Holds' は、「正しい」「成立する」という意味です。それ以上の説明は要らないように思えますが、そうではありません。メタ論理(モデル論や証明論)のモットーは、正しさや成立することを厳密に分析することです。

少なくとも、'|-'(ターンスタイル記号)と'|='(ダブルターンスタイル記号)はシッカリと区別する必要があります。ターンスタイル記号は“構文的に正しい”、ダブルターンスタイル記号は“意味的に正しい”という主張(に使う記号)です。今日は、内容的説明をする気はなくて、記法の話ですから、“構文的に正しい”と“意味的に正しい”がどう違うかは説明しません。

'|-' と '|=' をキーワードにするなら何がいいのだろう? 'IsProvable'と'IsValid'かな。

  • IsProvable x + y ≧ 0
  • IsValid x + y ≧ 0

'|-' と '|=' は、形は似てますが、使い方がだいぶ違います。'|-'の左側には証明の前提を書きます。

  • x ≧0, y ≧0 |- x + y ≧ 0

キーワードで書くなら(ピリオド打つのはやめた)、

For x ≧0, y ≧0
IsProvable  x + y ≧ 0

あるいは、

Given x ≧0, y ≧0
IsProvable  x + y ≧ 0

なんかGivenのほうがいいような気がしてきた。まったくの気分だが。

'|='の左側には、右側の命題を成立させるモデルを書きます。モデルとは、命題を解釈するための構造です。例えば、自然数の変数・定数・演算・関係を使うモデルをN-model、実数の変数・定数・演算・関係を使うモデルをR-modelとしたとき:

  • N-model |= ∀x, y.(x + y ≧ 0)
  • R-model |=/ ∀x, y.(x + y ≧ 0)

'|=/'は「正しくない」の意味です。全称限量子を付けないで、自由変数が残っていると妥当性〈validity〉の判断はできません。

  • R-model |= x + y ≧ 0 (なんともいえない)

変数への具体的な値の割り当てを、変数の状態〈state〉、束縛〈binding〉、付値〈valuation〉などと呼びます。状態まで付ければ妥当性が判断できます。

  • (R-model, {x←1, y←1}) |= x + y ≧ 0
  • (R-model, {x←0, y←(-1)}) |=/ x + y ≧ 0

状態の記述に'←'を使ったのは臨時の記法です(特に正式な記法はないと思います)*1

書き方の変種や修飾

'|-'で示す証明可能性は、証明を行う仕掛けである演繹系〈deduction system | 証明系〉が決まらないと定義できません。演繹系をSとして、「Sにより証明可能」は '|-S' を使えばいいでしょう。

  • x ≧0, y ≧0 |-S x + y ≧ 0

キーワード方式だと:

Given x ≧0, y ≧0
IsProvableBy S  x + y ≧ 0

By S はお尻のほうがいいか。

Given x ≧0, y ≧0
IsProvable x + y ≧ 0 By S

キーワードを使うと、“気分”と“見た目”が気になりだす。やはり、自然言語には言霊が宿るせいか?

'|='では、基本的には左側にモデルを書くのですが、何も書かないときがあります。

  • |= ∀x, y.(x + y ≧ 0)

実は、左が空白のときの解釈が場合により違うんですよ。ヤダナー。

  1. モデルをひとつに固定しているので、あえてモデルは書かない。
  2. 複数のモデルを想定するが、左側空白は、どのモデルに対しても成立することを意味する。

モデルがひとつであってもチャンと書くことにして、複数のモデルのどれでも成立するならワイルドカードの'*'を付けるとかすれば混乱は少ないでしょう。

  • N-model |= ∀x, y.(x + y ≧ 0)
  • * |= ∀x, y.(x + y ≧ 0)

モデルの集まりをMとして、左側にはモデルの集まりを書く約束なら:

  • {N-model} |= ∀x, y.(x + y ≧ 0)
  • M |= ∀x, y.(x + y ≧ 0)

左側にモデルの集まりを書く習慣はたぶんないと思うけど、「何も書かないで省略する」はたいていトラブルを招くんだよなー。

意味的帰結の書き方

ダブルターンスタイル'|='の左側にはモデルを書くので、論理式を書くことはできません。しかし、意味的判断で左側に論理式を書きたいことがあります。標準的記号がないので、僕は'|⇒'を使っています。

  • x ≧0, y ≧0 |⇒ x + y ≧ 0

これは、次の意味です。

  • いま考えているどんなモデルMと状態ρに対しても、 (M, ρ) |= x ≧0 かつ (M, ρ) |= y ≧0 ならば、(M, ρ) |= x + y ≧ 0 である。

論理式 A1, ..., An, B のあいだの関係 A1, ..., An |⇒ B は、通常は論理的帰結〈logical consequence〉と呼びます。しかし、これは意味的判断なので、意味的帰結〈semantic consequence〉と呼んだほうが適切でしょう。意味的帰結を伴意〈entailment〉ともいいます。次の記事を参照してください。

意味的帰結〈伴意〉を'|⇒'で表すと、左側に論理式を書けるようになりますが、今度は判断の根拠であるモデルの集まりが書けなくなります。右下添字かな。

  • x ≧0, y ≧0 |⇒M x + y ≧ 0

Mは、モデル(と状態)の集まりで、この意味的帰結を主張するときの根拠となったものです。こう約束すると、次の2つの書き方は同じ意味になります。

  1. M |= x + y ≧ 0
  2. |⇒M x + y ≧ 0

'|-' と '|=' は似てませんが、'|-' と '|⇒' は似た使い方ができます。左側に前提となる命題の並び、右下添字に判断の根拠となる仕掛けや集まりを書くことになります。'|=' は、'|⇒' を定義するための補助的なものと捉えたほうがいいような気がします。


関係しそうな過去記事:

*1:「型推論に関わる論理の概念と用語 その6:substitutionの記法」で色々な記法があることを書きました。状態〈束縛 | 付値〉と置換〈substitution | 代入〉は似てますが違う概念です。