Стендап Сьогодні 📢 Канал в Telegram @stendap_sogodni
🤖🚫 AI-free content. This post is 100% written by a human, as is everything on my blog. Enjoy!01.08.2023
Формальна верифікація: перетворення виразів
Приклад найслабкішої передумови та її спрощеної форми.
Всі ці теореми та конʼюнктивні нормальні форми звучать дуже абстрактно, але що воно являє собою та як з ним працювати. Думаю, не буде новиною, якщо я скажу, що тут теж синтаксичне дерево. Ну, або ж просто дерево, бо воно не відповідає ніякому синтаксису.
В ліспах взагалі код та структура мають буквально ідентичний вигляд. Хіба що для того, щоб якось відрізняти, я використовував не списки, а масиви як вузли дерева. (Може здаватись дивно, що масиви, а не обʼєкти, але в ліспі працювати з масивами природніше.) Операції пишуться в польській нотації, тобто спочатку йде оператор, а потім операнди.
Доведення виразу буде успішнішим, якщо спростити його. Вручну зрозуміло, як це робити: якщо ми бачимо вираз X || false, то відразу можемо замінити його просто на X. Щоб досягти такого результату автоматично, я побудував рушій пошуку зразків у виразі та заміни їх. Це виявилося зручною абстракцією - залишилось тільки зібрати словник відомих алгебраїчних тотожностей. Також рушій спрощення знаходив фрагменти виразу, де всі операнди є константами, та заміняв на результат обчислення.
Що мені особливо подобалось, так це те, як зручно обробляти деревоподібні структури функціональним кодом. А також те, що в Clojure всі структури даних мають порівняння за значенням. Це корисно, наприклад, коли треба шукати піддерева, що повторюються для пошуку зразків.