抽象的なセッティングで議論していても、最後は結局“具体的な計算”に頼ることはよくあります。具体的な計算には(インフォーマルな)ラムダ式/ラムダ計算が使われることが多いでしょう。具体的な計算をできるだけ楽にするために、ラムダ式の記法を工夫してみます。
内容:
簡単な事例
R2 の標準的ユークリッドノルムを norm と書くことにすると、次のようになります。
二乗する関数を sq 、足し算を sum 、平方根関数を sqrt とすると、norm は次の可換図式で定義されます。
は でもいいのですが、数の掛け算との混同を避けて記号''を使っています。
上図の可換性は、次の等式と同じです。
セミコロンは、関数の図式順結合記号です。
等式の左右をラムダ式で表現しようと思いますが、ラムダ式で使うラムダ変数〈引数変数 | 束縛変数〉を図式に記入しておきます。
記号 '' は、集合への所属を主張しているというよりは、変数の型宣言です。ペア(長さが2のタプル)を引数に取る関数は、多変数関数ではなくてタプル1変数関数と考えます(「タプル1変数関数と多変数関数」参照)。
可換図式に対応する等式は:
簡単なことをわざと複雑に書いている印象があるでしょうが(実際そうです)、事例として使うためにこんなことしてます。この等式の右辺のように、ラムダ式(の関数抽象)で書かれた関数が結合記号で繋がった形が今日の話題です。
一般に、結合記号で繋がれたラムダ式(関数抽象)を簡約化するルールは次のようです; がなんらかの式だとして、
ここで、=> は式の変形方向付きのイコール、凹レンズ括弧()は、直前の式に対する代入操作を表します。
この一般的なルールに基づいて、ノルムの例を計算してみます。
式も、その変形の過程も、あまり見やすくないですねぇ。
ブロックラムダ式
関数の結合や代入を簡潔に表すために、ブロックラムダ式を導入します。まず、 を次の形で書くことにします。
プログラムコードに近い雰囲気になりました。1行目は、繰り返しのfor文ではないので、区別したいときは所与for文と呼ぶことにします。"for given x" の意味です*1。2行目はreturn文で、常識的に解釈してください*2。
for, return 以外に、代入を示すlet文が書けるとします。例えば、前節最後の例だと:
随分と見やすいでしょう。関数結合の連続、代入の連続が、上から下に向かって読む順次実行の形で表現されます。手続き的な表現ですが、セマンティクスはラムダ計算のセマンティクス(表示的意味論)がそのまま使えます。
この書き方の式をブロックラムダ式〈block lambda {expression | term}〉と呼ぶことにします。ブロックラムダ式の変形(代入操作)は次のように行います。
変形の過程も見やすいですね。これは、可換図式を、ショートカットをしながら変形していく過程と同じことです。
ブロックラムダ式の動機は、可換図式が指示する計算を、なるべく素直に見やすく写し取ることです。
定義環境の記述
ノルムの例で、sum と sqrt は組み込み関数〈プリミティブ関数〉だとします。しかし、sq はユーザー定義関数だとしましょう。sq の定義がないと未定義エラーになってしまいます。
関数の定義もlet文で次のように書くことができます。
ただし、この書き方だと若干視認性が悪いし、関数定義であることをもっと強調したいので、次のようにします。
define文はシンタックスシュガーなので、let文による記述を禁止するものではありません(そもそも、letもシンタックスシュガーです)。必要なら、(記述順で)後から代入(むしろ束縛)を指定するwhere文を入れてもいいでしょう。
関数定義は何度も利用されることがあるので、別に書いておくこともできます(できるとします)。複数の関数をまとめて定義しておけば、関数ライブラリとして使えます。
おわりに
モナドやベックの分配法則などに関わる法則は、ストリング図等式や可換図式で表現されます。ストリング図ノードや図式矢印が行列計算や積分計算を含む複雑なものになることもあります。それらの関数をテキストに写し取るとき間違いを犯すことはよくあります。
絵図と親和性が高くて視認性が良いテキスト記法を採用すれば、間違いを減らせます。ブロックラムダ記法は、この目的で使えると思います。