Lambda calculus
The substitution operator is used extensively. The expression formula_4 means substitute every occurrence of "G" in "L" by "S" and return the expression. The definition used is extended to cover the substitution of expressions, from the definition given on the Lambda calculus page. The matching of expressions should compare expressions for alpha equivalence (renaming of variables).