On Wed, 4 Apr 2007, seha_at_informatik.uni-kiel.de wrote:
> I'd like to point out that addition only requires that argument to be
> ground on which the recursion takes place. Such equations then become
> either solvable or refutable with partial evalutation and first-order
> unification only. Narrowing should not be needed. Must have to do with
> Presburger arithmetic, the additive fragment of arithmetic, beeing
> decidable.
Yes, this would be a possible way to formalize addition by a unary
representation of numbers. For an actual implementation view however, this
might be a bit too inefficient. We adopted therefore a binary
representation which then is recursive on both arguments. In howfar this
changes the situation you describe is an interesting topic.
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Apr 11 2007 - 11:57:06 CEST