Re: Lambda abstraction

Hi Charles,

from your answer I understand that I didn't manage at all to make 
myself clear. Let me try again; this time, I'm writing the email 
while listening to Arvo Part's Te Deum (by Kaljuste, of course), so 
I'm sure I'll be clearer.

1) I'm not proposing any term calculus: in fact, I'd be happy if 
partial sharing diagrams were used, you know I like them.

2) I'm just making an observation; in formalism A one has:

    a) `local' discharging of hypotheses, like in natural deduction;
    b) all the good proof theoretical properties of the sequent calculus.

So, if what I'm saying is true and there are no problems of different 
kind, I would expect that finding a term calculus for formalism A 
will be more productive than doing the same for CoS. Since the 
relation between A and CoS is simple, doing it for A would also mean 
doing it for CoS, and then for the logics which are better 
represented in CoS than in other formalisms.

Now onto some specific answers.

At 1:58 +0000 3.5.04, Charles Stewart wrote:
>>   We all know that in natural deduction we can make the deduction
>>   transformation
>>
>>                [A]
>>      A          |
>>      |   ~>     B    ,
>>      B        ------
>>               A -> B
>>
>>   which corresponds to forming the term
>>
>>      t   ~>   lambda x.t .
>
>Just a caveat with what you've written above: since you only have 
>one premiss, you get the monadic lambda calculus, which is not all 
>that expressive.

No, there are many premises, [A] is a parcel where possibly many of 
them are gathered and erased.

>Why do you say that hypothesis parcels are cumbersome?  I found them 
>very natural when I wrote my DPhil.

Because their canceling is obtained by a weird mechanism.

In the sequent calculus you can achieve the same effect by using 
(several instances of) identity, which is, how to say?, more 
`logical'. But, in the sequent calculus, you have to make a global 
transformation to a given derivation in order to put yourself into 
the condition of erasing hypotheses, what is not the case in natural 
deduction, nor in formalism A.

>What is formalism A?

It's like CoS, but you can compose derivations by using the same 
operators that you use for structures.

For example, you can put a derivation in OR with another one: this is 
morally equivalent to interleave any two derivations in the one-sided 
sequent calculus (in a trivial case by just adding a formula to every 
sequent in a derivation).

BUT, in formalism A you do the interleaving IMPLICITELY, it's a bit 
like having a proof net, and the consequence on the term calculus is 
that you don't need to transform terms associated to derivations in 
order to express the composition at term level.

See the parallel use of contraction in the example below.

>>                               A
>>                     =====================
>>      (A,A,A)        [ [-A,-A]   (A,A,A) ]
>>         |      ~>   [ ------- ,    |    ] ,
>>         B           [   -A         B    ]
>
>Not like my PSDs: contraction is strictly tied to two formulae at a time.

No, the contraction above is only between two formulae.

>>   1) the language of derivations is entirely sufficient and natural for
>>   expressing all the details of the transformation, contrary to natural
>>   deduction, and
>
>I don't see the point here.

Erasing hypotheses is performed by logical rules, not by crossing 
them out with the pencil. This might be important for working easily 
with these objects, apart from giving a possibly better insight on 
the term calculus, in my opinion.

>>   2) it does so without having to touch the initial derivation,
>>   contrary to the sequent calculus.
>
>Hmmm.

Hope this is clear from what I said above; if not, I'll try again, 
you choose the music.

I'd really be happy to see partial sharing diagrams as a term 
calculus for formalism A. Now, this will be something exotic to 
experience, so exotic we still don't have all the names for the 
things, like in Macondo.

-Alessio