A *binding* is a special term that associates a variable name with another term. A binding has the following form.

  { bind $x -> 7, $y -> 21 }

This represents binding the variable \$ to the value 7, and the variable \$y to the value 21. A binding is *applicative*, meaning it can be applied to another term. This results in the given substitutions being performed.

An important item to consider is that variables are matched on both name and type, but are *bound* by name only. (This is done to make rewriting more efficient.) This means that rewriting relies on the variable name alone; types and any guards are used only during matching.

Applying a binding to a term replaces instances of the bound variables with the bound terms.

  { bind $x -> 7, $y -> 21} . add($x,$y)  --> add(7,21) --> 28
  { bind $x -> 7, $y -> 21} . concat($x: STRING,$y: STRING)  --> concat(7,21) --> type error