Guiraud on Higher-Dimensional Rewrite Rules
Posted by John Baez
In this quarter’s last class on Classical versus Quantum Computation, I hinted that one could use 3-dimensional structures to understand the process of computation. A key figure in this line of work is Yves Guiraud, and he just put some of his papers on this topic on the arXiv:
- Yves Guiraud, Termination orders for 3-dimensional rewriting, Journal of Pure and Applied Algebra 207 (2006), 341-371.
- Yves Guiraud, Termination orders for 3-polygraphs, Comptes-Rendus de l’Academie des Sciences Serie I, 342 (2006), 219-222.
- Yves Guiraud, Two polygraphic presentations of Petri nets, Theoretical Computer Science 360 (2006), 124-146.
- Yves Guiraud, The three dimensions of proofs, Annals of Pure and Applied Logic 141 (2006), 266-295.
Re: Guiraud on Higher-Dimensional Rewrite Rules
Thank you John for making some publicity for my work! Maybe I should explain a bit what this figure represents for people that do not want to bother reading the full paper. A preliminary remark: the correct figure is there. Since it is hardly readable without being able to turn around or make slices, the one John has chosen is better for explanations.
This figure represents a step-by-step computation on some kind of boolean circuits. For example, the one we see on the foreground computes the formula ((a and b) or (a and b)). The computation is built from axioms of the form (P implies Q), applied in some context. Here, each axiom used is pictured as a big 3D block transforming P into Q and leaving what remains unchanged. The computations are 3-dimensional because the objects on which they act live in a 2-category.
This is exactly the same idea as the last figure of this chapter of Classical versus Quantum Computation. The only difference is that I have chosen to emphasize the computations. If someone wants to see more of these 3-dimensional computations, there are some at the bottom of my research page. I would welcome any comments on all this stuff and answer any question on the subject (or at least try to!).