How to limit search space in Curry?

Question

Below is my first program in Curry. It prints sequence of steps required for reaching a desired solution (walking through a closed door).

Evaluating expression: main
Done
(Just [Open,Walk,Close])

How can I make it terminate when looking for Impossible? I am using Kics2 0.3.1.

import List
import AllSolutions
import IO
import ReadShowTerm
import Constraint

data State = Opened | Closed | Outside | Done | Impossible
data Action = Open | Walk | Close

e Open Closed = Opened
e Walk Opened = Outside
e Close Outside = Done

solution target | foldl (flip e) Closed actions =:= target & length actions <: 4  = actions
   where actions free

main = do
  target <- getContents
  getOneValue (solution $ readTerm target) >>= print 

Answer 1

In the case of Done, you prune the search space by using getOneValue. That is, when the first result is found, the function does not generate more possibilities for the free variable actions. However, when there is no solution, like in the case of Impossible, the use of getOneValue cannot prune the search space as it keeps on looking for the first solution. In fact, if you search for all solutions instead of only the first one, even the other call does not terminate after finding a solution.

In order to get a terminating version, you could try the following definition of solution.

solution target | foldl (flip e) Closed (take 4 actions) =:= target = actions
   where actions free

This way the search space is actually pruned because take does only evaluate the first four cons constructors of the list. In contrast, length causes the evaluation of all constructors of the list to calculate the length. Because it evaluates the whole list, the free variable actions generates more and more lists, as the generation of non-deterministic possibilities of a free variable is driven by the evaluation of the free variable.

Limiting the search space of a Curry program can be quite difficult because you have to reason about evaluation. For example, you also get a terminating program if you use peano numbers instead of primitive integers. More precisely, you can define the following functions using Peano numerals.

data Peano = Zero | Succ Peano

fourP :: Peano
fourP = Succ (Succ (Succ (Succ Zero)))

lengthP :: [a] -> Peano
lengthP [] = Zero
lengthP (_:xs) = Succ (lengthP xs)

lessP :: Peano -> Peano -> Success
lessP Zero     (Succ _) = success
lessP (Succ x) (Succ y) = lessP x y

By means of these functions you get a terminating version as follows.

solution target | lessP (lengthP actions) fourP & foldl (flip e) Closed actions =:= target = actions
   where actions free

However, note that you have to check for the length of the list first because & has a left bias with respect to evaluation. That is, if its first argument fails, it does not evaluate its second argument. If we switch the arguments of &, the condition will first check whether the list of actions yields the state Closed and afterwards check its length. That is, we do not use the length to prune the search space anymore.