式Mのxをyに置き換える
λ計算だとか、数学よりの話をするときはよく、
式Mのxをyに置き換えたものを
M[x:=y]
で表す．
なんて定義が出てきます。
本によっては、まったく同じことを表すのに、
[y/x]M
だとか、
M[y/x]
といった記法も使います。
本日、このM, x, yの順番に、意味がある(かもしれない)ことに唐突に気づきました。
式Mのxをyに置き換える
M[x:=y]
M[x:=y]は日本語表記と完全に一致するじゃないですか、
なんか読み易いと思ったらそういうことか。
それから、[y/x]Mは英語だと意味をなします。
Substitute y for all x in M.
[y/x]M
完全に一致。
しかし、そうなるとM[y/x]が浮いてしまうんですが、
これには何か意味があるんでしょうか。
謎です。