[Agda] Ringsolver seems ok, but how to get NF?

[Christoph HERRMANN]

Hi Nils,

the aim to let (Normal n p) appear in the type signature of
particular functions is  to have a certificate that the object 
is really  semantically equivalent to p. Maybe we can have 
something like (Normal n (normalised n p)) with *normalised*
being a function (instead of a constructor) and a proof connected
with the definition of *normalised* that (normalised n p) is 
semantically equivalent to p. This would be convincing enough I 
believe. Is this what you mean by deannotation?

Cheers
--
 Christoph

On 22 Aug 2010, at 10:13, Nils Anders Danielsson wrote:

> On 2010-08-20 16:54, Christoph HERRMANN wrote:
>> I want to use natural numbers expressed as arithmetic expressions
>> with unknown variables as type indices.
>> 
>> [...]
>> 
>> What is the problem in adding a function to the RingSolver which
>> delivers a normal form, i.e.,not only a polynomial but also with
>> a unique ordering of the products?
> 
> The function normalise does deliver a normal form:
> 
>   normalise : ∀ {n} (p : Polynomial n) → Normal n p
> 
> The result of normalise p is a normal form /which is equivalent to p/.
> 
> I suspect that the "p" argument to Normal gets in your way, though, and
> the proof components which are part of the normal form mean that normal
> forms are not unique. You may be better off with an unannotated normal
> form. Defining a new type and a function which deannotates the result of
> normalise should be very easy. (Another option is to use such a type in
> the ring solver, and use a separate correctness proof: this could lead
> to a substantial speedup.)
> 
> I have made some definitions in Algebra.RingSolver public, by the way.
> 
> --
> /NAD
>