Language, Lambdas, and Logic

Abstract

In (van Benthem 1986) it was observed that the Curry-Howard correspondence between proofs and λ-terms can be exploited to obtain a very elegant and principled match between Lambek Categorial Grammar and Montague Semantics. The correspondence associates each proof of the calculus with a λ-term and Van Benthem shows how such terms can be used as a recipe for obtaining the meaning of a complex expression in terms of the meanings of its parts. The method is easily extended to various other forms of Lambek calculi, including multimodal calculi (see (Moortgat 1997) and references therein). Van Benthem's original work concerned the undirected Lambek Calculus, for which the Curry-Howard correspondence is an isomorphism, but the use of undirected calculi has not caught on. Superficially it seems that using an undirected calculus entails that the permutations of any string that is predicted to be grammatical are likewise predicted to be grammatical and understandably categorial grammarians therefore have preferred directed systems. However, from (Oehrle 1994, Oehrle 1995) it is apparent that the permutation difficulty can be overcome by radicalising the approach. This is done by using the Curry-Howard isomorphism not only for obtaining a λ-term representing the semantics of an expression, but also for getting a λ-term representing its syntax. As will be argued below, the permutation problem then vanishes, for any effect of permutation on the semantic term is re ected by a similar effect on the syntactic term and vice versa. Since syntactic and semantic representations can only permute in tandem, they will not be coupled in an undesirable way.