Определение замещения в выражении Lambda

Question

Обозначим [x |-> v] t как «заменить все свободные вхождения x в t с v».

Правило замены моего учебника являются

[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 одинаковыми? Может ли у второго правила быть что-то вроде 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 не изменилось (второе правило).