短いお返事
その時点では形式的に構文規則を定めた所なので、実際にはXだとかZだとかに 意味はありません。
しかし私達は通常のプログラムの 意味論を踏まえてしまっているから 不思議に思えてしまうのです。
ただし、その後に定められている表示的意味論を解釈する限りは、 所与の変数値 と同等のものと考えられます。
しっかりしたお返事
そのテキストの文脈は、 構文規則 を定めた直後ですね。
実はその時点では、構文として一応そういった文が作れるということしか定めておらず、
現実にそれがどのような意味を持つものかを何も定めていない段階です。
つまり変数の記号 X
であるとはどういうことかが、まだ何も定まっていません。
そのためその場所に (構文規則に従っている限り) 突然登場することも、まったく可能なのです。
サンプルのあと、実際にお話は意味論(意味関数による表示的意味論ですね)に進みます。
ここで意味関数を与えたことで、始めてこの文がどんな意味を持つのか明らかになったのです。
そこで実際に意味論に従ってこの値を解釈して導出してみましょう。
まず 環境 ϕ
を任意に定めます。
たとえば ϕ = { (X, 30), (Y, 2), (Z, 1000), (その他の変数は適当に) }
なんてどうでしょうか。
(上記は集合を使った関数の定義です。つまりXを引数に取ると30,Yなら2、Zなら1000という関数を環境と思っています)
そして(ちょっとテキストの構成上、定まりの悪い ;
の意味論などに気をつけながら)展開すると
M_cmd[[Z := 0;for Y do Z := Z + X]]ϕ
= M_cmd[[Z := 0;for Y do Z := Z + X]]ϕ
= M_cmd[[for Y do Z := Z + X]](M_cmd[[Z := 0]]ϕ)
= M_cmd[[for Y do Z := Z + X]](ϕ(Z := 0))
= M_cmd[[Z := Z + X]](M_cmd[[Z := Z + X]](ϕ(Z := 0))) (ϕ(Y) = 2であるため2回展開した)
= M_cmd[[Z := Z + X]](ϕ(Z := 0)(Z := M_exp[[Z + X]]ϕ(Z := 0)))
= M_cmd[[Z := Z + X]](ϕ(Z := 0)(Z := M_exp[[Z]]ϕ(Z := 0) + M_exp[[X]]ϕ(Z := 0) ))
= M_cmd[[Z := Z + X]](ϕ(Z := 0)(Z := ϕ(Z := 0)(Z) + ϕ(Z := 0)(X) ))
= M_cmd[[Z := Z + X]](ϕ(Z := 0)(Z := 0 + 30))
= M_cmd[[Z := Z + X]](ϕ(Z := 0)(Z := 30))
= M_cmd[[Z := Z + X]](ϕ(Z := 30))
= ϕ(Z := 60) (ここはもう操作を省略しました。紙面などで試してみてください)
= { (X, 30), (Y, 2), (Z, 60), (その他の変数はϕに等しい) }
ϕ(X)
の値は、この文における意味論の課程で、特に書き換えられていない(最初から最後まで30でした)ことから、
つまるところ初期の ϕ(X)
に与えられた値がそのまま継承されているはずです。
結局、直感的には環境 ϕ
に依存した値 ϕ(X)
が、
この X
の値として該当コードの"実行"(そんな概念は無いのであくまで直感的に!)で採用されることになるでしょう。
もうちょっと言葉をスムーズにするならこれは「所与の変数 X
の値をそのまま採用しましょう。」
ということだと直感的には解釈できます。
しかし基本的には意味論を厳密に解釈するなら、値が「どこからくる」という考え方自体を、実はしていないのです。