Соответствие Карри — Говарда

Кульминация курса: программирование и доказательство теорем оказываются буквально одним и тем же.

Соответствие Карри — Говарда — изоморфизм между системами типов и системами логического вывода: типы = утверждения, программы = доказательства, вычисление = упрощение доказательства.

Полный словарь изоморфизма

В разделе про алгебраические типы мы собрали половину словаря. Теперь замкнём его — и увидим, что это не аналогия, а точное соответствие «один к одному».

Почему это так глубоко

Следствие ошеломляющее: проверить, что программа имеет тип, — то же самое, что проверить корректность доказательства. Компьютер, проверяющий типы, проверяет математическую теорему. И наоборот: чтобы доказать теорему, достаточно написать программу нужного типа. Программирование и доказательство — не «похожи», а изоморфны: один и тот же формальный объект, прочитанный с двух сторон.

Отсюда растут Coq, Agda, Lean, Idris: в них доказательство теоремы — это построение значения соответствующего типа, проверяемое тем же чекером, что проверяет программы. Доказали, что компилятор корректен? Значит, написали программу-доказательство, которую машина перепроверила без доверия к человеку.

Демонстрация: пишем доказательства как типизированные функции

Докажем несколько тавтологий, написав тотальные функции их типов. Раз функция строится и тотальна — доказательство есть. Возьмём транзитивность импликации и закон конъюнкции.

# транзитивность: (A -> B) -> (B -> C) -> (A -> C)
def trans(f, g):
    return lambda a: g(f(a))        # композиция = доказательство

# A и B -> B и A   (коммутативность конъюнкции)
def and_comm(pair):
    return (pair[1], pair[0])

# карринг: (A и B -> C)  ->  (A -> B -> C)
def curry(f):
    return lambda a: lambda b: f((a, b))

inc  = lambda x: x + 1
half = lambda x: x // 2
print("trans(inc, half)(7)  :", trans(inc, half)(7))     # half(inc(7)) = 4
print("and_comm (1, 'x')    :", and_comm((1, "x")))
print("curry(sum-pair)(3)(4):", curry(lambda p: p[0] + p[1])(3)(4))

Вывод:

trans(inc, half)(7)  : 4
and_comm (1, 'x')    : ('x', 1)
curry(sum-pair)(3)(4): 7

Композиция функций — это доказательство транзитивности импликации. Перестановка пары — доказательство коммутативности «и». Каррирование — доказательство логической эквивалентности. Эти программы вы писали тысячу раз, не зная, что доказываете теоремы.

Граница: конструктивная логика

Соответствие даёт интуиционистскую (конструктивную) логику. Закон исключённого третьего A или не-A здесь не доказуем: нужно было бы написать тотальную функцию типа forall a. Either a (a -> Void), а универсального способа решить «есть значение a или нет» не существует. Классическую логику получают, добавив исключённое третье как аксиому (значение-постулат без вычислительного содержания) — но тогда теряется свойство «доказательство = вычислимая программа».

Как работает под капотом

Изоморфизм работает и на уровне вычисления: бета-редукция программы соответствует упрощению доказательства (устранению сечения, cut elimination, в теории доказательств Генцена). Поэтому нормализация терма — это приведение доказательства к «прямой» форме без обходных лемм. Сильная нормализация STLC (раздел 4) на логической стороне означает, что всякое доказательство упрощается до конца — глубокая теорема, доказанная через типы.

Частые ошибки

• Считать соответствие метафорой. Это точный изоморфизм: те же деревья вывода, те же правила.
• Доказывать частичной функцией. Только тотальная и завершающаяся функция — доказательство; undefined/зацикливание «доказывает» что угодно, как ложь.
• Ждать классическую логику даром. По умолчанию логика интуиционистская; исключённое третье требует постулата.

Итоги

• Типы = утверждения, программы = доказательства, проверка типов = проверка доказательства.
• Импликация — функция, конъюнкция — пара, дизъюнкция — сумма, ложь — Void.
• На этом стоят Coq/Agda/Lean: доказательство = значение типа, проверяемое чекером.
• Логика интуиционистская; бета-редукция = упрощение доказательства.