[Prev][Next][Index][Thread]

Re: Proof Nets and Lambda Terms

Date: Wed, 25 Mar 92 13:08:10 EST
To: linear@cs.stanford.edu

  This is in regards to G. Bellin's recent note on proof nets and
equivalence classes of linear lambda terms. I believe that my recent
work relating proof nets and coherence is relevant to his result.
  
  The question of coherence arose originally in algebraic topology.
Basically, coherence amounts to determining which diagrams commute in
categories with certain additional structure. Typically, this
structure is a tensor product and implication (as in intuitionistic linear
logic), or a tensor product and a dualizing functor (as in classical
linear logic). Examples of such categories are numerous in algebraic
topology and homological algebra. 

  It was the fundamental observation of J. Lambek that logical
principles could be used to approach this problem. The idea is to view
the morphisms which comprise the diagram as deductions in a deductive
system, under a process analogous to the Curry-Howard isomorphism.
Then coherence reduces to determining the equivalence relation of the
corresponding deductive system. Given this interpretation, logical
methods, most notably cut-elimination, can be put to use. This
approach has yielded a great many results. (Please see the references
in my paper.)

  Since multiplicative linear logic can be viewed as a logic about
tensor categories, it was hoped that proof nets could be used to
provide better coherence results. There is a straightforward
translation procedure, which assigns a proof net to a morphism in an 
autonomous (tensor, implication) or *-autonomous (tensor, duality) category. 

Some of the results relating proof nets to coherence are:

1) In their '72 paper, Kelly and Mac Lane introduced the notion of 
``graph''. Graphs are used to classify which diagrams commute, i.e. 
which deductions are equivalent. Under the proof net interpretation,
they are seen to correspond exactly to the axiom links. 

2) The confluent cut elimination procedure for proof nets preserves
equivalence in the corresponding deductive system. The resulting cut
free net corresponds to a normal form of the deduction, analogous to a
normalized lambda term. From this, deriving coherence is
straightforward. 

3) The Danos-Regnier acyclicity condition corresponds to another
notion in the Kelly-Mac Lane paper, compatibility of graphs. Please see
my paper for the definition.

  These results are contained in my paper ``Linear Logic, Coherence and
Dinaturality'' which has been accepted at TCS. Unfortunately, I can't
put it on FTP, since there are a number of drawn diagrams. (TeXing
proof nets was beyond me) If anyone would like a copy, they could send
me their (ordinary) mail address and I will send it along. A short
version of this work appeared in SLNCS 530.

  Also relevant is recent work of Barry Jay, Journal of Pure and 
Applied Algebra Volumes 59 and 66. In these, he develops a lambda 
calculus for monoidal and monoidal closed categories. 


Rick Blute