Zulip Chat Archive

Stream: FoMM / Lean Together 2020

Topic: Term rewriting and PL theory


view this post on Zulip 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:)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 10 2020 at 18:38):

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

view this post on Zulip Johan Commelin (Jan 10 2020 at 18:39):

Discussions on Zulip are always a good idea (-;

view this post on Zulip 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?

view this post on Zulip Manuel Eberl (Jan 10 2020 at 21:07):

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

view this post on Zulip Harrison Grodin (Jan 10 2020 at 21:11):

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

view this post on Zulip 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.

view this post on Zulip 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