Чем больше вещей может представлять ваша система, тем меньше вы можете сказать об этих вещах.
Например, если вы храните строки в ASCII, вы не можете представить «∀∃?», а если в Unicode — длина строки уже становится не вполне однозначной. Будем считать, что Unicode более «способен» (выразителен), а ASCII — более «разрешим» (с ним проще строго рассуждать).
Это один из важнейших компромиссов в информатике, сопоставимый с компромиссом между временем и памятью. Причина у него довольно проста: чем больше вещей может представить система, тем меньше у них общего, и тем выше вероятность, что для любой формулируемой вами мысли найдётся контрпример.
Каноничный пример — иерархия по вычислительной мощности. Тезис Чёрча — Тьюринга утверждает, что машина Тьюринга — самая мощная из автоматов: если некоторая задача разрешимости (decision problem, задача с ответом «да/нет») неразрешима машиной Тьюринга, её нельзя решить ни на какой реализуемой вычислительной системе. Теорема об остановке гласит, что не существует алгоритма, который по произвольной машине Тьюринга и произвольному входу определяет, остановится эта машина или нет.1
Машины Тьюринга одновременно и очень выразительны, и плохо поддаются анализу. Автомат с магазинной памятью (pushdown automaton, PDA) — более слабая модель: он не может решать все задачи распознавания, но при этом всегда гарантированно возвращает «да/нет» для любого входа. Более разрешим, менее выразителен. Внизу иерархии — детерминированный конечный автомат (deterministic finite automaton, DFA), который может решать только очень ограниченный класс задач, но зато ещё более хорошо поддаётся анализу, чем PDA.
Обычно эту идею обсуждают именно в таком виде, но примеров куда больше. Например, система типов Rust — корректная: скомпилированная программа на Rust гарантированно не содержит типовых ошибок. Но любая корректная (sound) система типов неполна: существует множество корректных программ, которые компилятор Rust всё равно отвергнет. В Python, напротив, вы можете присваивать «всё чему угодно», и язык не будет жаловаться вплоть до момента, пока вы не попробуете взять поле employee_id у значения типа datetime. Это означает, что Python более «способен» и менее «разрешим», чем Rust: он допускает более широкий класс корректно типизированных программ, но при этом нет никаких гарантий, что конкретная программа на Python вообще корректно типизирована.
Но подождите: существует также множество программ на Rust, которые вообще нельзя выразить на Python! В частности, всё, что связано с прямой работой с памятью. В Python нет понятия адреса памяти, не говоря уже об указателе на него. В языке нет даже самого понятия «ошибка работы с памятью». Rust в этом смысле более способен и менее разрешим, чем Python: он может выражать гораздо более широкий класс программ, работающих с памятью напрямую, но при этом нет гарантии, что любая конкретная программа на Rust будет безопасной с точки зрения памяти.
Поэтому говорить о «способности» и «разрешимости» приходится применительно к конкретному свойству или классу представлений. Это скорее напоминает решётку (lattice), чем линейный спектр. Другие примеры компромиссов между выразительностью и разрешимостью:
Тег-системы
Связные списки → деревья → ориентированные ацикличные графы (DAG) → произвольные ориентированные графы (с циклами)
Данные, которые можно закодировать в JSON, YAML, XML или в SQL-базе данных
Конструктивные представления данных проще анализировать, предикативные — более выразительны
SAT-задачи решаются значительно проще, чем SMT или общее решение ограничений, но и выражают меньше классов задач
Статический анализ куда проще, когда в языке нет макросов, интроспекции или метапрограммирования
Это касается не только компьютерных наук! В математике комплексные числа являются надмножеством вещественных, но вещественные числа — линейно упорядочены, а комплексные — нет.
Как компромисс
Иногда у такого компромисса бывает «перекос» в одну сторону, например: «Разрешимость важнее, но иногда нужно подумать о выразительности». Но я не уверен, что здесь это работает. Скорее это компромисс, который приходится учитывать всегда. Разрешимость действительно кажется более важной: как только система становится достаточно выразительной, чтобы покрыть ваш сценарий, дополнительная выразительность уже не нужна. Но есть и другие факторы:
Требования меняются, и ваша система может оказаться недостаточно выразительной, чтобы поддержать эти изменения.
Обратная совместимость облегчает добавление новых функций (что жертвует разрешимостью ради выразительности), но усложняет удаление старых (что работает наоборот).
Если вы делаете систему более выразительной, вы можете разрушить предположения о разрешимости, на которых полагались другие части системы, и получить новые баги.
Можно использовать подмножество выразительной системы, чтобы сохранить разрешимость, и можно имитировать более сложные возможности в простой системе, чтобы чуть поднять её выразительность.
И не каждое изменение — «игра с нулевой суммой»: мы иногда открываем новые методы, которые повышают и разрешимость, и выразительность «бесплатно».
В общем, это вещь, о которой приходится задумываться в каждом отдельном проекте.
Важно понимать, что выразительность и разрешимость не связаны с удобством использования — тем, насколько легко что-то выражать или анализировать. Обычно удобство действительно конфликтует с первыми двумя характеристиками, но это вовсе не обязательное правило.
Существует распространённое заблуждение, что проблема остановки — чисто теоретическая, потому что у физических компьютеров конечное количество состояний и они «всегда должны завершиться». Но из проблемы остановки следует и другое: «не существует алгоритма, который сможет определить, завершится ли произвольная машина на произвольном вводе прежде, чем она упрётся в предел памяти». Аналогично, таймауты тоже не позволяют «обойти» проблему остановки.
Для заданного детерминированного конечного автомата (DFA) можно точно (алгоритмически) определить множество входов, которые он принимает, тогда как для автоматов с магазинной памятью (PDA) эта задача неразрешима.
Есть тот самый «borrow checker», которым известен Rust, но у него есть одно исключение: unsafe. Без unsafe Rust был бы недостаточно выразителен, чтобы конкурировать с C.
Если после этой статьи хочется не только спорить про выразительность и разрешимость, но и посмотреть, как эти компромиссы выглядят в живых системах, можно продолжить в формате бесплатных демо-уроков:
15 декабря. «Влияние развития технологий AI на корпоративную архитектуру». Записаться
22 декабря. «Dancing Links: задача о полном покрытии». Записаться