Email Gateway (Aug 19 2022 at 16:05): Email Gateway (Aug 19 2022 at 16:05):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
as part of an answer to a question on Stackoverflow
http://stackoverflow.com/questions/25622999/calculating-transitive-closures
I wrote my first simproc
I would be grateful for any comments by seasoned simproc writers.
And a more general question: Are methods (tactics, simprocs, ...) that
use "eval" in some way or another to be avoided? (I can't quite recall
whether "regexp" relies on "eval".)
cheers
chris
Email Gateway (Aug 19 2022 at 16:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
From my point of view, proof devices should never rely on the
(accidental) code setup at the time of their actual invocation but use a
fixed setup as present at their time of creation (»static evaluation«).
The tutorial on code generation gives some further hints.
The other question is indeed how much you want your proof procedure be
hardwired against code generation. I have no strict answer. NBE could
be an alternative to allow free variables also. The simplifier would
even be LCF-style. Depends on the kind and size of problems you want to
solve.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 16:20 UTC