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

info@vsetut.pro

Стать автором

Вернуться

25.02.2025 12:15:38 | Хабр

Хабы: Erlang/OTP, Prolog, Elixir/Phoenix

TL;DR: решение задачки Эйнштейна на прологе и объяснение, зачем мне вообще пролог в 2025 году.

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

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

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

Посмотреть на код

Подробнее