Как найти оптимальный порядок обработки?

У меня есть интересный вопрос, но я не уверен, как именно его сформулировать...

Рассмотрим лямбда-исчисление. Для данного лямбда-выражения существует несколько возможных порядков приведения. Но некоторые из них не прекращаются, в то время как другие делают.

В лямбда-исчислении оказывается, что существует один конкретный порядок редукции, который гарантированно всегда завершается неприводимым решением, если оно действительно существует. Это называется Нормальный порядок.

Я написал простой логический решатель. Но проблема в том, что порядок, в котором он обрабатывает ограничения, по-видимому, оказывает огромное влияние на то, находит ли он какое-либо решение или нет. По сути, мне интересно, существует ли что-то вроде нормального порядка для моего языка логического программирования. (Или не может ли простая машина детерминистически решить эту проблему.)

Так вот чего я добиваюсь. Предположительно, ответ критически зависит от того, что такое «простой логический решатель». Поэтому я попытаюсь краткоописать его.

Моя программа тесно связана с системой комбинаторов из главы 9 The Fun of Programming(Jeremy Gibbons & Oege de Moor). Язык имеет следующую структуру:

• Входными данными для решателя является один предикат. Предикаты могут включать переменные. Результатом решателя является ноль или более решений. Решение — это набор присваиваний переменных, благодаря которым предикат становится истинным.

• Переменные содержат выражения. Выражение — это целое число, имя переменной или кортеж подвыражений.

• Существует предикат равенства, который сравнивает выражения (не предикаты) на равенство. Это выполняется, если замена каждой (связанной) переменной ее значением делает два выражения идентичными. (В частности, каждая переменная равна самой себе, независимо от того, связана она или нет.) Этот предикат решается с помощью унификации.

• Существуют также операторы И и ИЛИ, которые работают очевидным образом. оператора НЕ нет.

• Существует оператор «существует», который фактически создает локальные переменные.

• Возможность определения именованных предикатовпозволяет использовать рекурсивные циклы.

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

Но иногда запуск предиката в обратном порядке приводит к бесконечному поиску, если только вы не измените порядок терминов. (Например, поменяйте местами левый и правый элементы И или ИЛИ.) Мне интересно, есть ли какой-нибудь автоматизированный способ определения наилучшего порядка запуска предикатов, чтобы обеспечить быстрое завершение во всех случаях, когда набор решений точно конечный.

Есть предложения?