| 5:04p |
Выделил все базисы бинарных логических операций из унарных+бинарных. Заняло целый месяц. Хотя казалось бы, - всего-то 20 исходных операций.
Сначала решил, как обычно, брут форсом пробовать. Строил дерево всевозможных выражений (которые тоже деревья) через данные операции, прменял их к всевозможным аргументам (которых 4) eval-ом и искал равенство искомой операции.
Eval, однако, довольно медленно работал. Тогда разделил подмножества (всех операций) по количеству элементов, и начиная сверху (с полного множества) спускался, уровень за уровнем... пока не понял, что в середине диаграммы подмножеств будет около 20 тысяч. Тогда стал, наоборот подниматься, и даже упростил ещё больше - решил выводить канонический базис (отрицание+или / отрицание+и) через потенциальные базисы.
И ничего не выходило. Получалось строить термы до высоты 5, а с высоты 5 термы уже не влазили в 30 ГБ памяти. И какая жалость, некоторые искомые формулы имеют высоту 5 (или больше). Да и метод, понял я, неполноценный. Ибо до какой высоты строить термы, чтобы быть уверенным, что подмножество не является базисом? Непонятно.
Тут меня осенило - ведь сколько термов ни строй, на B_2 (булев квадрат) их, по сути, будет не более 16 (они ведь тождественны логическим операциям). Поэтому надо строить клон (CLosed Operations Network) - замыкание с проекциями. Сразу отсекая термы, дающие уже найденные логические операции.
Второй инсайт - это то, что начальными аргументами надо брать сразу тождественные аргументы, то есть проекции, определённые на B_2 - они и являются, по сути, простейшими аргументами. Тогда оперировать можно сразу таблицами истинности и только ими, изоморфными бинарным логическим операциям. Дополнительный выигрыш в том, что тормозной eval не используется.
В исходном коде получается всё просто и элегантно. Искомое замыкание - это неподвижная точка при действиях операций (унарных и бинарных) на операции (только бинарные). Если в замыкании 16 различных таблиц истинности, то это все бинарные операции, и система полна на B_2. Сужением теми же проекциями на один аргумент можно получить все 4 унарные операции, поэтому она полна и на B_1.
Таким образом можно проверить на полноту подмножества всех операций (а их без проекций остаётся 17). Базис же определяется как нередуцируемое полное подмножество, поэтому, проверяя полноту некоторой системы, приходится проверять и (не)полноту её ближайших подмножеств.
Однако, начав опять спуск по подмножествам, понял, что это будет, ну, очень долгий поиск. Всё же построение клона быстро, но когда подножеств 130 тысяч, да помножить где-то на 5... в общем, применил мемоизацию. Теперь проверок на полноту не могло быть более 130 тысяч, но всё равно программа за сутки перебрала только с десяток тысяч. Проблема была в операциях на списках, которых набралось при рекурсивному проходе по этому дереву, видимо, уж слишком много (подмножеств-то 130 тысяч, а стрелочек между ними гораздо больше).
Короче, последние шаги дались непросто, но надо всего лишь было подниматься по диаграмме подмножеств, а не спускаться. Важно лишь понять, как этот класс полных подмножеств организован, - это, по сути, поддерево (ну, вообще-то, под-DAG, но можно считать, что поддерево) внутри полной диаграммы подмножеств, листьями которого являются базисы. И как только мы базис нашли, можно сразу отсечь все надмножества его содержащие.
С таким подходом программа стала работать гораздо быстрее, и базисы находятся за 3 секунды. Их 2 одноэлементных, 34 двуэлементных и 10 трёхэлементных (понятно, не учитывая проекции). И есть одно 9-элементное помножество среди унарных и бинарных операций, которое не является базисом (понятно, и все его подмножества тоже неполны). Вуаля.
Всё это, конечно, давно известно, но и ладно. Сатисфакция получена. Я называю такие занятия ретроматематикой. |