"Термы -- это деревья, а деревья -- это термы"
-- Банчи (книга "Конечные автоматы, их алгебры и грамматики – к теории формальных выражений")

Компиляторы, автоматы, AST, правила вывода, разбор json, редьюсинг алгебраических выражений, паттерн матчинг и многое многое другое -- это всё про переписывание термов.

На F# пацаны разбирают что-то вроде (^f.(^x.f(^y.xxy))(^x.f(^y.xxy))) легко и просто (редуцируется этот терм к нормальной форме? неа, он рекурсивен; подумайте, почему), а вот если термов сотня миллионов?? )))

Например, можно запилить hott-плагин для Lean , сэмулировав аксиому унивалентности:

universe u

constant U : Type u

-- простейшая версия эквивалентности типов :)
constant equiv : U → U → Type u
axiom univalence : ∀ (A B : U), equiv A B → A = B

example (A B : U) (e : equiv A B) : A = B := univalence A B e


Или расширить новыми теориями инструменты формальной верификации криптографических протоколов ProVerif или Tamarin (в них тоже активно используются термы и правила их переписывания) ...

=

Однако с лёгкой печалью обнаружил, что vds с озу 200 гиг под подобные задачки стоит дороже, чем дедик, меньше $100/месяц не получается...
(и хорошо масштабируемый русский облачный сервис для Jupyter я тоже не нашёл)

Рабочие станции Dell 7920, HP Z8 G4, Lenovo P920 (потенциально терабайты оперативки) продаются с 16 гб (!) от трёх тысяч долларов (а серваки уже от $5 тыс). Какие-то мутные материнки вроде ASUS ROG Rampage VI Extreme Encore 128гб продаются за 100 долларов, но крайне сомнительно, reconditioned сгорит через неделю.