Atomic flows

Hello,

Tom and I rewrote the paper on atomic flows, which has been accepted by LMCS.

Please, throw away the old version of that paper. 
There were no mistakes, but, thanks to the 
referees and those who read the old paper, 
especially Michel, this new version is much 
simpler and much better in almost every aspect. 
The only exception is that there is now a 
definition of atomic flow.

We plan to follow up this paper with another one 
where we will explore in much more detail the 
global transformations based on atomic flows. In 
particular, we obtain very simple cut elimination 
and interpolation procedures, and the 
streamlining procedure will be much more tightly 
determined by the topological structure of atomic 
flows.

I am now convinced of the truth and usefulness of the following slogan:

   bureaucracy-free proof system =
   CoS with inference rules on derivations =
   Formalism B =
   atomic flows + logical relations.

So, I think that atomic flows give us yet another 
perspective on which to base the design of a 
bureaucracy-free proof system of lasting value.

Please, keep the comments coming.

Ciao,

-Alessio


Normalisation Control in Deep Inference via Atomic Flows
Alessio Guglielmi and Tom Gundersen

We introduce `atomic flows´: they are graphs 
obtained from derivations by tracing atom 
occurrences and forgetting the logical structure. 
We study simple manipulations of atomic flows 
that correspond to complex reductions on 
derivations. This allows us to prove, for 
propositional logic, a new and very general 
normalisation theorem, which contains cut 
elimination as a special case. We operate in deep 
inference, which is more general than other 
syntactic paradigms, and where normalisation is 
more difficult to control. We argue that atomic 
flows are a significant technical advance for 
normalisation theory, because 1) the technique 
they support is largely independent of syntax; 2) 
indeed, it is largely independent of logical 
inference rules; 3) they constitute a powerful 
geometric formalism, which is more intuitive than 
syntax.

<http://cs.bath.ac.uk/ag/p/NormContrDIAtFl.pdf>