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

[Christoph HERRMANN]

Hi Nils,

I have attached an example T1.agda in which I (desperately)
tried to *deannotate*  the polynomial in the result type. However, 
while function *works* typechecks, function *fails* does not
although they only differ in the argument to the *normExp*
function which computes a unique result *ConstrNorm* that differs 
only in its type, which is indexed by the normal form.

I applied function *normalise* to the type expression
using *normType* which basically ends up in a set,
except that the normalised argument of *Norm* remains,
but removing this would enable all polynomials
being equal which I do not want.

Any ideas how to modify the program to make *fails*
working for the given argument, but still fail
for something semantically different such as "(cP 2) :+ m" ?

-------------- next part --------------
A non-text attachment was scrubbed...
Name: T1.agda
Type: application/octet-stream
Size: 896 bytes
Desc: T1.agda
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100823/bcdf7288/T1.obj
-------------- next part --------------


Cheers



On 22 Aug 2010, at 22:34, Christoph HERRMANN wrote:

> 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
>> 
> 

--
 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