Account Options

  1. Sign in
The old Google Groups will be going away soon, but your browser is incompatible with the new version.
Google Groups Home
« Groups Home
fa.isabelle
+ new post
About this group
Subscribe to this group
This is a Usenet group - learn more
Message from discussion BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
 
From:
To:
Cc:
Followup To:
Add Cc | Add Followup-to | Edit Subject
Subject:
Validation:
For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon. Listen and type the numbers you hear
 
Lawrence Paulson  
View profile  
 More options Oct 23 2012, 10:19 am
Newsgroups: fa.isabelle
From: Lawrence Paulson <l...@cam.ac.uk>
Date: Tue, 23 Oct 2012 14:19:58 UTC
Local: Tues, Oct 23 2012 10:19 am
Subject: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
Print | View thread | Show original | Report this message | Find messages by this author
That application is very interesting! And one can argue that a simproc is a very similar concept as a conversion, anyway.

Larry

On 23 Oct 2012, at 14:41, Brian Huffman <huff...@in.tum.de> wrote:

> On Tue, Oct 23, 2012 at 3:21 PM, Lawrence Paulson <l...@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


 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Create a group - Google Groups - Google Home - Terms of Service - Privacy Policy
©2013 Google