Term rewriting and PL theory

Stream: FoMM / Lean Together 2020

[Harrison Grodin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Discussions on Zulip are always a good idea (-;

[Jeremy Avigad]

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]

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

[Harrison Grodin]

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

[Neil Strickland]

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

[Johan Commelin]

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