Computability на собеседовании

На собеседовании в Google Research кандидату задали вопрос: 'Напишите программу, которая определяет, есть ли в данной программе бесконечный цикл.' Кандидат начал писать код. Интервьюер остановил через минуту: 'Это невозможно. Докажите.' Теория вычислимости - не абстракция для аспирантов. Это язык, на котором думают о фундаментальных ограничениях систем исследователи в Google, DeepMind и Microsoft Research.

• **FAANG Research interviews:** вопросы на доказательство неразрешимости задач статического анализа, верификации и компиляции - стандарт для senior/staff инженерных позиций
• **Статический анализ:** TypeScript, mypy, Coverity - все работают с аппроксимациями из-за теоремы Райса. Знание этого объясняет, почему нет 'идеального' анализатора
• **Архитектура надежных систем:** circuit breakers, watchdogs, таймауты - следствие неразрешимости проблемы остановки, не только heuristic best practices

Доказательства неразрешимости: шаблоны

На собеседованиях в исследовательские группы Google, DeepMind, MSR интервьюеры задают вопросы вида: 'докажите, что задача X неразрешима'. Есть три рабочих шаблона. Первый - диагонализация: предположить разрешимость, построить противоречие через самореференцию (классика Тьюринга для HP). Второй - редукция от HP: показать, что если бы X была разрешима, HP тоже была бы разрешима. Третий - теорема Райса: если X - непрямолинейное свойство языка ТМ, то X неразрешима.

Теорема Райса: любое непрямолинейное семантическое свойство языков машин Тьюринга неразрешимо. 'Непрямолинейное' - значит не все ТМ имеют это свойство и не все не имеют. 'Семантическое' - зависит от вычисляемой функции, а не от описания машины.

Редукции: конструирование и применение

Редукция A <=_m B ('A сводится к B') означает: существует вычислимая функция f такая, что x in A тогда и только тогда, когда f(x) in B. Если B разрешима, то A разрешима. Contrapositive: если A неразрешима, то B неразрешима. На собеседовании нужно уметь быстро строить f: принять описание входа задачи A, сконструировать экземпляр задачи B. Ключевой навык - определить направление редукции: от известно неразрешимой задачи к доказуемой.

Стандартный арсенал: HP (halting problem), ATM (acceptance problem), ETM (emptiness), EqTM (equivalence). Большинство неразрешимых задач на собеседовании сводятся от HP или ATM. Many-one reduction строже Turing reduction: A <=_m B, но не обратно.

Практические пределы вычислений

Пределы вычислимости проявляются не только в теории. Статический анализ кода (ESLint, mypy, Coverity) по теореме Райса не может точно определить ни одно непрямолинейное свойство программы - только аппроксимировать. Верификация программ (Hoare logic, model checking) полна и корректна только для ограниченных моделей. Все производственные верификаторы жертвуют полнотой (false negatives) или корректностью (false positives). LLM не решает проблему остановки - архитектура трансформера не меняет вычислительную модель.

Rice's theorem следствия для инженерии: (1) perfect static analysis невозможен, (2) любой linter имеет false positives или false negatives, (3) automated test generation не может гарантировать полное покрытие семантики, (4) формальная верификация работает только с ограниченными спецификациями.

Архитектурные выводы из теории вычислимости

Знание теории вычислимости меняет архитектурные решения. Если задача неразрешима - проектировать систему нужно вокруг аппроксимаций с явными гарантиями. Sound-анализатор (нет пропусков) или complete-анализатор (нет ложных срабатываний) - осознанный выбор, а не баг. Остановка программы: у production систем всегда нужен таймаут, watchdog, circuit breaker - не потому что код плохой, а потому что остановка неразрешима. Тест-генераторы (fuzzing, property-based testing) покрывают пространство частично - это неустранимое ограничение.

Вопрос на интервью в Google Research: 'Можно ли написать программу, которая определяет, содержит ли другая программа бесконечный цикл?' Ответ включает: (1) нет для общего случая (теорема Тьюринга), (2) да для ограниченных моделей (конечные автоматы, программы без рекурсии), (3) аппроксимация: bounded model checking, abstract interpretation.

Ключевые идеи

• **Три шаблона доказательства:** диагонализация (самореференция), редукция от HP/ATM, теорема Райса для семантических свойств.
• **Направление редукции:** для доказательства неразрешимости X строят A <=_m X, где A - известно неразрешимая задача.
• **Практические следствия:** идеальный статический анализ невозможен (Rice), таймаут обязателен (HP), верификация работает только для ограниченных моделей.
• **Язык для интервью:** 'непрямолинейное семантическое свойство', 'редукция', 'sound vs complete' - ключевые термины для исследовательских позиций.

Связанные темы

Подготовка к интервью по теории вычислимости опирается на классические результаты курса.

• Теорема Райса — Главный инструмент доказательства неразрешимости в этом уроке
• Mapping Reductions — Формальный аппарат редукций, используемый для всех доказательств

Вопросы для размышления

• Статический анализатор, гарантирующий отсутствие null-dereference ошибок, выдает много false positives. Это баг или фича? Как теорема Райса влияет на ответ?
• LLM-ассистенты (Copilot, Cursor) предсказывают, завершится ли функция. Они нарушают теорему Тьюринга? Что именно они делают вместо 'решения' проблемы остановки?
• Квантовые компьютеры меняют класс задач, которые можно решить эффективно. Меняют ли они границу разрешимости? Что остается неразрешимым для квантовых моделей вычислений?

Связанные уроки

• fl-01-intro