Задача Эйнштейна. Пролог к валидации конечных автоматов

Зачем нам пролог в 2025 году?

В библиотеке finitomata конечный автомат задаётся набором переходов в текстовой форме в формате plantuml и/или mermaid (с поддержкой пользовательских форматов, но это не суть). На этапе компиляции описание проверяется со всех возможных сторон на корректность (нет обособленных состояний, одно и только одно начальное, для всех неоднозначных переходов определены резолверы, ну и так далее). Долгое время добавление нового правила приводило к написанию очередного велосипеда по его проверке. Все-таки, эликсир — не самый удобный инструмент для валидации правил.

Наконец, мне все это надоело. Заколачивать утюгом шурупы — весело, но малоэффективно. Я даже попробовал прикрутить Coq, но микроскоп тоже плохо подходит для довольно грубой работы с шурупами. И тут меня осенило: пролог же. Оффтопик: почему-то вика в этом месте не переведена на русский язык, если эту заметку читает кто-то, кому не противно редактирование вики — сделайте доброе дело, пожалуйста. Оффтопик: еще вики.

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

Изучаем пролог за 3 минуты

Вот, что нужно знать для работы с прологом:

• это язык для логических доказательств

• все конструкции языка делятся на факты (иногда называемые правилами) и задачи(запросы, queries)

• в языке есть один тип: терм, который, в свою очередь, может быть одного из четырех подтипов: атом, число, переменная, составной терм

• синтаксис интуитивно понятен из пунктуации, принятой в английском языке, а в качестве разделителя определения факта/правила и реализации — используется смайлик «the dog’s bollocks» (:-)

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

В качестве самого простого примера, можно привести вот такой код.

Users = [user(1, Name1, male), user(2, Name2, female)],
member(user(_,ivan,male), Users),
member(user(_,maria,_), Users).

Результатом выполнения будет:

Name1 = ivan,
Name2 = maria,
Users = [user(1,ivan,male), user(2,maria,female)]

Как видно из примера выше, пролог вывел пол Марии и «индексы» (1 у Ивана, и 2 у Марии). Пока неясно, ради чего весь сыр-бор? — Ну что же, пора переходить к задачке Эйнштейна. Итак, откроем на всякий случай вкладку с синтаксисом и запустим vim.

Формулировка фактов

Для начала, освежим в памяти условие.

1. На улице стоят пять домов.

2. Англичанин живёт в красном доме.

3. У испанца есть собака.

4. В зелёном доме пьют кофе.

5. Украинец пьёт чай.

6. Зелёный дом стоит сразу справа от белого дома.

7. Тот, кто курит Old Gold, разводит улиток.

8. В жёлтом доме курят Kool.

9. В центральном доме пьют молоко.

10. Норвежец живёт в первом доме.

11. Сосед того, кто курит Chesterfield, держит лису.

12. В доме по соседству с тем, в котором держат лошадь, курят Kool.

13. Тот, кто курит Lucky Strike, пьёт апельсиновый сок.

14. Японец курит Parliament.

15. Норвежец живёт рядом с синим домом.

Кто пьёт воду? Кто держит зебру?

Приступим.

Сначала отразим непреложный факт: у нас есть пять домов, в каждом из которых живет человек, обладающий пятью признаками: национальность, предпочитаемый цвет, напиток, сигареты, питомец. Много домов — ходят и квакают — как список. Что ж.

% 1. There are five houses. They maintain a list.
houses(0, []) :- !.
houses(N, [(_Person,_Color,_Drink,_Smoke,_Animal)|T]) :- N1 is N-1, houses(N1,T).

Это определение — рекурсивно. Знакомые с зависимыми типами в идрисе, без труда узнают в коде выше список длиной не превышающей N и элементами, являющиеся кортежами из пяти элементов каждый.

Осталось 14 фактов, вот они (комментарии на английском, чтобы проще было сопоставлять с атомами в коде):

% 2. The Brit lives in the red house.
rule2([(brit,red,_,_,_)|_]).
rule2([_|T]) :- rule2(T).

% 3. The Spaniard owns the dog.
rule3([(spaniard,_,_,_,dog)|_]).
rule3([_|T]) :- rule3(T).

% 4. Coffee is drunk in the green house.
rule4([(_,green,coffee,_,_)|_]).
rule4([_|T]) :- rule4(T).

% 5. The Ukrainian drinks tea.
rule5([(ukranian,_,tea,_,_)|_]).
rule5([_|T]) :- rule5(T).

% 6. The green house is immediately to the right of the ivory house.
rule6([(_,ivory,_,_,_),(_,green,_,_,_)|_]).
rule6([_|T]) :- rule6(T).

% 7. The Old Gold smoker owns snails.
rule7([(_,_,_,old_gold,snake)|_]).
rule7([_|T]) :- rule7(T).

% 8. Kools are smoked in the yellow house.
rule8([(_,yellow,_,kool,_)|_]).
rule8([_|T]) :- rule8(T).

% 9. Milk is drunk in the middle house.
rule9([_,_,(_,_,milk,_,_),_,_]).
rule9([_|T]) :- rule9(T).

% 10. The Norwegian lives in the first house.
rule10([(norwegian,_,_,_,_)|_]).

% 11. The man who smokes Chesterfields lives in the house
%     next to the man with the fox.
rule11([(_,_,_,chesterfield,_),(_,_,_,_,fox)|_]).
rule11([(_,_,_,_,fox),(_,_,_,chesterfield,_)|_]).
rule11([_|T]) :- rule11(T).

% 12. Kools are smoked in the house next to the house
%     where the horse is kept.
rule12([(_,_,_,kool,_),(_,_,_,_,horse)|_]).
rule12([(_,_,_,_,horse),(_,_,_,kool,_)|_]).
rule12([_|T]) :- rule12(T).

% 13. The Lucky Strike smoker drinks orange juice.
rule13([(_,_,orange,lucky_strike,_)|_]).
rule13([_|T]) :- rule13(T).

% 14. The Japanese smokes Parliaments.
rule14([(japaneze,_,_,parliament,_)|_]).
rule14([_|T]) :- rule14(T).

% 15. The Norwegian lives next to the blue house.
rule15([(norwegian,_,_,_,_),(_,blue,_,_,_)|_]).
rule15([(_,blue,_,_,_),(norwegian,_,_,_,_)|_]).
rule15([_|T]) :- rule15(T).

Большинство фактов (правил) выше определены по принципу «отбрасываем элементы с начала списка, пока не найдем элемент, удовлетворяющий условию». Шестое правило — матчит два элемента, следующие строго один за другим. Одиннадцатое, двенадцатое и пятнадцатое — матчит два элемента рядом в любой последовательности. И, наконец, десятое — матчит норвежца строго в голове списка.

Осталось записать общий свод фактов.

solution(Persons) :-
  houses(5,Persons),

  rule2(Persons),
  rule3(Persons),
  rule4(Persons),
  rule5(Persons),
  rule6(Persons),
  rule7(Persons),
  rule8(Persons),
  rule9(Persons),
  rule10(Persons),
  rule11(Persons),
  rule12(Persons),
  rule13(Persons),
  rule14(Persons),
  rule15(Persons).

В принципе, задача уже решена. Можно пойти в ноутбук (да, пролог, как и питон с эликсиром, предоставляет возможность запускать код в онлайн-ноутбуке), скопипастить код и выполнить в правом окне solution(Persons). В качестве результата получится вот такой ответ:

Persons = [
    (norwegian,yellow,_,kool,fox),
    (ukranian,blue,tea,chesterfield,horse),
    (brit,red,milk,old_gold,snake),
    (spaniard,ivory,orange,lucky_strike,dog),
    (japaneze,green,coffee,parliament,_)
]

К сожалению, на месте любимого напитка норвежца и питомца японца — пробелы (_ означает переменную без привязки, unbound variable). Почему? — да потому что никто не спрашивал, что там. Пролог сделал ровно то, о чем его просили: расставил по местам цвета с сигаретами, но он же ничего не знает про воду и зебру. Давайте подскажем:

quest1(WaterDrinker,[(WaterDrinker,_,water,_,_)|_]).
quest1(WaterDrinker,[_|T]) :- quest1(WaterDrinker,T).

quest2(ZebraOwner,[(ZebraOwner,_,_,_,zebra)|_]).
quest2(ZebraOwner,[_|T]) :- quest2(ZebraOwner,T).

Теперь надо добавить это в список фактов и попросить обратно то, что нужно.

solution(WaterDrinker,ZebraOwner) :-
  houses(5,Persons),

  rule2(Persons),
  rule3(Persons),
  rule4(Persons),
  rule5(Persons),
  rule6(Persons),
  rule7(Persons),
  rule8(Persons),
  rule9(Persons),
  rule10(Persons),
  rule11(Persons),
  rule12(Persons),
  rule13(Persons),
  rule14(Persons),
  rule15(Persons),
  
  quest1(WaterDrinker,Persons),
  quest2(ZebraOwner,Persons).

Результат выполнения solution(WaterDrinker,ZebraOwner):

WaterDrinker = norwegian,
ZebraOwner = japaneze

Разумеется, Persons тоже можно затребовать через аргумент.

Обратно в эрланг

Итак, у меня в руках, вроде бы, есть прекрасный инструмент для валидации пользовательских правил описания конечного автомата. Но тащить за собой компилятор пролога — идея так себе, верно? Один из создателей эрланга — Роберт Вирдинг — похоже, уже ходил этой доро́гой, поэтому у нас есть интерпретатор пролога на эрланге erlog. Скорее всего, скорость исполнения будет чудовищная (она и у самого пролога так себе, прямо скажем) — но я напоминаю: это все выполняется на этапе компиляции, сиречь — единожды, и на рантайм не влияет вовсе. Так что всё в ажуре.

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

весь код в ноутбуке