いものやま。

雑多な知識の寄せ集め

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

技術 Lucid

前回の続き。

2.2 Iswimの構文

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

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

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

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

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

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

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

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

2.3 Iswimの意味論

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

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

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

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

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

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を指定すると \perpを返す。
これは、再帰に関する操作上の直感と一致している（以下を参照）。
上記の定義には、f(-1)の値を197にするようなものまで含む、多くの解決策がある。
しかし、もしIswimの実装がそのような値を返したとしたら、どうしてその値になったのかと、とても驚くことになるだろう。
ある意味では、定義の最小解というのは、定義から計算していていけない値の解決策と考えることが出来る。
上の方程式はf(-1)に対して値を指定していないので、 \perpが最小解として返された「結果」である。

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

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

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

ようは、

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

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

今日はここまで！