Email Gateway (Aug 18 2022 at 15:55): Email Gateway (Aug 18 2022 at 15:55):From: Steve W <s.wong.731@gmail.com>
Hi all,
Does anyone know if there's any documentation on how the simplifier works?
It'd be good if it covers both the theoretical and implementation aspects.
I've tried tracing the ML code, but there are quite a few functions involved
and they aren't documented unfortunately.
Thanks,
Steve
Email Gateway (Aug 18 2022 at 15:56):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
At the Isabelle Developers Workshop in 2009
(http://tphols.in.tum.de/idw.html), Stefan Berghofer described the
basics of how one would go about (re)implementing the simplifier.
It's not a description of the theory, but the Isabelle theory file
(http://tphols.in.tum.de/IDW/Conversions.thy) provides a nice
description of conversionals and they can be composed to build up
something like the simplifier.
For some theory about rewriting, I like "Term Rewriting and All That" by
Baarder and Nipkow.
best,
lucas
Steve W wrote:
Email Gateway (Aug 18 2022 at 15:59):From: Makarius <makarius@sketis.net>
Chapter 9 of the old "ref" manual of Isabelle gives some explanations that
are not totally outdated.
Makarius
Last updated: Apr 18 2024 at 04:17 UTC