[metis-users] rewrite structure in Metis

[James Bridge]

Thanks Joe.

I'll need to think about your idea - it is nearly midnight here so I'm not 
thinking all that clearly. One issue with saving structures and adding new 
clauses of the appropriate type is that it gets rather complicated when 
there are multiple split points. (Backtracking may occur at any split 
point, with lower split points being simply deleted, so all split points 
would need to have their rewrite structures saved and updated in parallel.)

Anyway, you've highlighted why my rather naive approach can run into 
trouble, which is useful, thankyou.

James



On Apr 7 2011, Joe Hurd wrote:

>Hi James,
>
>> In general, the problem with backtracking is that most Metis structures 
>> are well set up to accept new clauses but are much less happy about 
>> giving them back again! (This is not a criticism of Metis, I think most 
>> theorem provers are written in the same way.)
>
>I think you have put your finger on the root of the problem here, and
>I can illustrate why this is in a simple example.
>
>Suppose the rewrite set contains one equation
>
>{ a = b }
>
>and down one branch of a split the same equation happens to be added
>(which I will mark with a *):
>
>{ a = b, a =* b }
>
>During inter-reduction it might be the case that the original equation
>is rewritten:
>
>{ b = b,  a =* b }
>
>which would then get thrown out as a useless instance of reflexivity:
>
>{ a =* b }
>
>If you attempted to modify this rewrite set when going down the other
>branch you would be left with the empty set of rewrites
>
>{ }
>
>which is incomplete.
>
>This is a simple example which would probably not appear in practice
>because the second equation would be simplified before it could be
>added to the rewrite set and inter-reduced, but it is illustrative of
>a class of problems deriving from an attempt to delete rewrites after
>they have affected the state in hard-to-undo ways.
>
>One solution to this is save the original rewrite set at the split
>point, and then add extra equations that have been derived down one
>branch that do not depend on the split. Then you're only adding
>equations but obtaining the benefit of the extra equations that do not
>depend on the split.
>
>Does this strategy work in your use-case?
>
>Cheers,
>
>Joe
>