[Agda] Re: Commutativity problems in RingSolver

[Christoph HERRMANN]

Hi again,

this time I used the operator (= with * on top) which is obviously meant
for comparing polynomials semantically, omitting the call to normalise
then, of course. This time, function "checkWorks" passes again and 
"checkFails" does not explicitly deliver an error but reports unresolved 
metas, which I assume means that this does not count as a proof.

Maybe I did something wrong in the way I imported the solver or there
is a bug in the library. If anyone knows, please tell me as soon as
possible. The program is attached and the private attribute of the
operator (= with * on top) in the RIngSolver needs to be removed for that.

Best Wishes

-------------- next part --------------
A non-text attachment was scrubbed...
Name: CheckSolver2.agda
Type: application/octet-stream
Size: 671 bytes
Desc: CheckSolver2.agda
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100819/1e050002/CheckSolver2.obj
-------------- next part --------------



On 17 Aug 2010, at 18:11, Christoph HERRMANN wrote:

> 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
> 
> <CheckSolver.agda><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