カリーをもっと -- ラムダで考えるカリー化 - 檜山正幸のキマイラ飼育記 (はてなBlog)

「もっとかしこいカリー化」で紹介した、nanto_viさん、kilreyさん、KENZさんのコードはいずれも、ラムダ式によるカリー化の表現と正しく対応しています。最初からラムダ計算で考えればよかった。「なんでそんなことに気が付かないんだ？」と言われそうですが、それはですね；僕みたいに後知恵で理屈をこねるヘタレと、直観で判断しても正しい結果を得るエキスパートの違いですがね。テキスト処理の方法を思いついたら、そのまま無反省にやってしまったよ、僕は。＜＜実は脊髄野郎だろ

で、以下、後知恵でヘタレ理屈こねます、コネコネェ。

内容：

JavaScriptからfunctional風疑似言語へ
多変数関数のラムダ計算：構文の定義
あらためてカリー化の定義
ラムダ計算規則と計算例
curry関数がカリー化になっていること
補足または蛇足

自分的には、式のモーフィングがニャンカ面白い。

●JavaScriptからfunctional風疑似言語へ

JavaScriptとラムダ式の相互翻訳をするには、双方から歩み寄りが必要です。まず、JavaScriptの大域関数だけ考えて、記法を関数型言語に近づけてみます。

事例として、nanto_viさんのcurry関数：



function curry(func)

{

  return function (first) {

    return function () {

      var args = Array.prototype.concat.apply([first], arguments);

      return func.apply(this, args);

    };

  };

}

ここで、Array.prototype.concat.apply([first], arguments);という、やや技巧的な表現があるので、putfirstという関数を導入しておきましょう。で、var args = putfirst(first, arguments);と書き換わります。

returnを取り除いて、変数もやめると、次のような感じ。もちろん、この段階で疑似言語（実在しない）になってしまいますが：



curry(func) := 

  function (first) {

    function () {

      func.apply(this, putfirst(first, arguments));

    }

  }

あれ、applyはメソッドのままでした、大域関数applyに直します。applyの第一引数も（大域関数だけ扱うなら）不要。それと、特殊な変数であるargumentsも引数の形にすれば、次のようになります：



curry(func) := 

  function (first) {

    function arglist {

      apply(func, putfirst(first, [arglist]));

    }

  }

function arglistのように書いたとき、arglistは引数並びであり、[arglist]は並びを配列にまとめたものとします。

●多変数関数のラムダ計算：構文の定義

ラムダ計算を少し手直しします。もともと、ラムダ計算は1変数（1引数）関数の計算体系ですが、それじゃカリー化の出番がないので、f(x, y, z) のような表現を認めるように変更します。また、複合データとして配列も導入しましょう。

そんな方針で、以下にラムダ式（ラムダ項）の構文を定義します：

変数名と関数名は最初から区別しておきます（そのほうが話が簡単になるので）。変数は、アルファベット後半の英小文字と数字からなる名前、x, y, x1など。関数は、f, g, foo など。
変数（名）、関数（名）はそれだけで項です。
配列は、[項1, 項2, ...] の形。配列も項です。
並び（配列とは違う）は、(項1, 項2, ...) の形。並びは補助的表現で、これ自体は項ではありません。
関数適用は、関数（を表す項）Fと並びAを、F A と空白をはさんで並べた形。あいまいさなく区切れるなら空白を入れなくてもOK。関数適用は項です。
Xが変数並び、Mが項のとき、λX.M は項です。
まとまりを付けるためにカッコを使ってかまいません。厳密には並びを作るカッコと別な記号が必要ですが、「(」「)」を二重の用法で使ってしまえ（どっちの用法かは文脈で判断）。
関数ではない定数（例：1, "hello", null）は必要なだけ導入してかまいません。

項の例は、x, sum, sum(x, 1), mean3(a, b, sum(x, 1)), (curry(sum))(10)(y) など。実はこれだけでは、構文的に正しい項を判定できませんが、その話の前に、メタ記号の使い方を説明しておきます。

X, Y などは変数並びを表すメタ変数、F, Gなどは関数的項を表すメタ変数、M, Nなどは一般的な項を表すメタ変数、A, Bなどは並びを表すメタ変数として使います。
x, yなどは、計算体系内の変数としても、変数を表すメタ変数としても使います。同様に、f, gなどを関数（最初からある記号）を表すメタ変数としても使います。（ほんとは字体を変えて区別すべきだが、面倒だからね。）
Aが並びのとき、Length(A)はAの長さを表します。
Mが項、A=[A1, ..., An]が並びのとき、M@A は [M, A1, ..., An]を表します。
A=[A1, ..., An]、B=[B1, ..., Bm]が並びのとき、A#B は [A1, ..., An, B1, ...,Bm]を表します。

さらに、項のアリティ（arity; 引数の個数）を次のように定義します。

関数（名）には、最初からアリティが定められている。アリティの値は0以上の整数である。（複数のアリティを許すほうが便利ですが、複雑になるからやめましょ。）
Arity(λX.M) = Length(X)
変数、配列、定数（非関数）にアリティは定義されない。

これで、構文的に正しい関数適用を定義できます。

Arity(F) = Length(A) のときだけ、関数適用 F A は正しい構文。

Arity(sum) = 2, Arity(mean3) = 3 だとすれば、sum(x, y), mean3(a, b, c), curry(sum)(10)(y) は正しい項です、λ(x, y).mean3(x, b, y) も正しい項で、そのアリティは2ですね。(λ(x).sum(x, 1))(y, 10) はアリティ不一致でダメ。

以上、かなりインフォーマルな定義ですが、まー、これくらいでいいでしょう。実を言うと、メタ変数（X, Fなど）／メタ関数（Lengthなど）／メタ演算子（@と#）を含む計算体系も形式的（formal）に定義したほうがいいけど、それも、まー面倒だからいいや。

●あらためてカリー化の定義

「gがfのカリー化である」ことは、次のことです。



f(x, y) = g(x)(y)

一般化して、Yが(y1, ..., yn)のような並びだとして、



f x@Y = g(x) Y

x@Y = x@(y1, ..., yn) = (x, y1, ..., yn) 、g(x) Y = g(x)(y1, ..., yn) であることに注意。よーく考えると、「=」の使い方が不明ですが、「式（項）として同じ形」くらいに解釈してください。

もっと一般化すると、X = (x1, ..., xm), Y = (y1, ...,yn)のような状況で：



f X#Y = g X Y

●ラムダ計算規則と計算例

念のため、ラムダ式（項）の計算規則（ベータ還元）を述べます（アルファ変換は省略）。別にこれを理解しなくても、実際の計算は直観的にできると思います。

[ベータ規則] (λ(x1, ...,xm).M)(N1, ..., Nm) ⇒ M[N1/x1, ..., Nm/xm]

それと、いくつかの配列演算はプリミティブとして最初から準備しておきましょう。既に出現したapply, concat, putfirst はプリミティブ、配列のコンストラクタarrayも最初から入れておきます。arrayのアリティが問題になりますが、例外的に可変アリティを許しましょう、これだけは。以下に計算規則：

[apply規則] apply(F, array A) ⇒ F A
[concat規則] concat(array A, array B) ⇒ array A#B
[putfirst規則] putfirst(M, array A) ⇒ array M@A

メタ演算である ' '（空白；関数適用）、'#'（並び連接）、'@'（並びに追加）に対応する関数（記号）が apply、concat、putfirstなわけです。そして、arrayは並びを配列に変換します（メタレベルをオブジェクトレベルに落とす）。

んじゃ計算例、なるべく外側から計算する戦略で：



(λ(a, x).apply(mean3, putfirst(a, array(b, apply(sum, array(x, 1))))))(sum(y, z), 10)

⇒ // by ベータ規則

apply(mean3, putfirst(sum(y, z), array(b, apply(sum, array(10, 1)))))

⇒ // by putfirst規則

apply(mean3, array(sum(y, z), b, apply(sum, array(10, 1))))

⇒ // by apply規則（外側）

mean3(sum(y, z), b, apply(sum, array(10, 1)))

⇒ // by apply規則（内側）

mean3(sum(y, z), b, sum(10, 1)) 

// 記号的計算はこれでオシマイ

●curry関数がカリー化になっていること

ふー、やっと目的の計算ができる。（準備がなげーよ、マッタク。）



curry(f) :=

 λ(x).λY.apply(f, putfirst(x, array Y))

と定義すると、curry(f)が実際にfのカリー化になっていることを計算で確かめましょう。つまり、変数xと変数並びYに関して f x@Y = (curry(f)(x))Y を示します。



(curry(f)(x))Y

⇒ // by 定義

((λ(x).λY.apply(f, putfirst(x, array Y)))(x)) Y

⇒ // by ベータ規則

(λY.apply(f, putfirst(x, array Y))) Y

⇒ // by ベータ規則

apply(f, putfirst(x, array Y))

⇒ // by putfirst規則

apply(f, array x@Y)

⇒ // by apply規則

f x@Y

// オシマイ

今の計算は、(curry(f)(x))Y から f x@Y への方向なので、イコールを示したことになりませんけど、実際はこの方向の計算しか生じないからいいとします。

念のため、ラムダ式の定義がJavaScriptの定義に変容（モーフィング）していくさまを書いておきます：



curry(f) :=

 λ(x).λY.apply(f, putfirst(x, array Y))

｜ウニョニョニョ

↓

curry(f) :=

 function (x) {

  function Y {

   apply(f, putfirst(x, [Y])

  }

 }

｜ニョリニョリ

↓

function curry(f) {

 function (x) {

  function arglist {

   apply(f, putfirst(x, [arglist]);

  }

 }

}

｜ミュミュミュン

↓

function curry(f) {

 return function (x) {

  return function (/* 可変引数 */) {

   return f.apply(this, putfirst(x, arguments));

  };

 };

}

●補足または蛇足

JavaScriptのfunctionalな断片を、多変数ラムダ計算でモデリングするのは面白いような気がしてきたな。でも、面倒だからやらんと思う（ダハハ）。

もしやるのなら、メタ変数／メタ関数／メタ演算子も最初から計算体系に含めて考えたほうがいいでしょう。それと、「並びは項ではない」としたけど、並びも項だと定義して、LengthよりCoarityとでもして、関数適用(F A)の構文的条件は Arity(F) = Coarity(A) のときだけ、とするとカッコいい。ただし、関数名オーバーロードを許した上で、Arity/Coarityをちゃんと定義するのはちょと面倒かも。関数適用の構文条件もイコールで書けなくなるし。

[追記 date="当日"]ほんのちょっと考えてみたけど、Arity/Coarityをストレートに定義するのはできそうにありませんね。細工が必要、つうか、根本的に拡張しないとダメのよう。[/追記]

「並びも項だ」とすると、実際のJavaScriptから離れてしまうけど、本質的に多値（引数も値も複数あるのが普通）という計算体系の例になって、変わった現象が起こるかもよ、よくわからんけど。