0

[x |-> v] tを「t 内の x のすべての自由な出現を 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)

最初の 2 つのルールがよくわかりません。y が x であるかどうかで違いが生じるのはなぜですか? 最初の x と 2 番目の x は[x |-> v] x同じですか? 2 番目のルールの y は次のようになり1+xますか? ラムダ式または C/C++/C#/Java で、それぞれ 2 つのルールを使用する 2 つの例を挙げていただけますか?

どうもありがとう！

4

1 に答える 1

1

最初のルールは へのマッピングxですv。2 番目のルールは、変化しない変数は変更されないということxです。これらは両方とも、その動作を完全に定義するために必要な同じルールの一部です。

やや合理的な例は次のようになると思います。

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

(最初のルール)vの値に設定されていますが、 の値は変更されていません (2 番目のルール)。xy

于 2013-10-13T19:31:11.217 に答える