types - Lambda 表达式中替换的定义

Question

让我们表示[x |-> v] t为“用 v 替换 t 中所有自由出现的 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 和第二个 x[x |-> v] 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没有改变（第二条规则）。