## Stream: FoMM / Lean Together 2020

### Topic: Term rewriting and PL theory

#### Harrison Grodin (Jan 10 2020 at 18:27):

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:)

#### Johan Commelin (Jan 10 2020 at 18:38):

I don't know if it fits into mathlib. @Mario Carneiro would be the best person to answer that question.

#### Johan Commelin (Jan 10 2020 at 18:38):

You could certainly start a new package, add mathlib as dependency, and get started.

#### Johan Commelin (Jan 10 2020 at 18:39):

Discussions on Zulip are always a good idea (-;

#### Jeremy Avigad (Jan 10 2020 at 19:24):

Mario has in the past complained about the name mathlib, on the grounds that it should be a library good for e.g. program verification as well. Rewriting is pretty fundamental, and I'd personally be happy to see a library for it inside of mathlib.

But is everyone subscribed to this stream? Maybe the question would do better in general or new members?

#### Manuel Eberl (Jan 10 2020 at 21:07):

Do you know about IsaFoR? http://cl-informatik.uibk.ac.at/isafor/

#### Harrison Grodin (Jan 10 2020 at 21:11):

No, I wasn't aware - this seems quite good.

#### Neil Strickland (Jan 11 2020 at 15:32):

I know plenty of purely mathematical applications for confluent rewriting. I would be very happy to see this in mathlib.

#### Johan Commelin (Jan 11 2020 at 15:52):

Note that this thread was continued in the general stream: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Term.20rewriting.20and.20PL.20theory/near/185342815

Last updated: May 18 2021 at 09:14 UTC