Re: On the textual order of rules

From: Michael Hanus <>
Date: Thu, 27 Mar 2014 15:08:35 +0100

Hi Nikolay,

you are right. If you use a Peano representation for naturals
instead of number constants, the search space is automatically
cut to a finite one. Thus, define naturals and their addition by

    data Nat = O | S Nat

    add :: Nat -> Nat -> Nat
    add O x = x
    add (S x) y = S (add x y)

and use this in the definition of size:

    size :: BTree -> Nat
    size (Branch l r) = add (add (S O) (size l)) (size r)
    size (Leaf _) = S O

Then the search space of the query

    size t =:= S (S (S O)) where t free

is finite, independent of the order of rules and even in the
(incomplete) PAKCS implementation.

BTW, the order of rules used in KiCS2 is a bit tricky to
determine. As the default strategy, KiCS2 uses breadth-first
search. However, the initial example of Yi even works with
the depth-first search strategy in KiCS2, since KiCS2 uses
the order of declarations of data constructors to instantiate
free variables. Thus, changing the order of rules makes
no difference in KiCS2. This is also a reason why specifying
exact orderings is not a good idea in a definition of a
*declarative* language. It is more important to provide
good (complete) implementations.



On 03/27/2014 02:41 PM, Nikolay Orlyuk wrote:
> Hi,
> I think that Currey doesn't know that (1 + (1 + ...) + (1 + ...)) =:= 3
> can't succeed and there is no reason to walk further.
> Without any additional information that will cut off branch that
> definitely can't unify there is infinite amount of try/backtrack.
> When you treat infinite you that depends on from which side you treat
> it. In original code you try to calculate infinitely long tree at
> beginning and thus you wait infinite amount of time.
> In second variant you walk starting from "1".
> As I know Curry have special meaning for order of declaration. And this
> behavior totally suits it (in a same way as _ ? _ generates first and
> then second).
> You may want to consider using Nat to represent size. That may cut-off
> branch with 4+ size automatically due to (Succ (Succ (Succ (Succ _))))
> =:= (Succ (Succ (Succ Zero))) can't succeed. But I'm not sure if that
> will work out.
> Cheers
curry mailing list
Received on Do Mär 27 2014 - 15:10:28 CET

This archive was generated by hypermail 2.3.0 : Do Aug 06 2020 - 07:15:05 CEST