Free and bound variables nXX+y ·X: bound variable It y; Could be a free variable global variable int add(int x) return x+ y
Free and bound variables • x. x + y • x: bound variable • y: free variable int y; … … int add(int x) { return x + y; } Could be a global variable
Free and bound variables 入x.X+ Bound variable can be renamed(placeholder 入x(x+y) is same function asλz.、(z+y)c- equivalence (X+y is the scope of the binding nx int add(int x)i int add(int z) return x+ y; return Z+y x=0; //out of scope
Free and bound variables • x. x + y • Bound variable can be renamed (“placeholder”) • x. (x+y) is same function as z. (z+y) • (x+y) is the scope of the binding x int add(int x) { return x + y; } int add(int z) { return z + y; } x = 0; // out of scope! -equivalence
Free and bound variables 入x.X+ Bound variable can be renamed(placeholder") nx. x+y is same function as z (z+y a-equivalence (X+y) is the scope of the binding nX Name of free variable does matter nx.x+y is not the same as ix(x+z int y=10 int y =10; int z=20 int z=20: int add(int x)i return x+y: 1 int add(int x)( return x+Z;
Free and bound variables • x. x + y • Bound variable can be renamed (“placeholder”) • x. (x+y) is same function as z. (z+y) -equivalence • (x+y) is the scope of the binding x • Name of free variable does matter • x. (x+y) is not the same as x. (x+z) int y = 10; int z = 20; int add(int x) { return x + y; } int y = 10; int z = 20; int add(int x) { return x + z; }
Free and bound variables 入x.X+ Bound variable can be renamed(placeholder") nx. x+y is same function as z (z+y a-equivalence (X+y) is the scope of the binding nX Name of free variable does matter nx.X+y is not the same as ix(x+z · Occurrences intx=10: (x.X+y)(x+1): has bot int add(int x)i return x+y; a free and a bound occurrence add(x+1);
Free and bound variables • x. x + y • Bound variable can be renamed (“placeholder”) • x. (x+y) is same function as z. (z+y) -equivalence • (x+y) is the scope of the binding x • Name of free variable does matter • x. (x+y) is not the same as x. (x+z) • Occurrences • (x. x+y) (x+1) : x has both a free and a bound occurrence int x = 10; int add(int x) { return x+y;} add(x+1);
Formal definitions about free and bound variables Recall M,n: =X nXMMN fVM: the set of free variables in m fv(x)三{x} fv(XM)≡fvM)\{x} Defined by induction on terms fv(MN)≡fV(M)Jfv(N) Exampl de fv(X.x)×)={x fv(X.X+y)×)={y
Formal definitions about free and bound variables • Recall M, N ::= x | x. M | M N • fv(M): the set of free variables in M fv(x) {x} fv(x.M) fv(M) \ {x} fv(M N) fv(M) fv(N) • Example fv((x. x) x) = {x} fv((x. x + y) x) = {x, y} Defined by induction on terms