CODEWITHSUNDEEP
typeslambdatheorylambda-calculus
user746461
user746461

Reputation:

Definition of substitution in Lambda expression

Let's denote [x |-> v] t as "substitute all free occurrences of x in t with v".

The substitution rules of my textbook are

[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)

I don't quite comprehend the first two rules. Why whether y is x makes a difference? Are the first x and the second x in [x |-> v] x same? Can y of the second rule be something like 1+x? Can you give two examples in Lambda expression or C/C++/C#/Java, that use the two rules, respectively?

thanks very much!

Upvotes: 0

Views: 237

Answers (1)

Matt Bryant
Matt Bryant

Reputation: 4961

The first rule is mapping x to v. The second rule is saying any variables that are non-x remain unchanged. Both of those are parts of the the same rule that are necessary to fully define its behavior.

I suppose a somewhat reasonable example would be the following:

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

Note that v has now been set to the value of x (first rule), but the value of y has not changed (second rule).

Upvotes: 0

Related Questions