[Agda] Commutativity problems in RingSolver

[Christoph HERRMANN]

Hi,

it appears that the *normalise* function in the *RingSolver* module does
not respect commutativity. In case I have used it incorrectly please tell me
how to get a unique normal form for polynomials such that it can be used
in the unification process by the type checker.

I have an example program attached which assumes that the private 
annotations of the data type *Normal* and the function *normalise* are 
removed in the RingSolver module. In the attached file function *checkWorks*
typechecks, which means that the application of function *foo* is reduced.

Function checkFails delivers a type error which basically says that 0 unequal 1,
so commutativity  of + is not exploited by the ring solver. 
Therefore, I assume that the problem is in the use or the implementation
of the RingSolver module.

How can the RingSolver be used to compute a unique normal form for
using it in the typechecking process, akin to the paper by Ana Bove, Peter Dybjer
and Ulf Norell: "Ä Brief Overview of Agda -- A Functional Language with 
Dependent Types"? They present a monoid solver which seems to work, 
but for our project we would need a ring solver (or maybe just a calculation
of normal forms).

Best wishes

-------------- next part --------------
A non-text attachment was scrubbed...
Name: CheckSolver.agda
Type: application/octet-stream
Size: 861 bytes
Desc: CheckSolver.agda
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100817/d309192d/CheckSolver.obj
-------------- next part --------------





On 17 Aug 2010, at 12:22, Christoph HERRMANN wrote:

> Hi Andreas,
> 
> thank you for your hint. It was
> ----
> NF : {p : Polynomial 2} → Set
> NF {p} = Normal 2 p
> 
> foo : (p : Polynomial 2) → NF {p}
> foo p = normalise p
> ---
> what I meant. *Normal* is the type from the RingSolver
> and I have removed the private declaration there as
> well.
> 
> I think one should export the normalisation because
> if you want to compare polynomials it is more convenient
> to just compare the normal forms instead of reifying them
> first.
> 
> Best wishes
> 
> On 17 Aug 2010, at 11:49, Andreas Abel wrote:
> 
>> Hi Christoph,
>> 
>> I cannot load your code in Agda since "Normal" is out of scope.   
>> However, there could be a trivial error:
>> 
>>> NF : Set
>>> NF = {p : Polynomial 2} → Normal 2 p
>>> 
>>> foo : Polynomial 2 → NF
>>> foo p = normalise p
>>> -----------------------------
>>> -- error message
>>> 
>>> p != .p
>> 
>> If you expand out NF, the type of foo becomes
>> 
>> foo : Polynomial 2 -> {p : Polynomial 2} -> Normal 2 p
>> foo p {p'} = normalize p
>> 
>> So there are two different p's, did you mean them to be the same?   
>> Then you need to write
>> 
>> foo : (p : Polynomial 2) -> Normal 2 p
>> foo p = normalize p
>> 
>> If that does not help, please post your problem again, preferably in a  
>> form I can immediately load into Agda.
>> 
>> Cheers,
>> Andreas
>> 
>> 
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>> 
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>> 
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~abel/
>> 
> 
> --
> 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
> 
> 
> 
> 
> <ATT00001..txt>

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