Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue



On Tue, Oct 23, 2012 at 3:21 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> As a historical remark, I'm quite attached to conversions, which were the topic of my very first journal article:
>
> L. C. Paulson.
> A higher-order implementation of rewriting. Science of Computer Programming 3 (1983), 119–149.
>
> They made a lot of sense in the context of LCF and HOL, where users routinely wrote code as part of the verification process. Although I included this code in Isabelle, it didn't have a central role and I thought it'd got deleted. Obviously it would be sensible to correct any deficiencies or omissions. But I'm still intrigued regarding what sort of application you could have for them.
>
> Larry

I can't speak for Peter, but I am currently using conversions in a few places.

My main application is for writing simprocs: See e.g.
HOL/Tools/group_cancel.ML or nat_arith.ML. Rewriting these
cancellation simprocs to use conversions made the code significantly
shorter, simpler, more efficient, and more reliable. There used to be
a few simprocs that would sometimes return an equation whose
left-hand-side did not match the input term; using conversions ensures
that this will not happen.

I would definitely recommend conversions to anyone thinking about
writing a simproc.

I am also using conversions inside the transfer package, to do some
preprocessing steps. For this purpose, conversions are more
predictable and more customizable than using the simplifier.

- Brian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.