Yves Lafont (Université Aix-Marseille 2), Diagrammatic syntax for algebra


  • Feb. 27, 2012, 16:30 - 17:30


In algebra, rewriting is a model of symbolic computation: starting from a presentation by generators and relations, one tries to build a convergent rewrite system in order to compute normal forms. In proof theory, rewriting is a model of cut elimination, which corresponds to an execution of a proof (seen as a program). Those two approaches seem to be quite different, but there are similarities between them:

  • In both cases, people know use diagrams (or nets) rather than words or trees.
  • In both cases, people know use linear combinations (or formal sums) of such diagrams, which I call Σ-diagrams.

I will give an overview of rewriting techniques in those new frameworks.