Identifiers as Strings.

Lambda terms: variables, application, abstraction.

Compute all redexes of a given term.

The set of all variables occurring in a term. For example

vars (App (Var "x") (Abs "y" (Var "y"))) == ["x", "y"]

The set of free variables occurring in a term. For example

fvs (App (Var "x") (Abs "y" (Var "y"))) == ["x"]

Given a variable x and a set of variable names to avoid ys, freshName x ys computes a pair (x', ren) such that x' is a variable that is fresh for ys (that is, different from all elements of ys) and ren :: Term -> Term is a function that renames all occurrences of x in a term by x'.

Applying a substition [x := s] to a lambda term t. For example (note how the bound variable "y" is renamed in order to avoid variable capture)

subst "x" (Var "y") (Abs "y" (App (Var "x") (Var "y"))) == Abs "z" (App (Var "y") (Var "z"))

showsPrecTerm n t transforms term t within a context of precedence n into a "string" (for efficiency reasons actually the type ShowS is used).