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

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

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

［参照用 記事］

型付きラムダ計算 構文論 再入門 1/2： カリー／ハワード対応のために

雑記／備忘

「カリー／ハワード対応への障壁」において、カリー／ハワード対応（Curry-Howard correspondence/isomorphism）をうまく説明するのは難しい、という話をしました。その記事の最後の一言は：

いまだベストと思える説明に届かず。

その後も、ベスト（に近い）説明とはどんなものかと考えています。以前から僕は「大きなラムダ計算」という方法を使っているのですが、これをベースにするのがやはり良いように思えます。大きなラムダ計算は型付きラムダ計算の定式化のひとつです。大きなラムダ計算をまともに紹介したことがなかったので、この記事と引き続く記事の2回に分けて説明します（続く第2回もほぼ書き終えていますよ ^_^）。

この2回の記事で、大きなラムダ計算の構文的・証明論的側面を紹介します。ラムダ式への型付けアルゴリズムを形式的証明と捉えて、その証明系の性質を調べます。カリー／ハワード対応を意識してのことです。証明系に関するメタ定理は、ラムダ式と証明図の構造に沿った帰納法で（メタに）証明できますが、煩雑で若干テクニカルなのでだいたい省略します（いつかちゃんと書くかも）。

「型付きラムダ計算を、構文だけで理解するのは苦しい」と思うので、集合圏におけるインフォーマルな意味論にも少しだけ触れます。少数ですが、複圏／多圏のストリング図も（次回に）載せます。本格的な意味論や絵算（pictorial/graphical/diagrammatic calculation）は展開しませんが、単なる構文解説だけよりは実感が増すと思います。

今回 1/2 の内容：

次回 2/2 の内容：

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化： 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. 圏LLEの定義
  11. 圏LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

予備知識と参考資料

ゼロからのラムダ計算入門には、10年前（2007年）に書いた一連の記事が、今でも役立つと思います。

  1. JavaScriptで学ぶ・プログラマのためのラムダ計算 ： プログラミング言語JavaScriptを引き合いに出して、ラムダ計算をインフォーマルに説明しています。意図的ではありますが、関数抽象を（狭い意味の）「ラムダ式」と呼んだり、通例（「関数を引数に適用する」）とは逆の表現「引数を関数に適用する」をしているので注意してください。
  2. JavaScriptで学ぶ・プログラマのためのラムダ計算 問題集 ： すぐ上の記事に対する練習問題集です。
  3. 絵を描いて学ぶ・プログラマのためのラムダ計算 ： ラムダ項の構文解析木を使ってベータ変換を解説しています。なお、この過去記事で使っている絵はベータ変換の可視化が目的で、圏論ベース絵算のストリング図ではありません。

型無しラムダ計算の構文とベータ変換（簡約）を簡潔にまとめた記事として、id:tarao（たらお）さんによる次があります。

僕は、アルファ変換について説明してない（予告して不履行）ですが、アルファ変換はけっこう厄介です（ラムダ計算 - Wikipedia）。アルファ変換を知るには、id:sumii（住井）さんの次のテキストの1.5節あたりまで読むのがいいと思います。

ちなみに、上記テキストで"typing"の訳語が「型つけ」なのですが、ナルホド! 口頭でも「片付け」と混同しなくて良いですね。

型付きラムダ計算とデカルト閉圏の関係は次の記事達に書いています。解説というより、雰囲気を伝える“お話”です。興味があれば眺めてみてください。

大きなラムダ計算とは何か

型付きラムダ計算のラムダ式は、変数の型がハッキリしてないとダメなんです。ですから、λx.(g・(f・x)) のような式（ドット'・'は適用だとする）だけ出してもダメです。x, f, g の型を明示する必要があります。型の明示には型宣言を使うことにします*1。A, B, Cを型（の名前）だとして次のように宣言します。

  1. xの型は、A
  2. fの型は、AからBへの関数型
  3. gの型は、BからCへの関数型

これらの宣言を記号的に次のように書きます。

  1. x:A
  2. f:A->B
  3. g:B->C

'->'は関数型を作る記号で、普通の矢印'→'じゃなくて、ハイフンと不等号です。矢印'→'は他でも多用されるので記号を変えました。[A, B] という書き方も多いですが、ブラケットも他の目的で使うので、関数型は A->B にします。

ラムダ式と型宣言を一緒にしてパッケージしたものが大きなラムダ式*2です。ただし、ラムダ束縛変数の型宣言は'λ'の直後に埋め込んでいます（それが普通の書き方）。次は大きなラムダ式の例です。

  • 〈f:A->B, g:B->C| λx:A.(g・(f・x))〉

大きなラムダ式との対比のために、内側に置かれたラムダ式を小さなラムダ式とも呼びます。大きなラムダ式の基本的な形は次のようです。

  • 〈型宣言| 小さなラムダ式〉

小さなラムダ式（裸のラムダ式）ではなくて、常に大きなラムダ式を使って進めていくのが大きなラムダ計算です。基本はそれだけのことです。

この記事（＋次回）で大きなラムダ計算について最初から説明するので過去記事を参照する必要はありませんが、歴史的経緯を言えば、2008年／2009年あたりのセミナーでは、大きなラムダ計算をインフォーマルに導入しています。

大きなラムダ計算の短い説明ならば次の記事にあります。

概要と目標

前節で説明したような大きなラムダ式（後で少し定義を拡張します）の全体を考えます。すべての大きなラムダ式からなる集合をLLE（large lambda expressionから）とします。LLEに、圏の構造を与えることができます。正確な言い方をすると、集合LLEをベースに圏を作れる、となります。集合LLEをベースに作った圏のほうは太字でLLEと書くことにしましょう。

集合LLEと圏LLEとの関係は、

  • Mor(LLE) = LLE

です。つまり、大きなラムダ式は圏LLEの射（morphism）となります。

では、圏LLEの対象は何でしょうか？ それは、大きなラムダ計算で使う型の集合です。当該ラムダ計算で使用できるすべての型の集合をTypeとすると、

  • Obj(LLE) = |LLE| = Type*

です。Type*はTypeの要素を並べたリストの集合、つまり“単一の型を並べたリスト”の集合です。

この記事（＋次回）の目標は、圏LLEを構成することです。

注意すべきは、圏LLEは完全に構文的に作られているということです。（型付き）ラムダ計算に意味を与えることは、構文領域である圏LLEから意味領域となる圏Cへの関手を作ることです。（意味関手は、単なる関手以上にモノイド構造や閉構造などを保つことも要請します。）例えば、C = Set として、意味関手 SetSem:LLE→Set を作れば、ラムダ計算を集合と写像の計算として解釈することになります。

意味関手が値を取る圏Cを変えればまったく別な意味論ができます。例えば、順序代数構造（Heyting algebraなど）から作られたやせた圏をCとすることもできます。Cを固定しても意味関手は色々作れます*3。

今回（＋次回）は圏LLEを作るまでで、その上に意味関手を定義はしませんが、意味論を展開する構文的基盤を準備するのだと思うとよいでしょう。

集合と写像に関する基礎的事項

この節は、インフォーマルな意味論の説明に必要となる用語のまとめです。ザッと眺めるだけ、あるいは飛ばしてしまってもけっこうです。

A, B, Cなどは集合を表すとします。fがAからBへの写像であることを f:A→B と書きます。x∈A ならば、f(x)∈B です。A×Bは集合の直積で、g:A×B→C とは、「gが、AとBのペアを入力としてCの要素を返す写像である」ことです。x∈A, y∈B ならば、g(x, y)∈C です。なお、写像と関数は同義語として扱い、特に区別しません。

関数集合

AからBへの写像の全体を集合と考えたものをBAと書きます。この指数記法は入れ子にするのが辛いので、BAを A->B とも書きます。矢印風記法なら、入れ子も問題ありません； 例えば、A->(B->C) 。A->B を指数集合（exponential set; もともと指数記法で書いたので）とか関数集合（function set）と呼びます。

関数オブジェクト

f:A→B と f∈(A->B) は同じ意味ですが、「AからBへの写像」と「A->B の要素」を区別しないと混乱してしまうことが多いので、関数集合 A->B の要素を関数オブジェクト（function object）と呼ぶことにして、写像fに対応する関数オブジェクトを^fと書きます。（f^とも書きますが、今回は左肩にハットを付けます。）

  • f:A→B ⇔ ^f∈(A->B)

関数オブジェクト^fは、働きとしてのfをコンパイルした結果であるバイナリコードだと思うといいでしょう。^fはバイナリコード＝実行可能データです。

適用

入力データxと実行可能データ^fを渡して実行する仮想マシン（の概念的モデル）をappとすると、appは次のような写像です。

  • app:A×(A->B)→B

実行結果は、もとの写像fの値となるので、次の等式が成立します。

  • app(x, ^f) = f(x)

appと入力の順序が逆である写像をapp'とします。

  • app':(A->B)×A→B
  • app'(^f, x) = f(x)

appやapp'を適用写像（application）とか評価写像（evaluation）と呼びます。

写像の直積

集合だけでなくて、写像にも直積を定義しましょう。f:A→X, g:B→Y のとき、f×g:A×B→X×Y は次のように定義します。

  • (f×g)(x, y) := (f(x), g(y))
デカルトペア

<f, g>(x) = (f(x), g(x)) と定義される写像を、fとgのデカルト・ペア（Cartesian pair）と呼びます。写像の直積とデカルトペアは、対角写像Δ（定義： Δ(x) = (x, x)）により次のように関係付けられます。

  • <f, g> = Δ;(f×g)
射影と成分

A×B→A という射影をπ1、A×B→B という射影をπ2と書きます。f:C→A×B のとき、f1 = f;π1、f2 = f;π2 と書きます。f1をfの第一成分（first component）、f2をfの第ニ成分（second component）と呼びます。具体的に書くと：

  • f(z) = (x, y) のとき、f1(z) = x、f2(z) = y
単元集合と廃棄写像

1 = {0} として単元集合（シングルトン集合； singleton set）と呼びます。単元集合の唯一の要素は何でもいいです。単元集合を型とみなすときはユニット（unit）型とかヴォイド（void）型とか呼びます。

任意の集合Aから1への写像がただひとつだけあるので、それを!Aと書きます； !A:A→1。!Aには様々な呼び名があります： terminal morphism, final morphism, discarder, discharger など。ここでは、入力を捨ててしまうので廃棄写像（discarding map）と呼びましょう。

型システム

これから先「型」という言葉を頻繁に使います。「型」という言葉の解釈は、めちゃくちゃイッパイあります。ここでは、次の2つの立場を適宜使い分けます。

  1. 型とは集合である。
  2. 型とは単なる記号である。

インフォーマルな意味論としては、「型」は集合を表すと考えます。しかし今回は、オフィシャルな意味論の話はなくて、構文論だけです。実際のところは“ある種の記号”を「型」と呼ぶことになります。

インフォーマルな意味論も含めて、型を構成する手順を説明しましょう。まず、有限個の集合を選びます。例えば、自然数の集合 N = {0, 1, 2, ...} ひとつだだけを選びます。選んだ集合に名前（の記号）を割り当てます。例えば、自然数の集合に英字大文字'N'を割り当てます。他に、英字大文字'I'を単元集合1を表す記号として予約します。これで基本型記号（basic type symbol/name）が決まります。

何でもいいので2種類の結合子記号（connective symbol）を決めます。例えば'△'と'♂'にします。一般的な型記号（type symbol）、あるいは型項（type term）を帰納的に定義します。

  1. 基本型記号は型記号である。
  2. AとBが型記号ならば、(A△B) は型記号である。
  3. AとBが型記号ならば、(A♂B) は型記号である。
  4. 以上により定義されたものだけが型記号である。

心づもりとしては、型記号は集合を表すものです。基本型記号がNとIの場合、型記号Aが表す集合を〚A〛とすれば：

  1. 〚N〛 = N, 〚I〛 = 1
  2. 〚A△B〛 = 〚A〛×〚B〛
  3. 〚A♂B〛 = 〚A〛->〚B〛

例えば ((N△I)♂(N♂N)) の意味は 〚((N△I)♂(N♂N))〛 = (N×1)->(N->N) と計算できます。

以上の“記号の意味”はあくまで心づもり、想定であって、実際には意味論なしの構文論を考えます。したがって、オフィシャルには型とは型記号（型項）のことです。

型が等しいとは、集合の同一性や同型性ではなくて、記号として（図形として）の等しさです。(I△N) と N は違う記号なので違う型です。((N△N)△I) と (N△(N△I)) も違う記号なので違う型です。型Aと型Bがイコールだとは、AとBがまったく同じ記号のことです。

いま、結合子記号に'△'と'♂'を選びましたが、'×'と'->'にします。そうすると、集合のホントの直積／指数と区別が付かない問題が起きますが、文脈により、単なる結合子記号か集合の演算子記号かは区別できるでしょう。

また、(I×N) とか ((N×N)×I) のように律儀に括弧は付けず、I×N、N×N×I のように書きます。要するに、混乱がない限り普通の書き方をする、ということです。普通に書くと、人間の心理として集合を想定してしまいがちですが、オフィシャルには単なる記号だと肝に銘じてください。

続く

次回に続きます。次回で大きなラムダ式の構文を定義して、型付け（typing）を行うための形式的証明系を導入します。そして、構文論だけから得られる圏LLEを定義します。次回内容は：

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化： 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. 圏LLEの定義
  11. 圏LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

*1:変数に型情報をくっ付けるとか、型ごとに別な変数集合を準備するとかの方法もあります。ですが、型宣言が一番実用的だと思います。

*2:大きなラムダ式は、実質的には型付きラムダ項（typed lambda term）と変わりません。型宣言とのパッケージを徹底することが意図されています。

*3:[追記]構文的な体系をひとつに固定したとして、圏Cに値を取る意味関手がたくさん定義できるのは事実です。しかし、これは鬱陶しくてイヤな状況です。できるなら、Cを決めれば一意的に意味関手が定まって欲しい -- この希望をかなえるように意味論を構成することは可能です。僕が「セマンティック駆動」と言ってきた方法は、Cを先に与えて、それから一意に意味関手を作る方法です。[/追記]