Subject: Atomic flows
Newsgroups: gmane.science.mathematics.frogs
Date: 2008-02-25 10:38:56 GMT (10 weeks, 6 days, 16 hours and 20 minutes ago)
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>