1.1 Abstract Syntax Trees 1.1 Abstract Syntax Trees An abstract syntax tree,or ast for short,is an ordered tree whose leaves are variables,and whose in- terior nodes are operators whose arguments are its children.Asts are classified into a variety of sorts corresponding to different forms of syntax.A variable stands for an unspecified,or generic,piece of syntax of a specified sort.Asts can be combined by an operator,which has an arity specifying the sort of the operator and the number and sorts of its arguments.An operator of sort s and arity s1,...,sn combines n >0 asts of sort s1,...,sn,respectively,into a compound ast of sort s. The concept of a variable is central,and therefore deserves special emphasis.A variable is an unknown object drawn from some domain.The unknown can become known by substitution of a particular object for all occurrences of a variable in a formula,thereby specializing a general formula to a particular instance.For example,in school algebra variables range over real numbers, and we may form polynomials,such asx2+2x+1,that can be specialized by substitution of,say, 7 for x to obtain 72+(2 x 7)+1,which can be simplified according to the laws of arithmetic to obtain 64,which is (7+1)2. Abstract syntax trees are classified by sorts that divide asts into syntactic categories.For exam- ple,familiar programming languages often have a syntactic distinction between expressions and commands;these are two sorts of abstract syntax trees.Variables in abstract syntax trees range over sorts in the sense that only asts of the specified sort of the variable can be plugged in for that variable.Thus it would make no sense to replace an expression variable by a command,nor a command variable by an expression,the two being different sorts of things.But the core idea carries over from school mathematics,namely that a variable is an unknown,or a place-holder,whose meaning is given by substitution. As an example,consider a language of arithmetic expressions built from numbers,addition, and multiplication.The abstract syntax of such a language consists of a single sort Exp generated by these operators: 1.An operator num[n]of sort Exp for each n E N; 2.Two operators,plus and times,of sort Exp,each with two arguments of sort Exp. The expression 2+(3 x x),which involves a variable,x,would be represented by the ast plus(num[2];times(num[3];x)) of sort Exp,under the assumption that x is also of this sort.Because,say,num[4],is an ast of sort Exp,we may plug it in for x in the above ast to obtain the ast plus(num[2];times(num[3];num(4])), which is written informally as 2+(3 x 4).We may,of course,plug in more complex asts of sort Exp for x to obtain other asts as result. The tree structure of asts provides a very useful principle of reasoning,called structural induc- tion.Suppose that we wish to prove that some property P(a)holds of all asts a of a given sort. To show this it is enough to consider all the ways in which a can be generated,and show that the property holds in each case under the assumption that it holds for its constituent asts(if any).So, in the case of the sort Exp just described,we must show
PREVIEW 4 1.1 Abstract Syntax Trees 1.1 Abstract Syntax Trees An abstract syntax tree, or ast for short, is an ordered tree whose leaves are variables, and whose interior nodes are operators whose arguments are its children. Asts are classified into a variety of sorts corresponding to different forms of syntax. A variable stands for an unspecified, or generic, piece of syntax of a specified sort. Asts can be combined by an operator, which has an arity specifying the sort of the operator and the number and sorts of its arguments. An operator of sort s and arity s1, . . . ,sn combines n ≥ 0 asts of sort s1, . . . ,sn, respectively, into a compound ast of sort s. The concept of a variable is central, and therefore deserves special emphasis. A variable is an unknown object drawn from some domain. The unknown can become known by substitution of a particular object for all occurrences of a variable in a formula, thereby specializing a general formula to a particular instance. For example, in school algebra variables range over real numbers, and we may form polynomials, such as x 2 + 2 x + 1, that can be specialized by substitution of, say, 7 for x to obtain 72 + (2 × 7) + 1, which can be simplified according to the laws of arithmetic to obtain 64, which is (7 + 1) 2 . Abstract syntax trees are classified by sorts that divide asts into syntactic categories. For example, familiar programming languages often have a syntactic distinction between expressions and commands; these are two sorts of abstract syntax trees. Variables in abstract syntax trees range over sorts in the sense that only asts of the specified sort of the variable can be plugged in for that variable. Thus it would make no sense to replace an expression variable by a command, nor a command variable by an expression, the two being different sorts of things. But the core idea carries over from school mathematics, namely that a variable is an unknown, or a place-holder, whose meaning is given by substitution. As an example, consider a language of arithmetic expressions built from numbers, addition, and multiplication. The abstract syntax of such a language consists of a single sort Exp generated by these operators: 1. An operator num[ n ] of sort Exp for each n ∈ N; 2. Two operators, plus and times, of sort Exp, each with two arguments of sort Exp. The expression 2 + (3 × x), which involves a variable, x, would be represented by the ast plus( num[ 2 ] ; times( num[ 3 ] ; x ) ) of sort Exp, under the assumption that x is also of this sort. Because, say, num[ 4 ], is an ast of sort Exp, we may plug it in for x in the above ast to obtain the ast plus( num[ 2 ] ; times( num[ 3 ] ; num[ 4 ] ) ), which is written informally as 2 + (3 × 4). We may, of course, plug in more complex asts of sort Exp for x to obtain other asts as result. The tree structure of asts provides a very useful principle of reasoning, called structural induction. Suppose that we wish to prove that some property P(a) holds of all asts a of a given sort. To show this it is enough to consider all the ways in which a can be generated, and show that the property holds in each case under the assumption that it holds for its constituent asts (if any). So, in the case of the sort Exp just described, we must show
1.1 Abstract Syntax Trees 1.The property holds for any variable x of sort Exp:prove that P(x). 2.The property holds for any number,num[n]:for every n E N,prove that P(num[n]). 3.Assuming that the property holds for a and a2,prove that it holds for plus(a;a2)and times(a1;a2):if P(a1)and P(a2),then P(plus(a1;a2))and P(times(a1;a2)) Because these cases exhaust all possibilities for the formation of a,we are assured that P(a)holds for any ast a of sort Exp. It is common to apply the principle of structural induction in a form that takes account of the interpretation of variables as place-holders for asts of the appropriate sort.Informally,it is often useful to prove a property of an ast involving variables in a form that is conditional on the property holding for the variables.Doing so anticipates that the variables will be replaced with asts that ought to have the property assumed for them,so that the result of the replacement will have the property as well.This amounts to applying the principle of structural induction to properties P(a) of the form "if a involves variables x1,...,xk,and Q holds of each xi,then O holds of a",so that a proof of P(a)for all asts a by structural induction is just a proof that Q(a)holds for all asts a under the assumption that holds for its variables.When there are no variables,there are no assumptions,and the proof of P is a proof that Qholds for all closed asts.On the other hand if x is a variable in a,and we replace it by an ast b for which holds,then will hold for the result of replacing x by b in a. For the sake of precision,we now give precise definitions of these concepts.Let S be a finite set of sorts.For a given set S of sorts,an arity has the form (s1,...,sn)s,which specifies the sort s ES of an operator taking n >0 arguments,each of sort si E S.Let ={O be an arity-indexed family of disjoint sets of operators O of arity a.If o is an operator of arity(s1,...,sn)s,we say that o has sort s and has n arguments of sorts s1,...,Sn. Fix a set S of sorts and an arity-indexed family of sets of operators of each arity.Let {As}ses be a sort-indexed family of disjoint finite sets s of variables x of sort s.When is clear from context,we say that a variable x is of sort s if x E Ys,and we say that x is fresh for or just fresh when t is understood,if x As for any sort s.If x is fresh for and s is a sort,then x is the family of sets of variables obtained by adding x to As.The notation is ambiguous in that the sort s is not explicitly stated,but determined from context. The family A=Al]s ses of abstract syntax trees,or asts,of sort s is the smallest family satisfying the following conditions: 1.A variable of sort s is an ast of sort s:if x E &s,then x Al&]s. 2.Operators combine asts:if o is an operator of arity (s1,...,sn)s,and if a E A[s..., an∈AX]sn,theno(a1;.ian)∈A[Y]s. It follows from this definition that the principle of structural induction can be used to prove that some property P holds of every ast.To show P(a)holds for every a eA[],it is enough to show: l.Ifx∈Xs,then Ps(x). 2.If o has arity (s1,...,sn)s and Ps (a1)and...and Ps (an),then Ps(o(a1;...;an))
PREVIEW 1.1 Abstract Syntax Trees 5 1. The property holds for any variable x of sort Exp: prove that P(x). 2. The property holds for any number, num[ n ]: for every n ∈ N, prove that P(num[ n ]). 3. Assuming that the property holds for a1 and a2, prove that it holds for plus( a1 ; a2 ) and times( a1 ; a2 ): if P(a1) and P(a2), then P(plus( a1 ; a2 )) and P(times( a1 ; a2 )). Because these cases exhaust all possibilities for the formation of a, we are assured that P(a) holds for any ast a of sort Exp. It is common to apply the principle of structural induction in a form that takes account of the interpretation of variables as place-holders for asts of the appropriate sort. Informally, it is often useful to prove a property of an ast involving variables in a form that is conditional on the property holding for the variables. Doing so anticipates that the variables will be replaced with asts that ought to have the property assumed for them, so that the result of the replacement will have the property as well. This amounts to applying the principle of structural induction to properties P(a) of the form “if a involves variables x1, . . . , xk , and Q holds of each xi , then Q holds of a”, so that a proof of P(a) for all asts a by structural induction is just a proof that Q(a) holds for all asts a under the assumption that Q holds for its variables. When there are no variables, there are no assumptions, and the proof of P is a proof that Q holds for all closed asts. On the other hand if x is a variable in a, and we replace it by an ast b for which Q holds, then Q will hold for the result of replacing x by b in a. For the sake of precision, we now give precise definitions of these concepts. Let S be a finite set of sorts. For a given set S of sorts, an arity has the form (s1, . . . ,sn)s, which specifies the sort s ∈ S of an operator taking n ≥ 0 arguments, each of sort si ∈ S. Let O = { Oα } be an arity-indexed family of disjoint sets of operators Oα of arity α. If o is an operator of arity (s1, . . . ,sn)s, we say that o has sort s and has n arguments of sorts s1, . . . ,sn. Fix a set S of sorts and an arity-indexed family O of sets of operators of each arity. Let X = { Xs }s∈S be a sort-indexed family of disjoint finite sets Xs of variables x of sort s. When X is clear from context, we say that a variable x is of sort s if x ∈ Xs , and we say that x is fresh for X , or just fresh when X is understood, if x ∈ X / s for any sort s. If x is fresh for X and s is a sort, then X , x is the family of sets of variables obtained by adding x to Xs . The notation is ambiguous in that the sort s is not explicitly stated, but determined from context. The family A[X ] = { A[X ]s }s∈S of abstract syntax trees, or asts, of sort s is the smallest family satisfying the following conditions: 1. A variable of sort s is an ast of sort s: if x ∈ Xs , then x ∈ A[X ]s . 2. Operators combine asts: if o is an operator of arity (s1, . . . ,sn)s, and if a1 ∈ A[X ]s1 , . . . , an ∈ A[X ]sn , then o( a1 ; . . . ; an ) ∈ A[X ]s . It follows from this definition that the principle of structural induction can be used to prove that some property P holds of every ast. To show P(a) holds for every a ∈ A[X ], it is enough to show: 1. If x ∈ Xs , then Ps(x). 2. If o has arity (s1, . . . ,sn)s and Ps1 (a1) and . . . and Psn (an), then Ps(o( a1 ; . . . ; an ))
6 1.2 Abstract Binding Trees For example,it is easy to prove by structural induction that A[]Ay]whenever y. Variables are given meaning by substitution.If aA[,x]s',and b E A[X]s,then [b/xla E A']s is the result of substituting b for every occurrence of x in a.The ast a is called the target, and x is called the subject,of the substitution.Substitution is defined by the following equations: 1.[b/x]x=b and [b/xly=yif x #y. 2.[b/xlo(a;...;an)=o([b/x]a;...;[b/x]an). For example,we may check that num[2]/xplus(x;num(3])=plus(num[2];num[3]). We may prove by structural induction that substitution on asts is well-defined. Theorem 1.1.If a E A[X,x],then for every b E Alx]there exists a unique c A[x]such that [b/xla=c Proof.By structural induction on a.If a =x,then c =b by definition,otherwise if a =yx, then c =y,also by definition.Otherwise,a =o(a1;...;an),and we have by induction unique c1,...,cn such that [b/x]a1 ci and...[b/x]an cn,and so c is c=o(c1;...;cn),by definition of substitution. 口 1.2 Abstract Binding Trees Abstract binding trees,or abts,enrich asts with the means to introduce new variables and symbols, called a binding,with a specified range of significance,called its scope.The scope of a binding is an abt within which the bound identifier can be used,either as a place-holder(in the case of a variable declaration)or as the index of some operator(in the case of a symbol declaration).Thus the set of active identifiers can be larger within a subtree of an abt than it is within the surrounding tree. Moreover,different subtrees may introduce identifiers with disjoint scopes.The crucial principle is that any use of an identifier should be understood as a reference,or abstract pointer,to its binding. One consequence is that the choice of identifiers is immaterial,so long as we can always associate a unique binding with each use of an identifier. As a motivating example,consider the expression let x be a in a2,which introduces a variable x for use within the expression a2 to stand for the expression a1.The variable x is bound by the let expression for use within a2;any use of x within a refers to a different variable that happens to have the same name.For example,in the expression let x be 7inx+x occurrences of x in the addition refer to the variable introduced by the let.On the other hand in the expression let x bex *xinx+x,occurrences of x within the multiplication refer to a different variable than those occurring within the addition.The latter occurrences refer to the binding introduced by the let,whereas the former refer to some outer binding not displayed here. The names of bound variables are immaterial insofar as they determine the same binding. So,for example,let x bex*xinx+x could just as well have been written let ybex *xiny+y, without changing its meaning.In the former case the variable x is bound within the addition,and
PREVIEW 6 1.2 Abstract Binding Trees For example, it is easy to prove by structural induction that A[X ] ⊆ A[Y] whenever X ⊆ Y. Variables are given meaning by substitution. If a ∈ A[X , x] s ′ , and b ∈ A[X ]s , then [b/x]a ∈ A[X ] s ′ is the result of substituting b for every occurrence of x in a. The ast a is called the target, and x is called the subject, of the substitution. Substitution is defined by the following equations: 1. [b/x]x = b and [b/x]y = y if x ̸= y. 2. [b/x]o( a1 ; . . . ; an ) = o( [b/x]a1 ; . . . ; [b/x]an ). For example, we may check that [num[ 2 ]/x]plus( x ; num[ 3 ] ) = plus( num[ 2 ] ; num[ 3 ] ). We may prove by structural induction that substitution on asts is well-defined. Theorem 1.1. If a ∈ A[X , x], then for every b ∈ A[X ] there exists a unique c ∈ A[X ] such that [b/x]a = c Proof. By structural induction on a. If a = x, then c = b by definition, otherwise if a = y ̸= x, then c = y, also by definition. Otherwise, a = o( a1 ; . . . ; an ), and we have by induction unique c1, . . . , cn such that [b/x]a1 = c1 and . . . [b/x]an = cn, and so c is c = o( c1 ; . . . ; cn ), by definition of substitution. 1.2 Abstract Binding Trees Abstract binding trees, or abts, enrich asts with the means to introduce new variables and symbols, called a binding, with a specified range of significance, called its scope. The scope of a binding is an abt within which the bound identifier can be used, either as a place-holder (in the case of a variable declaration) or as the index of some operator (in the case of a symbol declaration). Thus the set of active identifiers can be larger within a subtree of an abt than it is within the surrounding tree. Moreover, different subtrees may introduce identifiers with disjoint scopes. The crucial principle is that any use of an identifier should be understood as a reference, or abstract pointer, to its binding. One consequence is that the choice of identifiers is immaterial, so long as we can always associate a unique binding with each use of an identifier. As a motivating example, consider the expression let x be a1 in a2, which introduces a variable x for use within the expression a2 to stand for the expression a1. The variable x is bound by the let expression for use within a2; any use of x within a1 refers to a different variable that happens to have the same name. For example, in the expression let x be 7 in x + x occurrences of x in the addition refer to the variable introduced by the let. On the other hand in the expression let x be x ∗ x in x + x, occurrences of x within the multiplication refer to a different variable than those occurring within the addition. The latter occurrences refer to the binding introduced by the let, whereas the former refer to some outer binding not displayed here. The names of bound variables are immaterial insofar as they determine the same binding. So, for example, let x be x ∗ x in x + x could just as well have been written let y be x ∗ x in y + y, without changing its meaning. In the former case the variable x is bound within the addition, and
1.2 Abstract Binding Trees 7 in the latter it is the variable y,but the "pointer structure"remains the same.On the other hand the expression let xbey *y inx+x has a different meaning to these two expressions,because now the variable y within the multiplication refers to a different surrounding variable.Renaming of bound variables is constrained to the extent that it must not alter the reference structure of the expression.For example,the expression letxbe2inletybe3inx+x has a different meaning than the expression letybe 2inletybe3iny+y, because the y in the expression y+y in the second case refers to the inner declaration,not the outer one as before. The concept of an ast can be enriched to account for binding and scope of a variable.These enriched asts are called abstract binding trees,or abts for short.Abts generalize asts by allowing an operator to bind any finite number(possibly zero)of variables in each argument.An argument to an operator is called an abstractor,and has the form x1,...,x.a.The sequence of variables x1,...,Xk are bound within the abt a.(When k is zero,we elide the distinction between.a and a itself.)Written in the form of an abt,the expression let x be a ina2 has the form let(a;x. a2),which more clearly specifies that the variable x is bound within a2,and not within a1.We often write X to stand for a finite sequence x1,...,n of distinct variables,and write a to mean x1,…yxn.a. To account for binding,operators are assigned generalized arities of the form(v1,...,Un)s,which specifies operators of sort s with n arguments of valence v1,...,Un.In general a valence v has the form s1,...,sk.s,which specifies the sort of an argument as well as the number and sorts of the variables bound within it.We say that a sequence of variables is of sort s to mean that the two sequences have the same length k and that the variable xi is of sort si for each 1<i<k. Thus,to specify that the operator let has arity (Exp,Exp.Exp)Exp indicates that it is of sort Exp whose first argument is of sort Exp and binds no variables,and whose second argument is also of sort Exp,within which is bound one variable of sort Exp.The informal expression let x be 2+2inx x x may then be written as the abt let(plus(num[2];num[2]);x.times(x;x)) in which the operator let has two arguments,the first of which is an expression,and the second of which is an abstractor that binds one expression variable. Fix a set S of sorts,and a family of disjoint sets of operators indexed by their generalized arities.For a given family of disjoint sets of variables Y,the family of abstract binding trees,or abts B]is defined similarly to A],except that is not fixed throughout the definition,but rather changes as we enter the scopes of abstractors. This simple idea is surprisingly hard to make precise.A first attempt at the definition is as the least family of sets closed under the following conditions: 1.IfxEX,thenx∈B[X]s
PREVIEW 1.2 Abstract Binding Trees 7 in the latter it is the variable y, but the “pointer structure” remains the same. On the other hand the expression let x be y ∗ y in x + x has a different meaning to these two expressions, because now the variable y within the multiplication refers to a different surrounding variable. Renaming of bound variables is constrained to the extent that it must not alter the reference structure of the expression. For example, the expression let x be 2 in let y be 3 in x + x has a different meaning than the expression let y be 2 in let y be 3 in y + y, because the y in the expression y + y in the second case refers to the inner declaration, not the outer one as before. The concept of an ast can be enriched to account for binding and scope of a variable. These enriched asts are called abstract binding trees, or abts for short. Abts generalize asts by allowing an operator to bind any finite number (possibly zero) of variables in each argument. An argument to an operator is called an abstractor, and has the form x1, . . . , xk . a. The sequence of variables x1, . . . , xk are bound within the abt a. (When k is zero, we elide the distinction between . a and a itself.) Written in the form of an abt, the expression let x be a1 in a2 has the form let( a1 ; x . a2 ), which more clearly specifies that the variable x is bound within a2, and not within a1. We often write ⃗x to stand for a finite sequence x1, . . . , xn of distinct variables, and write ⃗x . a to mean x1, . . . , xn . a. To account for binding, operators are assigned generalized arities of the form (υ1, . . . , υn)s, which specifies operators of sort s with n arguments of valence υ1, . . . , υn. In general a valence υ has the form s1, . . . ,sk .s, which specifies the sort of an argument as well as the number and sorts of the variables bound within it. We say that a sequence ⃗x of variables is of sort ⃗s to mean that the two sequences have the same length k and that the variable xi is of sort si for each 1 ≤ i ≤ k. Thus, to specify that the operator let has arity (Exp, Exp.Exp)Exp indicates that it is of sort Exp whose first argument is of sort Exp and binds no variables, and whose second argument is also of sort Exp, within which is bound one variable of sort Exp. The informal expression let x be 2 + 2 in x × x may then be written as the abt let( plus( num[ 2 ] ; num[ 2 ] ) ; x . times( x ; x ) ) in which the operator let has two arguments, the first of which is an expression, and the second of which is an abstractor that binds one expression variable. Fix a set S of sorts, and a family O of disjoint sets of operators indexed by their generalized arities. For a given family of disjoint sets of variables X , the family of abstract binding trees, or abts B[X ] is defined similarly to A[X ], except that X is not fixed throughout the definition, but rather changes as we enter the scopes of abstractors. This simple idea is surprisingly hard to make precise. A first attempt at the definition is as the least family of sets closed under the following conditions: 1. If x ∈ Xs , then x ∈ B[X ]s
8 1.2 Abstract Binding Trees 2.For each operator o of arity (s1.s1,...,Sn.sn)s,if a E B[X,]s,...,and an E B[,Enlsn then o(.a1;...;n.an )E B[s. The bound variables are adjoined to the set of active variables within each argument,with the sort of each variable determined by the valence of the operator. This definition is almost correct,but fails to properly account for renaming of bound variables. An abt of the form let(a;x.let(a2;x.a3))is ill-formed according to this definition,because the first binding adds x to &which implies that the second cannot also add x to t,x,because it is not fresh for ,x.The solution is to ensure that each of the arguments is well-formed regardless of the choice of bound variable names,which is achieved using fresh renamings,which are bijections between sequences of variables.Specifically,a fresh renaming (relative to A)of a finite sequence of variables is a bijection p:between and 'where x'is fresh for We write p(a)for the result of replacing each occurrence of x;in a by p(xi),its fresh counterpart. This is achieved by altering the second clause of the definition of abts using fresh renamings as follows: For each operator o of arity (s1.s1,...,sn.sn)s,if for each 1 i<n and each fresh renaming pi:,we have pi(ai)E B[,,then o(.a1;...;an)EB[a]s. The renaming,pi(ai),of each ai ensures that collisions cannot occur,and that the abt is valid for almost all renamings of any bound variables that occur within it. The principle of structural induction extends to abts,and is called structural induction modulo fresh renaming.It states that to show that P[(a)holds for every a E B],it is enough to show the following: 1.if xE &s,then P[]s(x) 2.For every o of arity (s1.s1,...,sn.sn)s,if for each 1si<n,P[,s (pi(ai))holds for every Pi:with,then P[]s(o(.a1;...;n.an )) The second condition ensures that the inductive hypothesis holds for all fresh choices of bound variable names,and not just the ones actually given in the abt. As an example let us define the judgment x e a,where a E BY,x,to mean that x occurs free in a.Informally,this means that x is bound somewhere outside of a,rather than within a itself. If x is bound within a,then those occurrences of x are different from those occurring outside the binding.The following definition ensures that this is the case: 1.x∈x. 2.x eo(.a1;...;an)if there exists 1 <i<n such that for every fresh renamingp: Ziwe have x∈p(a;) The first condition states that x is free in x,but not free in y for any variable y other than x.The second condition states that if x is free in some argument,independently of the choice of bound variable names in that argument,then it is free in the overall abt. The relation a =ab of a-equivalence (so-called for historical reasons),means that a and b are identical up to the choice of bound variable names.The a-equivalence relation is the strongest congruence containing the following two conditions:
PREVIEW 8 1.2 Abstract Binding Trees 2. For each operator o of arity (⃗s1.s1, . . . ,⃗sn.sn)s, if a1 ∈ B[X ,⃗x1]s1 , . . . , and an ∈ B[X ,⃗xn]sn , then o(⃗x1 . a1 ; . . . ; ⃗xn . an ) ∈ B[X ]s . The bound variables are adjoined to the set of active variables within each argument, with the sort of each variable determined by the valence of the operator. This definition is almost correct, but fails to properly account for renaming of bound variables. An abt of the form let( a1 ; x . let( a2 ; x . a3 ) ) is ill-formed according to this definition, because the first binding adds x to X , which implies that the second cannot also add x to X , x, because it is not fresh for X , x. The solution is to ensure that each of the arguments is well-formed regardless of the choice of bound variable names, which is achieved using fresh renamings, which are bijections between sequences of variables. Specifically, a fresh renaming (relative to X ) of a finite sequence of variables ⃗x is a bijection ρ : ⃗x ↔ ⃗x ′ between ⃗x and ⃗x ′ , where ⃗x ′ is fresh for X . We write ρb(a) for the result of replacing each occurrence of xi in a by ρ(xi), its fresh counterpart. This is achieved by altering the second clause of the definition of abts using fresh renamings as follows: For each operator o of arity (⃗s1.s1, . . . ,⃗sn.sn)s, if for each 1 ≤ i ≤ n and each fresh renaming ρi : ⃗xi ↔ ⃗x ′ i , we have ρbi(ai) ∈ B[X ,⃗x ′ i ], then o(⃗x1 . a1 ; . . . ; ⃗xn . an ) ∈ B[X ]s . The renaming, ρbi(ai), of each ai ensures that collisions cannot occur, and that the abt is valid for almost all renamings of any bound variables that occur within it. The principle of structural induction extends to abts, and is called structural induction modulo fresh renaming. It states that to show that P[X ](a) holds for every a ∈ B[X ], it is enough to show the following: 1. if x ∈ Xs , then P[X ]s(x). 2. For every o of arity (⃗s1.s1, . . . ,⃗sn.sn)s, if for each 1 ≤ i ≤ n, P[X ,⃗x ′ i ]si (ρbi(ai)) holds for every ρi : ⃗xi ↔ ⃗x ′ i with ⃗x ′ i ∈ X / , then P[X ]s(o(⃗x1 . a1 ; . . . ; ⃗xn . an )). The second condition ensures that the inductive hypothesis holds for all fresh choices of bound variable names, and not just the ones actually given in the abt. As an example let us define the judgment x ∈ a, where a ∈ B[X , x], to mean that x occurs free in a. Informally, this means that x is bound somewhere outside of a, rather than within a itself. If x is bound within a, then those occurrences of x are different from those occurring outside the binding. The following definition ensures that this is the case: 1. x ∈ x. 2. x ∈ o(⃗x1 . a1 ; . . . ; ⃗xn . an ) if there exists 1 ≤ i ≤ n such that for every fresh renaming ρ : ⃗xi ↔ ⃗zi we have x ∈ ρb(ai). The first condition states that x is free in x, but not free in y for any variable y other than x. The second condition states that if x is free in some argument, independently of the choice of bound variable names in that argument, then it is free in the overall abt. The relation a =α b of α-equivalence (so-called for historical reasons), means that a and b are identical up to the choice of bound variable names. The α-equivalence relation is the strongest congruence containing the following two conditions: