Fwd: linear and non-linear terms

[Carl Pollard]

Hi Ash,

>
In particular, this reveals that the issue is not vacuous abstraction in
the *meaning language* or linguistic semantics, just in the proof terms.
>>

That's not quite right. In a type-theoretic semantics, you have a
propositional logic whose formulas are the semantic types, and the
proof terms are PRECISELY the terms of the typed lambda calculus
(= the meaning language). This is the Curry-Howard perspective
applied strictly to the semantic domain. So if you had a relevant
semantic type theory your meaning language would not have vacuous
abstraction.

>
The reason I got alarmed and came across like a jerk in the message below
is that 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).
>>

Can you say briefly why that is?


Carl