[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: RELITERS

On Sat, Jan 20, 2001 at 10:11:00PM +0100, Andrzej Trybulec wrote:
> 
> Piotr Rudnicki wrote:
> 
> > ...
> > It only indicates that a utility which actually removes superflous
> > steps in iterative equalities is needed.
> >
> 
> What strategy do you propose?
> 
> Let us look to an example (I have substitued  *  for d249):
> 
> Lm10:
>  2 to_power 4 = 16
> proof
>  thus 2 to_power 4 = 2 to_power (2+2)
>                   .= (2 to_power 2)*(2 to_power 2) by POWER:32
> ::>                                                 *746
>                   .= 4*4 by Lm8
> ::>                       *746
>                   .= 16;
>  thus thesis;
> end;
> 
> One may remove the second step or the third one, but not both. In general if we
> got consecutive errors we
> may remove odd steps or even steps, but maybe something a bit smarter may be
> used (removing steps wiht biggest terms?).

I do not know about biggest terms but if we remove every second step and
then recursively run RELITER we may save even more.

> On the other hand the lemma should be written as:
> 
> Lm10:
>  2 to_power (2+2) = 4*4 by Lm8,POWER:32;
> 
> So it is btter to correct the text by hand.

Sure - but where to find the hand: do not count on mine.

The problem is interesting as it involves only equality of terms and
I am sure that in the rewriting literature there will be plenty to
learn from.

Best,

-- 
Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr