Fwd: linear and non-linear terms

[Carl Pollard]

Hi Ash,

This stuff would be easier to talk about over a cup of coffee and a
nice pad of lined yellow paper, but let's see if we can reach a common
understanding of this stuff in this mode.

>
Well, I'm coming from the Glue perspective, where we really have:
semantics : proof terms : linear logic

The CH relates the linear logic to the proof terms: the proof terms
therefore have only linear lambdas and no vacuous abstraction. However,
you can have vacuous abstraction or nonlinear lambdas in the meaning
language, by which I mean the linguistic semantics, not the semantics of
the proof terms. I think this same distinction should be possible in
Type-Logical Grammar. Am I confused?
>>

Forget about glue and type-logical grammar for a second, and just
think of the meaning language. The usual setup is that you have a
bunch of basic semantic types (imagine, say, an intensional meaning
language with basic types Prop [propositions] and Ind [individual
concepts]), and then you get to freely generate more types using
whatever type constructors you have allowed yourself -- let's be
generous and give ourselves x as well as => so we can have ordered
pairs in the semantics and not always have to curry functions if we
don't want to. Then we have a type logic with x as conjunction and =>
as implication, with the types themselves being the formulas. For this
logic, the (term encodings of the) proofs are closed terms of the
meaning language. For example, the term Kim' is a proof of Ind and the
term walk'(Kim') is a proof of Prop.

What I just described is the Curry-Howard situation just at the level
of meaning.  At the level of glue, there is a DIFFERENT C-H situation,
which is the one you referred to. In Lambek calculus there is yet
another CH situation where the type logic is Lambek's calculus and the
proof terms are terms of the two-sided lambda calculus of Wansing
1992.

Now coming back to the semantics: usually the type logic there is just
the positive (i.e. conjunction-implication) fragment of ordinary
[i.e. with weakening, contraction, and exchange] intuitionistic
propositional logic, and the corresponding language of proof terms is
just the familiar simply typed lambda calculus. I think what Howard is
proposing is essentially that, no, the type system for the semantics
is not ordinary intuitionistic logic but rather relevant logic
(discarding the structural rule of weakening). In that case the
language of proof terms (which is just the meaning language) is not
the usual lambda calculus but rather the lambda I-calculus, which
disallows vacuous lambda abstraction. Is that the gist of it, Howard?

>
I actually need vacuous abstraction in the meaning langauge in the
theory of resumption that I'm working on for my thesis (at least I'm
pretty sure I need it, but the thesis is still in progress).

I'm thinking about resumptive pronouns in the context of
resource-sensitivity. These pronouns are contributing an extraneous
resource. Their distribution I argue is conditioned by
lexically-contributed "manage resources" that basically dispose of a
pronominal resource. These not only occur in "traditional" resumptive
pronoun cases, but also in finite control (e.g. Balkan-style) and copy
raising. When the manager resource disposes of the pronoun's resource, it
also disposes of its meaning: the manager resource vacuously abstracts
over the pronouns meaning, so the end result is that it disappears from
the semantics.
>>

I think the resource metaphor is getting in the way of my understanding
this. Can you say it another way?

Carl