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

[Christoph HERRMANN]

Hi Nils,

On 20 Aug 2010, at 11:09, Nils Anders Danielsson wrote:

> On 2010-08-19 12:56, Christoph HERRMANN wrote:
>> However, this still does not provide a normal form
>> which can be used as a type.
> 
> Can you explain in more detail what you want to accomplish?

I want to use natural numbers expressed as arithmetic expressions
with unknown variables as type indices. 

My current solution is, instead of placing the normal form directly
into the type argument, to put a free variable in those places and add an 
argument to the function which define an polynomial equality between 
that free variable and the unnormalised expression I have. For the proof 
I can then use the ring solver. Thank you, this is actually very nice
and saves much tedious work.

Although all these proofs look basically the same, so can potentially
even be generated automatically, they clutter up the program and
I have the suspicion that they also slow down the type check
significantly.

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? Unfortunately, my understanding
of the internals of the ring solver is vague, otherwise and if it would
be easy to reuse most of the code already there, I would have
written this function myself.

Best wishes
--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532