Fwd: linear and non-linear terms

[Carl Pollard]

Hi Glyn,

>
> > Did Glyn and Bob argue for no vacuous abstraction in the syntax,
> > or in the semantics, or both? Evidently neither of them stuck with it.
> > I gather you are advocating relevance logic for the semantics?

Just to reassure you that I'm not hitting delete through all this.

I would say we argued for no vacuous abstraction 'in the semantics',
but because it was all tied up with compositionality, it was in the
syntax as well. This stuff was presented at LSI/ASL at Stanford
in 1987, but even before that Mark Steedman was saying that K
did not enter into the semantics of NL.
>>

Following Curry (knowingly or not I don't know).


>
I'm not sure how to take 'neither of them stuck with it', because I
never left off believing that we wanted multiple abstraction, but not
vacuous abstraction.  >>
>>

The context of my remark above was relevant logic, or (at the level
of proofs) lambda I-calculus. I just meant that if that's what you
were doing then, you must have decided to stop doing it and do
(extensions of)(noncommutative) linear logic instead. Do you
currently advovate relevant logic for the meaning type theory?

>
The problem is that I never got into non-naive models
of the lambda calculus, so you will always find me talking about
the monolithic set-based semantics and the language including
vacuous abstraction.
But I think it's great if people are thinking
about this again; in particular I'm looking for semantics of
lambdaI calculus, i.e. semantics of relevant proofs.
>>

As Howard pointed out, the Restall book dicusses (both algebraic and
categorical) models for the whole range of substructural logics.


Carl