Dynamic Lambda Calculus
Michael Kohlhase, Susanna Kuschert · 1999
In this paper, we introduce an lambda calculus DLC that is intended a meta-logic for compositional discourse logics, and we investigate its meta-theory. DLC extends simply typed -calculus with an operator ffi for the declaration of referents. In contrast in classical - 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 -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 behaviour is captured in the type system. 1 INTRODUCTION 1 Introduction Over the past decade, there has been a series of attempts [Zee89, GS90, vEK96, Mus96, KKP96, Kus96, vE97] to combine Montague's type theoretic framework for compositional construc...