capture of global identifiers

[bodeveix]

When a global identifier has the same name as a binder and is inserted under the binder after beta reduction, the binder should be renamed.

In the following example, x is declared global. The reduction of (λ y x, x = y) x is printed as "λ x, x = x" while it should be printed "λ x1, x = x1" This is only a printing problem. The two occurrences of x are distinguished internally: assert |- (λ y x, x = y) x ≡ λ x, x = x fails.

symbol Prop: TYPE;
symbol π: Prop → TYPE;
symbol Set: TYPE;
constant symbol τ: Set → TYPE;
builtin "T" ≔ τ;
builtin "P" ≔ π;

symbol = [a:Set] : τ a → τ a → Prop;

notation = infix 10;

symbol T: Set;
symbol x : τ T;

compute ((λ y x, x = y) x); // prints "λ x, x = x"