Fwd: linear and non-linear terms

[Glyn Morrill]

Hi Howard, Carl, Ash and All,

>
> Hi Carl,
>
> Many thanks for your message. Just a few comments - I will write again later.
>
> > Good to hear from you, and look forward to reading your papers.
> > 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. 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 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.

All those years ago a friend wrote me a poem which began:

	"Shall I compare thee to a lambda K ..."

:-)

-- Glyn