Найти в Дзене
ΩTrueMagic

TomEditor. Программа для решения задач на модальную логику

Меня занимает модальная логика. А именно, эпистемическая логика (логика знаний). Эпистемическая логика содержит в себе утверждения вида: и т.д. Для того, чтобы успешно взаимодействовать с миром, Алиса строит в голове модель мира. В этой модели она знает, какого цвета небо, и другую полезную информацию. Боб тоже имеет свою модель мира. И частью этой модели является Алиса с её моделью. Т.е. внутри модели Боба есть подмодель Алисы, внутри которой есть информация о том, какого цвета небо. Мне нравится размышлять о том, как модели Боба и Алисы могут вкладываться друг в друга на бесконечную глубину. Мне кажется, в умении мыслить "вложенными контекстами" и заключается настоящий интеллект. Для того, чтобы поиграться с этими моделями, я написал программу TomEditor. Формулировка задачи: Три мудреца поспорили, кто из них самый умный. Чтобы рассудить, четвёртый (судья/прохожий/султан) достаёт пять колпаков: три чёрных и два белых. Он показывает их всем, потом каждому завязывает глаза, надевает
Оглавление

Меня занимает модальная логика. А именно, эпистемическая логика (логика знаний).

Эпистемическая логика содержит в себе утверждения вида:

  • Небо голубое
  • Алиса знает, что небо голубое
  • Боб знает, что Алиса знает, что небо голубое
  • Алиса знает, что Боб знает, что Алиса знает, что небо голубое

и т.д.

Для того, чтобы успешно взаимодействовать с миром, Алиса строит в голове модель мира. В этой модели она знает, какого цвета небо, и другую полезную информацию.

Боб тоже имеет свою модель мира. И частью этой модели является Алиса с её моделью. Т.е. внутри модели Боба есть подмодель Алисы, внутри которой есть информация о том, какого цвета небо.

Мне нравится размышлять о том, как модели Боба и Алисы могут вкладываться друг в друга на бесконечную глубину. Мне кажется, в умении мыслить "вложенными контекстами" и заключается настоящий интеллект.

Для того, чтобы поиграться с этими моделями, я написал программу TomEditor.

Задача о трех мудрецах

Формулировка задачи:

Три мудреца поспорили, кто из них самый умный.
Чтобы рассудить, четвёртый (судья/прохожий/султан) достаёт пять колпаков: три чёрных и два белых. Он показывает их всем, потом каждому завязывает глаза, надевает на голову по одному колпаку (всем троим достаются чёрные), а оставшиеся два прячет. Потом повязки снимают.
Каждый мудрец видит два чёрных колпака на товарищах и не видит свой собственный.
Судья говорит: «Тот, кто первым логически правильно назовёт цвет своего колпака — самый мудрый».
Мудрецы долго молчат, думают… и в какой-то момент все трое одновременно восклицают: «У меня чёрный колпак!». Вопрос: почему они это поняли и как именно рассуждал каждый?

Возможно, вы встречали другие формулировки этой задачи.

Задача для n+1 мудрецов сводится к задаче про n мудрецов, поэтому по индукции можно доказать, что её можно сформулировать для любого количества мудрецов.

Про эту задачу я уже написал отдельную статью на хабре, поэтому не хочется сильно повторяться.

TomEditor

Программа TomEditor предназначена для симуляции ситуаций, описанных в задаче.

Ссылка на репозиторий и программу.

Интерфейс программы выглядит следующим образом.

Задача о трех мудрецах в программе TomEditor
Задача о трех мудрецах в программе TomEditor

Здесь смоделирована та самая задача о трех мудрецах. Давайте, разберем, как это работает.

1. Персонажи

Каждая строчка в таблице задает игрока/персонажа.

В контексте нашей задачи мы имеет трех персонажей: Алиса, Боб, Хлоя.

2. Состояние системы

Состояние системы описывается набором булевых переменных, каждой из которых соответствует свой столбец таблицы. Каждый шарик - это булева переменная, которая принимает значение ноль (белый) или единица (черный).

Первые три столбца - это "свободные" переменные. Мы задаем их значения напрямую.

Последний столбец P1 - это производная переменная. Ее значение зависит от "свободных" переменных. Формула, по которой вычисляется P1, изображена в самом низу под таблицей.

В нашем примере P1 принимает значение 1 (черный), если хотя бы одна из свободных переменных принимает значение 1 (черный) .

На гифке ниже показано, как значение/цвет столбца P1 меняется в зависимости от значений первых трех столбцов.

P1 принимает значение 1 (черный) если хотя бы один из шариков имеет значение 1 (черный)
P1 принимает значение 1 (черный) если хотя бы один из шариков имеет значение 1 (черный)

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

3. Доступ к знаниям

Ячейки таблицы задают доступ персонажей к информации.

Зеленая ячейка означает, что персонаж имеет доступ к соответствующей информации.

Оранжевая ячейка означает, что персонаж не имеет доступ к соответствующей информации, но пытается её угадать.

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

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

По сути, значение в оранжевой ячейке, это и есть главный результат вычислений программы TomEditor.

На гифке ниже показано, как программа автоматически пересчитывает значения в оранжевых ячейках

-3

С помощью TomEditor можно менять "правила игры" и симулировать поведение каждого из игроков.

4. Генерация условий задачи

TomEditor позволяет сгенирировать текст задачи в более строгом виде (чтобы её можно было скормить, например, AI).

Задача о трех мудрецах
Задача о трех мудрецах

Сгенерированный текст задачи о трех мудрецах выглядит следующим образом:

Имеется 3 шара неизвестного цвета. Цвет шара может быть либо ЧЕРНЫМ, либо БЕЛЫМ.
В конверте №1 лежит информация, верно ли, что среди шаров №1 №2 №3 хотя бы один шар ЧЕРНЫЙ. Значение в конверте №1 либо 'ИСТИНА', либо 'ЛОЖЬ'.
Алиса знает:
- цвет шара №2;
- цвет шара №3;
- содержимое конверта №1;
Боб знает:
- цвет шара №1;
- цвет шара №3;
- содержимое конверта №1;
Хлоя знает:
- цвет шара №1;
- цвет шара №2;
- содержимое конверта №1;
Игроки пытаются угадать неизвестную им информацию. Они это делают с помощью одновременного тайного голосования.
В раунде голосования №1:
- Алиса сообщила, что ей не известен цвет шара №1;
- Боб сообщил, что ему не известен цвет шара №2;
- Хлоя сообщила, что ей не известен цвет шара №3;
Результаты голосования №1 становятся общеизвестными.
В раунде голосования №2:
- Алиса сообщила, что ей не известен цвет шара №1;
- Боб сообщил, что ему не известен цвет шара №2;
- Хлоя сообщила, что ей не известен цвет шара №3;
Результаты голосования №2 становятся общеизвестными.
В раунде голосования №3:
- Алиса сообщила, что ей теперь известен цвет шара №1;
- Боб сообщил, что ему теперь известен цвет шара №2;
- Хлоя сообщила, что ей теперь известен цвет шара №3;
Найди:
- цвет шара №1;
- цвет шара №2;
- цвет шара №3;
- содержимое конверта №1;
Правильный ответ:
- цвет шара №1: ЧЕРНЫЙ;
- цвет шара №2: ЧЕРНЫЙ;
- цвет шара №3: ЧЕРНЫЙ;
- содержимое конверта №1: ИСТИНА;

В условиях задачи не указано реальное состояние системы. Его предлагается угадать исходя из того, как проголосовали игроки.

Иногда, невозможно точно угадать полное состояние системы. В этом случае предлагается угадать только часть переменных.

5. Рандомизация

С помощью кнопки "Рандомизация" можно заполнить ячейки случайными значениями и сгенерить новую задачу любой сложности.

Рандомизация условий задачи
Рандомизация условий задачи

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

В среди релизов есть пак с "MathProblems_20260202.zip" с набором задач разного уровня сложности.

Например, самая сложная из них выглядит следующим образом

-6

В этой задаче задействованы:

  • 5 персонажей
  • 6 свободных переменных
  • 3 производные переменные
  • после 7 раундов голосования полное состояние системы (9 переменных) становится полностью вычислимым для стороннего наблюдателя, не обладающего вообще никакой информацией

Заключение

Получается интересный результат:

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

Если кого-то заинтересовала программа, дублирую ссылки на репозиторий и саму программу.