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

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

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

参照用 記事

デカルト閉圏を計算するスタックマシン、シーケント計算、カリー/ハワード対応

デカルト閉圏(Cartesian Closed Category; 略称CCC)は、型付きラムダ計算のモデルです。でも、僕らが普通にデカルト閉圏で計算するとき、ほんとうに型付きラムダ計算を使っているかと言うと、そうでもなくて、多変数の関数とかも使います。タプルの一変数じゃなくて多変数の関数を扱うなら、普通の圏より複圏(multicategory)のほうが便利です。多値関数も含めるなら多圏(polycategory)を使うといいですね。

我々は無意識に、デカルト閉圏Cから作った多圏 M = M(C) を使っているような気がするんですよ。ここいらへんの事情を「うまく説明する方法がないのかなー」とずっと考えていました*1。「スタックマシンを使えばいいかもな」とフト思いついたので簡単に紹介します。

内容:

スタックマシン

スタックが1つとコード領域からなるマシンを考えます。スタックの状態は、x1, x2, ... のように書き、左がスタックトップだとします。別に右がトップでもいいけど、決めないと話が先に進まないので。関数の引数と戻り値は1つのスタックで受け渡しを行います。

プログラムコードは関数の列です。関数はスタックから引数を取って、計算結果を同じスタックに積みます。スタックの状態とプログラムコードの組を計算状況、または単に状況と呼びましょう。状況は (プログラムコード | スタック状態) の形で書きます。

例を挙げると、(add; mult | 2, 3, 4) は計算状況です。プログラムコードである関数列は左から順に実行します。実行すべき関数がなくなるとプログラムの実行全体が終了します。次のようです。

   (add; mult | 2, 3, 4)
  ------------------------[STEP]
    (mult | 5, 4)
  ----------------[STEP]
     ( | 20)

div(割り算)は商と余りを返す多値関数だとすると、次のような計算ができます。

   (div; add; mult | 10, 3, 5)
  ----------------------------[STEP]
    (add; mult | 3, 1, 5)
  ------------------------[STEP]
     (mult | 4, 5)
    --------------[STEP]
      ( | 20)

関数のプロファイル

関数の引数と戻り値の仕様をプロファイルと呼びます。次のように書くのが普通です。

  • add : integer, integer → integer
  • mult : integer, integer → integer
  • div : integer, integer → integer, integer

ここでは少し記法を変えます。コロンとセミコロンは紛らわしいので、「:」を「::」にします。Haskellなんかと同じです。矢印は「⇒」にします。一本棒矢印を別な意味に使いたいからです。この記法でプロファイルを書き直すと:

  • add :: integer, integer ⇒ integer
  • mult :: integer, integer ⇒ integer
  • div :: integer, integer ⇒ integer, integer

一本棒の矢印は、指数型(ベキ型、関数データ型)に使います。A→B は、型Aから型Bへの関数データの型です。A→B の代わりに B←A も使います; このほうが BA という書き方と似ていて具合がいいです。

強い型付け

関数(プログラム)にもデータにも型を持たせましょう。関数の型はプロファイルです。データの型は普通にintegerとかbooleanとかです。3 : integer とか true : boolean とか書くことにします(データのときはコロン1つ)。スタックマシンは強く型付けされた計算をするとして、型エラーはハードウェアが検出してハードウェア・ランタイムエラーとなると仮定します。

計算状況のすべてに型を明示すると、実行ステップの図は次のようになります。記述が長くなるのを避けるために、integerをiと略記します。

   (div::i,i⇒i,i; add::i,i⇒i; mult::i,i⇒i | 10:i, 3:i, 5:i)
  -------------------------------------------------------------[STEP]
    (add::i,i⇒i; mult::i,i⇒i | 3:i, 1:i, 5:i)
  ---------------------------------------------[STEP]
     (mult::i,i⇒i | 4:i, 5:i)
    --------------------------[STEP]
      ( | 20;i)

プログラムの同値性

このスタックマシンのプログラムは、プロファイルが指定された関数の列です。それは次のような形をしています。

  • (f1::A1⇒B1; f2::A2⇒B2; ...; fn::An⇒Bn)

長さが1の列や空列も認めます。プログラムをギリシャ文字大文字Γ、Δなどで表し、スタック状態はギリシャ文字小文字σ、τなどで表すことにします。計算状況は (Γ | σ) のようになります。プログラムを実行すると、最終的には計算状況の左側は空になるので、( | τ) という形になります。スタック状態τのトップがプログラムの結果です。ただし次の場合はハードウェア・ランタイムエラーです。

  1. 関数が必要とする引数がスタック上に存在しない。
  2. 関数の引数の型と、スタック上のデータの型が一致してない。

さて、プログラムΓとΔが同値であるとは、どんなスタック状態σに対しても、2つのプログラムの結果が一致することです。もう少し詳しく言うと:

  1. (Γ | σ) がエラーするなら (Δ | σ) もエラーする。逆も成立する。
  2. (Γ | σ) が成功するなら (Δ | σ) も成功し、結果が一致する。逆も成立する。

(Γ | σ) の実行がエラーすることを (Γ | σ)↑、実行が成功して結果が x になることを (Γ | σ)↓x と書くことにすれば、「ΓとΔが同値である」という命題は次のように書けます。「⊃」は含意、「∧」は連言を表す論理記号です。

  1. ∀σ.[((Γ | σ)↑ ⊃ (Δ | σ)↑) ∧ ((Δ | σ)↑ ⊃ (Γ | σ)↑)]
  2. ∀σ.[∀x,y.((Γ | σ)↓x ⊃ ((Δ | σ)↓y ∧ x = y)) ∧ ∀x,y.((Δ | σ)↓y ⊃ ((Γ | σ)↓x ∧ x = y))]

プログラムΓとΔが同値であることを、Γ≡Δ と書きます。

カリー化

f :: A, B⇒C という関数があるとき、二番目の引数でカリー化(ラムダ抽象)することを大文字Λで表します。カリー化した関数のプロファイルは、Λ(f) :: A⇒C←B となります。C←B は、 BからCへの関数を表すデータの型でしたね。型がC←Bであるデータは関数そのものではなくて、関数の表現とみなします。「関数の表現とデータから関数値を計算する」関数はApplyとします。

  • Apply :: C←B, B ⇒ C

カリー化の操作Λは、必ず最後の引数に対して働くと約束しておきます。次はカリー化の例です。

      f :: A, B⇒C
 ----------------------[CURRY]
  Λ(f) :: A ⇒ C←B

      g :: A, B, C ⇒ D
 ------------------------[CURRY]
  Λ(g) :: A, B ⇒ D←C

      h :: A, B ⇒ C, D
 ------------------------[CURRY]
  Λ(h) :: A ⇒ C, D←B

ラムダ計算の基本公式

デカルト閉圏Cで考えると、カリー化の操作Λは、C(A×B, C) と C(A, CB) の同型を与えます。この事実(の表現)は「ラムダ計算の基本公式」と呼んでいいでしょう。Λの逆を具体的に与えるにはApply(Evalと呼ばれることもある)を使います。このことをスタックマシンを使って説明します。

f :: A, B⇒C が関数、つまりプログラムの実行単位だとします。スタックマシンは実行だけでなく、プログラムの変形操作をサポートするとします。それがΛ(CURRYとも書く)です。f :: A, B⇒C と、これを変形した Λ(f) :: A ⇒ C←B は事実上同値ですが、同値性にはApplyが介入します。以下に示す2つの実行過程が同値性を与えます。

  (f :: A, B⇒C | a:A, b:B)
 ---------------------------[STEP]
    ( | f(a, b) : C)
  (Λ(f) :: A ⇒ C←B; Apply :: C←B, B ⇒ C | a:A, b:B)
 --------------------------------------------------------[STEP]
   (Apply :: C←B, B ⇒ C | λy.f(a, y):C←B, b:B)
  -------------------------------------------------[STEP]
      ( | (λy.f(a, y))・b = f(a, b) : C)

Applyは、このスタックマシンの機械語命令です。一方、カリー化操作Λ(あるいはCURRY)は、実行のなかで使われるのではなくて、実行とは別なレベルのプログラム変形を行うのでメタ命令となります。メタ命令Λが、計算状況のプログラム側にだけ働くとして、メタ命令も含めた実行過程を図示すると次のようになります。SETは、プログラムを計算状況の適切な場所に埋め込む操作とします。

      f :: A, B⇒C
  ----------------------[CURRY]
   Λ(f) :: A ⇒ C←B
  -------------------[SET]
  (Λ(f) :: A ⇒ C←B; Apply :: C←B, B ⇒ C | a:A, b:B)
 --------------------------------------------------------[STEP]
   (Apply :: C←B, B ⇒ C | λy.f(a, y):C←B, b:B)
  -------------------------------------------------[STEP]
      ( | (λy.f(a, y))・b = f(a, b) : C)

上の図で表される実行過程が、 (f :: A, B⇒C | a, b) のワンステップ実行(単一の関数呼び出し)と同じなのです。スタック状態に関わらず同じ結果を与えるので、次の同値性が成立します。

  • (f :: A, B⇒C) ≡ (Λ(f) :: A ⇒ C←B; Apply :: C←B, B ⇒ C)

シーケント計算を少しでもご存知の方は、実行過程を描いた図がシーケント計算の証明図と似ていると感じたでしょう。はい、そうです。カリー/ハワード対応です。多圏における絵算を使えば、これらの事がより鮮明に直感的に説明できます。絵算を少しでもご存知の方は試してみてください。

*1:以前から説明に使っていた方法は、大きなラムダ式(関数)と小さなラムダ式(関数データ)です。