Yves Lafont (Université Aix-Marseille 2), Diagrammatic syntax for algebra
Schedule
- Feb. 27, 2012, 16:30 - 17:30
Abstract
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.
Attachments
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.