Суть понятия
Разрешающая процедура (алгоритм разрешимости) — механический тест, который для любой строчки за конечное время отвечает «да» или «нет» на вопрос, является ли она теоремой формальной системы. Перечисление теорем таким тестом не является: оно может подтвердить «да», но никогда не докажет «нет». На примере системы MIU и головоломки MU разрешающая процедура строится через инвариант — свойство, которое сохраняет каждое правило вывода.
Кратко об алгоритме
Задача. Для любой строчки выяснить, выводима ли она в системе MIU. Перебор выводов не подходит: их бесконечно много, и «нет» им не доказать.
Идея. Ищем свойство, которое не меняется ни одним правилом (инвариант). Таким свойством оказывается остаток от деления числа букв I на 3:
- правила I и IV число I не меняют;
- правило III вычитает 3, остаток прежний;
- правило II удваивает число I, остаток 1 и 2 меняются местами, а ноль никогда не появляется.
Аксиома MI содержит одну I, остаток 1. Значит, у каждой теоремы число I не кратно 3. В MU букв I нет (ноль кратен 3), поэтому MU не теорема.
Алгоритм. Строчка является теоремой, если одновременно:
- она начинается с M, и других M в ней нет;
- остальные буквы только I и U;
- число I не делится на 3.
Код и визуализация алгоритма здесь: https://colab.research.google.com/drive/1WmdH0Wvun6aB3l0hfBvAojkmFMJmZ0FN?usp=sharing
Где встречается в тексте
| Глава | Контекст |
|---|---|
| Глава I: Головоломка MU | понятие разрешающей процедуры; головоломка MU как задача о выводимости |
Связанные карточки
Подробный разбор: игра, в которую мы играем
Представьте, что у нас есть конструктор.
У нас есть одна начальная деталь (аксиома): MI.
У нас есть 4 правила, как из одних деталей собирать другие.
Цель: Получить строчку MU.
Главный вопрос: Можно ли вообще получить MU?
Давайте посмотрим на код, который пытается это выяснить, и разберем, почему простой перебор всех возможных вариантов здесь не работает.
Блок 1. «Фабрика» строчек (Правила игры)
Сначала посмотрим на функцию successors(s). Это наша «фабрика». Она берет одну строчку и возвращает все возможные строчки, которые можно из неё получить за один шаг.
def successors(s):
"""
Возвращает список строк, которые можно получить из s за один шаг
по четырём правилам системы MIU.
"""
result = []
# Правило I: если строка заканчивается на I, добавить U
if s.endswith('I'):
result.append(s + 'U')
# Правило II: если строка имеет вид Mx, добавить x (удвоить хвост)
if s.startswith('M'):
x = s[1:]
result.append(s + x)
# Правило III: заменить любое вхождение III на U
idx = s.find('III')
while idx != -1:
result.append(s[:idx] + 'U' + s[idx+3:])
idx = s.find('III', idx + 1)
# Правило IV: удалить любое вхождение UU
idx = s.find('UU')
while idx != -1:
result.append(s[:idx] + s[idx+2:])
idx = s.find('UU', idx + 1)
return resultЧто здесь важно для слушателей:
Фабрика работает слепо. Она не знает, какая цель. Она просто применяет правила механически. Из одной строчки может получиться две, из двух — четыре, из четырех — шестнадцать. Дерево возможных строчек растет экспоненциально.
Блок 2. Ловушка слепого поиска (Почему перебор не дает ответа)
Теперь смотрим на функцию explore(depth). Она запускает «поиск в ширину». Мы берем аксиому MI, применяем фабрику, записываем новые строчки. Потом берем новые строчки, снова применяем фабрику и так далее, пока не достигнем заданной depth (глубины).
def explore(depth):
"""
Поиск в ширину: генерирует все теоремы до заданной глубины.
Возвращает множество всех достигнутых строк.
"""
seen = {'MI'}
frontier = {'MI'}
for step in range(depth):
new_frontier = set()
for s in frontier:
for t in successors(s):
if t not in seen:
seen.add(t)
new_frontier.add(t)
frontier = new_frontier
print(f"Глубина {step + 1}: всего строк {len(seen)}, новых {len(new_frontier)}")
return seen💡 ГЛАВНЫЙ МОМЕНТ ДЛЯ АУДИТОРИИ (Почему вывод теорем не предсказывает разрешимость)
Задайте слушателям вопрос:
«Представьте, что мы запустили этот код, он перебрал все теоремы до глубины 1 000 000. Строчки
MUсреди них нет. Можем ли мы сделать вывод, чтоMUполучить невозможно?»
Ответ: НЕТ!
Потому что на глубине 1 000 001 она может внезапно появиться.
Перебор (генерация теорем) может доказать, что MU — это теорема (если мы её найдем).
Но перебор никогда не сможет доказать, что MU — не теорема. Мы всегда будем сомневаться: «А вдруг мы просто недостаточно глубоко искали?».
Именно поэтому простой вывод списка всех теорем не является разрешающей процедурой. Разрешающая процедура должна уметь отвечать «НЕТ» за конечное время, не перебирая бесконечность.
Блок 3. «Чит-код» или Разрешающая процедура (Инвариант)
Чтобы не перебирать миллиарды строчек, математики ищут инвариант — свойство, которое не меняется, какие бы правила мы ни применяли.
Посмотрим на функцию is_theorem(s):
def is_theorem(s):
"""
Разрешающая процедура на основе инварианта:
количество букв I по модулю 3 не может быть равно 0 ни в одной теореме.
"""
count_i = s.count('I')
return count_i % 3 != 0Что делает последняя строчка?
Она считает количество букв I в строчке и смотрит на остаток от деления на 3.
- Если остаток не равен 0 (то есть букв
I: 1, 2, 4, 5, 7…) — функция говорит «Да, это может быть теоремой». - Если остаток равен 0 (букв
I: 0, 3, 6, 9…) — функция говорит «Нет, это точно НЕ теорема».
Разбор инварианта на пальцах:
Почему это работает? Давайте мысленно проверим наши 4 правила из блока 1. Как они меняют количество букв I?
- Правило I (добавить U): Буквы
Iне трогаем. Количество не изменилось. Остаток от деления на 3 остался тем же. - Правило II (удвоить хвост): Количество букв
Iумножается на 2. Если число не делилось на 3, то и его удвоенная версия на 3 не разделится. Остаток сохранится! - Правило III (заменить III на U): Мы удалили ровно 3 буквы
I. Если вычесть 3 из любого числа, остаток от деления на 3 не изменится. - Правило IV (удалить UU): Буквы
Iне трогаем. Остаток тот же.
Вывод: Какое бы правило мы ни применили, остаток от деления количества I на 3 никогда не меняется.
У нашей аксиомы MI одна буква I. Единица не делится на 3 (остаток 1).
Значит, ни в одной теореме системы MIU количество букв I не может быть кратно 3!
А теперь посмотрим на нашу цель — MU.
В строчке MU ноль букв I. Ноль делится на 3 без остатка.
Следовательно, MU получить невозможно. Точка. Нам не нужен перебор.
Блок 4. Визуализация доказательства (Трассировка)
Чтобы слушатели увидели инвариант в динамике, в коде есть функция trace. Она просто красиво печатает таблицу.
def trace(strings):
"""
Печатает таблицу: строка, количество I, остаток от деления на 3.
"""
print(f"{'Строка':<12} {'n (кол-во I)':<15} {'n mod 3':<10}")
print("-" * 40)
for s in strings:
n = s.count('I')
print(f"{s:<12} {n:<15} {n % 3:<10}")Как это объяснить:
«Колонка
n— это сколько буквI. Колонкаn mod 3— это остаток от деления на 3. Посмотрите на эту колонку. Как бы мы ни извращались, применяя правила, она никогда не станет равна нулю. А для строчкиMUона должна была бы стать нулем. Это и есть наша разрешающая процедура: мы смотрим не на саму строчку, а на её математическую “душу”».
Блок 5. Финал (Главный блок)
Остался только блок if __name__ == '__main__':
if __name__ == '__main__':
# Демонстрация разрешающей процедуры
for s in ['MU', 'MUIIU', 'MIII', 'MUUU']:
print(f"{s}: {is_theorem(s)}")
# Демонстрация трассировки
print()
trace(['MI', 'MII', 'MIIII', 'MIIIIU', 'MU'])Здесь мы видим, как is_theorem мгновенно, за долю секунды, без всякого перебора и деревьев, отвечает:
MU—False(потому что 0 буквI, делится на 3)MUIIU—True(2 буквыI, не делится)MIII—False(3 буквыI, делится на 3)MUUU—False(0 буквI, делится на 3)
Резюме (Шпаргалка)
-
Генерация теорем (перебор / explore) — это как искать иголку в стоге сена, перебирая соломинки одну за другой. Если мы не нашли иголку, мы не знаем, её там нет, или мы просто плохо искали. Это не разрешающая процедура.
-
Инвариант (is_theorem) — это как использовать магнит. Мы не перебираем сено, мы смотрим на свойство (магнитность). Если свойство не совпадает — иголки там нет. Это разрешающая процедура.
В математике и информатике важно искать инварианты и свойства: они позволяют доказывать невозможность (неразрешимость) без бесконечного перебора.
Комментарий составителя
Материал подготовлен к встрече 4 (15.10.2026) и вынесен со страницы встречи в отдельную карточку.