The formalism previously described enables us to define functions that have functions as arguments. For example,
can be regarded as a function of the numbers m and n and the sequence tex2html_wrap_inline953 . If we regard the sequence as a function f we can write the recursive definition
displaymath957
or in terms of the conventional notation
Functions with functions as arguments are called functionals.
Another example is the functional least(p) which gives the least integer n such that p(n) for a predicate p. We have
displaymath967
where
displaymath969
In order to use functionals it is convenient to have a notation for naming
functions. We use Church's [1] lambda notation. Suppose we have a function f
defined by an equation tex2html_wrap_inline973 where e is some expression in tex2html_wrap_inline641 . The name of this function is tex2html_wrap_inline979 . For example, the name
of the function f defined by tex2html_wrap_inline603 is tex2html_wrap_inline985 .
Thus we have
displaymath987
but
displaymath989
The variables occurring in a tex2html_wrap_inline991 definition are dummy or bound variables and can be replaced by others without changing the function provided the replacement is done consistently. For example, the expressions
displaymath993
displaymath995
and
displaymath997
all represent the same function.
In the notation tex2html_wrap_inline999 is represented by tex2html_wrap_inline1001 and the least integer n for which tex2html_wrap_inline1005 is represented by
displaymath1007
When the functions with which we are dealing are defined recursively, a difficulty arises. For example, consider factorial defined by
displaymath1011
The expression
displaymath1013
cannot serve as a name for this function because it is not clear that the occurrence of ``factorial'' in the expression refers to the function defined by the expression as a whole. Therefore, for recursive functions we adopt an additional convention, Namely,
displaymath1015
stands for the function f defined by the equation
displaymath1019
where any occurrences of the function letter f within e stand for the function being defined. The letter f is a dummy variable. The factorial function then has the name
displaymath1027
and since factorial and n are dummy variables the expression
displaymath1033
represents the same function.
If we start with a base domain for our variables, it is possible to consider a hierarchy of functionals. At level 1 we have functions whose arguments are in the base domain. At level 2 we have functionals taking functions of level 1 as arguments. At level 3 are functionals taking functionals of level 2 as arguments, etc. Actually functionals of several variables can be of mixed type.
However, this hierarchy does not exhaust the possibilities, and if we allow functions which can take themselves as arguments we can eliminate the use of label in naming recursive functions. Suppose that we have a function f defined by
displaymath1039
where tex2html_wrap_inline1041 is some expression in x and the function variable f. This function can be named
displaymath1047
However, suppose we define a function g by
displaymath1051
or
displaymath1053
We then have
displaymath1055
since g(x,g) satisfies the equation
displaymath1059
Now we can write f as
displaymath1063
This eliminates label at what seems to be an excessive cost. Namely, the
expression gets quite complicated and we must admit functionals capable of
taking themselves as arguments. These escape our orderly hierarchy of
functionals.
