Просто типизированное лямбда-исчисление

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году[1]. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году[2].

Формальное описание[править | править вики-текст]

Синтаксис типов и термов[править | править вики-текст]

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

Различают две версии просто типизированной системы. Если в качестве термов используются те же термы, что и в бестиповом лямбда-исчислении, то систему называют неявно типизированной или типизированной по Карри. Если же переменные в лямбда-абстракции аннотируются типами, то систему называют явно типизированной или типизированной по Чёрчу. В качестве примера приведём тождественную функцию в стиле Карри: , и в стиле Чёрча: .

Правила редукции[править | править вики-текст]

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

.

-редукция определяется так

.

Для -редукции требуется, чтобы переменная не была свободной в терме .

Контексты типизации и утверждения типизации[править | править вики-текст]

Контекстом называется множество утверждений о типизации переменных, разделённых запятой, например,

Контексты обычно обозначают прописными греческими буквами: . В контекст можно добавить «свежую» для этого контекста переменную: если  — допустимый контекст, не содержащий переменной , то  — тоже допустимый контекст.

Общий вид утверждения о типизации таков:

Это читается следующим образом: в контексте терм имеет тип .

Правила типизации (по Чёрчу)[править | править вики-текст]

В просто типизированном лямбда-исчислении приписывание типов термам осуществляется по приведённым ниже правилам.

Аксиома. Если переменной присвоен в контексте тип , то в этом контексте имеет тип . В виде правила вывода:

Правило введения . Если в некотором контексте, расширенном утверждением, что имеет тип , терм имеет тип , то в упомянутом контексте (без ), лямбда-абстракция имеет тип . В виде правила вывода:

Правило удаления . Если в некотором контексте терм имеет тип , а терм имеет тип , то применение имеет тип . В виде правила вывода:

Первое правило позволяет приписать тип свободным переменным, задав их в контексте. Второе правило позволяет типизировать лямбда-абстракцию стрелочным типом, убирая из контекста связываемую этой абстракцией переменную. Третье правило позволяет типизировать аппликацию (применение) при условии, что левый аппликант имеет подходящий стрелочный тип.

Примеры утверждений о типизации в стиле Чёрча:

    (аксиома)
    (введение )
     (удаление )

Свойства[править | править вики-текст]

  • Просто типизированная система обладает свойством типовой безопасности: при -редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
  • В 1967 году Уильям Тэйт доказал[3], что -редукция для просто типизированной системы обладает свойством сильной нормализации: любой допустимый терм за конечное число -редукций приводится к единственной нормальной форме. Как следствие -эквивалентность термов оказывается разрешимой в этой системе.
  • Изоморфизм Карри — Ховарда связывает просто типизированное лямбда-исчисление с так называемой «минимальной логикой» (фрагментом интуиционистской логики высказываний, включающим только импликацию): населённые типы являются в точности тавтологиями этой логики, а термы соответствуют доказательствам, записанным в форме естественного вывода.

Примечания[править | править вики-текст]

  1. A. Church A Formulation of the Simple Theory of Types // J. Symbolic Logic. — 1940. — С. 56-68.
  2. H. B. Curry Functionality in Combinatory Logic // Proc Natl Acad Sci USA. — 1934. — С. 584–590.
  3. W. W. Tait Intensional Interpretations of Functionals of Finite Type I // J. Symbolic Logic. — 1967. — Т. 32(2).

Литература[править | править вики-текст]