Re: [isabelle] (no subject)



John, Matt:

The HOL-4 simplifier, which is similar to the one in Isabelle, just picks one of the matching congruence rules. No backtracking. In the mid-90's I met Andrew Martin (at Oxford) who wanted to make the Isabelle-style simplifier a back-tracking one.
Not sure if he ever implemented it ... googling ...

http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/ tactics.pdf

Hmm ... this has a whisper about backtracking and rewriting, but is mostly about tactic algebra and monads. Also, I think I recall Amy Felty having a backtracking rewriter. However I don't remember if her work dealt with congruence rules. I think it didn't, having mostly to do with higher order rewriting where there could be multiple
matches on a single rewrite rule and you might like to backtrack through
the different substitutions. Backtracking during rewriting seems a nightmare, on both efficiency and understandability grounds, but maybe you have evidence to the contrary?

Konrad.

On Mar 1, 2006, at 2:11 PM, John Matthews wrote:

Hi all,

Matt Kaufmann and I are interested in how Isabelle's simplifier handles the case where there are multiple congruence rules that match a particular subterm. Does it try all the rules in some order, or does it just pick one?

Thanks,
-john






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