Term rewriting and PL theory

Stream: general

[Harrison Grodin]

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]

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

[Simon Cruanes]

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

[Rob Lewis]

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]

Even a general src/cs_theory directory might make sense.

[Harrison Grodin]

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]

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

[Agnishom Chattopadhyay]

I know plenty of purely mathematical applications for confluent rewriting.

I am curious what they could be

[Neil Strickland]

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.