SKS church booleans Part 2: atomic flows
The previous post didn't arrive to conclusion as computation caused the proofs to grow beyond manageable. Classical propositional logic appears to have a laborious cut elimination but it is not as bad as it seems. Deep inference proofs can be rewritten into atomic flows and we can complete our study this way.
I'm going to apply rules described in Alessio Guglielmi's & Tom Gundersen's paper "Normalisation Control in Deep Inference via Atomic Flows" (arXiv pdf).
The 'bc', and 'ex' reductions from the paper are not used here. I did not understand them well enough at the time of writing this post.
These are the same proofs as before, just represented with atomic flows.
I resorted to using the refined proof for 'and', which was also representable in typed lambda calculus.
These atomic flows are in their normal forms.
Next we are going to see how these proofs normalise when we compose them. We do the task in two parts for the clauses "and true true" and "and false true".
The series of abstractions and cuts leave a wriggled line after them. I assume it would be safe to erase that wriggle there, for now it's better to assume it has some meaning.
These two pictures differ by where the weakening goes. The weakening in the "and true" annihilates with the contraction.
Observing at the flows it's clear that the 'false' directs the weakening to the output of the second argument.
Aside the wriggle here, everything would seem to match.
Note the 'and false' already set the stage, like it should do. It suggests that this system can indeed compute a truth table for 'and'. Well, if we get rid of the wriggles.
Peculiarities
There are plenty of peculiarities in here. They appear due to the symmetry in the rules.
If we invert our boolean representations, we get inverse versions of our booleans. Practically they behave and normalise the same way as the normal booleans but they are just upside down.
Aside "true" and "false" -proofs, I'm also able to construct an atomic flow which contracts the output atom and interacts with the both inputs. I think it's an interesting construct but I'm not sure what it is.
It also suggests that there could be a simpler way to represent booleans with this system. For example. single 'interaction' as "true" and two 'weakenings' as "false".
Occurrence of commutative contraction rule
The following rule appears in Lamping's algorithm for optimal lambda calculus reduction, and in symmetric interaction combinators.
The other two systems also has an annihilative version of this contraction rule, which is used when the flavor of contraction and co-contraction match.
This is a slight concern because it seems to be those properties that define the whole system, and it quite seem to give additional meaning for the whole contraction and co-contraction beyond it being just copying of atomic terms.
Cycle elimination
When different proofs are connected there appear cyclic atomic flows which seem to be the only rules that require effort and cannot be removed with local reduction rules such as those presented above.
This is the part that appears to match with the cut elimination we attempted the previous time.
The problem is that the rule involves copying everything that ends up between the cycle and a simple edge.
The paper "Removing Cycles from Proofs" is in my reading list.
Conclusion and thoughts
The computation possibilities present here seem to correspond to that of lambda calculus with some peculiarities. It is possible that the inversion matches with the game-theoretic idea of presenting logical formulas as games between two players. That way it might allow us to introduce computability logic into the mix.
It would seem like an easy task to implement an evaluator for atomic flows. Detecting cycles and copying proofs seem expensive operations and I hope there are some nice ways to work around this problem.
Next it's time to look into uniform proofs in deep inference.