NATURAL LANGUAGE SEMANTIC REPRESENTATIONS AS TYPES

   				Tim Fernando

    Can we view natural languages as programming languages fit for computers?
    This course surveys some topics in linguistic semantics where such a view
    has arguably advanced Montague's slogan `English as a formal language.' 
    These include work on anaphora and presupposition commonly labelled 
    `dynamic semantics' (DS), and investigations into what T. Parsons calls 
    `sub-atomic semantics' (SS), delving into, for example, verbs. DS has a 
    proof-theoretic formulation (detailed by A. Ranta within intuitionistic
    type theory) that equates a proposition with the type of its proofs, 
    providing a declarative alternative to the imperative (assignment-based) 
    languages of Quantified Dynamic Logic. But `propositions-as-types' says 
    nothing about what proofs of atomic formulae are, or where models
    interpreting such formulae come from.

    The bulk of the course covers a formulation of propositions-as-types
    for SS, pushing systems of typed-lambda calculi/functional programming
    down to regular languages to analyze the notion of an event(-type).
    Events are conceived as sequences of observations (much like comics
    and movies) that are accepted by finite automata. Mereological approaches
    to events are reconstructed in terms of suitable entailments between the 
    regular languages, grounded in time. Forcing conditions are formed from
    strings in the languages, relative to which worlds and models are 
    derived from generic sets. Ideas about temporality from Reichenbach and 
    Vendler discussed by Steedman in connection with the frame problem from 
    AI are analyzed in a finite-state setting. Notions of causation and 
    inertia are considered, and related to recent work on M. Shanahan's event
    calculus by Hamm and van Lambalgen, inspired by Moschovakis' view of 
    sense-as-algorithm and denotation-as-value.

    Finally, adverbs of quantification are re-considered, and conservativity 
    in generalized quantifiers is linked to presupposition filtering under 
    a propositions-as-types analysis.