Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
On Tue, 23 Oct 2012, Lawrence Paulson 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.
They found again some uses in relatively small-scale tinkering with
sub-term structure, things that would be hard with the Simplifier engine
and its builtin strategies. This is not so much compared to the
ancient times and past glory of LCF conversions.
What I found quite interesting was the presentation by Stefan Berghofer of
Isabelle conversions at the 2009 isabelle-dev workshop at Munich. He
first showed how to make a simplifier with a few conversions and
conversion combinators, then showed how to make it a little faster using a
"Boultonized" version of the same (like "Q" conversions in HOL), and then
showed how to make it really fast using the Isabelle Simplifier techniques
that came after conversions so many years ago.
This archive was generated by a fusion of
Pipermail (Mailman edition) and