Re: residuation for compositional search?

From: Sebastian Fischer <>
Date: Tue, 14 Jun 2011 17:58:59 +0200

Hello Wolfgang,

thanks for clarifying.

> MCC's strategy uses stability like AKL, i.e., it performs a
> non-deterministic reduction steps only when no thread can perform a
> deterministic reduction step (Andorra principle) and when only
> non-deterministic reduction steps are possible MCC systematically chooses
> the "left-most" thread (stability).

I would expect that MCC terminates in both examples, then.

> On the other hand, reduction of the
> concat application introduces fresh variables that are becoming subject to
> narrowing themselves by the second rule of concat:
> concat (xs:xss) = xs ++ concat xss
> So this constraint has an infinite search space as well (repeatedly
> instantiating xs in the above rule to the empty list []).

Whenever xs is bound to [] by this constraint, the branch can be
refused by the other constraint (which checks that xs is not null).
Then, I would expect that xs is bound to (y:ys) which allows concat to
produce a list headed by y. This is only possible a finite number of
times, afterwards even the binding of xs to a non-empty list will fail
because the result of concat should be empty.

Am I missing something?

curry mailing list
Received on Di Jun 14 2011 - 18:30:07 CEST

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