пятница, июля 23, 2010

Вычислимость, λ-исчисление, теория типов, автоматизация доказательств

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

λ-исчисление

λ-исчисление было создано в начале 50-х гг. XX века для формализации понятий вычисления и вычислимости в математике. λ-исчисление оперирует символами и λ-выражениями. Символ — это одиночный абстрактный объект, иногда символы называют переменными. Символы обозначают маленькими латинскими буквами: x,y,z… λ-выражение определяется рекурсивно:

  • Если x — это символ, то x — это λ-выражение;

  • Если x — символ, а E — λ-выражение, то запись λx.E — тоже λ-выражение;

  • Если E — λ-выражение, то (E) — λ-выражение;

  • Если E1 и E2 — λ-выражения, то E1 E2 — тоже λ-выражение.

Выражения вида λx.E называют λ-функциями, или просто функциями. Если в таком выражении символ x встречается в выражении E, он называется связанным. Несвязанные символы, встречающиеся в λ-выражении, называются свободными.

Для любого λ-выражения E можно записать выражение λx.E, где x — свободный символ выражения E (и, таким образом, связать символ x). Эта операция называется λ-абстракцией.

Введём обозначение: записью E[x=T] будем обозначать выражение, полученное из E заменой всех вхождений символа x на T.

Над λ-выражениями можно производить следующие операции:

α-конверсия

E → E[x=y]; т.е. переменные можно переименовывать;

β-редукция

(λx.E1) E2 → E1[x=E2]; это подстановка;

η-редукция

λx.(E x) → E (избавление от лишней абстракции).

Видно, что α-конверсию можно применить к любому выражению, а редукции — только к выражениям определённого вида.

Если к выражению нельзя применить никаких редукций, говорят, что оно находится в нормальной форме.

Теорема. Если у выражения есть нормальная форма, то она только одна. Любая последовательность редукций приведёт к этой нормальной форме.

Таким образом, выполняется единственность. Но существование выполняется не всегда: не у всех выражений есть нормальная форма.

Example 1: Пример.

ω = (λx.x x) (λx.x x)

ω = (λx.x x) (λy.y y) = (λy.y y) (λy.y y) = (λy.y y) (λz.z z) = (λz.z z) (λz.z z) = …

Последовательность редукций не изменяет это выражение.

Процесс применения редукций к выражению называется вычислением. Выражения, имеющие нормальную форму, называются вычислимыми.

Это вполне соответствует ситуации с программами для машины Тьюринга, среди которых есть как завершающиеся, так и не завершающиеся (работающие бесконечно).

Доказывается, что λ-исчисление тьюринг-полно, то есть любой алгоритм, который можно записать для машины Тьюринга, можно записать в виде λ-выражения, и наоборот. В качестве иллюстрации рассмотрим, как вводятся в λ-исчислении некоторые привычные в программировании сущности.

Введём обозначение: λx.λy.λz.λ…E будем записывать как λx y z….E.

Натуральные числа.

За 1 примем выражение λx.x. Для каждого «числа» E следующим числом будем считать выражение λx.E. Таким образом, двойке будет соответствовать выражение λx y.y, тройке — λx y z.z, и т.д. Далее определения действий над числами вводятся как в аксиоматике Пеано. Такая запись чисел называется кодировкой Чёрча.

Выражения «если-то».

За логическую истину примем выражение λx y.x, за логическую ложь — λx y.y. Тогда выражение λc x y.c x y будет соответствовать конструкции «if-then-else». Действительно,

  • if TRUE A B = (λc x y.c x y) (λx y.x) A B = (λx y.x) A B = A;

  • if FALSE A B = (λc x y.c x y) (λx y.y) A B = (λx y.y) A B = B. Кроме того, оказывается, что можно ввести и обычные логические действия — and, or и т.д.

Пары (кортежи из двух элементов).

Пусть

pair = λf.λs.λb.b f s
fst = λp.p TRUE
snd = λp.p FALSE

Тогда выражение pair x y создаёт кортеж (x,y), функция fst возвращает первый элемент кортежа, snd — второй. Действительно,

pair x y = λb.b x y;
fst (pair x y) = (λp.p TRUE) (λb.b x y) = (λb.b x y) TRUE = TRUE x y = x;
snd (pair x y) = (λp.p FALSE) (λb.b x y) = (λb.b x y) FALSE = FALSE x y = y.

Кортежи из трёх и более элементов, очевидно, можно составлять из пар, например pair x (pair y z) — кортеж из трёх элементов.

Проблема останова

Проблема останова ставится следующим образом. Дан алгоритм (записанный в виде программы для машины Тьюринга или в виде λ-выражения). Нужно, не выполняя его, выяснить, завершается ли он или работает бесконечное время.

Теорема. Проблема останова в общем случае неразрешима.

Дальнейшее развитие теории вычислимости шло в направлении выяснения классов алгоритмов, для которых проблема останова разрешима. В случае с теорией машины Тьюринга такая задача не решена до сих пор. В случае с λ-исчислением решением стала теория типов.

Теория типов

Введём в λ-исчисление типизацию. Именно, кроме символов и выражений, теперь в теории будут фигурировать типы — тоже абстрактные объекты. Типы будем обозначать маленькими греческими буквами: τ, σ… Любое λ-выражение должно иметь тип, и при том только один. Это записывается как E : τ. Типы определяются также рекурсивно:

  • Если τ — тип, то (τ) — тип;

  • Если τ и σ — типы, то τ → σ — тип.

Типы без стрелок и других операций называются простыми типами. Все символы имеют простые типы.

Тип выражения определяется по следующим правилам:

  • Если x : τ и E : σ, то (λx.E) : τ → σ;

  • Если F : τ → σ и x : τ, то (F x) : σ.

При этом если в выражении F x окажется, что F : τ → σ и x : τ1, причём τ ≠ τ1, то говорят, что выражение неверно типизированное. В типизированном λ-исчислении рассматриваются только верно типизированные выражения.

Тип называется населённым, если существует хотя бы одно λ-выражение, имеющее такой тип.

Example 2: Пример.

Попробуем типизировать выражение λx.x x. Пусть x : τ. Тогда, чтобы к x, стоящему в выражении последним, можно было применить предыдущий x, этот предыдущий x должен иметь тип τ → σ, где σ — какой-то ещё тип. Но (x : τ) и (x : τ → σ) не может выполняться одновременно, т.к. у каждого символа может быть только один тип. Пришли к противоречию. Итак, рассматриваемое выражение неверно типизировано, а значит, неверно типизировано и упомянутое в предыдущем примере выражение ω. Таким образом, оказалось, что невычислимое выражение ω не входит в типизированное λ-исчисление.

Оказывается, что верна следующая

Теорема. Если λ-выражение верно типизировано, то оно вычислимо.

Таким образом, в рамках типизированного λ-исчисления проблема останова решается очень просто: все выразимые в этой системе алгоритмы завершаются.

Неудивительно, что при этом оказывается, что эта система не является тьюринг-полной. Т.е. существуют алгоритмы, которые можно представить в виде программы для машины Тьюринга, но нельзя записать в рамках типизированного λ-исчисления. Из этого можно сделать два замечания:

  • Само по себе типизированное λ-исчисление не несёт большой практической ценности, т.к. не позволяет выразить многие алгоритмы;

  • С другой стороны, т.к. множество типизированных выражений является подмножеством нетипизированных, появляется намёк на решение проблемы останова: чтобы выяснить, вычислимо ли данное выражение, нужно только проверить, является ли оно верно типизированным. Неудивительно, что как раз эта задача (проверить возможность типизации для произвольного выражения) оказывается неразрешимой.

Для возможности практического применения λ-исчисления разработаны системы типов, накладывающие меньше ограничений, чем вышеприведённая. Такие системы:

  • достаточно выразительны, т.к. являются тьюринг-полными;

  • вывод типов в них оказывается разрешимой задачей;

  • но проблема останова, как и в случае нетипизированного λ-исчисления, неразрешима.

На таких "промежуточных" системах типов основаны имеющие практическое применения функциональные языки программирования.

Автоматизация доказательств

Для нужд практического программирования в теории типов обычно добавляют такое правило:

  • Если τ и σ — типы, то τ*σ и τ+σ — тоже типы.

В λ-исчислении можно определить понятие пары (E1,E2) и понятие «одно из двух» E1|E2. При этом оказывается, что:

  • Если E1 : τ, E2 : σ, то (E1,E2) : τ*σ,

  • и E1 | E2 : τ+σ.

Оказывается, что между терминами теории типов и терминами логики высказываний существует естественное соответствие. Именно:

  • Простой тип τ соответствует простому высказыванию;

  • Сумма типов соответствует дизъюнкции;

  • Произведение типов — коньюнкции;

  • Стрелка — импликации.

Таким образом, любую теорему логики высказываний можно записать как некий тип. При этом оказывается верной следующая важная

Теорема (изоморфизм Карри-Ховарда). Теорема логики высказываний верна тогда и только тогда, когда соответствующий ей тип населён, т.е. любое λ-выражение, имеющее этот тип, можно рассматривать как доказательство теоремы.

Более сложные, чем вышеприведённая, системы типов позволяют записывать не только теоремы логики высказываний, но и теоремы логики более высоких порядков. При этом изоморфизм Карри-Ховарда остаётся в силе.

Задача «по данному типу найти выражение, имеющее такой тип, или доказать, что таких выражений нет» для многих классов типов решена. Таким образом, задача «по данной теореме найти её доказательство или опровержение» сводится к следующему:

  • Записать данную теорему в виде типа в одной из систем типов;

  • Найти выражение, населяющее этот тип;

  • Записать это выражение на языке предметной области.