Re: [isabelle] Conversion for translation into combinatory logic?
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.
On 02/10/2014 17:59, Florian Haftmann wrote:
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and