ABSTRACT. This paper, which attempts to develop an abstract construct that generalizes the intensionalization procedure introduced by Kanazawa and de Groote, advocates for the use of logical relations in order to establish conservativity results.

ABSTRACT. We have proposed a framework based upon the λ -calculus with higher-order intuitionistic types for the symbolic computation of the semantic analysis, integrating lexical data. This proposal is sufficient for many phenomena and accurately incorporates lexical semantics by the means of type theory, but some issues linger in the linguistic data. In the present paper, we revisit this proposal with a version of the λ -calculus based upon higher-order linear types, that aims to resolve those issues and present an integrated framework for meaning assembly.

ABSTRACT. Pregroup grammars [Lambek 1999] are a recent descendant of the original categorial grammars [Bar-Hillel 1950, Lambek 1958]. The driving idea of these frameworks is that we can assign mathematical types to elements of our language and then perform grammaticality checks on concatenations of them by inspecting the corresponding string of types and making use of their mathematical properties. When it comes to doing semantics (both lexical and derivational are possible), one of the main approaches in type-logical grammars [Carpenter 1997] is to assign semantic terms to the lexical items and perform parallel derivations on both those terms and on the syntactic types to end up with a compositional meaning of the sentence; the λ-calculus is often used for that purpose. One of the problems with trying those approaches in pregroup grammars is that it is hard to think of pregroups as having function types because of their algebraic nature. So few constraints are put on the order of their reductions and assigning λ-terms to them without somehow explicitly marking on their type the order in which they should be reduced would fail at creating a sound system. On the other hand, something like a non-associative pregroup grammar would add too much constraint on the types and make them lose one of their most attractive properties. We show how to define a term-calculus that resembles the λ-calculus in its internal functioning, with one huge difference, namely bi-directionality. We also define the term reduction rules so that they follow closely the syntactic derivations without adding extra complexity to the whole system.

ABSTRACT. We study nonlinear connectives (exponentials) in the context of Type Logical Grammar (TLG). We devise four conservative extensions of the Displacement calculus with brackets, \DbC, \DbCM, \DbCb and \DbCbMr which contain the universal and existential exponential modalities of linear logic (\LL). These modalities do not exhibit the same structural properties as in \LL, which in TLG are especially adapted for linguistic purposes. The universal modality \univexp for TLG allows only the commutative and contraction rules, but not weakening, whereas the existential modality \exstexp allows the so-called (intuitionistic) mingle rule, which derives a restricted version of weakening called \emph{expansion}. We provide a Curry-Howard labelling for both exponential connectives. As it turns out, controlled contraction by \univexp gives a way to account for the so-called parasitic gaps, and controlled Mingle \exstexp iterability, in particular iterated coordination. Finally, the four calculi are proved to be Cut-Free but decidability is only proved for $\DbCb$, whereas for the rest the question of decidability remains open.

ABSTRACT. We present the grammar/semantic formalism of Applicative Abstract Categorial Grammar (AACG), based on the recent techniques from functional programming: applicative functors, staged languages and typed final language embeddings. AACG is a generalization of Abstract Categorial Grammars (ACG), retaining the benefits of ACG as a grammar formalism and making it possible and convenient to express a variety of semantic theories.

We use the AACG formalism to uniformly formulate Potts' analyses of expressives, the dynamic-logic account of anaphora, and the continuation tower treatment of quantifier strength, quantifier ambiguity and scope islands. Carrying out these analyses in ACG required compromises and the ballooning of parsing complexity, or was not possible at all. The AACG formalism brings modularity, which comes from the compositionality of applicative functors, in contrast to monads, and the extensibility of the typed final embedding. The separately developed analyses of expressives and QNP are used as they are to compute truth conditions of sentences with both these features.

AACG is implemented as a `semantic calculator', which is the ordinary Haskell interpreter. The calculator lets us interactively write grammar derivations in a linguist-readable form and see their yields, inferred types and computed truth conditions. We easily extend fragments with more lexical items and operators, and experiment with different semantic-mapping assemblies. The mechanization lets a semanticist test more and more complex examples, making empirical tests of a semantic theory more extensive, organized and systematic.

ABSTRACT. We prove that non-linear second order Abstract Categorial Grammars (2ACGs) are equivalent to non-deleting 2ACGs. We prove this result first by using the intersection types discipline. Then we explain how coherence spaces can yield the same result. This result shows that restricting the Montagovian approach to natural language semantics to use only $\L I$-terms has no impact in terms of the definable syntax/semantics relations.