3.4.4 [Sidetrack] Simply Typed Lambda-Calculus

In this section we discuss two topics that are important in connection with -calculus, but that have been ommited so far: Types and the semantics of -expressions in terms of functions.

The perspective we've been taking on -calculus so far has been a very technical one. We 've been viewing it simply as a tool for controlling substitutions, without caring much what single -expressions actually mean. If you've heard about -Calculus before in other semantics textbooks or lectures, you will probably feel that we have left out a discussion of at least two points:

Types: The version of -calculus most commonly used in linguistics is simply typed -calculus . In this calculus, expressions get assigned types that regulate function application.
Functions: -expressions can be given an interpretation in terms of functions over a system of complex domains. (In fact -calculus was originally designed to investigate function definition, function application and recursion.)

As regards the first point: The version of -calculus we're going to use is untyped, and we'll argue below that we don't have to interpret any -expressions for our purposes. Nevertheless, the two points just mentioned are very important theoretical topics concerning the use of -calculus in formal semantics. Therefore, we will now give a short sketch of some of the central ideas involved in an interpreted simply typed -calculus.

Types

Every expression gets assigned a unique type in simply typed -calculus. On the one hand such types restrict how applications can be formed and regulate what the results of applications will be after -reduction. On the other hand types correspond to certain classes of semantic entities and thereby tell us that the typed expressions are to be interpreted in terms of these entities.

Basic types

But how does all of this work? Let's assume we are using simply typed -calculus to construct first order meaning representations with the goal of evaluating them in a given model. So we know what the domain of that model is. Now for our type system. Initially, we have two basic types, written as and . The type corresponds to the domain of our model (i.e. the set of our basic individuals). It gets assigned to constant symbols, which pick out entities from that set in our model. So for instance, a constant symbol would be assigned type because it picks out a basic entity (for instance Mary). Moreover, standard first order variables (which range over the domain of our model) are also of type .

The other basic type is . It corresponds to the set of truth values (that is, the set , and it gets assigned to complete well-formed first order formulae (i.e. to expressions that can be evaluated to a truth value in our first order model).

Complex types

We can then recursively construct complex types from these two basic types. Such complex types are written as , where and are themselves types. For example from the basic types and we can form the complex type , and from this complex type and type , we can form . A complex type of the form corresponds to the set of functions from things of type (the argument type ) to things of type (the result type ). For instance, type corresponds to the functions from basic entities (like, for instance, John and Mary) to the truth values.

But what do we need complex types for? They are the types that get assigned to -expressions. A -abstraction of the form is of type , where is the type of the -bound variable , and is the type of the scope of the abstraction.

For example (assuming that is a well-formed first order formula), the type of the abstraction is . The reason is that is a first order variable ranging over individuals, hence of type , and is a first-order formula, hence of type .

Well-Typedness

Types regulate which applications are possible: In typed -calculus, applications are only allowed if the type of the argument (to the right of the @ in the expression) is the same as the argument type of the functor (to the left of the @). The result of -reducing such an application is then always of the result type of the functor. If all applications in an expression are allowed according to this criterion, the expression is well-typed .

Consider the following expression:

The application is allowed (it is well-typed), because is of type and this is also the argument type of the functor

Recall that this functor is of type . The result of -reducing the above application is of type - the result type of the functor.

In contrast the application

is not admissible (it is not well-typed), because the type of the argument (, this time) and the functor's argument type () don't match.

Thus one aspect of the type system is that it formalizes what we express by a typographic convention in our untyped approach: The different kinds of missing information that -bound variables may stand for. But more than this. If we form our abstractions only from well-formed first order formulae and respect the well-typedness restrictions, we really know for sure that we can always return to a well formed first-order formula through a series of well-typed applications and -reductions. Consider for instance the -expression , where is of type , and and are of type (incidentally, this is the kind of -expression we will be using for transitive verbs). The expression is built up from the first-order formula , abstractions and a well typed application. Hence we can be sure that we will be able to get a well-formed first order formula (namely with and possibly replaced by some constants) if we feed our original expression arguments of the right type and then -reduce. Notice that this ``guarantee of full -reducibility'' is a property we plainly took for given with our untyped -calculus when we said above that we would view it as a simple notational extension of first order logic.

Interpreting Abstractions and Applications

We have not said much about the interpretation of -abstractions and applications so far. Yet keeping in mind what sets correspond to complex types, this becomes an easy matter: For each complex type, we have the corresponding set of functions from its argument type to its result type. Thus, we will simply interpret each -abstraction as one function from the set corresponding to its (complex) type. Applications are interpreted by really applying the interpretation of the functor to the interpretation of the argument.

For instance, we will interpret (of type ) as a function from individuals to truth values. The application will be interpreted by applying this function to the interpretation of .

Moreover, given a model, we will choose as interpretation for the function that yields exactly for those members of the domain that are in the set interpreting the predicate (the so-called characteristic function of that set). Hence, the interpretation of will be the same as the interpretation of the -reduced formula in our given model. Generally, choosing characteristic functions as the interpretation of -abstractions of type , we can couple the interpretation of -terms with the first-order interpretation of our goal formulae: We can be sure that the interpretation of any well-typed application that can be -reduced to a first order formula will be the same as the interpretation of this formula itself.

Let's add one final, more fundamental remark to our discussion. We have just seen how simply typed -calculus allows us to give an interpretation of the -expressions involved in semantic construction in terms of well-understood mathematical entities (namely functions). This is a great achievment from the point of view of compositionality. Remember that one of the requirements made by the principle of compositionality was that we should be able to give individual semantic interpretations to the syntactic parts and sub-parts of the expressions in our language. Semantic construction using simply typed -calculus fulfills this requirement in the particularily strict sense of d-compositionality, thus even beyond the level of meaning representations: The interpretation in terms of functions which we've dicussed enables us to state exactly which of the functions built up over the domain of our model corresponds to any syntactic part of a sentence.

Then why do we use the untyped version?

But although very interesting from a theoretical perspective, the issues just discussed are not nearly as important for understanding the -based semantic construction mechanism we're going to implement. In particular:

For a start, we do not care to interpret any -expressions before they're fully -reduced. Also, we will not ask for the meaning of any individual parts of our sentence relative to a model. Below sentence level, we will be happy with having a meaning representation to work ourselves through to the whole sentence. Most of the time, the first-order formula that we get after -reducing is all that interests us. So any arguments about interpreting unreduced -expressions aren't of great relevance for our purposes.
As regards the guarantees about getting useful results after -reduction that come with simply typed -calculus: We will basically use our untyped version of -calculus as if it was typed. All the (well formed) expressions we will encounter would also be well typed in a typed -calculus. Thus we may safely take it for granted that we can always reduce the meaning reprentations for sentences to first order formulae. This is only due to our own discipline, we could do less decent things with our untyped calculus (and the implementation we're going to base on it).

Implementing typed -calculus would require a lot of efforts particularily for managing the type system. So we will use a disciplined approach to the untyped version instead.