Email Gateway (Aug 19 2022 at 16:10): Email Gateway (Aug 19 2022 at 16:10):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Florian,
Sure:
ML {*
Meson_Clausify.introduce_combinators_in_cterm @{cterm "%x::'a. Suc 0"}
*}
Jasmin
Email Gateway (Aug 19 2022 at 16:11):From: Tobias Nipkow <nipkow@in.tum.de>
I am scpetical about using combinators in practice. There was a time when
people thought that is a good idea, but I don't think aybody does it anymore.
I find it a bit worrying that lambda's should be a problem in code generation.
Tobias
Email Gateway (Aug 19 2022 at 16:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The combinators, if relevant at all, would only be introduced in the
outermost term to be evaluated and save considerable trusted code
there. Details still to be awaited…
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
in HOL, is there any conversion turning a term t into an equivalent t'
with all abstractions turned into expressions of combinatory logic? E.g.
comblogic_conv «%x. Suc 0» ~> «K (Suc 0)»
I dimly remember that metis and/or sledgehammer once used to have
something like this, and maybe it is still there somewhere.
The reason is that I collect some ideas how to implement a more robust
approach towards evaluation using code generation, and a preliminary is
that the terms to be evaluated are lambda-free. Hence such a conversion
would make a convenient preprocessor.
Thanks a lot,
Florian
signature.asc
Last updated: Apr 26 2024 at 08:19 UTC