Re: Lambda abstraction

Hi,

>  for several reasons (Elaine and intersection types, Kai and
>  intuitionistic logic, etc.), we got to the point in which we should
>  ask ourselves questions about term calculi related to deep inference
>  formalisms.

>  I just noticed a trivial fact, I don't know whether it might be
>  important or not.

>  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 .

>  There are a few cumbersome technicalities one has to deal with, like
>  discharging hypothesis and taking care of `parcels' of them, which
>  means using some care in variable bindings, etc.

Yep, I've thought quite a bit about these issues; they are one of the
driving forces behind the design of my partial sharing diagrams.  At
the risk of blowing my own trumpet, I think that if you care about these
sorts of issues, you should look at what I've done there.

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.  If you start adding combinators to get the power, then
everything works again: if you add the axioms of minimal logic, then you
get Curry's combinatory logic or if you add categorical combinators you
get the system described in Lambek and Scott, or ... you get the general
idea, I hope.

>  In this case, one can argue that the typed lambda calculus notation
>  is superior to the natural deduction one because the lambda term is
>  more precise, for example the names of variables are enough for
>  taking care of parcels of hypothesis and which of them are
>  discharged, what is instead cumbersome in natural deduction notation.

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

>  The situation is worse in the sequent calculus: if you want to
>  express a `->' introduction with discharging of hypotheses you have
>  to perform a global transformation of the proof in which you add
>  hypothesis A everywhere, and you only use it in some axioms
>  somewhere. Terrible from the point of view of making the relation to
>  a term calculus.

Yes, although the classical case turns out to be easier that the
intuitionistic case, hence innovations like the various symmetric
lambda- and lambda-mu- calculi out there.  I'll sell my own work
here again: I did a paper with a confluent rewriting mechanism with
a reasonably simple relationship (in the sense of trasnlating back and
forth doing something OK) to the sequent calculus, and which has the
usual notion of analytic form.

>  Instead, and this is the observation, I noticed that if you use
>  formalism `A', the whole thing becomes natural, so possibly
>  convenient in view of the search for a term calculus.

What is formalism A?  CoS with the liberal quotienting equations?

>  The same transformation as above simply becomes:
>
>                  t
>              ----------
>     A        [      A ]
>     |   ~>   [ -A , | ] ,
>     B        [      B ]

>  in the case there is only one hypothesis A. Notice that in formalism
>  `A' the conclusion of the derivation on the right is [-A,B].

OK, looks a bit like my PSDs so far.  Do you recall all the systems
for bundling up groups of formulae onto a wire?

>  In the case there are, say, three hypotheses A, two of which in the
>  parcel, one uses contraction on -A and explicitly kills those that
>  are in the parcel; for example:

>                              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.

>  What is, I believe, important here:

>  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.

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

Hmmm.

>  You see that what is crucial is being able to put the `hypothesis
>  killer' in parallel to an entire derivation, what is possible in
>  formalism `A' and impossible in CoS, sequent calculus, natural
>  deduction, etc.

...and possible in partial sharing diagrams, which have something of
a worked out relationship to both regular CoS (Formalism B?) and
Lampings sharing graphs.

>  I think this should be useful for designing a term
>  calculus.

Why reinvent the wheel?  Why not use my PSDs?  An advantage of doing
so is that they have a nice relationship to all the hard work that
Yves Lafont has done with his Circuit Algebras.

>  I've put the description of formalism `A' as a note on the web:
>  <http://www.ki.inf.tu-dresden.de/~guglielm/res/notes/AG11.pdf>.

I'll look carefully at this, if you look carefully at my PSDs...

Charles