1.4.2 Reducing Complex Expressions

So the use of -bound variables allows us to mark places where information is missing in a partial first order formula. But how do we fill in the missing information when it becomes available? The answer is simple: We substitute it for the -bound variable. We can read a -prefix as a request to perform substitution for its bound variable.

We will use concatenation (marked by an @-symbol) to indicate when we have to perform substitutions, and what to substitute. By concatentating a -expression with another expression, we trigger the substitution of the latter for the -bound variable. Consider the following expression (we use the special symbol @ to indicate concatenation):

Functional Application, -Reduction

This compound expression consists of the abstraction written immediately to the left of the expression , both joined together by @. Such a concatenation is called functional application ; the left-hand expression is called the functor, and the right-hand expression the argument. The concatenation is an instruction to discard the prefix of the functor, and to replace every occurrence of that was bound by this prefix with the argument. We call this substitution process -reduction (other common names include -conversion and -conversion). Performing the -reduction demanded in the previous example yields:

The purpose of -bound variables is thus to mark the slots where we want substitutions to be made, the purpose of -prefixes is to indicate at what point in the reduction process substitutions should be made, and the arguments of applications provide the material to be substituted. Abstraction, functional application, and -reduction together will drive our first really systematic semantic construction mechanism. Next, let's see how it works in practice.