最近ラムダ計算つまりラムダ式について調べているのですが、その中の値の定義的な話で躓いてしまいました。その詳細ですが、こちらの 2.1 構文規則 は全体の90%程は理解できましたが、問題の 2.1.4 プログラムの意味 にある、

Z := 0;
for Y do Z := Z + X

のXがどこから出てきたのかが分かりません。for文からして恐らく

for X do Z

ではないかと思いますが、これだと言える確証がありません。stackoverflowが学問的な、計算論理学的な疑問に対応しているかは分かりませんが(念の為書いておきますがレベルが低いなどと言っている訳ではありません)、良質な日本語対応の質問サイトをここ以外知らないもので、こちらに質問させていただきました。