ノラ・ミャオとかアンジェラ・マオとか知っている人はいるだろうか？
という話とは何の関係もなく；；
「letrecとwhere」において：
letrecはものすごく役立つ概念なんですが、書き方で悩みます。
と書きました。
letrecがなんでものすごく役立つかというと、それは不動点方程式の解を与えるからですね。
「カザネスク／ステファネスク／ハイランド／長谷川の定理」によると、トレース付きデカルト圏では、不動点方程式の解はトレースを使って書き下すことができます*1。具体的には、f:A×X→X の不動点は、Tr(f;Δ):A→X で与えられます。ここで、Δは対角です。余単位!と対角Δを持つ対称モノイド圏がデカルト圏なのでした。特に、A = 1 なら、f:X→X とみなしてよく、f;Δ:X→X×X で Tr(f;Δ):1→X となり単一の不動点を与えます。
letrec R in E という形が、トレース付きデカルト圏でどう解釈されるかを、以下に簡単に示しましょう。
Rはletrecの束縛で、x1 = F1, ..., xn = Fn という形をしています。ここで、xi達は互いに異なる変数で、Fi達は式（ラムダ項）です。x≡(x1, ..., xn)、F≡(F1, ..., Fn) というベクトル記法（タプル記法）を使うなら、x = F と書いてもいいでしょう。すると、letrec式は、letrec x = F in E と書けます。
F1, ..., Fn に含まれる（x1, ..., xn以外の）自由変数を a1, ..., am とします。また E に含まれる x1, ..., xn, a1, ..., am 以外の自由変数を b1, ..., bk とします。このletrec式に関係する変数は、x1, ..., xn, a1, ..., am, b1, ..., bk で全部だとします。
ベクトル変数 x≡(x1, ..., xn) が走るであろう変域をXとします。同様に、a≡(a1, ..., am) の変域をA、b≡(b1, ..., bk) の変域をBとします。これらの変域は、デカルト圏の対象と解釈します。
そうすると、F≡(F1, ..., Fn) の意味は、f:A×X→X という射となります。Eの値の型は変域Yに対応するとすれば、式Eの意味は、g:B×A×X→Y となります。
letrecは、不動点方程式 x = F を解くので、意味的には、Fix(f) = Tr(f;Δ):A→X が得られます。式Eは不動点方程式の解である x≡(x1, ..., xn) と、もともとあったパラメータ（自由変数） a≡(a1, ..., am), b≡(b1, ..., bk) を使うので、入力情報として (idB×ΔA);(idB×idA×Fix(f)) を受け取ることになります。
結局、letrec R in E の意味は、
- f:A×X→X
- g:B×A×X→Y
だとして、
- (idB×ΔA);(idB×idA×Fix(f));g : B×A→Y （Fix(f) = Tr(f×ΔX)）
ということになります。
複雑そうに見えますか？ だとしたら、letrecはそんな複雑なことを自然な構文でサラリとやってのけていてエライ！ってことになります。
