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.

Tobias

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 MHonArc.