51606


最近ラムダ計算つまりラムダ式について調べているのですが、その中の値の定義的な話で躓いてしまいました。その詳細ですが、[こちら](https://www.ed.tus.ac.jp/j-mune/sem/text/1.pdf)の
**_2.1 構文規則_** は全体の90%程は理解できましたが、問題の **_2.1.4 プログラムの意味_** にある、

[code]

    Z := 0;
    for Y do Z := Z + X
    
[/code]

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

[code]

    for X do Z
    
[/code]

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


CC BY-SA 4.0
2018-12-29T10:30:07.297
51602
2018-12-30T10:36:37.783
30493
question
プログラミング言語
プログラム意味論的な話で「for Y do Z := Z + X」のXがどこから出てきたのか解らない


直後を読む限り、`X`も`Y`も所与の変数(気分的には引数)では？

> 掛け算を行うプログラム： 変数XとYに，負でない整数を代入して実行すると，変数ZにX*Yの値が代入されて停止する．


CC BY-SA 4.0
2018-12-29T11:23:37.520
51604
2018-12-29T11:23:37.520
10685
51602
answer


> 掛け算を行うプログラム ： 変数 X と Y に，負でない整数を代入して実行すると，変数 Z に X ∗ Y の値が代入されて停  
>  止する．

という注釈を読む限り、`X`を`Y`回足したもの`Z`の結果が、式

[code]

    sum = X * Y
    
[/code]

でいう、`sum`と`Z`が等しい事の説明であると読めるので、リンク先の式で合っていると思います。


CC BY-SA 4.0
2018-12-29T11:38:10.917
51605
2018-12-29T11:38:10.917
14745
51602
answer


質問の出典を最後まで読むと、これは掛け算をするプログラムを表しています。

> 2.1.4 プログラムの意味
[code]

>     Z := 0;
>     for Y do Z := Z + X
>  
[/code]

>
> 掛け算を行うプログラム ： 変数 X と Y に，負でない整数を代入して実行すると，変数 Z に X ∗ Y の値が代入されて停止する．  
>  <https://www.ed.tus.ac.jp/j-mune/sem/text/1.pdf> より抜粋

ここで、`X` は被乗数（かけられる数）、`Y`は乗数（かける数、掛け算の回数）、 `Z` は
[@Чайка](https://ja.stackoverflow.com/users/14745)
氏の指摘するとおり`sum`、つまり掛け算の繰り返しの途中で結果を保存する変数として登場しているようです。

Rubyがお得意のようですので、この内容をRuby風に書くと以下のようになるでしょうか。

[code]

    def multiply(x, y)
      z = 0
      (1..y).each{
        z = z + x
      }
      return z
    end
    
    puts multiply(5, 8)
    
[/code]


CC BY-SA 4.0
2018-12-29T13:08:02.390
51606
2018-12-29T13:08:02.390
29826
51602
answer


# 短いお返事

その時点では形式的に構文規則を定めた所なので、実際にはXだとかZだとかに **意味はありません。**  
しかし私達は通常のプログラムの **意味論を踏まえてしまっているから** 不思議に思えてしまうのです。

ただし、その後に定められている表示的意味論を解釈する限りは、 **所与の変数値** と同等のものと考えられます。

# しっかりしたお返事

そのテキストの文脈は、 **構文規則** を定めた直後ですね。  
実はその時点では、構文として一応そういった文が作れるということしか定めておらず、  
現実にそれがどのような意味を持つものかを何も定めていない段階です。  
つまり変数の記号 `X` であるとはどういうことかが、まだ何も定まっていません。  
そのためその場所に (構文規則に従っている限り) **突然登場することも、まったく可能** なのです。

サンプルのあと、実際にお話は意味論(意味関数による表示的意味論ですね)に進みます。  
ここで意味関数を与えたことで、始めてこの文がどんな意味を持つのか明らかになったのです。

そこで実際に意味論に従ってこの値を解釈して導出してみましょう。

まず 環境 `ϕ` を任意に定めます。  
たとえば `ϕ = { (X, 30), (Y, 2), (Z, 1000), (その他の変数は適当に) }` なんてどうでしょうか。  
(上記は集合を使った関数の定義です。つまりXを引数に取ると30,Yなら2、Zなら1000という関数を環境と思っています)

そして(ちょっとテキストの構成上、定まりの悪い `;` の意味論などに気をつけながら)展開すると

[code]

      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), (その他の変数はϕに等しい) }
    
[/code]

`ϕ(X)` の値は、この文における意味論の課程で、特に書き換えられていない(最初から最後まで30でした)ことから、  
つまるところ初期の `ϕ(X)` に与えられた値がそのまま継承されているはずです。

結局、直感的には環境 `ϕ` に依存した値 `ϕ(X)` が、  
この `X` の値として該当コードの"実行"(そんな概念は無いのであくまで直感的に！)で採用されることになるでしょう。  
もうちょっと言葉をスムーズにするならこれは「所与の変数 `X` の値をそのまま採用しましょう。」  
ということだと直感的には解釈できます。

しかし基本的には意味論を厳密に解釈するなら、値が「どこからくる」という考え方自体を、実はしていないのです。


CC BY-SA 4.0
2018-12-29T17:45:35.570
51610
2018-12-30T10:36:37.783
2018-12-30T10:36:37.783
30827
30827
51602
answer