Grail Tutorial - Semantics

The simply typed lambda calculus

The semantics of categorial grammars (and the semantics used by Grail is no exception) is usual presented in the form of typed lambda calculus. This is due to the fact that the Curry-Howard homomorphism gives us a direct mapping from categorial proofs to typed lambda terms.

This section gives a very brief introduction to the (extensional) typed lambda calculus. For more extensive and detailed introductions, see (Gamut 1991). Types τ are defined as follows: there are two basic types e (for entities) and t (for truth values) and two recursively defined types. When α and β are types, so are α → β and α × β. α → β is the set of functions from α to β whereas α × β is the Cartesian product of α and β.

For terms, we will often write tα to indicate term t is of type α, though, when the type can be deduced from the context we will often omit it. Given a set of variables vα (of each type α ∈ τ) and a set of constants cα (of each type α ∈ τ) we defined the set of terms as follows.

    1. vα is a term of type α
    2. cα is a term of type α
    1. If T is a term of type α → β and u is a term of type α then (t u) is a term of type β.
    2. If T is a term of type β and v is a variable of type α then λv.t is a term of type α → β.
    1. If T is a term of type α and U is a term of type β then ⟨T,U⟩ is a term of type α × β.
    2. If T is a term of type α × β then π1T is a term of type α and π2T is a term of type β
    1. If T is a term of type t (ie. a truth value) then ¬T is a term of type t.
    2. If T and U are terms of type t then TU, TU and TU are terms of type t.
    3. If T and U are terms of type α then T = U is a term of type t.
    4. If T is a term of type t and v is a variable of type e (ie. an entity) then ∀v.T and ∃v.T are terms of type t.

Clause 1 is the base case. It introduces both variables (1.a) and constants (1.b) into the system.

Clause 2 introduces the application (2.a) and abstraction operations (2.b) for the functional types.

Clause 3 introduces the pairing (3.a) and projection operations (3.b) for the Cartesian product types.

Clause 4 introduces the logical connectives of negation (4.a), conjunction, disjunction and implication (4.b), equality between terms of the same type (4.c) and the existential and universal quantifiers (4.d).

(We can also follow Church and treat the logical symbols ¬, ∧, ∀ etc. as constants. However, Grail follows the strategy indicated above in clause 4).

Normalization

Now a term t of the form λxα.t can be seen as a function which takes a variable x of type α as its argument. Now, if we give such a function an argument of the right type, that is to say a term u of type α the result will be term t, but with all occurences of the variable x replaced by the term u (to be precise, we need to make sure that no free occurrences of x become bound by this substitution; however, this can always be assured by renaming variables). This rule is called beta conversion. The cases for the Cartesian product are shown in the table below. The first projection selects the first element of a pair, the second projection selects the second element.
v.t) u =βt[v:=u]
π1t,u=β t
π2t,u=β u

Table 1. β-conversion rules.

We say a lambda term is in normal form if it does not contain any of the left hand sides of the equalities shown in Table 1 as a subterm.

An important theorem of the simply typed lambda calculus is that β conversion is confluent. In other words, whenever there are two ways to reduce a lambda term, both reductions will (eventually) reduce further to the same result term. As a consequence the normal form of a term is unique.

In addition, the calculation of a normal form is terminating. That is to say, any reduction sequence of beta steps is finite and ends with a normal form.

The formulas-as-types interpretation for categorial grammars

type(s) = t
type(n) = et
type(np) = e
type(A/B) = type(B) → type(A)
type(B\A) = type(B) → type(A)
type(A•B) = type(A) × type(B)

Table 2. Typing rules for basic and complex formulas.

Links for NL with the
semantics added in blue

Figure 1. The graph connections with the corresponding typed lambda term semantics

Find out how to represent typed lambda terms in your lexicon.


Last modified: Thu Oct 20 18:05:53 CEST 2011