## Stream: general

### Topic: Term rewriting and PL theory

#### Harrison Grodin (Jan 10 2020 at 19:31):

Following up on this thread (here, as per recommendation):

I've been thinking about formalizing fundamentals of term rewriting (e.g. lemmas about equivalence of various notions of confluence, proof techniques for termination/confluence, completion procedures, etc. - formalizations of Term Rewriting and All That, Advanced Topics in Term Rewriting) and PL theory (definitions of statics/dynamics for common languages, safety proofs, and related utilities), especially based on the recent discussions. Would this be useful to people?

If I were to take a stab at this, what would be the recommended way to develop? Should I build in an independent GitHub repo and discuss on Zulip? Does it make sense in mathlib (i.e. creating src/pl_theory, src/rewriting), and if so, are there any guidelines about structure? (Apologies if I'm missing something - don't have much experience contributing to Lean projects yet. :slight_smile:)

Does anyone have thoughts on this?

#### Rob Lewis (Jan 10 2020 at 19:33):

I'd have no objections to putting this in mathlib.

#### Simon Cruanes (Jan 10 2020 at 19:34):

would it be inspired from http://color.inria.fr/ ?

#### Rob Lewis (Jan 10 2020 at 19:35):

There's no need to decide on a directory structure up front. If you start with a reasonable directory for whatever the first targets are, we can always move/refactor things as the theory grows.

#### Rob Lewis (Jan 10 2020 at 19:35):

Even a general src/cs_theory directory might make sense.

#### Harrison Grodin (Jan 10 2020 at 19:39):

would it be inspired from http://color.inria.fr/ ?

I'm not familiar with this; seems like it might be worth drawing from at first glance. My overall idea was to begin by formalizing some definitions/theorems from Term Rewriting and All That, the canonical fundamental source for the subject.

#### Gabriel Ebner (Jan 10 2020 at 20:21):

Another prominent formalization of term rewriting is the isafor library (http://cl-informatik.uibk.ac.at/software/ceta/).

#### Agnishom Chattopadhyay (Jan 12 2020 at 05:11):

I know plenty of purely mathematical applications for confluent rewriting.

I am curious what they could be

#### Neil Strickland (Jan 12 2020 at 07:42):

For example, small cancellation theory for understanding the structure of groups given by generators and relations, such as the fundamental group of a closed surface. Or algebras given by generators and relations, such as the Steenrod algebra.

Last updated: May 14 2021 at 04:22 UTC