このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

中学レベル代入計算からカリー／ハワード流証明の圏へ

雑記／備忘

Coqをいじっていると、カリー／ハワード対応の威力を実感します。一方で、証明といえども所詮は計算なんだな、とも思います。中学校くらいでやる代入計算の直接的な延長線上に証明の合成操作があるんですよね。中学レベルの計算と形式的証明では、用語や記号がまったく違うのですが、そこにうまく通路を作ってやると、やってることは大差ないことが分かります。

「寄り道Coq： exactタクティクと型理論と圏論」の最後の節「大きなラムダ式／小さなラムダ式」で述べたことの敷衍です。

内容：

1次式の代入計算

話を簡単にするために、式としては1次式だけを考えます。1次式による計算結果を変数に代入することを次の形で書きます。

  • v := 2x + 3y - 1

連立の場合もあります。

  1. v := 2x + 3y - 1
  2. w := y + 3

いくつかの代入操作を1行で書くときは、カンマで区切って全体を中括弧（ブレイス）で囲むことにします。先の例なら、{v := 2x + 3y - 1, w := y + 3} です。この書き方は、「型推論に関わる論理の概念と用語 その6：substitutionの記法」において、次のように述べたものです。

で、どれを採用するべきか？ 色々な書き方があることを承知の上ならどれでもいいでしょう。「置換の圏から代入の圏へ」では {x := E, y := F} を使っています。たぶん、説明では今後もこの記法を使うでしょう。

ここで言っている「色々な書き方」とは、次のようなものです（詳細は「型推論に関わる論理の概念と用語 その6：substitutionの記法」を）。どれも意味は同じです。

  1. {(2x + 3y - 1)/v, (y + 3)/w}
  2. {v |→ 2x + 3y - 1, w |→ y + 3}
  3. {v = 2x + 3y - 1, w = y + 3}
  4. {v <= 2x + 3y - 1, w <= y + 3}
  5. {v : 2x + 3y - 1, w : y + 3}

書き方はなんでもいいとして、“変数と式のペア”をいくつか並べたもの全体を代入（substitution）と呼びます。substitutionは、メモリ領域を破壊的に書き換えるassignmentとは違うのですが、僕は、substitutionもassignmentも「代入」で済ませています。

代入を一般的に表すときは、σ（シグマ）, ρ（ロー）などギリシャ文字の小文字を使うことにします。例えば、σ = {v := 2x + 3y - 1, w := y + 3}。連立ではなくて単独の代入操作でももちろんかまいませんから、{w := y + 3} も代入です。空な代入 {} も認めます。

σ = {v := 2x + 3y - 1, w := y + 3}、ρ = {s := w, t := v + w} であるとき、σとρの結合 ρ・σ は次のように計算します。

   ρ・σ
 = {s := w, t := v + w}・{v := 2x + 3y - 1, w := y + 3}
 = {s := (y + 3), t := (2x + 3y -1) + (y + 3)}
 = {s := y + 3, t := 2x + 4y +2}

このテの代入計算は、1次関数や1次方程式の練習問題としてやったことがあると思います。やったことない人は今から練習してください :-)

代入の圏

代入の圏については次の記事で述べてます。

上記の記事では、代入を {x := f(x), y := g(y, z)} のように一般的な式（f(x)とかg(y, z)とか）で書いてますが、今回は式を1次式に限って単純化してます。また「置換の圏から代入の圏へ」では、変数の名前をリネームしても代入の意味は変わらないので名前の違いを無視（捨象）してますが、今回は名前の問題には言及していません。リネーミングの扱いは次の課題とします。なお、名前を取り去ってしまったラムダ計算の話が「代入の圏Subst[Σ]上のラムダ計算」にあります。

さて、代入σとρのこの順での結合（composition）をρ・σと書いたのですが、このナカグロ記号「・」は反図式順結合（anti-diagrammatic order composition）の記号になっています。僕は、反図式順が嫌いで、図式順結合（diagrammatic order composition）の記号「;」を使っています。まー、個人的な好みなんですが、「・」から「;」に切り替えます。

結合の順序を図式順にすると、「変数 := 式」という書き方と相性が悪くなるので、“変数と式のペア”を「式 >: 変数」と書くことにします。「>:」は、左の計算結果を右に向かって突っ込む感じです*1。新しい記法での代入計算は次のようになります。中間の変数 v, w を消す計算です。

   σ;ρ
 = {2x + 3y - 1 >: v, y + 3 >: w};{w >: s, v + w >: t}
 = {(y + 3) >: s, (2x + 3y -1) + (y + 3) >: t}
 = {y + 3 >: s, 2x + 4y +2 >: t}

左から右に向かう図式順で統一されたのはいいのですが、{2x + 3y - 1 >: v, y + 3 >: w} という書き方には曖昧性があります。2番目の代入操作である y + 3 >: w を見ると、変数xが出現してません。変数xが式に出現してなくても、入力変数にxは存在しています。ここらへんの事情がハッキリしません。

ラムダ記号と引数リストを使って、λ(x, y).(y + 3) のように書けばハッキリします。λ(y).(y + 3) と λ(x, y).(y + 3) と λ(x, y, z).(y + 3) とは違うものとして区別します。代入の前にもラムダ引数リストを付けて、λ(x, y).{2x + 3y - 1 >: v, y + 3 >: w} と書きましょうか。鬱陶しいけど。

引数リストを明示した場合、λ(x, y).{2x + 3y - 1 >: v, y + 3 >: w} と λ(x, y, z).{2x + 3y - 1 >: v, y + 3 >: w} は違う代入です。一番目の引数変数（入力変数）は {x, y} 、代入先変数（出力変数）は {v, w} です。ニ番目の引数変数（入力変数）にはzが入って {x, y, z} です。

σ = λ(x, y).{2x + 3y - 1 >: v, y + 3 >: w}、τ = λ(x, y, z).{2x + 3y - 1 >: v, y + 3 >: w} と置いたとき、σとτが使用している変数をハッキリ示すために次のように書きます。

  • σ:{x, y}→{v, w}
  • τ:{x, y, z}→{v, w}

ん？ この形は… そうです。もう圏が定義できたも同然ですね。{x, y}とか{v, w}のような変数のリストを対象として、代入を射とする圏があるのです。引数リストが明示された代入に対して、domとcodを次のように定義します。

  • dom(σ) = (σの引数変数のリスト）
  • cod(σ) = (σの代入先変数のリスト）

{x, y}のような書き方をしてますが、変数の集合ではなくてリストである点に注意してください*2。変数のリスト X = {x1, ..., xn} に対して、idX は次の代入です。

  • idX = λ(x1, ..., xn).{x1 >: x1, ..., xn >: xn}

代入の結合は既に述べました。次の法則も明らかでしょう（結合律を厳密に示すのは意外と面倒だけど）； σ:X→Y、ρ:Y→Z、τ:Z→W として、

  • (σ;ρ);τ = σ;(ρ;τ)
  • idX;σ = σ
  • σ;idY = σ

変数と1次式の代入計算の全体が圏になるのですが、次の事実を示すことは良い練習問題です。

  • 1次式を定数項のない1次式に制限して、変数の名前の違いを無視すると、行列の圏となる。

定数項を許しても、次元を1つ増やした行列で表現できます（アフィン写像の行列表現）。

代入をシーケントで表す

代入 λ(x, y).{2x + 3y - 1 >: v, y + 3 >: w} には、2つの基本代入操作が含まれます。それぞれを代入の成分（component, member）と呼ぶことにします。成分が1つでも、成分がまったくなくても（空代入）いいのでした。成分の個数は、代入先変数（出力変数）の個数と同じです。

成分にもラムダ引数リストを付けると、λ(x, y).(2x + 3y - 1 >: v)、λ(x, y).(y + 3 >: w) のように書けます。ここで、ラムダ記号の代わりに太い矢印を使って書いてみます。

  1. x, y ⇒ 2x + 3y - 1 >: v
  2. x, y ⇒ y + 3 >: w

書き方が変わっただけで、意味はまったく同じです。その意味を念の為に確認しておくと：

  1. xとyの値が具体的に与えられるならば、2x + 3y - 1 を使ってvの値を計算できる。
  2. xとyの値が具体的に与えられるならば、y + 3 を使ってwの値を計算できる。

太い矢印「⇒」は「ならば」の記号ですが、上記の意味記述に出てくる「ならば」と対応しています。「⇒」を使った書き方をシーケント記法と呼びます。

シーケント記法は本来は論理で使う記法です。1次式の代入を形だけシーケントにしてみてもそれほど嬉しいことはありません。しかし、変数に型があるときはシーケント記法がフィットします。

次のシーケントを考えてみます。

  • n:integer, m:integer ⇒ plus(n, m):intger >: sum

これは次のような意味を持ちます。

  • 変数nの型が整数型、変数mの型が整数型ならば、式 plus(n, m) の型は整数型である。
  • また、nとmの値が具体的に与えられるならば、plus(n, m) を使ってsumの値を計算できる。

「plus(n, m) の型は整数型」と「plus(n, m) を使ってsumの値を計算」から、次の事実も導けます。

  • 変数sumの型は整数型である。

この例で、plusはその名前から足し算だろうと想定してましたが、plusの型もちゃんと宣言することにしましょう。

  • n:integer, m:integer, plus:integer×integer->integer ⇒ plus(n, m):intger >: sum

plus:integer×integer->integer の意味は、「関数plusは2つの整数を引数にして整数を返す」ですが、plusをカリー化すれば、plus:integer->(integer->integer) と書けます。右側に付ける括弧は省略できるので、plus:integer->integer->integer でOK。この書き方でシーケント書き直すと：

  • n:integer, m:integer, plus:integer->integer->integer ⇒ (plus n m):intger >: sum

横1行で見づらいのなら、Coq風フォーマットで縦に並べて：

  n : integer
  m : integer
  plus : integer -> integer - >integer
 ==========================
 (plus n m) : intger >: sum

この形は、型理論における型判断（typing judgement）そのものです。型判断と型付け（typing）に関しては「型推論に関わる論理の概念と用語 その5：型付けの簡単な例から型判断へ」を参照してください。

型判断としては、お尻に付いている「>: sum」は余計な情報ですが、代入としては代入先変数（出力変数）の名前は必要です。代入先変数が書かれてないと、代入の余域（codmain）を決定できません。例えば、次の2つ型判断を考えましょう。

  • n:integer, m:integer, plus:integer->integer->integer ⇒ (plus n m):intger
  • n:integer, is_even:integer->boolean ⇒ (is_even n):boolean

この2つの型判断をまとめて1つの代入とするには、「⇒」の左側を水増しして揃え、代入先変数の名前を添えます。

  • n:integer, m:integer, plus:integer->integer->integer, is_even:integer->boolean ⇒ (plus n m):intger >: sum
  • n:integer, m:integer, plus:integer->integer->integer, is_even:integer->boolean ⇒ (is_even n ):boolean >: evenness

出来上がった代入をσとするならば、そのプロファイル（domとcod）は次のとおり。代入先変数の情報からcodを決定できます。

  • dom(σ) = {n:integer, m:integer, plus:integer->integer->integer, is_even:integer->boolean}
  • cod(σ) = {sum:integer, evenness:boolean}

型判断を成分とする代入

型付き変数を使うシーケントの一般的な形は次のようなものです； a1, ..., an, b が変数（の名前）、A1, ..., An, B が型（を表す式）だとします。

  • a1:A1, ..., an:An ⇒ t:B >: b

ここでtは式（項ともいう）です。tのなかに出現できる自由変数は a1, ..., an ですが、必ず出現する必要はありません。「⇒」の左側は型コンテキスト（あるいは単にコンテキスト）とも呼ばれ、しばしばΓ, Δなどで表します。

今述べた形のシーケントは、型理論では型判断と呼ぶのでした（「型推論に関わる論理の概念と用語 その5：型付けの簡単な例から型判断へ」を参照）。

型判断を何個か（0個でも1個でもよい）を並べたものは、前節で述べたように代入となり、代入はコンテキスト（型宣言の並び）からコンテキストへの射とみなせます。前節の例のσならば、dom(σ)はコンテキスト {n:integer, m:integer, plus:integer->integer->integer, is_even:integer->boolean} であり、cod(σ)はコンテキスト {sum:integer, evenness:boolean} です。それぞれのコンテキストをΓとΔと置けば、代入の圏において σ:Γ→Δ です。

カリー／ハワード対応による再解釈

前節の、代入先変数（出力変数）を付加した型判断（シーケント）をもう一度繰り返し書くと：

  • a1:A1, ..., an:An ⇒ t:B >: b

このシーケントは、変数とその型に関するものですから、次のように解釈します。

  1. a1, ..., an は、変数の名前である。
  2. A1, ..., An は、変数の型である。
  3. tは、変数 a1, ..., an を含む（かもしれない）項である。
  4. Bは、項tの型である。
  5. bは、項tの計算結果を代入する変数の名前である。

カリー／ハワード対応とは、次のような対応です。

  • 命題 ←→ 型
  • 証明 ←→ 項

Propositions as Types , Proofs as Terms で、どちらも省略するとPATなので、PAT-PAT原理とも言えます。

型を命題、項を証明と言い換えて再解釈すると：

  1. A1, ..., An は、仮定となる命題である。
  2. a1, ..., an は、仮定となる命題に付けられたラベル（名前）である。
  3. Bは、結論となる命題である。
  4. tは、仮定 a1, ..., an を前提とする（かもしれない）証明である。
  5. bは、証明された命題（＝定理）に付けられたラベル（名前）である。

つまり、一本のシーケント（型判断）は証明を含めた定理を記述することになります。お尻に付く代入操作「>: b」は、「証明された命題を今後はbと呼ぶ」という「定理の名付け」に相当するわけです。

いくつかのシーケントをまとめた代入は、一群の命題を仮定として他の一群の命題を結論とする証明を並べたたものです。証明の並びを“代入”と呼ぶのは相応しくないかも知れませんが、それはカリー／ハワード対応のマシンに乗って別な世界に来ているからです。「型の世界」と「命題の世界」では、別な概念／別な言葉／別な記号が使われますが、構造的には同型（isomorphic）なのです。

カリー／ハワード流証明の世界における“代入”（の対応物）は、名前付きの命題（仮定）の並びから別な名前付き命題（結論）の並びを導出する証明（実体は項）の並びです。型コンテキストと代入が圏を形成したのと同様に、カリー／ハワード流証明の世界も圏です。

  • 名前付き命題の並びが圏の対象
  • それらのあいだの証明の並びが圏の射

この圏のなかで圏的計算をすることが、我々が公理・定理・証明を扱う行為のモデルになっています。例えば、射の結合は、既にある証明達を合成してより長い証明を合成する操作です。

Coqにおける実例

「Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4）」では、A∧B -> B∧A という命題を証明しました。このときのコンテキスト（仮定の並び）は、A : Prop, B : Propです。その証明の実体は次のような項です。

  • fun (H : A∧B) => match H return (B∧A) with conj H1 H2 => @conj B A H2 H1 end

この項を the_proof と置けば、定理全体の記述は次のシーケントとなります。

  • A:Prop, B:Prop ⇒ the_proof:(A∧B -> B∧A) >: and_is_commutative

証明項the_proofを計算手段と考えれば、次のような解釈もできます。

  • 命題AとBが具体的に与えられるならば、the_proof を使って命題 (A∧B -> B∧A) の証明を構成できる。

ひとつ注意しておくと、Coqにおけるコンテキストには、ゴールの仮定だけではなくて、Parameter、Variableコマンド（それらの同義語）で宣言された仮定も含まれます。その意味で、定理の意味は定理が書かれた場所に依存します。

さて、もうひとつ、「Coqの型クラスの使い方：バンドル方式とアンバンドル方式」にある例を取り上げましょう。

フィールド名を使うバンドル方式でも、パラメータ名を使うアンバンドル方式でも、要するに名付けられた型／命題を並べることに変わりはないので、シーケントで書けます。横1行のシーケントだと見づらいので縦に並べたレイアウトを採用して例題を書きます。

  A : Set
  op : A -> A -> A
  u : A
  unit_l : forall(x: A), op u x  = x
  comm : forall(x y: A), op x y  = op y x
 ==========================
  the_proof : forall(x: A), op x u  = x >: unit_r

この例における証明項the_proofの中身は具体的に書きませんが、このシーケントの意味は次のようなことです。

  • 二項演算opと特定要素uを備えた集合A上で、左単位律と可換律が成立しているなら、右単位律が成立する。

このシーケントのコンテキストに登場する名前は {A, op, u, unit_l, comm} で、このシーケントの代入先変数の名前（定理の名前）はunit_rです。それぞれの名前は型（命題を含む）を持ち、型で制約されます。

まとめと展望

1次式の代入計算は初等的（中学レベルの）計算です。変数のリスト {x, y} などを対象と考えることにより、1次式の代入の全体は圏になります。型付き変数のリスト {n:integer, m:integer, plus:integer->integer->integer} などを考えれば、型判断シーケントを射とする圏が形成されます。型付き変数のリストはコンテキストとも呼ばれるので、コンテキストとシーケント列（代入に相当）の圏です。

カリー／ハワード対応は、「命題 ←→ 型」「証明 ←→ 項」という対応関係を与えるので、コンテキストとシーケント列の圏は、名前付き命題と証明の圏と解釈されます。「型なし変数→型付き変数→命題としての型」と一般化はされていますが、圏の結合は一貫して代入計算で与えられています。このような一貫性を見せてくれるのが、カリー／ハワード対応のありがたいところです。

コンテキストとシーケント列の圏は、単なる圏以上の構造を持っています。デカルト閉構造はありそうです。複圏（オペラッド）、多圏として考えるとどうでしょうか。この圏をベースとするインデックス付き圏やファイバー圏も作れそうです。絵の描き方（絵算法）も整備したいし。

*1:CatyScriptでは、代入に '>' と '>:' を実際に使っていました。

*2:依存タブルを扱うときに、順序を持つリストでないとまずいのです。