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

paper annoucement



I recently obtained a geometrical interpretation of the provability
of multiplicative formulas in linear logic, based on a previous
homological approach of proofnets, as explained in the paper: 

     "VOLUME OF MULTIPLICATIVE FORMULAS AND PROVABILITY"

It can be obtained by anonymous ftp at frege.logique.jussieu.fr
Look for vmfp.dvi.Z in pub/scratch.
Here follows an introduction to the paper. Questions and comments are 
mostly welcome.

Best regards, 

Francois Metayer 

-----------------------------------------------------------                   

A module is a (possibly incorrect) proof-structure M together
with a set F of vertices of M, which we call the border
of M. Some extra conditions are required in the precise definition.
A typical example is the graph associated to a multiplicative formula,
with the set of vertices indexed by atomic subformulas
as border. Now the decision problem for multiplicative
formulas is a particular instance of the following question:

Is it possible to paste two given modules along their common
border such that the resulting graph becomes a proof-net?

This paper introduces a correspondance between modules with a given
border and subspaces of an euclidian space, in
such a way that the correct pasting of two modules M1 and
M2 along their common border can be expressed by an equation

                 a(X1,X2*)=k                (E)

Here Xi denotes the subspace associated with Mi, a is
a geometrical  invariant of a pair of subspaces, and k
is a constant depending on M1 and M2 as separate modules,
not on the way they are pasted together.

Since this interpretation stems from the homological correctness
criterion we introduced in a previous work (homology of proof-nets[HPN]), 
we first recall the main definitions and results of [HPN].

A paired-graph (pg) is a graph G with a set P=P(G) of mutually disjoint
pairs of adjacent edges. 
The motivation for considering this notion is that proof-structures
in multiplicative linear logic can be seen as pg's,
where pairs correspond to par-links.

Abstract proof-nets can be defined in this setting: given two pg's
G1, G2, with respective vertices v1, v2, we denote by
t(G1,G2,v1,v2) the graph obtained by pasting together G1 and G2
at v1, v2. Likewise, given G with distinct vertices u, v, 
p(G,u,v) denotes the graph obtained by adjoining a new vertex
w and a new pair {uw,vw}. Then the smallest class of pg's containing trees 
(connected, acyclic graphs, without pairs), and closed by t and p is the
class of proofnets.

The starting point of [HPN] is the following remark: a paired-graph G,
just like an ordinary one, gives rise to a complex of
abelian groups:

              0-->C1(G)-->C0(G)-->Z-->0         (C)

where C0(G) is the free abelian group generated by the vertices of
G and C1(G) is the subgroup of the f.a.g on the edges, generated by
(1) the elements e+e*, where {e,e*} runs over P(G) and (2) the remaining
edges (i.e not belonging to a pair). The non-trivial arrows
are the restriction to C1(G) of the boundary morphism given by
d(uv)=v-u and the augmentation morphism defined by e(u)=1 on vertices.
Since ed=0, (C) determines homology groups

H1(G)=ker(d) and H0(G)=ker(e)/im(d).

The relevance of this homology lies in the fact that it
characterizes proof-nets among arbitrary paired-graphs, as
shown by the main result of [HPN]:

Theorem: G is a proofnet if and only if H1(G)=0 and
card(H0(G))=2^p, where p is the number of pairs.


It should be pointed out that, for each graph G, not
necessarily a proof-net, satisfying H1(G)=0 and H0(G) finite,
the cardinal of the latter cannot be greater than 2^card(P(G)). 

Finally, the above theorem gives a correctness condition
for the pasting of two modules. This can be expressed by the equation (E),
if we consider the homology group H0(F) of the common border
as a discrete subgroup of the euclidian space.