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

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
ところで、アーカイブってけっこう便利ですよ。タクソノミーも作成中。今は疲れるので作っていません。

2016-07-20 (水)

モノイド自然変換とモノイド同値関手

| 11:19 | モノイド自然変換とモノイド同値関手を含むブックマーク

ジョン・バエズ(John C. Baez)が2010年に書いた短いノートに

というのがあります。このEveryoneって誰だよ? という気もしますが、まーともかく「誰でも」知っておくべき事として13個の定義が挙げられています。1番目は圏の定義で、13番目(最後)が圏のブレイド付きモノイド同値関手(ついでに対称モノイド同値関手も)です。そのひとつ前(12番目、最後から2番目)は、モノイド圏のあいだのモノイド同値(monoidal equivalence)関手です。

この記事では、バエズが12番目に取り上げたモノイド同値関手について紹介します。基本となるモノイド関手の概念と関連事項については次の記事で解説しています。

この記事でもモノイド関手の復習をします。

なお、この記事は、「自然演繹の再構築への道」で述べた計画の一環です。

内容:

  1. 各種のモノイド関手の呼び名
  2. ストライプ図の復習
  3. 状況設定
  4. モノイド自然変換
  5. モノイド同値関手

各種のモノイド関手の呼び名

モノイド関手にはいくつかの種類があります。単に形容詞なしで「モノイド関手」と言ったときに何を意味するかは人により違います。以下に、モノイド関手の種類を挙げます。

  1. 厳密モノイド関手(strict monoidal functor): F(A¥otimesB) = F(A)¥otimesF(B) などの法則が等式として成り立つ。
  2. 強モノイド関手(strong monoidal functor): F(A¥otimesB) ¥stackrel{¥sim}{=} F(A)¥otimesF(B) などの法則が同型として成り立つ。
  3. ラックス・モノイド関手(lax monoidal functor): F(A)¥otimesF(B) → F(A¥otimesB) などの法則を与える射が存在するが、同型とは限らない。
  4. 反ラックス・モノイド関手(oplax monoidal functor): F(A¥otimesB) → F(A)¥otimesF(B) などの法則を与える射が存在するが、同型とは限らない。

一時期(「緩関手、反緩関手、強関手、厳密関手とか、おぼえられねー」の頃)、"lax"を「緩」と訳してましたが、最近はカタカナ「ラックス」です。ちなみに、「おぼえられねー」悩みは、マッカーディのストライプ図により解消しました。

ラックス・モノイド関手と反ラックス・モノイド関手は、定義に登場する矢印の向きが逆になるという意味で双対です。反ラックス(oplax)の代わりに余ラックス(colax)を使うこともあります。laxにopだのcoだの付けるのではなくて、ラックス・コモノイド関手(lax comonoidal functor)がいいのではないか、という意見もあります。モノイド関手/コモノイド関手を使うなら、形容詞はラックス(lax)ではなくて弱(weak)でもいいかも知れません。

「強モノイド関手/弱モノイド関手/弱コモノイド関手」が一番辻褄があってる気がしますが、よく使われていると思われる「強モノイド関手/ラックス・モノイド関手/反ラックス・モノイド関手」を使うことにします。

モノイド関手/ラックス・モノイド関手とその実例」の注釈

ここで定義するモノイド関手は、強モノイド関手(strong monoidal functor)と呼ばれることがありますが、これが標準的なモノイド関手だと思われるので特に形容詞は付けないことにします。

と書きましたが、曖昧さを避けるために今回は形容詞を常に付けます

ストライプ図の復習

ラックス・モノイド関手は、2つのモノイド圏C, Dのあいだの関手Fの上に載る自然変換μ, εで構成された代数構造と考えたほうがいい、と「ラックス・モノイド関手について、もうちょっと」で注意しました。実際、自明なモノイド圏からモノイド圏Cへのラックス・モノイド関手はC内のモノイドになります。

マッカーディのストライプ図を使えば、モノイドとラックス・モノイド関手の類似性を視覚的に確認できます。ストライプ図については、「モノイド関手/ラックス・モノイド関手とその実例」で述べてますが、ここで復習しておきます。

この記事で採用する描画方向は ↓→ です。旗で示すならば:

次の図を見てください。

(1)は、モノイド乗法 m:A¥otimesA→A を描いたものです。ワイヤーがA、黒丸が乗法mです。(2)は、それに厚みを付けたもの。乗法は白丸になっています。(3)は、厚み付きワイヤーを心線(芯線)と青い関手シースとして描いたものです。これが、ラックス・モノイド関手 (F, μ, ε) の乗法 μA,B:F(A)¥otimesF(B)→F(A¥otimesB) を表します。(4)は、μA,Bを小さな黒丸で代表させたものです。

次は単位に関する図です。

乗法の場合と事情は同じです。(1)は、モノイドの単位 e:I→A の図ですが、その後はラックス・モノイド関手 (F, μ, ε) の単位 ε:I→F(I) を表します。

状況設定

CDをモノイド圏として、(F, μ, ε) と (G, ν, ι) を CDである2つのラックス・モノイド関手とします。この設定で、モノイド自然変換 ψ::(F, μ, ε)⇒(G, ν, ι):CD を定義したいのですが、状況設定をもう少し詳しく述べます。

C = (C, ¥otimes, I), D = (D, ¥otimes, I) とします。C, D はモノイド圏の構造全体の意味でも、台となる圏(underlying category)の意味でも使います(記号の乱用)。Cのモノイド積/単位対象と、Dのモノイド積/単位対象は別物なので、ほんとは別な記号で表すべきですが、同じ記号 ¥otimes, I を使い回しています(面倒だから)。

C, D は厳密とは限らないモノイド圏なので、それぞれに結合律子、左単位律子、右単位律子があります(律子(りつし)に関しては「律子からカタストロフへ」を参照してください)。これらの律子は明示されてませんが、必要があればそれらを α, λ, ρ で示します。Cの律子とDの律子は別物ですが、同じ記号 α, λ, ρ で書きます(面倒だから)。

F:CD は関手で、μ::¥otimes¥circ(F×F)⇒F¥circ¥otimes:C×CD は自然変換、εは I→F(I) in D という射です。εも自然変換と呼ぶことがありますが、定数関手 KI(A) = I からもうひとつの定数関手 KF(I)(A) = F(I) への自然変換と考えることができるからです。

μ::¥otimes¥circ(F×F)⇒F¥circ¥otimes が自然変換であることは次のように図示できます。青いストライブ内の2つのオダンゴは、f:A→B, g:C→D in C で、(F(f)¥otimesF(g));μB,D = μA,C;F(f¥otimesg) を示しています。

ラックス・モノイド関手の法則は、マッカーディのストライプ図で次のように描けます。

関手Fと自然変換μ, εに関して、この図を等式に書き下しましょう。律子 α, λ, ρ も考慮した形にします。

結合律 左辺:

(F(A)¥otimesF(B))¥otimesF(C)
  ↓ μA,B¥otimesF(C)
F(A¥otimesB)¥otimesF(C)
  ↓ μA¥otimesB,C
F((A¥otimesB)¥otimesC)
  ↓ F(αA,B,C)
F(A¥otimes(B¥otimesC))

結合律 右辺:

(F(A)¥otimesF(B))¥otimesF(C)
  ↓ αF(A),F(B),F(C)
F(A)¥otimes(F(B)¥otimesF(C))
  ↓ F(A)¥otimesμB,C
F(A)¥otimesF(B¥otimesC)
  ↓ μA,B¥otimesC
F(A¥otimes(B¥otimesC))

  • 結合律 等式:(μA,B¥otimesF(C));μA¥otimesB,C;F(αA,B,C) = αF(A),F(B),F(C);(F(A)¥otimesμB,C);μA,B¥otimesC

左単位律 左辺:

I¥otimesF(A)
  ↓ε¥otimesF(A)
F(I)¥otimesF(A)
  ↓μI,A
F(I¥otimesA)
  ↓F(λA)
F(A)

左単位律 右辺:

I¥otimesF(A)
  ↓λF(A)
F(A)

  • 左単位律 等式: (ε¥otimesF(A));μI,A;F(λA) = λA

右単位律も同様で、

  • 右単位律 等式: (F(A)¥otimesε);μA,I;F(ρA) = ρA

(G, ν, ι) がもうひとつのラックス・モノイド関手なら、文字を置き換えただけの次の等式が成立します。

  • 結合律 等式:(νA,B¥otimesG(C));νA¥otimesB,C;G(αA,B,C) = αG(A),G(B),G(C);(G(A)¥otimesνB,C);νA,B¥otimesC
  • 左単位律 等式: (ι¥otimesG(A));νI,A;G(λA) = λA
  • 右単位律 等式: (G(A)¥otimesι);νA,I;G(ρA) = ρA

モノイド自然変換

ラックス・モノイド関手のあいだのモノイド自然変換(monoidal natural transformation)は、モノイドの準同型写像の類似物です。気分としては、次の“比例式”が成立します。

  • モノイド : モノイドの準同型写像 = ラックス・モノイド関手 : モノイド自然変換

(A, m, e), (B, n, i) がモノイド圏内の2つのモノイドとして、f:A→B がモノイドの準同型写像なら、次の等式が成立します。

  • (f¥otimesf);m = m;f
  • e;f = i

絵に描けば次のようです。

これをヒントに、モノイド自然変換 ψ::(F, μ, ε)⇒(G, ν, ι) の絵を描きましょう。ここで、(F, μ, ε) と (G, ν, ι) はラックス・モノイド関手です。絵で、青い関手シースがFを表し、紫(青に赤を上塗り)の関手シースがGを表します。白いオダンゴがψです。

絵を見ながら等式に書き下します。

  • ψA¥otimesψBA,B = μA,BA¥otimesB
  • ε;ψI = ι

これらの等式が、自然変換 ψ::F⇒G:CD がモノイド自然変換であるための条件です。

ψがモノイド自然変換で、すべての成分 ψA:F(A)→G(A) in D が同型(可逆)であるとき、モノイド自然同型(monoidal natural isomorphism)と呼びます。(F, μ, ε) と (G, ν, ι) がモノイド自然同型で結ばれるとき、これらのラックス・モノイド関手は同じだとみて差し支えありません。

モノイド同値関手

DCがモノイド圏で、F:CD, G:DC がラックス・モノイド関手とします。ラックス・モノイド関手どうしの結合は再びラックス・モノイド関手になりますから(これは証明を要することですが)、G¥circF:CC, F¥circG:DD はラックス・モノイド関手です。

¥circは、関手の反図式順結合です。常に図式順結合を使っている僕が、ここだけ反図式順にしているのはちょっとした事情がありますが、まーそれはいいとしましょう。

FとGが次の等式を満たすとき、互いに(inverse)になります。

  • G¥circF = IdC
  • F¥circG = IdD

しかし、逆は強すぎる条件なので、イコールをモノイド自然同型に弱くします。この場合は、互いに弱逆(weak inverse)となります。つまり、FとGが互いに弱逆とは:

  • モノイド自然同型 ψ::G¥circF⇒IdC:CC が存在する。
  • モノイド自然同型 φ::F¥circG⇒IdD:DD が存在する。

弱逆を持つようなラックス・モノイド関手をモノイド同値関手(monoidal equivalence functor)と呼びます。冒頭で引用したバエズの定義では、強モノイド関手に限定してモノイド同値を定義していますが、定義の形はラックス・モノイド関手でも強モノイド関手でも変わりません。要するに、弱可逆な関手です。

2つのモノイド圏が、弱可逆なモノイド関手(ラックス・モノイド関手または強モノイド関手)で結ばれているなら、その2つのモノイド圏を区別する必要がないことを意味します。あるモノイド圏Cが扱いにくいとき、同値なモノイド圏Dを代わりに使っても、本質的な差異は生じないのです。

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

2016-07-19 (火)

自然演繹の再構築への道

| 10:04 | 自然演繹の再構築への道を含むブックマーク

5日前の記事「自然演繹はちっとも自然じゃない -- 圏論による再考」において、次のように書きました。

自然演繹に対する再考は出来たと思います。でも、再構築には至っていません。

...[snip]...

いずれ別記事としてストリング図と多圏を準備した上で、自然演繹の再構築ができたらいいな、と思っています。

目論見としては出来ると思ってます。が、実際に遂行する気力が続くか? はまた別な問題です。自然演繹の再構築に何が必要かは見当がついているので、それについて書いておきます。

まず、セマンティクスとしては多圏(polycategory)を使いたい -- 長年、言及するだけで定義も構成も不十分という状態なので、多圏をちゃんと構成したいですね。

モノイド圏Cから、対応する多圏Poly(C)を構成するのですが、いきなり多圏は難しいです。準備として、Cから別なモノイド圏Spid(C)を作ります。Spid(C)はモノイド圏Cのスパイダー圏と呼んでいるものです。

もとのモノイド圏Cとそのスパイダー圏(これもモノイド圏)Spid(C)の関係を調べるには、モノイド関手、モノイド自然変換、モノイド同値などの道具を揃える必要があります。また、モノイド圏における一般化された結合律や単位律も使います。ここらは、モノイド圏の一般論に関する準備となります。

スパイダー圏Spid(C)が構成できて、その基本性質が明らかになれば、多圏Poly(C)の構成は容易です。もとのモノイド圏Cが対称なら、Poly(C)にも対称性を持ち込めるし、Cが対称でなくてもPoly(C)は作れます。

セマンティック駆動の立場では、圏/多圏を作っておいて後から構文構造である形式的体系を作ります。したがって、形式的体系は一意には決まりません。推論規則や公理の選び方には恣意性がある、ということです。とはいえ、何かを選んで形式的体系(演繹系、論理システム)を組み立てる必要があります。複数の形式的体系を作ってもいいかも知れません。

今まで述べた手順をまとめると:

  1. モノイド圏の一般論の準備
    1. モノイド同値 →「モノイド自然変換とモノイド同値関手
    2. モノイド圏が作る2-圏
    3. 一般化された結合律と単位律
  2. モノイド圏からのスパイダー圏の構成
  3. モノイド圏からの多圏の構成
  4. 形式的体系の構成

これらの大項目をさらに細分する必要があるかも知れません*1が、項目を実行した記事が書けたら、ここからリンクを張ることにします。

*1[追記 date="2016-07-20"]実際に、1番目を細分しました。[/追記]

2016-07-14 (木)

自然演繹はちっとも自然じゃない -- 圏論による再考

| 13:01 | 自然演繹はちっとも自然じゃない -- 圏論による再考を含むブックマーク

自然演繹は、その名の通りに「自然で分かりやすい」と言われたりします。僕は、そうは思いません。むしろ「不自然で分かりにくい」と感じます。導入規則と除去規則のあいだに綺麗な対称性がある、と言う人がいます。僕にはどこが綺麗か分かりません。無理クリに対称に見せてるだけで、むしろ歪んでいて汚ないじゃないか、と思います。

自然かどうか、綺麗かどうかは主観の問題ですから、議論しても不毛です。しかし、代替の定式化を示して、それを自然演繹と比較することにより、自然演繹を相対化することは出来ます。やってみます。

この記事の内容は、ここ10年くらい思っていたことです。口頭でしゃべったことはありますが(最後の節を参照)、まとまった記述はなかったので、割と丁寧に書きました。その結果、けっこう長大な記事となりました。

論理や圏論を学ぶには、まっとうな教科書を手元に置くのがよいでしょう。その教科書が主治医とするなら、僕の記事はちょっと変わったセカンドオピニオン程度の参考になれば幸いです。

内容:

  1. 自然演繹はどこがダメなのか
  2. 自然演繹の推論図の例
  3. この記事の方針と記号の約束
  4. 自然演繹の推論図一式
  5. 暗黙の前提もちゃんと描くと
  6. 自然演繹からシーケント計算へ
  7. 証明オブジェクトとリーズニング
  8. セマンティック駆動な圏的意味論
  9. 圏論的に自然な演繹とは
  10. 存在が保証された射
  11. 圏論的に自然なリーズニングの例 その1
  12. 表現は色々あっても実体は同じ
  13. 圏論的に自然なリーズニングの例 その2
  14. 僕が思っていたこと/思っていること

自然演繹はどこがダメなのか

僕が自然演繹はダメだと思う理由は次の2点です。

  1. 自然演繹で通常使われる推論図/証明図の図示法は、できが悪く分かりにくい。
  2. セマンティクス(意味論)との対応を取りにくい。

図示法の問題点をもっと詳しく言うと:

  1. 本来、時間に沿って変化するアニメーションであるものを、無理に1枚の静止画で描くので、意味不明となる。
  2. 図に描かれてない、暗黙の前提(不可視な了解事項)が多すぎる。
  3. 証明を進めるために、証明図の局所的な追加変更だけでは済まず、全面描き換えが発生する。

例えば、含意導入規則の推論図は次のように描かれます。


 [A]
 ・
 ・
 ・
 -----
 A⊃B

この図を見て含意導入を理解できるのは既に知っている人で、はじめての人がこの絵をスンナリ理解できるとは考えにくいです。

含意導入規則は、証明図の時間的変化のことですから、変化のbeforeとafterがあります。ですから、少なくとも2枚の絵により表現すべきことです。

before

  A
 ・
 ・
 ・
 -----
  B

after

 [A]
 ・
 ・
 ・
 -----
  B
 -----
 A⊃B

もちろん、縦に並んだ点々や、afterのAをブラケットで囲んでいることなどは別途説明が必要です。

自然演繹の推論図の例

自然演繹の図示法は「できが悪く分かりにくい」と言ったのですが、とりあえずは現状の図示法がどんな感じかを紹介します。インターネット上で見つけた自然演繹に関する解説から、含意の導入と選言の除去に関する規則の図(推論図)を見てみましょう。

http://www.h6.dion.ne.jp/~ooya/Kougiroku/Ronri/Ronri10.pdf より

http://web.sfc.keio.ac.jp/~mukai/modular/gentzen-NK.pdf より

http://logicmanual.philosophy.ox.ac.uk/jsslides/ll6p.pdf より

細部では差がありますが、図示法の基本は共通していることが分かるでしょう。

念のためにお断りしておきますが、僕は自然演繹の伝統的な図示法そのものが問題を抱えていると思っているのであって、上記に挙げた解説やまとめは優れたものです。誰がやったところで、伝統的な図示法を分かりやすく解説することには限界があります。だって、本質的に分かりにくいんだもの。

この記事の方針と記号の約束

ここでは、自然演繹とシーケント計算は事実上同じだとみなします。自然演繹とシーケント計算は表現方法が違うだけで、同じモデルを持つということです。

ではモデルとは何でしょうか。ここでは、直和を持つデカルト閉圏を論理システムのモデルとします。むしろ、デカルト閉圏が先にあり、それの記号的表現として論理システムを考えます。意味論(セマンティクス)を先に考えて、構文論を後から付けるスタイルで、僕が「セマンティック駆動」と呼んだ*1やり方です。

デカルト閉圏から出発するセマンティック駆動な計算については既に述べています。

  1. 演繹系とお絵描き圏論
  2. 圏論からシーケント計算へ
  3. 圏論の筆算としてのシーケント計算
  4. シーケント計算と圏論(続きみたいな)
  5. セマンティック駆動な圏的ラムダ計算とシーケント

必要があれば上記の記事群を参照してもらうことにして、この記事で使う記号を約束しておきます。

論理結合子としては、∧、∨、⊃ を使います。含意は → ではなくて ⊃ を使います。論理定数は⊥(矛盾、偽)とI(真)です。直和を持つデカルト閉圏との関係は次のようです。

論理 圏論 ひとこと
A∧B A×B 連言、直積
A∨B A + B 選言、直和
A⊃B BA 含意、指数
0 偽、始対象
I 1 真、終対象

圏論からシーケント計算へ」と同じ記号にしています。否定(¬)はありませんが、必要なら、¬A は A⊃⊥ の略記だとします。

矢印 → は、シーケントの左右区切りに使います(含意ではありません!)。自然演繹の証明図は、シーケントと同じ意味だとします。つまり:

  A
 ・
 ・
 ・
 ---
  B

このような証明図があるとき、それを横方向にして A → B と書こう、ということです。

この対応関係をよりハッキリさせるために、証明図の一部省略を表す点々を縦向き矢印で書くことにします。A, B → C というシーケントに対応する自然演繹証明図は次のように書きます(描きます)。

   A  B
  -----
    ↓
    B

縦向き矢印↓の部分には、なにやらあるかも知れないが、その詳細は問題にしない、ということです。

自然演繹の推論図一式

自然演繹の推論図/証明図のメリットは、テキストでも描けることです。以下に、伝統的な自然演繹の8つの推論図を列挙します。

 A    B
 -------[∧導入]
  A∧B

 A∧B
 -----[∧除去1]
  A

 A∧B
 -----[∧除去2]
  B

   A
 -----[∨導入1]
 A∨B

  B
 -----[∨導入2]
 A∨B

       A    B
      ---  ---
      ↓   ↓
 A∨B  Y   Y
 -------------[∨除去]
       Y

  [A]
  ---
  ↓
  B
 -----[⊃導入]
 A⊃B

 A⊃B  A
 --------[⊃除去]
    B

これらの推論図が、セマンティックに(意味論から)導けることを示し、セマンティック駆動なシーケント計算との対応を付けることがこの記事の目的です。

暗黙の前提もちゃんと描くと

再度、http://logicmanual.philosophy.ox.ac.uk/jsslides/ll6p.pdf の図を引用します。

他の資料の図では付いてない縦の点々が付いてます。この点々をちゃんと描くことにします。さらに、点々の上側にあるはずの仮定を描きます。点々を下向き矢印で代用すると次のようになります。

 Γ   Δ
 ---  ---
 ↓   ↓
 A    B
 -------[∧導入]
  A∧B

 Γ    A    B
 ---  ---  ---
  ↓  ↓   ↓
 A∨B  Y   Y
 -------------[∨除去]
       Y

ここで、ΓとΔは、いくつか(0個かもしれない)の論理式の並びを1文字で表現したものです。

自然演繹はどこがダメなのか」において、「本来、時間に沿って変化するアニメーションであるものを、無理に1枚の静止画で描くので、意味不明となる」と指摘しました。であるならば、ひとつの推論規則を、beforeとafterに分けて描くことにすればよいでしょう。(次の図で、レイアウトのバランスを取るために、縦向き矢印を余分に挿入しています。)

[∧導入 before]

 Γ   Δ
 ---  ---
 ↓   ↓
 A    B

[∧導入 after]

 Γ   Δ
 ---  ---
 ↓   ↓
 A    B
 -------
   ↓
  A∧B

[∨除去 before]

 Γ    A    B
 ---  ---  ---
  ↓  ↓   ↓
 A∨B  Y   Y

[∨除去 after]

 Γ
 ---
  ↓
 A∨B
 ----
  ↓
  Y

after側の詳細を気にしないなら、中間部分を矢印に押し込めて次のようになります。

[∧導入 before]

 Γ   Δ
 ---  ---
 ↓   ↓
 A    B

[∧導入 after]

 Γ   Δ
 --------
   ↓
  A∧B

[∨除去 before]

 Γ    A    B
 ---  ---  ---
  ↓  ↓   ↓
 A∨B  Y   Y

[∨除去 after]

 Γ
 ---
  ↓
  Y

縦方向の書き方から横方向の書き方にして、before/afterを上下の段で表すなら:

before Γ→ A   Δ → B
 ========================[∧導入]
after  Γ,Δ → A∧B

before Γ → A∨B   A → Y   B → Y
 ====================================[∨除去]
after     Γ → Y

自然演繹の推論図/証明図と区別するために、横線を二重(イコールの並び)にしました。

自然演繹からシーケント計算へ

もうお分かりと思いますが、自然演繹の推論図のbefore/afterを明示的にちゃんと書いて、よりコンパクトにすると、結局はシーケント計算になります。先に挙げた自然演繹の推論図に対応するシーケント計算の8つの推論図は次のようになります。上段がbefore、下段がafterです。

 Γ→ A   Δ → B
 =================[∧導入]
 Γ,Δ → A∧B

 Γ → A∧B
 ===========[∧除去1]
 Γ→ A

 Γ → A∧B
 ===========[∧除去2]
 Γ→ A

 Γ → A
 ===========[∨導入1]
 Γ→ A∨B

 Γ → B
 ===========[∨導入2]
 Γ→ A∨B

 Γ → A∨B   A → Y   B → Y
 =============================[∨除去]
    Γ → Y

 Γ,A → B
 ===========[⊃導入]
 Γ → A⊃B

 Γ → A⊃B  Δ → A
 ====================[⊃除去]
    Γ,Δ → B

シーケントに書き換えることにより、スペースを必要とする縦方向の図が横方向1行で書けます。また、before/afterを上段/下段に分離するので「無理に1枚の静止画で描くので、意味不明」な問題は解決します。暗黙の前提をΓなどで明示しているので「図に描かれてない、暗黙の前提(不可視な了解事項)が多すぎる」も解決します。

シーケント計算の証明図は、自然演繹の証明図の描き換えを上段と下段として記録するので、シーケント計算の証明図の全面描き変えは発生しません。ツリー状の図形が上から下、または下から上に成長していくだけです。これで、自然演繹の証明図の三番目の問題「証明図の局所的な追加変更だけでは済まず、全面描き換えが発生する」が解決します。もっとも、自然演繹レベルの全面書き換えの前後を簡略化して記録しているだけなので、描画の手間はたいして減りません。

こう言うと、シーケント計算はいいことずくめのようですが、欠点もあります。自然演繹の証明は、それを描く中間段階を見なくても、最後に得られた証明図だけ見れば、証明の正しさを判定できます。一方、シーケント計算では、最後に得られたシーケント(最下段のシーケント)を見ても、証明全体の正しさを検証できません。これは、シーケント計算の証明図の上段から下段に移るとき、情報を落としているからです(自然演繹では情報が累積されます)。実用上は、証明の正しさの証拠となる単一のデータがあったほうが便利です。

証明オブジェクトとリーズニング

前節の最後で言った「証明の正しさの証拠となる単一のデータ」を証明オブジェクト(proof object)と呼びます。証明オブジェクトとして使われるデータの種類は次のモノがあります。

  1. ラムダ計算の項
  2. 自然演繹の証明図
  3. ストリング図

意味論にデカルト閉圏を使うなら、この3つは実際は同じものです。いずれも、デカルト閉圏の射を表現する形式なのです。「ラムダ計算の項」と「自然演繹の証明図」が同じであることを具体的に示せば、それがカリー/ハワード対応になります。

「証明」という言葉が、証明オブジェクトというデータを表すこともありますが、証明オブジェクトを作り出す行為を「証明」と呼ぶこともあります。この2種の「証明」はシッカリ区別すべきです。「証明オブジェクト」と「証明行為」とすれば区別できますが、もっと明確に区別するために、証明行為をリーズニング(reasoning)と呼ぶことにします。

すると、次のことが言えます。

  • 自然演繹では、証明オブジェクトを証明図として図示する。リーズニングを図示する方法はなくて、リーズニングの扱いは曖昧なままである。
  • シーケント計算では、リーズニングを証明図として図示する。証明オブジェクトは定義されてなくて、証明オブジェクトは無視されたままである。

伝統的論理のなかでは、証明オブジェクトとリーズニングの両方をちゃんと記述する方法がないのですよね。ちゃんと書く(描く)と、情報が多いので冗長/煩雑/めんどくさい、って事情はあります。

型理論では、型判断(typing judgement)をシーケントとして、ラムダ項の型付けを証明図風に描きますが、これは証明オブジェクト(ラムダ項)とリーズニング(型付けの行為)の両方を記述していると言えます。

セマンティック駆動な圏的意味論

セマンティック駆動な立場では、デカルト閉圏(やその拡張)が先にあり、その圏を記述・計算するための記号的体系を後から準備します。Cがモデル(意味領域)となる圏だとすると、Cの対象そのものを原子論理式(基本命題)として採用します。なお、論理式と命題はここでは同義語とします。

論理記号 ∧, ∨, ⊃, ⊥, I はそれぞれ、圏Cの 直積、直和、指数、始対象、終対象 と解釈します。“基本命題=Cの特定の対象”から論理記号を使って組み立てられた論理式は、Cの対象と同一視します。

命題(論理式)をカンマで区切った列 A1, ..., An は、A1∧...∧An と解釈します。そして、シーケント A1, ..., An → B の意味は、Cのとある射 f:A1∧...∧An→B in C のことです。「セマンティック駆動な圏的ラムダ計算とシーケント」の「型シーケント」も参照してください。

もっと正確な議論をしたいなら、複圏(オペラッド)、多圏を導入する必要がありますが、複圏/多圏の話題は先延ばしになっています。

命題(Cの対象)をカンマで区切った列をΓとして、シーケントの一般的な形は Γ → B となります。カンマをCの直積だと解釈して、シーケントはCの射を表すことになります。Γが空列のときは、I→B in C (Iは終対象)という射とします。

シーケントを圏の射とみなす話は、次の記事でもう少し詳しく書いています。

圏論的に自然な演繹とは

今までに述べたことをまとめると:

  1. 証明オブジェクトに焦点を合わせ、リーズニングについては曖昧イイカゲンにしてしまった定式化が自然演繹。
  2. リーズニングに焦点を合わせ、証明オブジェクトは無視してしまった定式化がシーケント計算。
  3. 「どこに注目するか?」と表現方法は異なるが、自然演繹もシーケント計算もやっていることは同じ

演繹系とお絵描き圏論」で述べたように、「TEH・自然演繹」や「THE・シーケント計算」があるわけではないので、定式化を微妙に変えるだけでいくらでも変種(バリアント)を作れます。実際に無闇と変種があるので、論理のお勉強が博物学・分類学になる傾向があるわけです(このことは「論理とはなにか?」でも指摘しました)。そして、「論理におけるさまざまな「矢印」達」で述べたように、用語と記号もグジャグジャです。

型理論では、ラムダ式(ラムダ計算の項)を証明オブジェクトとして、シーケント計算風の型付け(typing)の導出ツリー図でリーズニングを表しています。証明オブジェクトとしてラムダ式に拘る必要もないので、圏論で通常使われる記法による式(expression)を証明オブジェクトにしてもいいでしょう。

圏論で通常使われる記法とは:

  1. 射 f:A→B と g:B→C の結合(composion)は f;g:A→C と書く。
  2. 射 f:A→B と g:C→D の直積(デカルト積)は f∧g:A∧C→B∧D と書く。
  3. 射 f:A→Y と g:B→Y のデカルト余ペアリングは [f, g]:A∨B→Y と書く。

記号を増やしたくないので、「圏の直積/直和/指数」も論理記号「∧/∨/⊃」で表すことにします。三番目のデカルト余ペアリングは、デカルトペアリング <f, g>:X→A∧B の双対で、次の等式が成立します。

  • <f, g> = ΔX;(f∧g) (ΔXは対角)
  • [f, g] = (f∨g);∇Y (∇Yは余対角)

シーケント A1,...,An → B では、左側がカンマで句切られた列なので、結合が少し変形されて次のようになります。

  • f:A1∧...∧An→B と g:B∧C1∧...∧Cm→D の結合を f;Bg:A1∧...∧An∧C1∧...∧Cm→D とする。

f;Bg という記法の意味は、(f∧idC1∧...∧Cm);g です。絵で描けば次のよう。

Cデカルト閉圏なので、カリー同型があります。

  • C(X∧A, B) ¥stackrel{¥sim}{=} C(X, A⊃B)

この同型の左から右に向かうカリー化写像を ΛX A B (大文字ラムダ)とします。下付き添字内の区切りにカンマではなくて空白を使っているのは、カンマが直積の意味で使われているからです -- A,B = A∧B。

結合、直積、余ペアリング、カリー化という圏論的オペレーションをリーズニングの基本ステップとみなすと、次のような4つの基本リーズニング図が得られます。

 f:Γ → A  g:A,Δ → B
 =======================[comp 射の結合]
 f;Ag:Γ,Δ → B

 f:Γ → A  g:Δ → B
 =====================[prod 射の直積]
 f∧g:Γ,Δ → A∧B

 f:A → Y  g:B → Y
 ===================[copair 射の余ペアリング]
 [f, g]:A∨B → Y

 f:Γ,A → B
 ===================[curry カリー化]
 ΛΓ A B(f):Γ→A⊃B

自然さは主観的です。既知の事項や過去の経験とのギャップが少ないと「自然だ」と感じるのでしょう。「既知の事項や過去の経験」は人ごとに違うので、自然さも人ごとに違うことになります。デカルト閉圏の知識と経験があるなら、上記の4つのオペレーションを基本とする演繹系は自然なものとなるでしょう。

僕が言いたいことは、伝統的な自然演繹の“自然さ”に強い根拠はない、ということです。対称だ、綺麗だ、というのも、気分と趣味の問題に過ぎません。例えば、モデルとなるデカルト閉圏ありきの立場なら、伝統的な自然演繹は使い勝手が悪く、「自然でも対称でも綺麗でもない」と感じることでしょう。この感覚が、この記事のタイトルの由来です。

存在が保証された射

Cが直和を持つデカルト閉圏ならば、存在が保証された対象や射があります。例えば、終対象かつ直積の単位である1、始対象かつ直和の単位である0は存在が保証された対象です。この2つの対象は、本記事内では論理定数I、⊥で表現されています。

どんな圏であれ、対象Aに対する恒等射 idA:A→A の存在は保証されます。終対象、始対象があるので、!A:A→I、θA:⊥→A も存在が保証されています。このような、在ると分かっている射を列挙しましょう。

記号 呼び名 プロファイル ひとこと
idA id A→A 恒等射
!A term A→I 終対象への唯一射
θA init ⊥→A 始対象からの唯一射
π1A B proj1 A∧B→A 直積の第1射影
π2A B proj2 A∧B→B 直積の第2射影
ι1A B inj1 A→A∨B 直和の第1入射
ι2A B inj2 B→A∨B 直和の第2入射
λA lunit I∧A→A 左単位律子
ρA runit A∧I→A 右単位律子
αA B C assoc (A∧B)∧C→A∧(B∧C) 結合律子
σA B symm A∧B→B∧A 対称
ΔA diag A→A∧A 対角射
A codiag A∨A→A 余対角射
evA B ev (A⊃B)∧A→B 評価射

律子(りつし)に関しては「律子からカタストロフへ」を参照してください。

これらの射は、シーケント計算で言う公理シーケントとして使うことができます。例えば idA は、A → A というシーケントです。公理と基本リーズニング規則(シーケント計算の推論規則)という二本立てが嫌なら、公理シーケントは上段が空であるリーズニング規則とみなすことができます。

    *
 ========[id]
  A → A

上段のアスタリスクは、「何もない」を明示する目印です。

対称性を表す射 σA B:A∧B→B∧A をリーズニング規則にするなら、

       *
 ==============[symm]
  A∧B → B∧A

A∧B は A,B とカンマで書いてもいいので、

       *
 ==============[symm]
  A,B → B∧A

でもかまいません。

あるいは、いわゆる“構造規則”として定式化する手もあります。

 Γ,A,B,Δ → C
 ===============[exch]
 Γ,B,A,Δ → C

これは、換(exchange)構造規則です。

圏論的に自然なリーズニングの例 その1

実は、直積の対称性 A∧B → B∧A は、公理シーケントとして仮定する必要はなく、リーズニングで導き出すことができます。このとき、次の減(contraction)構造規則は仮定します。

 Γ,A,A,Δ → C
 ===============[cont]
 Γ,A,Δ → C

対角射 ΔA:A→A∧A の存在が減(contraction)構造規則の根拠です。

A∧B → B∧A を導く(作り出す)リーズニングは次のようになります。

      *                   *
 ==========[proj2]  ===========[proj1]
 A∧B → B           A∧B → A
 ==============================[prod]
 A∧B,A∧B → B∧A
 ==================[cont]
   A∧B → B∧A

上記のリーズニング図がリーズニング規則[symm]の定義になっていることは、デカルト閉圏Cにおいて次の等式が成立することに相当します。

  • σA B = ΔA∧B;(π2A B∧π1A B)

リーズニング図の各段階における証明オブジェクトの式を書いてみると、このことが明らかになります。

      *                   *
 ==========[proj2]  ===========[proj1]
    π2A B             π1A B
 ==============================[prod]
      π2A B∧π1A B
 ====================[cont]
 ΔA∧B;(π2A B∧π1A B)

リーズニングの結果である最下段の証明オブジェクト ΔA∧B;(π2A B∧π1A B) を、自然演繹の証明図風に描くと次のようになります。

       A∧B
 --------------------[コピー]
 A∧B           A∧B
 -----[∧除去2] -----[∧除去1]
  B               A
 -------------------[∧導入]
       B∧A

一番上の横線である[コピー]は、上段のモノを2つに増やすことです。この[コピー]は、最後のリーズニングステップである減(contraction)構造規則によって追加されたことに注意してください。

頑張って、自然演繹の証明図(の類似物)を証明オブジェクトとするリーズニング図を描いてみましょうか。

     *                 *
  ========[proj2]  ===========[proj1]
    A∧B              A∧B
    -----             -----
      B                 A
  =============================[prod]
     A∧B        A∧B
     -----      -----
       B          A
     ---------------
           B∧A
  =========================[cont]
          A∧B
    -----------------
     A∧B        A∧B
     -----      -----
       B          A
     ---------------
           B∧A

こういう複合的な図は、場所を取るしめんどくさいので誰も描こうとしません。その結果、自然演繹ではリーズニングが暗黙的曖昧に扱われ、シーケント計算では証明オブジェクトがハッキリせず、自然演繹とシーケント計算の関係もモヤモヤのままとなります。残念なことです。

表現は色々あっても実体は同じ

直和を持つデカルト閉圏Cがありまして …… という所から話を始めると、式や絵による表現は色いろあるよね、ってことになります。

例えば、直積の第1射影 π1A B:A∧B→A は、自然演繹の推論図/証明図風に描けば次のようです(もう何度も出しました)。

  A∧B
 -----[π1]
   A

ストリング図なら次のよう。

シーケント風なら、

  • A∧B → A

単一の命題で書けば、

  • A∧B⊃A

型付きラムダ式で書くなら、

  • λ(x, y):A∧B.x

これらはいずれも“証明オブジェクト=圏Cの射の表現”なんです。既存の証明オブジェクトを加工したり組み合わせたりして新しい証明オブジェクトを作り出す行為・過程がリーズニングですけど、リーズニングにも色々な表現があります。

感動か効率性か」に次のように書きました:

「同じもの」とは、同じ意味論的な対象物を指していて、表現としての構文が違うだけ、ということです。同じ意味論的な対象物とは、デカルト閉圏やその変形・拡張のことです。そうであるなら、同じ対象物に対する異なる構文を異なるままにしておく意義ってあるんでしょうか?

...[snip]...

そろそろ、歴史的な経緯は無視して、記法・用語法・定式化を統合してもいいんではないでしょうか。計算論と型理論と論理を別々に勉強して、それでやっとカリー/ハワード対応ではあまりにも大変過ぎます! 歴史や伝統に拘らなければいくらでもショートカットはあるでしょうに。

歴史や伝統を完全に無視するのは行き過ぎですが、「実体は同じ」だと知って、表現の多様性に惑わされないことも大事です。

圏論的に自然なリーズニングの例 その2

圏論的に自然なリーズニングをベースにしたとき、伝統的な自然演繹のリーズニングがどう書けるか、連言(∧)の除去規則と含意(⊃)の除去規則を例としてやってみます。

              A → Y   B → Y
             =================[copair]
 Γ → A∨B    A∨B → Y
 ========================[comp]
   Γ → Y

これは、伝統的な[∨除去]規則になります。証明オブジェクトとしての式も一緒に書くと次のようです。

              g:A → Y   h:B → Y
             =====================[copair]
 f:Γ → A∨B   [g, h]:A∨B → Y
 ================================[comp]
   f;[g, h]:Γ → Y

念のため、証明オブジェクトとして自然演繹の証明図風の図を使ったリーズニングも描いておきましょう(めんどくさいけど)。分かりやすいように、縦矢印の横に射の名前・式も添えておきます。

                 A     B
                ---   ---
               g↓   h↓
                 Y     Y
             ===============[copair]
     Γ           A∨B
     ---          ----
    f↓     [g, h]↓
    A∨B           Y
 ========================[comp]
           Γ
           ---
          f↓
          A∨B
          -----
     [g, h]↓
            Y

次は含意(⊃)の除去です。証明オブジェクトも添えたリーズニング図の1枚だけにします(色々描くの疲れた)。

 f:Γ → A⊃B  g:Δ → A                 *
 ========================[prod]  =================[ev]
 f∧g:Γ,Δ → (A⊃B)∧A         ev:(A⊃B)∧A → B
 =================================================[comp]
    (f∧g);ev:Γ,Δ → B

これって、伝統的な[⊃除去]規則になってるでしょ。

僕が思っていたこと/思っていること

自然演繹の証明図は静止画じゃダメ、アニメーションさせなきゃ!」とは、ずーっと思っていることです。2009年あたりにやっていたセミナーでは、そのアニメーションをホワイトボード上で実演していました。その状況を文字で伝えようとした次の記事では、「書き換える前書き換えた後もっと書き換えた後」のような見出し付きで何枚も証明図を出しています。

いわばパラパラ漫画の手法ですが、次の記事もパラパラ漫画=紙芝居で、絵や式の時間的変化を表現しようと試みています。

比較的最近(2016年2月)も、絵を描く様〈さま〉を連続的に写真に撮って証明オブジェクトの構成過程(リーズニング)を記録してみる実験をしてみたり。

ソフトウェアを使えば、ホワイトボードや紙を使わないでアニメーションを実現できるはずです。それをやるソフトウェアといえば -- 証明支援系ですよね。でも、現状の証明支援系のユーザーインターフェイスは、証明オブジェクトとリーズニングの可視化としてはとても貧弱な段階で不満があります。

Coqの証明ゲームの表側と裏側 (誰も書かないCoq入門以前 4)」より:

  • Coqシステムは、そして自分は、いったい何をやっているんだ?
  • これが証明って、いったい何でだ?

こういう疑問を払拭できないのは、CoqのUIが貧弱なせいもあると思います。眼前の敵=モンスター=ゴールだけを表示するのは、バトルに没入するにはいいかも知れませんが、全般的な戦況が読めないのです。証明の現状を俯瞰的に眺めたいとか、出来上がった証明=終わった戦いを(時系列ではなくて)構造的に視覚化したいとかの要望に応える機能がありません。

Isabelleでも不満足な事情は同じです。Globularはなかなか良い視覚化のUIを持ってますが、別な意味で難しいソフトウェアです。と、そんな現状なので、ホワイトボードや紙から離れるのはまだ難しそうです。

この記事のサブタイトルを「圏論による再考」と付けました。自然演繹に対する再考は出来たと思います。でも、再構築には至っていません。自然演繹の圏論による再構築とはどんなものでしょうか?

まず、証明オブジェクトです。どんな種類の証明オブジェクトを選ぶかは多分に好みの問題ですが、僕はストリング図がいいと思います。ストリング図は、自然演繹の証明図にもラムダ式にも容易に変換できるし、視覚的直感に訴えます。「直感」というと厳密性に欠けるようですが、ストリンググラフにより組み合わせ構造を抽出できます。

証明オブジェクトとしてストリンググラフを使ったとき、リーズニングはグラフ書き換え(graph rewriting)となります。

この記事では、論理システム(論理を行うための形式的体系)のモデルとして直和を持つデカルト閉圏を使いましたが、もっと精密なモデル化には多圏(polycategory)が必要です。

ストリング図や多圏の話をこの記事に入れようかとも思いましたが、あまりにも長大になるのでやめました。いずれ別記事としてストリング図と多圏を準備した上で、自然演繹の再構築ができたらいいな、と思っています。

*1:セマンティクス駆動のほうが正しい気もしますが、語呂からセマンティックを使いました(セマンティックWebなんて言葉もあったりしたので)。semantic-drivenも誤用ではないようです。

mandel59mandel59 2016/07/19 11:12 この話を読んで、 Deep inference を思い出しました。“It is a methodology for designing proof formalisms that generalise Gentzen formalisms, i.e., the sequent calculus and natural deduction.” (http://alessio.guglielmi.name/res/cos/) ってことで、目指す方向性は違うのかもしれませんが、自然演繹の再構築という点では似た話に思えます。

m-hiyamam-hiyama 2016/07/19 19:42 mandel59さん、
Deep inferenceに関する情報をありがとうございます。
http://alessio.guglielmi.name/res/cos/ をチラッと眺めてみました。確かに、ちょっと似た雰囲気を感じます。
演繹系はゲンツェンのモノが唯一無二ではないので、色々とオルタナティブがあってもいいと思うわけです。そうなると、同じモデルに構文はいくらでも作れちゃうので、むしろモデル側を主体に考えたらいいんじゃないだろうか、というのが僕の動機です。

2016-07-11 (月)

論理におけるさまざまな「矢印」達

| 10:27 | 論理におけるさまざまな「矢印」達を含むブックマーク

論理では、矢印または矢印類似の記号がたくさん出てきます。それらの矢印記号に関連する名前や動詞もたくさんたくさんあります。記号と呼び名・動詞を表にまとめてみました。ただし、この表にはたいした根拠はありません。誰も根拠など持ってないと言っていいでしょう。

矢印記号 動詞 左側 右側 全体
 → imply antecedent succedent conditional proposition
 ⇒ derive assumptions conclusion sequent
 |- prove premises statement provability judgment
 |= satisfy model sentence validity judgment
 |⇒ entail facts consiquence semantic entailment

世の中の標準がこの表だ、なんてことはまったくありません! 僕がこんな言葉使いをしている、というわけでもありません

論理における記号法/用語法は滅茶苦茶のグジャグジャです(論理に限ったことじゃないですが。例えば「型推論に関わる論理の概念と用語 その2」「絵算(ストリング図)における池袋駅問題の真相」参照)。似たりよったりの記号/言葉が山のようにあって、それらを明確に区別する人もいれば、同義語として使う人もいれば、なんだかワカラナイままに使っている人もいます。

この表は、先に枠組み(空欄の集まり)を作っておいて、そこに同じ言葉が入らないように埋めていったものです。出来るだけそれらしい言葉を選んだつもりではありますが。

類似の話題は次の記事でも扱っています。

いくつかの注意を述べておきます。

  • 日本語を使うと、翻訳の曖昧性が入ってさらに話がややこしくなるので英語のままにしました。
  • derive, prove, entail(名詞:derivation, proof, entailment)の区別は、あまりされてないと思います。僕もしてません。
  • 含意記号(imply)は、→ 以外に ⊃ もよく使われます。僕は ⊃ を使うことが多いです。
  • シーケント(sequent)の矢印は、→ も ⇒ も使われます。|- を使うこともあります。
  • |- の右側をstatement、|= の右側をsentenceとしたのは苦し紛れです。conclusionかconsiquenceを使うことが多いと思います。
  • satisfy, model, sentenceはインスティチューションの用語です。インスティチューションでは、|= をsatisfaction relationと呼びます。
  • 動詞として、deduce, refine, infer, reasonなどもありますが、この表では使ってません。
  • |- を使ったjudgmentの左(premisesと書いた)はcontextということもあります。特に型理論ではcontextが多いです。


記号法/用語法だけでなく、内容的な補足をちょっとしておきます。

|-, |=, |⇒ は論理システム(演繹系、論理の形式的体系)の内部で使う記号ではなくて、メタな言明を記述するために使います。ただし、|- はシーケントの区切りにもよく使われているので、そのときはシーケント計算(という論理システム)の内部の記号です。

Sをなんらかの論理システムだとして、AをSの論理式(formula)、ΦをSの論理式の集合だとします。このとき、Φ |-S A は、Φに含まれる論理式を仮定した場合にAを証明できることを表します。Sが事前に分かっているなら、下付きのSは省略します。Φが有限集合 {B1, ..., Bn} ならば、B1, ..., Bn |- A と書きます。特に、Φが空集合なら |- A ですね。

|- は構文論的(証明論的)な概念を表しますが、|= は意味論的(モデル論的)概念を表します。Mがモデルのとき、M |=S A は、論理式AがモデルMに対して成立することを表します。|=S をキチンと定義するのはそれほど楽じゃありません。

モデルの集合をU(宇宙)として、Uに所属する任意のモデルMに対して M |=S であるとき、|=S A と書きます。Sが了解されているなら |= A です。ほんとはUも明示したほうがいいのでしょうが、暗黙に決まっているとして省略します。

論理システムS、意味論的妥当性 |=S、宇宙Uが決まっている状況で、Φ |⇒ A は次のような意味です。

  • B∈Φ である任意の論理式Bに対して M |= B であるなら、必ず M |= A である。

Φ |- A と Φ |⇒ A は似てますが、Φ |- A は構文論的な主張で Φ |⇒ A は意味論的な主張です。


「論理における記号法/用語法は滅茶苦茶のグジャグジャ」と言いましたが、論理と関連したソフトウェアである証明支援系では、さらに輪をかけて酷いことになります。論理の用語に加えてアルゴリズムや実装に由来する用語が入り、コミュニティの隠語も混ざってきます。例えば、Coqにおける「ゴール」という言葉の困った使い方

証明支援系はカリー/ハワード対応を使うことが多いので、型理論の用語も使います。型理論の用語法はいいかげん混乱してますが、この混乱も持ち込まれます。

その結果、証明支援系のマニュアルや解説の記述は悲惨なことになります。冒頭の一覧表(の枠組み)を作った動機は、Isabelleのマニュアルの激しく曖昧・多義的な用語法を整理するためでした。

論理や論理的ソフトウェアが自分自身を語るときの論理性や整合性がグダグダなのは、「なんとかならんのかよ」と思います。

2016-07-09 (土)

この広告怖いよ

| 10:08 | この広告怖いよを含むブックマーク

みずほ銀行のシステム統合がヤバイよ、という記事を読んでいたら、出てくる広告がコレ↓

シュールというかホラーというか、不気味すぎてゾワゾワしてしまうんですけど(記事内容との相乗効果ありで)。

[追記]みずほ銀行の件は、まとめがあります。ここから色々リンクが出ています。

[/追記]

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

2016-07-07 (木)

ストリンググラフとストリング図

| 16:12 | ストリンググラフとストリング図を含むブックマーク

ストリング図とストリンググラフ、何が違う?」で触れたストリンググラフを、もう少し詳しく説明します。

内容:

  1. アンチ反射的単純有向グラフ
  2. ストリンググラフとラベリング
  3. ストリンググラフの描画=ストリング図
  4. 描画の例
  5. その他の話題

アンチ反射的単純有向グラフ

グラフ理論に関する定義をズラズラと並べます。退屈ですが、言葉の確認です。

有向グラフは、頂点(vertex)の集合をV、(edge)の集合をEとして、四つ組 (V, E, src, trg) で定義します。ここで、

  • src:E→V は、辺にその始頂点(source vertex)を対応させる写像
  • trg:E→V は、辺にその終頂点(target vertex)を対応させる写像

勝手に取った2つの頂点 a, b に対して、src(e) = a, trg(e) = b となる辺eが高々一本しかないとき、その有向グラフは単純(simple)である、と言います。なお、単純グラフの定義として「自己ループ辺も認めない」を追加するときもあります。自己ループ辺とは、src(e) = trg(e) となる辺eです。

(V, E, src, trg) が単純有向グラフのとき、E⊆V×V とみなしてかまいません。第1射影 V×V→V をEに制限してsrcとして、第2射影 V×V→V をEに制限してtrgとします。今回は、単純有向グラフしか扱わないので、E⊆V×V と考えます。srcとtrgは射影として自動的に決まるので、単純有向グラフを単に (V, E) と書くことにします。

有向グラフが反射的(reflexive)とは、self:V→E という写像があり、src(self(a)) = a, trg(self(a)) = a となることです。selfは、頂点に対して自己ループ辺を対応させる写像です。単純有向グラフのときは、反射的であることは次のように表現できます。

  • ΔV⊆E

ΔVは、{(a, b)∈V×V | a = b} という対角集合です。このとき、self(a) := (a, a) としてselfを定義できます。このselfは一意的に決まってしまいます。

単純有向グラフがアンチ反射的(anti-reflexive)であるとは次のことだとします。

これは、「反射的でない(反射的の否定)」ではなくて、自己ループ辺を全く持たないことです。

今後考えるグラフはアンチ反射的単純有向グラフ(狭義の単純有向グラフ)だけです。つまり、自己ループ辺はありません。しかし、アンチ反射的単純有向グラフの準同型写像を定義するときに自己ループ辺を使います。

(V, E) と (V', E') がアンチ反射的単純有向グラフだとして、f = (fvert, fedge) は写像の組で、

  • fvert:V→V'
  • fedge:E→(E'∪ΔV')

とします。fedgeの余域に自己ループ辺を含めていることに注意してください。

f = (fvert, fedge) がアンチ反射的単純有向グラフの準同型写像(homomorphism)であるとは、次を満たすことです。

  • src(fedge(e)) = fvert(src(e))
  • trg(fedge(e)) = fvert(trg(e))

(V, E) の辺eを潰すときに、ΔV'の自己ループ辺を使うのです。辺を潰す手段がないと、例えば自明な離散グラフ ({a}, {}) への準同型写像を作ることが出来ません -- それでは不便なので、ちょっと技巧的な定義としたのです。

ストリンググラフとラベリング

ストリンググラフは、アンチ反射的単純有向グラフに対してさらに構造と条件を加えたものです。事前に「ストリング図とストリンググラフ、何が違う?」を読んでおくと理解が早いと思います。

アンチ反射的単純有向グラフ (V, E) の頂点の集合Vが、V = W + N と直和分解されているとします。Wに所属する頂点をワイヤー頂点(wire vertex)、Nに所属する頂点をノード頂点(node vertex)と呼びます。通常、「頂点」と「ノード」は同義語ですが、ここでは区別します。

頂点集合がワイヤー頂点とノード頂点に分割されたアンチ反射的単純有向グラフを (W, N, E) と書くことにします。(W, N, E) がストリンググラフ(string graph)だとは、次を満たすことです。

  • ワイヤー頂点の入次数(in-degree)と出次数(out-degree)の組 (indeg, outdeg) は、次のいずれかに限る:(0, 1), (1, 1), (1, 0)
  • 任意の辺eに対して、src(e)かtrg(e)の少なくとも1つはワイヤー頂点である。

頂点の入次数とは、その頂点に入る辺の本数、出次数は出る辺の本数です。

ストリンググラフの定義から、ワイヤー頂点はその入次数/出次数により三種類に分類できます。

  1. 入次数が0であるワイヤー頂点を進入境界頂点(incoming boundary vertex)と呼ぶ。
  2. 出次数が0であるワイヤー頂点を退出境界頂点(outgoing boundary vertex)と呼ぶ。
  3. 入次数、出次数ともに1であるワイヤー頂点を内部ワイヤー頂点(interior wire vertex)と呼ぶ。

進入境界頂点と退出境界頂点をあわせて境界頂点(boundary vertex)と呼びます。

次の図(http://arxiv.org/pdf/1504.02716.pdf)の(b)はストリンググラフで、2個の進入境界頂点、1個の退出境界頂点、6個の内部ワイヤー頂点を持ちます。

ストリンググラフの準同型写像(homomorphism)は、下部構造(underlying structure)であるアンチ反射的単純有向グラフの準同型写像で、ワイヤー頂点をワイヤー頂点に、ノード頂点をノード頂点に写すものとして定義します。

(W, N, E) がストリンググラフのとき、ラベルの集合をLとして、写像 label:(W + N)→L が次の条件を満たすときラベリング(labeling)と呼びます。

  • v, wが隣接するワイヤー頂点のとき、label(v) = label(w)

「v, wが隣接する」とは、「src(e) = v かつ trg(e) = w」または「src(e) = w かつ trg(e) = v」となる辺eがあることです。

ストリンググラフでは、ワイヤー頂点が辺を代表していると考えられるので、辺に対するラベルは考えません。

ストリンググラフ(ストリング図のグラフ化)を圏論で使うときは、ラベル集合に圏Cを使い、

  • ワイヤー頂点には、圏Cの対象をラベルとする
  • ノード頂点には、圏Cの射をラベルとする
  • 隣接する頂点に圏論的な条件を付ける

とします。

ストリンググラフの描画=ストリング図

ストリンググラフは、ストリング図に対応するデータ構造として生み出されました(「ストリング図とストリンググラフ、何が違う?」参照)。幾何的対象としてストリング図があり、その組み合わせ構造を抽出したものとしてストリンググラフがあるわけです。

しかしここでは、先にストリンググラフありき、として、ストリンググラフの幾何的描画(geometric rendering)/幾何的実現(geometric realization)としてストリング図を導入します。

(W, N, E) をストリンググラフとします。Xをなんらかの位相空間だとして、連続写像 ψvert:(W + N)→X と ψedge:E×[0, 1]→X の組 ψ = (ψvert, ψedge) を考えます。ここで、W + N とEには離散位相を入れて、[0, 1]は実数の単位区間で、普通の位相です。ψ = (ψvert, ψedge) が次の条件を満たすとき、ψをストリンググラフ (W, N, E) の描画(rendering)と呼びます。

e∈E に対して、ψedge の {e}×[0, 1] への制限を ψe:{e}×[0, 1]→X として:

  1. ψe(0) = ψvert(src(e))
  2. ψe(1) = ψvert(trg(e))

写像ψにより、グラフの辺がX上の“線分”として実現されて、その両端が、グラフ構造における両端(始頂点と終頂点)に一致している、ということです。

単位区間 [0, 1] の内部である開区間を (0, 1) と書くことにして(これは紛らわしい記法ですが、文脈で判断してください)、ψの E×(0, 1) への制限が単射のとき、埋め込み描画(embedding rendering)と呼ぶことにします。いつでも埋め込み描画が可能なわけではありませんが、埋め込み描画は扱いやすい描画です。

ストリンググラフ (W, N, E)、キャンバスとなる空間X、描画写像 ψ = (ψvert, ψedge) によりストリング図(string diagram)が定義されます。

キャンバス空間Xに変な空間を考えるとややこしくなって嬉しくないので、通常は、素直な空間である多様体を使います。

描画の例

ストリンググラフの描画先であるキャンバス空間として一番簡単なものは、ユークリッド平面R2でしょう。[0, 1]→R2 という写像なら微分可能性を考えることができるので、辺eに対するψeは(適当な回数の)微分可能性を要求しましょう。また、微分係数(速度ベクトル)はいたるところゼロでないと仮定します。

上記のような仮定をすれば、描画 ψ = (ψvert, ψedge) は、かなり扱いやすいものになります。ストリンググラフがラベル付きである場合は、ラベル値を色や文字列で表現すれば、現実的な描画が可能です。

辺eを描く写像 ψe:{e}×[0, 1]→R2 に色々な関数を選べますが、一番簡単なのは1次関数(アフィン線形写像)です。辺の描画に1次関数を使った描画を区分線形描画(piecewise linear rendering)と呼びます。

ワイヤーの曲線は、内部ワイヤー頂点をたくさん取れば折れ線(つまり区分線形描画)で近似できます。よって、区分線形描画だけを考えても、考察対象が限定されてしまうことはありません。

その他の話題

描画のキャンバス空間として、円板や矩形を考えたほうがいいことがあります。そのときは、円板や矩形の境界と、ストリンググラフの境界頂点との関係も考慮します。さらに、円環(anulus)のように穴の開いた図形をキャンバスにすることもあります。

キャンバスに描かれた“絵”としてのストリング図に対して、それらの組み合わせ(composition, combination)を考えると、ストリング図の全体が圏、複圏(オペラッド)、多圏などの構造を持つことになります。

2016-07-05 (火)

無料で入手できる本格的(紙なら高額)な理数系専門書15選

| 12:04 | 無料で入手できる本格的(紙なら高額)な理数系専門書15選を含むブックマーク

インターネットで資料探しをしていると、出版されている書籍と同じ内容のPDFがゴロンと置いてあってビックリすることがあります。以下に挙げるのは、そのような、“出版物と同等な内容”が無料公開されている理数系専門書のリストです。

紙の本とまったく同じものもありますし、ドラフト原稿が公開されているものもあります。紙の本の出版後もメンテナンスされていて、インターネット版のほうがより新しくより充実していることもあります。

例えば"Monoidal Functors, Species and Hopf Algebras"は、ハードカバー本は735ページで、現時点で24,650円もする大部な書籍です。公開されているPDFは書籍より増量して836ページあり、誰でも無料ダウンロード可能です。

著作権があやしいものは除外し、著者本人または著者の所属組織のWebサイト、あるいはarXiv.orgで公開されているものだけを選びました。

  1. Algebraic Topology
  2. Elementary Applied Topology
  3. Category Theory for the Sciences
  4. Higher Topos Theory
  5. Tensor Categories
  6. Lectures on Tensor Categories and Modular Functors
  7. Monoidal Functors, Species and Hopf Algebras
  8. Homotopy Theory of Higher Categories
  9. The Blind Spot: Lectures on Logic
  10. Bayesian Reasoning and Machine Learning
  11. An Introduction to Measure Theory
  12. Towards the Mathematics of Quantum Field Theory
  13. Eloquent Javascript
  14. Advanced R
  15. Software Engineering for Internet Applications

書籍の表紙画像が表示されないときは、このページをリロードしてみてください。

トポロジー

Algebraic Topology
Algebraic Topology

Algebraic Topology

絵、具体例、練習問題が大変に豊富な代数トポロジーの教科書です。著者のAllen Hatcherは、他の本もダウンロード可能にしており、https://www.math.cornell.edu/~hatcher/ からたどって彼の著作物をダウンロードできます。

Elementary Applied Topology
Elementary Applied Topology

Elementary Applied Topology

著者のR. Ghristは、応用トポロジーのパイオニアです。上記Webページから本の章ごとにPDFで読むことができます。綺麗で楽しい絵がたくさん載っています。

この本のモトになったらしい多色手書き原稿(素晴らしい!)には、次のURLでアクセスできます。一見の価値あり。

圏論

Category Theory for the Sciences
Category Theory for the Sciences (MIT Press)

Category Theory for the Sciences (MIT Press)

関手データモデル/圏論データベースのスピヴァックによる圏論入門書です。「スピヴァックの圏論教科書」で紹介しています。PDFは紙の本より少し古い内容で、タイトルも微妙に異なっています。

Higher Topos Theory
Higher Topos Theory (Annals of Mathematics Studies)

Higher Topos Theory (Annals of Mathematics Studies)

同時代の天才ジェイコブ・ルーリーの大部な著作です。ルーリーはホームページ http://www.math.harvard.edu/~lurie/ から著作物を公開していて、例えば千ページを超える大作"Higher Algebra"も公開されています。

Tensor Categories

加群圏の創始者であるEtingof達によるテンソル圏の教科書です。「テンソル圏」は人により定義が異なりますが、ホムセットがベクトル空間であるアーベル圏でモノイド構造を持ち、さらにいくつかの条件を満たす圏としてテンソル圏を定義しています。

Lectures on Tensor Categories and Modular Functors

上記のページから、章ごとのps.gzファイルをダウンロードできます。絵算に関してけっこう詳しいです。

Monoidal Functors, Species and Hopf Algebras
Monoidal Functors, Species and Hopf Algebras (Crm Monograph Series)

Monoidal Functors, Species and Hopf Algebras (Crm Monograph Series)

圏論、組合せ論、幾何、代数にまたがる広大な話題を扱っているようです。デカくて難しい本なので、僕には無理。

なお、Marcelo Aguiarも、http://www.math.cornell.edu/~maguiar/books.html から著作物を公開しています。

Homotopy Theory of Higher Categories

紙の本はハードカバーで652ページあるので、arXiv版は短縮版になっています。

論理

The Blind Spot: Lectures on Logic
The Blind Spot: Lectures on Logic

The Blind Spot: Lectures on Logic

線形論理のジラールによる論理の講義です。圧縮された7つのPDFファイルに分かれています。

統計/機械学習

Bayesian Reasoning and Machine Learning
Bayesian Reasoning and Machine Learning

Bayesian Reasoning and Machine Learning

PDFは、紙の本(735ページ)より少し短いようです。

測度論

An Introduction to Measure Theory

人類で最もIQが高いだろうと言われているテレンス・タオの測度論の教科書です。https://terrytao.wordpress.com/books/ から他の本も公開されています。

場の量子論

Towards the Mathematics of Quantum Field Theory

パート1が、色々な概念のまとめとして使えます。

プログラミング言語/ソフトウェア

Eloquent Javascript
Eloquent Javascript: A Modern Introduction to Programming

Eloquent Javascript: A Modern Introduction to Programming

PDFだけでなく、HTMLを使ったサイトとしても書籍と同等な内容を提供しています。

Advanced R
Advanced R (Chapman & Hall/CRC The R Series)

Advanced R (Chapman & Hall/CRC The R Series)

書籍に対応するWebサイトです。コードのコピペもすぐ出来るので書籍よりサイトのほうが便利かも知れません。

Software Engineering for Internet Applications
Software Engineering for Internet Applications (MIT Press)

Software Engineering for Internet Applications (MIT Press)

HTMLとして書籍の内容を公開しています。

2016-06-20 (月)

JavaScript界隈は日本語がお好き?

| 15:52 | JavaScript界隈は日本語がお好き?を含むブックマーク

JavaScriptのSVGライブラリを探していたら、bonsaiというライブラリが見つかりました。

ロゴもこんな(↓)ですから、これは「盆栽」ですね。

Kendo UIというUIライブラリもあるようです。

Kendo UIのオンライン・プレイグラウンドとして、「剣道 道場」というのがあります。

dojoといえば、prototype.jsとjQueryのはざまの時期に出現したUIライブリのひとつにDojo Toolkitってのがありましたよね。あれも「道場」なんじゃないの。今はどうしてるのか? と思ったら、開発は続いているようです。

Dojo Toolkit、YUI(Yahoo! User Interface)と並んでExt JSってのもありましたが、Ext JSを作っていた会社はSencha。

https://www.sencha.com/

ロゴは:

「煎茶」ですね。

海外でも広く知られている日本語と言えば「忍者」ですよね。jQueryのジョン・レシグは忍者の本書いています。

Ninjustu(忍術)をNinjitsuと書くこともありますから、Node.jsを扱っている会社のNodejitsuって「Node術」なのかな?

なんか、日本語が好きなんだね。

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

2016-06-13 (月)

Isabelle小ネタ:min-plus半環

| 11:32 | Isabelle小ネタ:min-plus半環を含むブックマーク

Isabelleをいじっているあいだ(=飽きるまで ^^;)は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。

ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*」をオーバーロードする話でしたが、今回はエキゾチックな演算子記号「¥oplus」「¥odot」を使います -- 「零の概念とmax-plus半環の紹介」の説明と同じ記号法になります。

とりあえず書いてみたのは:[追記]コメント内の to proof は to prove ですね。テキストならすぐ修正するけど、画像だから面倒だ、直さない。[/追記]

セオリー記述をお見せするのにスクリーンショット貼り付けるのが、もうナントモ複雑な気分ですが、生のソースコード・テキストじゃ読むの辛いし。(一応、最後にテキストも貼っておきます。)

min-plus半環の台集合は非負実数の集合ですが、realやdoubleがIsabelleに(少なくともMainセオリーには)入ってなかったのでintを台にしました。¥oplus¥odotの定義は見りゃわかると思います。生ソースで ¥oplus は \<oplus>、¥odotは \<odot> で、TeXと同じ記号名です。([追記 date="2016-06-20"]Realというセオリーをインポートすると実数が使えますね。[/追記]

Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか」でも触れたように、Isabelleのソースファイルは7ビットASCIIエンコーディングで*1、演算子記号に対する生のUnicode文字は入っていません。参考までに、「¥oplus」と「¥odot」のUnicodeコードポイントは:

min-plus半環が実際に半環の公理の満たすことを一部だけ示しています。この程度の定理なら自動証明でいけます。

「min-plus半環は半環である」という主張をIsabelleのなかでキッチリ示すには、半環を型クラスとして定義して、具体的に与えたmin-plus半環が型クラスのインスタンスになることを証明すれば良さそうです。「Coqで半環:アンバンドル方式の例として」でやったような、代数構造の階層的構成もたぶん型クラスで出来るでしょう。

ソースコードのテキスト:

[追記]間違いも画像と同じまま。簡単に直せるけど直さない。[/追記]

theory MinPlus
imports "Main"
begin

section \<open>Definition of MinPlus sum and product\<close>

fun minplus_sum :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "\<oplus>" 60)
where 
 "minplus_sum x y = min x y" 

fun minplus_prod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "\<odot>" 70)
where
 "minplus_prod x y = x + y"

section \<open>Some MinPlus expressions and evaluated values\<close>

value "1 \<oplus> 1" (* is 1*)
value "1 \<odot> 1" (* is 2 *)
value "10 \<oplus> 3\<odot>5" (* is 8*)

section \<open>Theorems (insufficient)\<close>

theorem sum_assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
apply(auto) (* We do not need to proof by hand. *)
done

theorem sum_comm: "x \<oplus> y = y \<oplus> x"
apply(auto)
done

theorem dist_l: "x\<odot>(y \<oplus> z) = x\<odot>y \<oplus> x\<odot>z"
apply(auto)
done

*1:HTML4までのデフォルトエンコーディングはISO-8859-1で、これは日本人には迷惑な話だったりします。Unicode対応しないのなら、7ビットASCIIのほうがいっそ清々しいですが、UTF-8でいいから対応してよ。

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

2016-06-09 (木)

Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか

| 09:46 | Isabelleについて: 証明支援系は何を目指し、どこへ向かうのかを含むブックマーク

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。

内容:

  1. Isabelleの独自な世界
  2. Isabelleの未来

Isabelleの独自な世界

Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より:

PIDE構想は、Isabelleプロジェクト/コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか? なかなかに興味深いですな。

Isabelleが世の趨勢と離れるのか? という話をしてますが、有り体に言えば、もともとIsabelleは独特の文化を持った癖の強い処理系で、利用者は特殊な人々です。証明支援系を使いたくても、Isabelleを避ける人はいるでしょう。僕自身、Isabelleは「ダメだこりゃ」と思った1人です。

2005年の夏に、証明支援系を動かしたくなったことがあるのですが、そのとき僕が選んだのは Poly/ML + Isabelle ではなくて、 Moscow ML + HOL でした。当時のメモが残っています*1

Isabelleの何がそんなに嫌だったのかというと、余りにも不格好で気持ち悪い構文です。例えば、SML(Standard ML言語)で次のように書ける関数定義が、

fun conc [] ys = ys
  | conc (x :: xs) ys =  x :: (conc xs ys);

Isabelleでは次のように書きます。

fun conc :: "'a list => 'a list => 'a list"
where
  "conc [] ys = ys"
| "conc (x # xs) ys = x # (conc xs ys)"

Isabelleには外部構文(outer syntax)と内部構文(inner syntax)の区別があり、内部構文は引用符のなかに書きます。それがまるで文字列に見えてしまい、sh(シェル)スクリプトでevalを使っているような気持ち悪さです。「これは生理的に耐えられない」と思いました*2

今でも外部構文/内部構文の区別はそのままで、ソースコード気持ち悪さはパワーアップしています。

とあるIsabelleソースの一部*3 :

    from \<open>\<exists>!y. ?R m y\<close>
    obtain y where y: "?R m y"
      and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
    show "\<exists>!z. ?R (succ m) z"

TeXコントロールシークエンス/XMLタグのような書き方は、特殊文字を表現するマークアップです。もはや、ソースコードを直接目視することやテキストエディタでの入力は考えてないようです。Isabelle/jEditで見れば:

そして、特殊文字の入力はシンボルパレットからどうぞ。

プログラミング言語APLでは、専用のキーボードや印字装置が必要だった、という話がありますが、IsabelleはAPL的方向に進んでいるようです。現代では、専用ハードウェアは不要で、ソフトウェアで入出力(編集と表示)をサポートできます。そのソフトウェアがIsabelle/jEditというわけです。

Isabelleのチュートリアルなどで、サンプルコードとして次のようなテキストが載っていたりします。

面食らいますよね。「いやっ、擬似コードじゃなくて、実際のソースコードサンプルを載せてくれよ」と。これが、実際のソースコードサンプルなんですよね。ただし、Isabelle/jEditじゃないと入出力(編集と表示)が出来ませんけど。

Isabelleの未来

「いったいどこへ向かう気なんだよ? Isabelle」、「それが正しい方向なのかい? Isabelle」と問いたくなります。

汎用の編集系Emacsや広く普及したSML処理系SML/NJを切り捨てたことは、より独自な閉じた世界へと向かっている印象を受けます。

しかし、ウェンツェルの意図はそうじゃないようです。むしろ逆で、証明支援系をより広い用途でより多くの人々に使って欲しい、だから古臭くて低機能なEmacsやSML/NJとは決別した、ということみたい。

ウェンツェルの2010年のスライド(のPDF)を見ると、PIDEという言葉こそ使っていませんが、この時点で既にIsabelle/jEditのアイディアは確立されていたことが分かります。

このスライドの冒頭には、次の2つの目標が掲げられています。

  1. 我々の証明エンジンをそこら辺にいる人々に使ってもらおう。(Make our provers accessible to many more people out there.)
  2. 証明エンジンのフロントエンドを作るのをうんと簡単にしよう。(Make building front-ends for provers really easy.)

証明エンジン/フロントエンドの用途のひとつとして、例えば教育が想定されています。

PIDEアーキテクチャは、Isabelleに限らず、他の証明支援系のUI構築にも使えるものです。実際ウェンツェルは、頼まれもしないのに(たぶん)、CoqのPIDEフロントエンドを試作したりしています。

現状のCoqのフロントエンドは、証明コマンド(タクティク)を実行して証明状態を遷移させていくものです。つまり、対話的スクリプティング環境なんです。これに対してPIDEのフロントエンドは、スクリプティング環境ではなくてドキュメント作成編集環境です。

「証明スクリプトから証明ドキュメントへ」 -- PIDEのキャッチフレーズのひとつです。動作記述である証明スクリプトでは、人がそれを読んで理解するのは困難です。宣言的で人が読める証明、それがウェンツェルの言う証明ドキュメント(proof document)です。

と、ここ数年のウェンツェルの主張を追ってみると、Isabelleの世界を広げようと尽力しているのが分かります。証明支援系の利用が広がらないネックは、「難読な証明記述言語と貧弱なユーザーインターフェースだ」との認識のもと、Isar(Isabelleの宣言的証明記述言語)とIsabelle/jEditにより障壁を取り除く戦略のようです。

この戦略が功を奏するのか? 僕には予測できません。が、このような戦略と方向性の文脈のなかで、11年前に抱いた悪印象はだいぶ緩和されました。広がりゆく(であろう)Isabelleの世界にちょいと入り込んでみようかな。


独白的余談:「ソースコードはプレーンテキストで書くべきで、プレーンテキストとして十分に読みやすくあるべき」だと僕は思っています。けど、プレーンテキストで見たときに気持ち悪いIsabelleコードは、Isabelle/jEditが綺麗に見せてくれたほうが助かります。引用符は見せないでくれ、型変数 'a もイタリックのaにしてくれ。

*1:結局このときは、MoscowML+HOLがビルド出来ず、Prolog処理系で推論計算しました。

*2[追記]今見たら、HOLでもけっこう引用符を使ってますね。|- や [ ] を使うと引用符を省けるので「多少はマシ」という判断だったのでしょう、覚えてないけど。[/追記]

*3:~~/HOL/ex/Abstract_NAT.thy lemma Rec_functional: 50行目

shiroshiro 2016/06/09 20:37 イマドキなら、Unicode使えばテキストオンリーでもそこそこ書けそうな感じはします。それはプレーンテキストなのかと言われると、ソースに日本語コメント混ぜるのにさえ最近まで躊躇してた世代としてはうーん、となるのですが、アメリカ人が日本語顔文字をばりばり使うネイティブUnicode世代だと実はそれほど抵抗は無いのかもしれません。

(最近では自分も、論文のアルゴリズムを書いてみる時などはギリシャ文字など抵抗なく使うようになりました。論文読み解きながらの入力ではタイプの手間はそれほど大きくありませんし。)

m-hiyamam-hiyama 2016/06/10 09:52 shiroさん、
僕はUnicodeも含めてプレーンテキストだと思ってますが、Isabelleの人達は、Unicodeはレンダリングの手段であっても、生のUnicode文字をソースに入れる発想はないみたいです。
そのへんは保守的。ASCII文化。
キーワードレベルでUnicodを使う言語が登場すると時代が変わるかもですね。
id := ∀α.λx:α.x とか書けて、ASCIIによる代替表現はC/C++のトライグラフのような扱い。

chiguri_schiguri_s 2016/06/10 11:58 jEditでの入力ではテキスト入力時にコマンドのように打つことで記号を出せますね。てっきり出来ている物もUnicodeテキストだと思っていたのですが、中身までコマンド風文字列だったとは。
AgdaはUnicodeでの記法をサポートし、むしろそっちを使って記述をすることが多いです。中身もUnicodeの記述になります。

m-hiyamam-hiyama 2016/06/10 14:35 chiguri_sさん、
> 中身までコマンド風文字列だったとは。
このへんのバランス感覚がなーんかオカシイ印象を受けます。
> 中身もUnicodeの記述になります。
それが普通ですよね。今のIsabella/jEditはUTF-8でさえ読めません。
記号の入出力にアプリケーション(Isabella/jEdit)が頑張るって発想も違和感あります。
かな漢字変換FEPの文化がない欧米だと、そうなっちゃうのかな。

nshinchan01nshinchan01 2016/06/19 00:33 思わずツイートするくらい笑わせてもらいましたw