Abstract: |
Can we view natural languages as programming languages fit for
computers? This talks looks at 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 labeled `dynamic semantics' (DS), and investigations into
what Terry Parsons calls `sub-atomic semantics' (SS), delving into,
for example, verbs. DS has a proof-theoretic formulation (detailed by
Aarne 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. Nor does time or change (often crucial to the
information conveyed by a verb) receive any special treatment under
`propositions-as-types.'
With an eye to SS, we push systems of typed-lambda calculi/functional
programming down to finite-state machines, formulating an event-type
as a regular regular language. The strings in such a language are
sequences of observations (much like comics and movies) that for an
event-type given by a discrete temporal logic formula can be viewed
not only as events but also as proofs.
|