Синтаксический сахар (расширенный язык):
Для удобства ввода можно использовать:
• Цифры 0-99 автоматически заменяются на соответствующие термы S...S0
Примеры: 0 → 0, 1 → S0, 3 → SSS0, 10 → SSSSSSSSSS0
• * (звёздочка) автоматически заменяется на ++ (умножение)
Примеры: 2*3 → SS0++SSS0
• Примеры формул в расширенном синтаксисе: "2+3=5", "2*3=6", "x=141", "∃xx(x=xx*xx)"
Процесс обработки формулы:
1. Расширенная формула (с цифрами и *) → преобразование в базовый синтаксис
2. Базовая формула (только символы из таблицы) → синтаксический разбор и проверка корректности
3. Код (последовательность цифр 0-9) → вычисление истинностного значения
Важные замечания:
• x - свободная переменная (используется в формулах φ(x))
• xx - связанная переменная (используется только под квантором ∃xx)
• Замкнутые формулы - формулы без свободных переменных x
• При подстановке конкретного значения x формула становится замкнутой и имеет определённое значение
• ++ обозначает умножение (два плюса подряд кодируются как 33)
• + обозначает сложение (кодируется как 3)
• При вычислении квантора ∃xx проверяются значения от 0 до 1000
• Если нужное значение не найдено в этом диапазоне, квантор считается ложным (с пометкой о пределе проверки)
Приоритеты операций (от высшего к низшему):
1. S (функция следования) - применяется первым
2. ++ или * (умножение) - выше сложения
3. + (сложение)
4. = (равенство) - сравнение термов
5. ¬ (отрицание) - логическая операция
6. ∧ (конъюнкция) - логическая связка
7. ∃ (квантор существования) - самый низкий приоритет
2. Проверка формул и кодов
Проверьте, является ли текст корректной формулой или число корректным кодом:
Можно использовать синтаксический сахар:
• Цифры 0-99 (преобразуются в S...S0)
• * для умножения (преобразуется в ++)
• Примеры: x=5, 2*3=6, x=141, ∃xx(x=xx*xx), ¬(∃xx x=3*xx)
Примечание: Код может содержать только цифры от 0 до 9.
Умножение кодируется как 33 (два плюса подряд).
3. Выбор формулы φ(x) для поиска неподвижной точки
Алгоритм поиска неподвижной точки:
Генерируются замкнутые бескванторные формулы в порядке возрастания сложности.
Для каждой сгенерированной формулы θ проверяется условие: значение(θ) = значение(φ(⌜θ⌝))
где φ(⌜θ⌝) получается подстановкой кода формулы θ вместо переменной x в формулу φ.
Структура генерации:
1. Генерируются базовые термы - числа от 0 до N (в формате S...S0)
2. Создаются атомарные формулы - все возможные равенства термов: терм₁=терм₂
3. На каждом уровне глубины применяются логические операции:
• Отрицание: ¬формула
• Конъюнкция: формула₁∧формула₂
Примерное количество формул:
• При N=5, глубина 0: (5+1)² = 36 атомарных формул
• При N=5, глубина 1: 36 + 36 отрицаний + 36² конъюнкций ≈ 1368 формул
• При N=10, глубина 1: 121 + 121 + 14641 ≈ 14883 формул
• При N=10, глубина 2: десятки тысяч формул (может быть медленно!)
• Глубина 3 и выше - экспоненциальный рост, не рекомендуется
(генерируются числа 0, 1, 2, ..., N)
(0 - только атомы, 1 - с ¬ и ∧, 2+ - вложенные операции)