「Lucid, the Dataflow Programming Language」を翻訳してみた。（その9）

前回の続き。

2.2 Iswimの構文

Iswim()という言語の（抽象）構文（syntax）と意味論（semantics）は代数によって完全に定まる。
Iswimファミリはシンプルであり、以下の数段落で合理的で正確な仕様を与えることが出来る。

代数が与えられると、そのシグネチャはIswim()の構文（つまり構文的に正しいプログラムの集合）を決定する。
Iswim()のプログラムは、引数をとらない変数とシグネチャの個体定数から構築される式である。
式は、シグネチャの操作定数への適切な数の引数の適用と、関数への引数（実引数）のリストの適用、および、where節の形成によって構築される。
where節の中で定義された変数と関数は、節のローカルであると言われる。
構文で必要とされる制約は、次のことを保証するだけである：

1. 節の各ローカルは、その節の中で1回だけ定義される。
2. 節の各ローカルは、その節の中では、その定義と同じアリティで使用される。
   つまり、関数呼び出しの実引数の数は、最も内側の節の定義の仮引数の数と同じでなければならない。
   （特に、変数として定義されているローカルは、 その節で変数として使用される）
3. 関数定義の仮引数は、互いに異なっていて、かつ、定義しようとしている関数とも異なること。
4. 関数定義の仮引数は、定義の右辺で変数として使用される。
5. シグネチャの各操作定数は、によって規定されたアリティで使用される。

これをより正確に書くと、以下のようになる。
任意のシグネチャが与えられたとき、ランク付き（-ranking）とは、の操作定数にランクがあるのと同様に、すべての変数にランクを割り当てることによってを拡張したオブジェクトである。
シグネチャと、というランク付きが与えられたとき、Iswimの-式（-expressin）とは、で定められたランクに一致するように定数と変数（関数も含む）が使用された式である。（where節の中で、変数（関数も含む）は再定義され、別のアリティ（＝ランク）を持ちうる ）

一般に、-式は、以下のいずれかである：

1. 単独のシンボル、すなわち、でランクが0と割り当てられている定数もしくは変数
2. 一連の実引数を伴った関数もしくは操作定数；ここで、でそのランクがと割り当てられている場合、一連の実引数はそれぞれ-式
3. 1つの-式（主題（subject））と-定義（-definitions）の集合（本体（body））からなるwhere節；はで定義された変数（関数を含む）に割り当てられたランクで、とは異なる；での定義は矛盾があってはいけない、すなわち、ある変数（関数を含む）の定義は、ただ一度だけされる

1つの-定義は、定義される変数（関数を含む）と、一連の変数（仮引数）、および、-式（右辺）で構成され、は仮引数のランクに0が割り当てられるのを除いて、と同じランク付けとなっている。
仮引数は、定義される変数と異なるものでなければならない。
仮引数の長さは、定義される変数（関数を含む）がで割り当てられているランクと同じでなければならない。

Iswim()のプログラムは、1つの-式である；ここでいうはのシグネチャのすべての変数にランク0を割り当てて拡張したランク付けである。
したがって、プログラムは自由（未定義）変数を持つことができるが、そういった変数は、関数としてではなく、単独のシンボルとしてだけ使用される。

2.3 Iswimの意味論

Iswimの意味論（semantics）は、構文よりもさらに簡単に定められる。
解釈（Interpretation）の概念が必要で、代数がシグネチャで示されるのと同じように、解釈はランク付け（ranking）によって示される。
シグネチャと、-代数である代数、そして、ランク付きのが与えられたとき、-解釈（-interpretation）とは、定数（個体定数と操作定数）と同様に、変数や関数に意味（meaning）を与えることによってを拡張した数学的なオブジェクトであるーーそして、意味はによって与えられているランクの情報と一致したものになっている。
解釈が与えられると、とを回復することが出来るので、「のシグネチャ」または「の宇宙」について話すことは理にかなっている。（※ここはちょっとよく分からない）

シグネチャを伴った代数が与えられたとき、-解釈に対するIswim()の-式の値は、以下のように定義される。

1. が単独の変数または定数の場合、対するの値は、によってに割り当てられた値
2. が、実引数[tex: F_0 , F_1 , \cdots , F{n-1}]を伴った、ランクがの操作定数または関数である場合、に対するの値は、[tex: g(v_0, v_1, \cdots , v{n-1})]；ここでいうはによってに割り当てられた宇宙上の演算であり、はそれぞれに対するの意味
3. がwhere節で構成されている場合、に対するの値は、最小の解釈に対するの主題の値；ここでいうは、の本体でのそれぞれの定義がに対して真となり、と異なるのはの本体で定義されている変数に割り当てられた値だけであるような解釈

単独の変数の定義が環境に対して真となるのは、両辺で環境に対する値が等しくなる場合であり、また、そのときに限る。
言い換えれば、解釈によって単独の変数に割り当てられる値は、右辺の解釈に対する値である。
関数の定義が真となるのは、仮変数に任意の値を指定しても両辺が同じ値になる場合であり、また、そのときに限る。
言い換えれば、解釈によって仮引数の値が変わったとしても、両辺は同じ値を持つ。
（以下、原文を訳せなかったので、こういうことを言いたいはず、という内容）
解釈には順序があり、下の解釈（＝ローカル、内側の解釈）で上の解釈（外側の解釈）を上書きする。
最小の解釈は、一番内側の解釈である。

さて、代数の世界が追加のオブジェクトを持っていた理由を見ていこう。
Iswimのセマンティクスでは、解釈は半順序である必要があるため、節には最小の解釈がある。
解釈の順序は、の宇宙での操作上の順序と、の宇宙での順序（が底にある）によって引き起こされる。（※何を言ってるのかよく分からない）
Iswimを（半順序とを伴わない）従来の代数の概念に基づいて構築することは不可能であろう。
問題は、のような（正しい）等式がある1つ以上ある一方で、のような従来の代数で正しくない等式もあるということである。
しかし、オブジェクトは、定義の作業を行うために追加された、単なる無意味な仕掛けであるというわけではない。
このオブジェクトはとてもシンプルな操作上の解釈を持っている。
それはすなわち、このオブジェクトは決して終了しない計算の「結果」を表している。
たとえば、以下で定義された関数

f(x) = if x eq 0 or x eq 1 then 1 else f (x - 1) + f (x - 2) fi;

は、（Iswimの意味論に従って）引数4を指定すると値5（4番目のフィボナッチ数）を返すが、引数として-1を指定するとを返す。
これは、再帰に関する操作上の直感と一致している（以下を参照）。
上記の定義には、f(-1)の値を197にするようなものまで含む、多くの解決策がある。
しかし、もしIswimの実装がそのような値を返したとしたら、どうしてその値になったのかと、とても驚くことになるだろう。
ある意味では、定義の最小解というのは、定義から計算していていけない値の解決策と考えることが出来る。
上の方程式はf(-1)に対して値を指定していないので、が最小解として返された「結果」である。

Iswim()のプログラムは、前述のように、自由（未定義）変数を持つことがある。
これは、プログラム自身では意味（＝変数への値の割り当て）を持たない可能性があるということを意味し、その場合、自由変数の値を私たちが指定する必要がある。
これらの値が、プログラムへの入力となる。
したがって、Iswimでの入力は「名前付き」または「ラベル付き」入力となる。

より正確には、を代数とし、を入力変数（自由変数）を持つIswim()プログラムとする。
への入力は、各入力変数にの宇宙の要素を割り当てる関数である。
を、すべての変数にランク0を与えることでのシグネチャを拡張するランク付けとする（したがってはtex: r]-式となる）。
入力を与えられたの出力は、入力変数にを割り当てるような、任意の、-解釈に対するの値である。

---

ということで、Iswimの構文とその意味論。
言ってることはシンプルなはずなんだけど、どうしてここまで難しい話になるのか・・・

ようは、

• Iswimの式は、単独の変数/定数、演算や関数の適切な数の引数での適用、where節を伴った式からなる
• Iswimの式の値は、単独の変数/定数ならその値、演算や関数の適用なら適用させた値、where節を伴った式ならwhere節での解釈を使った式の値
• where節は入れ子になるので、そこ（式から見える一番内側）に定義があればそれを使い、なければより外側の定義を探しにいく
• 計算で得られない値（＝エラー）はとなる
• 自由変数は入力として扱われる

ということだけのはずなんだけど（＾＾；

今日はここまで！