Functions

function type

The function type is one of the most important in modern mathematics. As we have noted, Frege patterned his treatment of logic which we are following on the concept of a function. In some ways this type represents the divide between abstract and concrete mathematics. By quantifying over functions we enter the realm of abstract mathematics. Indeed, the very notion of obtaining a function from an expression is called abstraction.

The day-to-day notation for functions at the beginning of the century was that one wrote phrases like ``the function sin(x) in x or e^x in x''. Russell's notation, $\phi \hat{x}$, and Church's lambda notationlambda notation, $\lambda x. e^x$, brought flexibility to the notation, creating a single name for the function with a binding operator $(\lambda)$ to indicate the arguments. The modern working notation in mathematical articles and books (used in Bourbaki for example) is $x \mapsto b$ for a function with argument x and value given by the expression b in x; for example $x \mapsto x$ for the identity, $x \mapsto e^x$ for the exponential.

As we did for propositional functions, we will adopt the lambda notation in the form $\lambda(x.b)$ for $x \mapsto b$. In Nuprl one can display this in a variety of ways, including $x \mapsto b$ or $b\hat{x}$ or fun $x \Rightarrow b$. The important points are:

• There is an operator name, lambda that distinguishes functions. Their canonical value is $\lambda(x.b)$.lambda notation

• A binding phrasebinding phrase, $x.\ b$ is used to identify the name of the argument (or formula parameter), x, and the body of the function.

• The usual rules about binding phrases apply concerning bound variables, scope, and $\alpha$-equality.

Essentially the only way to use a function is to apply it to an argument.¹⁹ Informal notation for applying a function f to an argument a is to write f(a) or fa or even to show the substitution of ``actual'' argument for the ``formal'' one as in sin(a) or e^a. We adopt an operator name to remind ourselves that applicationapplication is a distinct operation. So we write ap(f; a). But again, Nuprl can display this anyway the user pleases, e.g. as f(a) or fa or even $f.\ a$ or f@a.

One of the major discoveries from a systematic study of function notations, especially the lambda calculus and combinatory calculus and later programming languages, is that rules for formally calculating with functions can be given independently of their meaning, especially independently of types.

The rules for calculation or for ``definitional equality'' can be expressed nicely as evaluation rules. Here is the so called ``call_by_name''call by name evaluation rule.definedness ( $\downarrow$)

$$\frac{f \downarrow \lambda(x.\ b)\ \ \ b[z/x] \downarrow c}{ap(f; a) \downarrow c}$$

The ``call_by_value''call by value rule is this definedness ( $\downarrow$)

$$\frac{f \downarrow \lambda(x.\ b) \ \ a \downarrow a'\ \ b[a'/x] \downarrow c}{ap(f; a) \downarrow c}$$

Closed expression functions like $I== \lambda(x.\ x)$ or $K== \lambda(x.\ \lambda(y.\ x))$ are called combinatorscombinator; these two are ``polymorphic''polymorphic in that we can compute their values regardless of the form of the input. Thus $ap(\lambda(x.\ x); K) \downarrow K$and $ap(\lambda(x.\ x); 0) \downarrow 0$, and $ap(K; I) \downarrow \lambda(x.\ I)$.

Other functions like $\lambda(z. 1 o\!f(z))$ or $\lambda(z. add(1 o\!f(z); 2 o\!f(z)))$ can only be reduced to values on inputs of a specific form, and others like $\lambda(x. suc(x))$ or $\lambda(x.\ 4/x)$ reduce to meaningful values (typed values) only on specific inputs. For example, $ap(\lambda(z. 1 o\!f(z); 0) \downarrow 1 of(0)$but $1 o\!f(0)$ is not a canonical value let alone a sensible value. In the case $ap(\lambda(x.\ suc(x)); pair(0; 0))$ the result of evaluation is the value suc(pair(0; 0)), but this value has no type.