Re: (Frogs) Calculus of Structures and substructura

[re-sending, I still had the old list address -Kai]

Arno,

you're in a weaker logic, but let me tell you anyway what happens in
intuitionistic logic, maybe it also applies in your case. The rules of
the form

A ^ (A -> B)
----------------(app, or eval, or counit)
      B

are easily decomposed into CoS-style i-up and switch rules as

A ^ (A -> B)
----------------switch
(A -> A) -> B
-----------------i-up
 top -> B
---------------=
       B

where switch is the familiar

A ^ (B -> C)
-----------------
(A -> B) -> C

which is an instance, modulo units, of

(A -> B) ^ ( C -> D)
-------------------------- switch a la Alessio's recipe.
(B -> C) -> (A -> D)

You can imagine the i-up-rule, it's restricted to negative contexts.

Now I don't know which of your implications make these rules sound and
whether they together form a complete system for your logic. For
intuitionistic logic they do.

Why didn't we do this in our paper "An algorithmic interpretation..."?

The reason we chose app-style rules was to stay as simple and as close
to lambda calculus as possible. These inference rules already allow
for proof reductions which are more fine-grained than what people
typically have in explicit substitution calculi, let alone lambda
calculus. Making things even more fine-grained, by decomposing app
into i-up+switch+unit, is undoubtedly interesting, but will also turn
a system with (essentially) four inference rules and eight reduction
rules into a system with eight inference rules and probably something
like fifteen reduction rules.

-Kai