Представьте что у нас имеется два выражения, состоящие их переменных и констант. Ну или два дерева, ведь выражения однозначно представляются деревьями. И нам хочется сравнить эти два выражения или дерева. Это одно и тоже или разные вещи? В том смысле, что при каких-то значениях переменных выражения совпадают.

Такой алгоритм сопоставления назвали унификацией. Когда-то на нём строили экспертные системы: помните язык Пролог? Алгоритм унификации пытается сделать два символических выражения равными, вычисляя объединяющую подстановку для этих выражений. Подстановка — это функция, заменяющая переменные другими выражениями. Очень важно, что она действует одинаково на все вхождения одной и той же переменной: если подстановка меняет одно вхождение переменной x на a, она должна заменить все вхождения x на a.

Объединяющая подстановка (или унификатор) для двух выражений e1 и e2 — это подстановка σ, такая что применение σ делает e1 и e2 структурно одинаковыми. Рассмотрим на примерах.

Пример 1: простая унификация. Выражения f(x) и f(y) можно унифицировать, заменив y на x (или наоборот).
Тогда унификатор σ действует так:

σ(y) = x

σ оставляет остальные переменные без изменений.

Пример 2: неудачная унификация. Выражения x + 1 и y + 2 нельзя унифицировать. Может показаться, будто можно подставить 3 вместо x и 2 вместо y, чтобы оба выражения стали равны 4. Но унификация требует символического равенства, а выражения 3 + 1 и 2 + 2 — всё ещё разные синтаксические структуры, хотя и дают одинаковое числовое значение.

Пример 3: несколько возможных унификаторов. Для выражений f(x, y) и f(1, y) возможны разные унификаторы:

σ₁ = { x ↦ 1 } даёт результат f(1, y).
σ₂ = { x ↦ 1, y ↦ 5 } даёт f(1, 5).

Оснований менять y нет, поэтому σ₁ предпочтительнее.

Алгоритмы унификации обычно стремятся получить наиболее общий унификатор (most general unifier, MGU). Это когда делаются только необходимые подстановки. Все остальные унификаторы получаются из MGU путём добавления новых замен. В примере выше σ₁ — MGU, а σ₂ — его частный случай.

Красивая реализация унификации приведена как пример в книжке The Scheme Programming Language: Section 12.10. A Unification Algorithm. Меньше сотни строчек с комментариями, но понять непросто: unify.ss.

А давайте перепишем на смешной язык Gisp. Который внутри тот же Scheme, но с синтаксисом Go. Мне кажется, гораздо яснее выходит.

( исходный код )

Zed интересный редактор, из всех появившихся за последнее время. Всё бы хорошо, но... Открываю в нём текстовый файл. Встаю куда-нибудь в середину окна, скажем на строку 20, и нажимаю PageDown. Файл перелистывается на страницу вперёд, а курсор улетает... вниз окна, на 4-ю строку снизу. Что за ерунда. Жму PageUp, файл листается обратно, но не на всю страницу, а на несколько строк. Курсор оказывается вверху экрана, на 4-й строке сверху. Ëшкин кот! Я не готов прыгать глазами в поисках курсора, увольте.

Легкими пинками мне удалось привести Zed в приемлемое состояние. Переделать клавиши PageUp и PageDown как предписано богом. Чтобы при перелистывании текущая строка (курсор) сохраняла своё относительное положение на экране. Когда вы уже находитесь на последней странице, клавиша PageDown ничего не делает. Верхняя строка остаётся на месте, а курсор не перемещается. В emacs такой режим включается установкой:

(setq scroll-preserve-screen-position t)

Настройки такой в редакторе нет. Надеялся найти плагин - благо, к Zed уже понаделано много extensions. Однако увы, не могут extensions обрабатывать клавиши и влиять на позицию текста в окне. Пришлось править исходник самого Zed.

Сам бы я в исходниках долго ковырялся. Но теперь в помощниках имеем Cursor. Он за пару минут разобрался и передеалал функции move_page_up() и move_page_down(). С первого раза это дело крашанулось, но я показал Курсору дамп стека и он шустро исправил проблему. Правку можно видеть вот тут:

https://github.com/sergev/ved/commit/e1896e99aeaa76b18944e8c0277647366aabe5a2

Чтобы получить такую версию Zed, вам придётся собрать его из исходников. Это нетрудно, по сути одна простая команда "cargo build --release".

Давно ли вам приходилось форматировать 5-дюймовую дискету? И грузиться с неё. А я сегодня получил удовольствие. 😀 Вот так выглядит загрузка MS-DOS 3.31, исторически последней 8-битной версии. Последующие уже на XT-шках не использовались.



Провозившись пару часов, удалось собрать из имеющихся в гараже причандалов работающий флоповод, пересобрать линуксный драйвер, чтобы умел форматировать, и записать загрузочный флопик с MS-DOS.



Флопик приятно в руках подержать.



Вот из чего состоял тогда MS-DOS.

Текстовым редактором в Visual Studio Code невозможно пользоваться, по одной простой причине. При листании клавишами PageUp/PageDown текущая строка (которая с курсором) прыгает по экрану то вверх, то вниз - невозможно предсказать. Нажав PageDown, а потом PageUp, возвращаешься не в исходную точку, а не знамо куда. Поэтому до сих пор я избегал VS Code.

Но сегодня решил разобраться. Как выяснилось, проблема имеет решение. Я сваял расширение, которое обрабатывает кнопки PageUp/PageDown классическим образом, как принято в старых добрых Vim, Emacs и прочих редакторах. Пользуйтесь на здоровье:

github.com/sergev/vscode-classic-paging

Народ умудрился загрузить Windows 95 на микроконтроллере ESP32-S3. Затащили туда симулятор i386. Тормознуто, но прикольно.

hackaday.io/project/204408-tiny386

Как превратить карточку CompactFlash в диск IDE для писишки? Есть решение.



А дальше эта штука воткнётся в дисковый контроллер для 8-битной шины ISA.

Все ржут над российским роботом, а может он вовсе и не кретин. Просто его искусственный интеллект натренирован на советской классике.

"Ничего, ничего, закройся от ветра и потихоньку иди. И дыши так редко, редко. Так дыши, чтобы ноги за коленки не задевали. И куда-нибудь да иди. Все равно куда. Если даже ты пойдешь налево попадешь на Курский вокзал; если прямо - все равно на Курский вокзал; если направо - все равно на Курский вокзал. Поэтому иди направо, чтобы уж наверняка туда попасть. - О тщета!"



Моя дипломная специальность называлась «Системы автоматического управления роботами и космическими летательными аппаратами». База - институт прикладной математики Келдыша. Математика прикладывалась качественная, спутники неплохо летали, а вот с роботами был полный швах. Изготовить точную механику советские заводы были неспособны. Шарниры и шестерёнки выходили говённые. В результате суставы у роботов расшатывались как у прокажённых.

Микропроцессоров для управления роботами не было. Мой шеф мечтательно рассказывал, что ему обещали привезти в кармане из-за бугра микроконтроллер Motorola 68000. Теоретически существовали советские 8080, но и их было не достать в конце 80-х. Клятые буржуи ставят по 32-битному процессору на каждую степень свободы, а нам хоть бы один 8-битный на всего робота.

Звали в аспирантуру, но я поглядел на это убожество, и сказал: спасибо, лучше буду юниксом в курчатнике заниматься. Удачно проинтуичил.