Michael Kohlhase
Department of Computer Science
CMU and Saarbr"ucken, Germany

Abstract:
In this talk, I will introduce a lambda calculus originating from the goal of formalizing compositional discourse logics. Discourse logics are variants of first-order logic that provide a notion of state (they are dynamic). The meaning of a sentence in a discourse is posited not only to affect the truth conditions, but also on its effect on the state of the so-called discourse referents. The state in turn affects the interpretation of e.g. anaphoric pronouns, that can refer back to discourse referents in the state.

Compositional semantics construction has been one of the main pillars of natural language semantics, since it allows simple and logic-based syntax-semantics interface. Following Richard Montague's approach, the intended goal representation (e.g. first-order logic) is embedded into a higher-order language (e.g. simply typed lambda-calculus), so that all syntactically well-formed sentence constituents are given meanings as higher-order objects. Syntactic composition of syntactic constituents is mapped into functional application or composition of constituent meanings and the goal representation is computed by beta-reduction.

Combinations of these approaches have been used in practical computational linguistics without a proper logical foundation or meta-theory. In this talk I will present the dynamic lambda calculus DLC that tries to remedy this situation. DLC extends simply typed lambda-calculus with an operator delta for the declaration of referents. In contrast in classical lambda-abstraction, the scope of declaration is not a lexical one but may extend to its context: This allows declaration to capture referents, which breaks a taboo in traditional lambda-calculi.

DLC provides an expressive type system which allows to encode information about the scope of declaration in terms of so-called modalities. Since different linguistic theories may need to employ different notions of scope, the modalities are made signature-dependent, while their interaction behavior is captured in the type system.