For example if p is false and q is undefined, we see that according to the definitions given above is false, but is undefined. For our applications this noncommutativity is desirable, since is computed by first computing p , and if p is false q is not computed. If the computation for p does not terminate, we never get around to computing q . We shall use propositional connectives in this sense hereafter. Because we shall later compute with expressions for functions, we need a distinction between functions and forms and a notation for expressing this distinction.
Church calls an expression like , a form.
A form can be converted into a function if we can determine the correspondence between the variables occurring in the form and the ordered list of arguments of the desired function. This is accomplished by Church's -notation. If is a form in variables then will be taken to be the function of n variables whose value is determined by substituting the arguments for the variables in that order in and evaluating the resulting expression. For example, is a function of two variables, and . The variables occurring in the list of variables of a -expression are dummy or bound, like variables of integration in a definite integral.