The lambda calculus is a simple language that is often used to study the theory of programming languages. This language only consists of variable references, functions that take a single argument, and applications of functions.
The lambda calculus consists of a language of lambda terms. The syntax of the lambda calculus defines that all valid lambda terms can be built by applying the following three rules:
1. a variable x, which is a nonempty string other than lambda, is itself a lambda term;
2. if t is a valid lambda term, and x is a variable, then (lambda (x) t) is a lambda term (called a lambda abstraction), here x has at least one occurrence in t;
3. if t and s are lambda terms, then (t s) is a lambda term (called an application).
Nothing else is a lambda term. Thus a lambda term is valid if and only if it can be obtained by repeated application of these three rules. Note that the parentheses in the second and the third rule can NOT be omitted.
A lambda abstraction (lambda (x) t) is a definition of an anonymous function that is capable of taking a single input x and substituting it into the term t. The abstraction binds the variable x in term t, so we call it a lambda binding of variable x.
An application (t s) represents the application of a function t to an input s, that is, it represents the act of calling
function t on input s to produce t(s).
To see how this works, consider the lambda calculus extended with arithmetic operators. In that language, a lambda abstraction (lambda (x) x + 5), in which x is bound, defines a function f(x) = x + 5. And an application ((lambda (x) x + 5) 3) applies function f(x) = x + 5 to input 3 and produces f(3) = 3 + 5 = 8.
We say that a variable occurs free in an lambda term t if it has some occurrence in t that is not inside some lambda binding of the same variable. For example,
$\bullet$ x occurs free in x;
$\bullet$ x does not occur free in y;
$\bullet$ x does not occur free in (lambda (x) (x y));
$\bullet$ x occurs free in (lambda (y) (x y));
$\bullet$ x occurs free in ((lambda (x) x) (x y)), which is an application that produces (x y) in which x occurs free;
$\bullet$ x occurs free in (lambda (y) (lambda (z) (x (y z)))).
Now you are given a lambda term t, you need to find all distinct variables that occur free in t.