Adding the Function Space Type

Given two types, and , we write for the type of all computable functions from type to type . As soon as we add a this type, we get ``abstract'' math. For example, the type has an uncountable number of elements. Recall that the number of functions from to is , where and are the cardinalities of and , respectively. Thus, the elements of a function type cannot be recursively enumerated. There are inherently fewer representations of (or names for) functions than there are functions themselves. In a programming language, we can name partial functions as well as total functions. One can recursively enumerate all partially recursive functions, e.g. by enumerating Turing machines.

Distiguishing characteristics of abstract mathematical objects:

• not recursively-enumerable
• equality is not necessarily decidable (i.e. for functions)
• the canonical names of the data do not give a complete picture of it, so there are no standard unique names for the data

In order to name functions, we shall make us of the lambda calculus notation , e.g. . Here, is the formal parameter and is the body. The function thus constructed is in the type iff for all , . We can apply such a function to an argument , giving .

In ML we write as \x.b, where the backslash is intended to be visually similar to . ML syntax also allows multiple abstractions to be written without having to repeatedly write the backslash; e.g., becomes \x1 . . . xk.b.

It also has the following entry forms:

• let f x = b
• let f = \ x . b
• letrec f x = b

The last of these is different from the others; in it, f may appear free in b. This makes it possible to come up with examples of a non-terminating functions that would not otherwise arise. This is in contrast to the usual practice of mathematics, where the concept of non-terminating functions does not arise. A simple ML example of a non-terminating function is: letrec f x = f x