前回の続き。
2.4 サンプルプログラム
where節の本体が「補助定義」であるという非形式的な考え方に形式的意味論がどう一致しているかを説明するために、前に出てきた次の式を考えてみる：
C + A * Z
where
A = 5;
B = 5;
C = Z * A + 1
where
A = 3;
Z = A + W * B;
end
end
をすべての変数にランク0を割り当てるランク付けとし、
を、
に9、
に7、他のすべての変数に0を割り当てる整数の
-解釈とする。
形式的意味論を用いて、に関するこの式の値を決定してみる。
定義3.により、この式の値は本体の等式の「最小解」に対する式
の値である。
は、変数
、
、
にそれぞれ5、5、115が割り当てられることを除いて、
と同じ解釈でなければならないことは、簡単に分かる。
（※）
（、
、
だけがこの節で定義された変数なので、他の変数についてはすべて、
で割り当てられた値に
は一致しなければならない）。
式は、二項演算子
とその引数
、
からなっている。
次に、定義2.により、に関する
の値は、整数の
の解釈に2つの引数の値（つまりそれらの
に対する値）を適用した結果である。
最初の項の値は、定義1.により、が
に割り当てている値、つまり115である。
2つ目の項の値は45と簡単に分かるので（は
と
にそれぞれ5と9を割り当てている）、最終結果は160である。
が外側の
where節の本体の3つの等式の解であることを確認するには、それぞれについて、に対して左辺の値が右辺の値と同じであることを検証する必要がある。
最初の2つの等式については明らかだが、3つ目の等式については、に関して内側の
where節の値を計算する必要がある。
定義3.は、（内側のwhere節の）主題の式のの値が、（内側の
where節の）本体の中での定義の最小解に対する値であることを示している。
は、
と
にそれぞれ3と38（＝3 + 7 * 5）を割り当てていることを除いて、
と同じである。
したがって、（内側のwhere節の）主題の式の値は115である。
これにより、は
に115を割り当てることが分かるので、
は外側の節の等式の解であることが確認できる。
もちろん、これはが最小解であることを証明するものではないが、定義は非再帰的であり、解は唯一のものである。
自由（未定義）変数が単独の（＝ランク0の）変数として使用されるため、上記の式は実際にはプログラムである。
以上から、このプログラムの出力は、入力がのとき（すなわち、
の入力値が9、
の入力値が7のとき）、160である 。
2.5 Iswimの操作的意味論
Iswimの形式的意味論は単純で正確である。
この「最小不動点（least fixed point）」という仕様は、実装が正しく、かつ完全であると判断するための標準として使用できる。
例えば、（6章で与えるような）ある変換規則が正しいことを証明するといった、言語の妥当性の判断にも使用できる。
しかしながら、形式的な定義は、プログラムの読み書きの良いガイドとはならず、また、言語を実装するのにも直接は使用できない。
幸いにも、Iswimファミリのほとんどのサブクラスは、比較的従来通りの概念を使用して理解、実装することが出来る。
「従来の」モデルは、変数の定義を代入文として解釈し、関数の定義を関数処理の宣言として解釈するという考え方に基づいている。
この解釈は、代数の世界（universe）が（のように）「通常の」有限オブジェクトに
を加えた集合である場合、適用可能である。
where節の本体の中での定義は、どのような順序であってもよいので、代入文のようにそれらを実行し、意味のある結果を得ることが出来るとは限らない。
しかし、Iswim()と同様の言語では、再帰的に定義された変数は（ほとんどの場合）値が
となるので、そのような定義は無意味である。
循環定義が許されないのであれば、右辺に出てくるすべての変数がすでに定義済みであるように定義を並べ替えることが出来るのは、容易に分かる。
（※変数間の参照関係を有向グラフで書いたとき、循環定義がなければツリー（もしくはフォレスト）になるので、リーフから並べていけばいい）
例えば、
X + Y
where
C = A + B;
X = C * C - D;
D = A - B;
Y = C + D * D;
end
という式では、本体を一連の代入文として解釈することは出来ない。
なぜなら、の値は3つ目の文で計算されるため、2つ目の文を実行できないからだ。
しかし、次のように定義を並べ替えることが出来る：
X + Y
where
C = A + B;
D = A - B;
X = C * C - D;
Y = C + D * D;
end
こうすれば、4つの定義が順番に実行され、結果の「格納された」値を使用して主題の式が評価されると想像することが出来る。
評価後、ローカル変数（、
、
、
）の値は元に戻さなければならない。
ここで、where節の本体の中で
f(X, Y) = P - Y
where
Q = X + Y;
R = X - Y;
P = Q * R;
end
というような定義を持っていて、本体のどこか（上記の定義が関係する位置）でという形の式があるとする。
この定義を手続きの宣言と解釈し、式をこの手続きの呼び出しとして考えたとき、その呼び出しはALGOLやPASCALと同様に実行されると想像することが出来る。
言い換えれば、仮引数に5、
に
と
の差が一時的に与えられ、
の手続き本体（
の定義の右辺の式）が実行され、結果が呼び出しの結果として返され、仮引数の元の値が復元される。
「従来の」モデルは全体として、特殊なオブジェクトの正しい解釈を与える。
例えば、次のプログラムを考えてみる：
f(3) where f(n) = n * f(n - 1); end
手続き的意味論をガイドとして用いると、このプログラムからは何の値も得られないと予想できる。
の「呼び出し」は
を呼び出し、それは
、
、
、
と、無限の呼び出しを生じさせる。
これは手続き的意味論が失敗したように見えるかもしれないが（値が得られないため）、実際にはちゃんと動作する！
形式的意味論は、が常に
を返す関数であることを指し示し、そして、
がプログラム全体の出力となる。
したがって、を「非停止（nontermination）」あるいは「出力なし」と解釈するならば、手続き的意味論は正しい。
これこそがの真の意味である。
オブジェクトは、永遠に実行され、決して何も返さないプログラムの「出力」である。
このオブジェクトは、動的な操作的動作の「非停止」に対応する静的な意味値である。
との組み合わせに関するさまざまな規則はすべて、この解釈でとても自然に説明することが出来る。
例えば、3との合計が
であるという事実を考えてみる。
計算によって2つの値の加算が行われるが、最初の値の（部分）計算で3が得られるのに対し、2つ目の計算は結果を生み出さずに永久に実行されることになる。
したがって、（この計算は永遠に終わらないので）合計の「値」はでなければならず、これは3と
の（拡張された意味での）合計と一致している。
ということで、前回の分かりにくかった説明の具体的な例と、それを操作的にはどう解釈するのかという話。
正直、前回の内容を理解していなかったときは、このサンプルプログラムも「？」な感じではあったのだけど（変数のスコープがちゃんと理解できていなかった）、理解すればそんなに難しくはないかな？
where節の主題の右辺のスコープがすでにローカル内だというのがちょっと間違えやすい気はするけど・・・
今日はここまで！
