Fwd: linear and non-linear terms

[Carl Pollard]

Hi Jonathan,

>
Another perspective on the issue of vacuous/multiple abstraction---in
Ivan Sag's and my book _Interrogative Investigations_ we treat
questions as propositional abstracts.  We use abstraction over sets,
which can be empty, singleton, or multiple.  This makes for simplicity
in two respects: answerhood can be characterized uniformly and
similarly retrieval/binding across all interogative construction
types, incl polar interrogatives.

Polar questions come out as 0-ary abstracts (crucially distinct from
propositions) and we derive some fairly interesting results by having our
schemas generalize to the vacuous abstraction case (e.g. "intonation
questions" are an instance of a construction type for wh-in-situ, which
arises by abstracting over no parameters, whereas cases like A: Who left?
B: Who left?  [=Are you asking who left?]  are an instance of a
construction type for echo questions, which arises by abstracting over no
parameters.)
>>

This is similar to the treatment in the simply typed lambda calculus
(with ordinary intuitionistic propositional logic as the type theory)
as long as as you follow Lawvere, Lambek etc. (not Church, Henkin,
Montague etc.) in allowing finite cartesian products (including
crucially the unit type 1 (= null cartesian product)). In that case,
if \phi is a closed term of type P (that is, a proposition), then the
corresponding null abstract is

   \lambda x \phi

where x is a variable of type 1. This is a closed term of type
1 => P. Of course P and 1 => P are isomorphic, with the iso |.| from
P to 1 => P being

   \lambda y. \lambda x y

i.e. |\phi| = \lambda x \phi

That is, the polar question |\phi| is the Lawvere name of the
proposition \phi. Here's the curry-eval diagram:


            1 x 1
            |    \
            |     \ \pi'
            |      \
            |       _|         N.B. \pi' is the second projection and
id x |\phi| |         1
  1         |          \       |\phi| =    curry(\phi o \pi')
            |           \ \phi         def
            |            \
           \|/            _|
      1 x (1 => P) -------> P
                   eval

>
The abstraction Ivan and I use is admittedly a somewhat non-orthodox
version (it is essentially the simultaneous abstraction operator
axiomatized in Seligman and Moss' _Situation Theory_ paper in the
Handbook of Logic and Language.), but Robin Cooper has recently showed
me how this can be recast in Martin L\"of Type Theory
>>

That stands to reason. Martin L\"of type theory can be viewed as an
extension of the simple theory of types where the types can have term
parameters, which can be existentially or universally quantified
over. (Roughly speaking that means the formulas-as-types logic is
first-order instead of propositional.) So the treatment of polar
questions I just mentioned can be done in ML type theory too. But this
in no way depends on the additional strength of ML type theory
(viz. dependent types).

But maybe you are referring to a different construction?

>
(a preliminary
version is in an appendix to our paper from this year's Edilog,
`Clarification Ellipsis in Dependent Type Theory'.).
>>

Sorry, what is Edilog? I'd like to look at this.

All best,

Carl