Lambda表達式中替換的定義

Question

讓我們將[x |-> v] t表示爲「用v替換x中的所有空閒事件」。

我的教科書的替代規則是

[x |-> v] x=v 
[x |-> v] y=y (where y is not x) 

[x |-> v] (function x -> t) = (function x -> t) 
[x |-> v] (function y -> t) (where y is not x) = 
     (function y -> [x |-> v]t) 

[x |-> v] (t1 t2) -> ([x |-> v]t1 [x |-> v]t2) 

我不太理解前兩個規則。 爲什麼y是x有區別？[x |-> v] x中的第一個x和第二個x是否相同？第二條規則y可以像1+x？ 您可以在Lambda表達式或C/C++/C＃/ Java中分別使用兩個規則給出兩個示例嗎？

非常感謝！

Answer 1

第一條規則是將x映射到v。第二條規則是說任何非x的變量保持不變。這兩者都是完全定義其行爲所必需的相同規則的一部分。

我想稍微合理的例子是以下幾點：

int x = 1337; 
int y = 9001; 
int v; 
v = x; 

注意v現在已經設置爲x（第一條）的值，但y的價值沒有改變（第二條規則）。