Enriched Meanings

This book presents a theory of enriched meanings for natural language interpretation. Certain expressions that exhibit complex effects at the semantics/pragmatics boundary live in an enriched meaning space while others live in a more basic meaning space. These basic meanings are mapped to enriched meanings just when required compositionally, which avoids generalizing meanings to the worst case. The theory is captured formally using monads, a concept from category theory. Monads are also prominent in functional programming and have been successfully used in the semantics of programming languages to characterize certain classes of computation. They are used here to model certain challenging linguistic computations at the semantics/pragmatics boundary. Part I presents some background on the semantics/pragmatics boundary, informally presents the theory of enriched meanings, reviews the linguistic phenomena of interest, and provides the necessary background on category theory and monads. Part II provides novel compositional analyses of the following phenomena: conventional implicature, substitution puzzles, and conjunction fallacies. Part III explores the prospects of combining monads, with particular reference to these three cases. The authors show that the compositional properties of monads model linguistic intuitions about these cases particularly well. The book is an interdisciplinary contribution to Cognitive Science: These phenomena cross not just the boundary between semantics and pragmatics, but also disciplinary boundaries between Linguistics, Philosophy and Psychology, three of the major branches of Cognitive Science, and are here analyzed with techniques that are prominent in Computer Science, a fourth major branch. A number of exercises are provided to aid understanding, as well as a set of computational tools (available at the book's website), which also allow readers to develop their own analyses of enriched meanings.

Denotational semantics of recursive types in synthetic guarded domain theory

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.