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

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

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

参照用 記事

letとletrec 再論

以前、「letrecとwhere」という記事を書きました。この頃僕は、letとletrecという二つのキーワードは要らないのじゃないのか、と思っていました。最近、「スンマセンデシタ、二つ要ります」と反省しています。

let = letrec としたかったのは、letrecが6文字もあるので書くのがめんどくさい、というショーモナイ理由です。3文字のletをletrecの意味で使えば、短く書けていいな、っと。

3文字のletをletrecの意味に使うと、本来のletは使えなくなります。でもwhereで代用できます。つまり、次のように使い分ければいいかな、と。

  1. 前置のlet -- 実はletrecの意味で、再帰を考慮する。
  2. 後置のwhere -- 再帰を考慮しない単純な置き換え。

しかし、「letrecとwhere」に書いたように、letとwhereのペアが構文としてバランスが悪いなー、とも思ったりしました。バランスの悪い構文で、前置と後置を使い分け、whereは5文字だし、… と、そんなにいいことないじゃん。3文字余分にキーボードを叩くことを我慢して、前置のletとletrecに統一したほうが幸せみたい。

どうでもいい話を書いているので、ちょっと理屈の補足をします。f:X→X に対する不動点は、ミュー記号を使って μx.t のように書きます。ここでtは、関数fを表現する項(term)で、変数xは、変域Xを走ると想定しています。項tに自由変数aが含まれるなら、f:A×X→X のように考えて、μx.t はAでパラメータ付けされた不動点族 A→X を表すと考えます。

letrecは、μx.t を使いやすくした形で、g:X→Y という後続する関数を一緒にして、g(μx.t) を letrec x = t in s と書くのです。sは関数gを表す項です。sも自由変数を持っていてもかまいません。tとsの自由変数を一緒にしたパラメータ領域を改めてAと書くと、letrec x = t in s は、g(μx.t) の別表記であり、A→Y という関数を表現します。

X = X1× ... ×Xn、A = A1× ... ×Am ならば、fを成分表示して、


f(x1, ..., xn, a1, ..., xm)
= (
f1(x1, ..., xn, a1, ..., xm),
...
...
...
fn(x1, ..., xn, a1, ..., xm)
)

のように書けます。成分fi に対応する項をtiとすれば、g(μx.t) は、letrec x1 = t1 ... xn = tn in s となるわけです。letrecが再帰を表現できるのは、関数の再帰的な定義が高階関数不動点を求めることであり、ミューオペレータが不動点を求めるオペレータだからです。

一方、letは再帰不動点とは無関係で、let x1 = t1 ... xn = tn in s は、関数合成 g(f) に対応する項を作るだけです。letはパラメータ(自由変数)を持てたり、部分的な束縛を書けたりするので、単なる関数合成(=射の結合)よりは柔軟ですけど。


「6文字もあって長い」なんてブータレたんですが、letrecはホントに良く出来たシンタックスシュガーだなー、と感心します。letやwhereとも組み合わせて書くと、人間にとって比較的に自然で、それでいて厳密な記述ができます。素晴らしいですね。

[追記]

letrecの話は去年(2013年)の夏にもしてますね。僕の好みの話題。

letrecといえば、まさに「不動点方程式とトレース付き圏」を具現している構文なんですが、そこらへんのことは、長谷川真人さんの素晴らしいスライドで見事に解説されています。

長谷川さんのスライドの絵は「これはひどい誤解だ -- フローチャートは手続き型…だってぇー?!」でも引用しています。

上のほうの letrec x = g(f(x)) in x = letrec y = f(g(y)) in g(y) という等式は、先日話題にした対角自然性(dinaturality)です。9月30日の記事で出しておいた等式 (f#g) = (g#f)#g が、letrec でちゃんと表現できます。

下側の letrec x = {letrec y = h(x, y) in y} in x = letrec z = h(z, z) in z は、ダブルダガー公式とか対角性とか呼ばれているものです。これも不動点の大事な性質(形式的には公理として扱う)です。

フローチャートをめぐる迷信と妄言と愚昧」でも次の絵を引用しているのでした。

式の右側が切れてしまっていますが、等式は letrec x = f(x, y), y = g(x, y) in x = letrec x = f(x, {letrec y = g(x, y) in y}) in x となります。これは、連立不動点方程式が、ガウスの消去法で解けることを主張しているもので、ベキッチ(Beki'c)の公式と呼ばれたりします。成分の方程式を順番に解いていけば連立方程式が解ける、という実にありがたい公式です。

[/追記]