Как ограничить пространство поиска в карри?

Question

Ниже моя первая программа на карри. Он печатает последовательность шагов, необходимых для достижения желаемого решения (пройти через закрытую дверь).

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

Как я могу сделать это прекратить при поиске Impossible? Я использую 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

В случае Doneвы сокращаете пространство поиска с помощью getOneValue, То есть, когда найден первый результат, функция не генерирует больше возможностей для свободной переменной actions, Однако, когда нет решения, как в случае Impossible, использование getOneValue не может обрезать пространство поиска, так как оно продолжает искать первое решение. Фактически, если вы ищете все решения, а не только первое, даже другой вызов не завершается после нахождения решения.

Чтобы получить завершающую версию, вы можете попробовать следующее определение solution,

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

Таким образом, пространство поиска на самом деле сокращается, потому что take оценивает только первые четыре конструктора из списка. По сравнению, length вызывает вычисление всех конструкторов списка для вычисления длины. Поскольку он оценивает весь список, свободная переменная actions генерирует все больше и больше списков, поскольку генерация недетерминированных возможностей свободной переменной определяется оценкой свободной переменной.

Ограничение пространства поиска в программе Curry может быть довольно сложным, потому что вы должны рассуждать об оценке. Например, вы также получаете завершающую программу, если используете простые числа вместо простых чисел. Точнее, вы можете определить следующие функции, используя Peano числительные.

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

С помощью этих функций вы получаете завершающую версию следующим образом.

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

Однако обратите внимание, что сначала вы должны проверить длину списка, потому что & имеет левое смещение в отношении оценки. То есть, если его первый аргумент терпит неудачу, он не оценивает свой второй аргумент. Если мы переключим аргументы &, условие сначала проверит, выводит ли список действий состояние Closed и затем проверьте его длину. То есть мы больше не используем длину для сокращения пространства поиска.