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.
Regards,
Michael
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
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Mär 27 2014 - 15:10:28 CET