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

Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система λ → {displaystyle lambda ^{ ightarrow }} ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году.

Формальное описание

Синтаксис типов и термов

В базовой версии системы λ → {displaystyle lambda ^{ ightarrow }} типы конструируются из набора переменных с помощью единственного бинарного инфиксного конструктора → {displaystyle ightarrow } . По традиции для переменных типа используют греческие буквы, а оператор → {displaystyle ightarrow } считают правоассоциативным, то есть α → β → γ {displaystyle alpha ightarrow eta o gamma } является сокращением для α → ( β → γ ) {displaystyle alpha ightarrow (eta o gamma )} . Буквы из второй половины греческого алфавита ( σ {displaystyle sigma } , τ {displaystyle au } , и т.д.) часто используются для обозначения произвольных типов, а не только переменных типа.

Различают две версии просто типизированной системы. Если в качестве термов используются те же термы, что и в бестиповом лямбда-исчислении, то систему называют неявно типизированной или типизированной по Карри. Если же переменные в лямбда-абстракции аннотируются типами, то систему называют явно типизированной или типизированной по Чёрчу. В качестве примера приведём тождественную функцию в стиле Карри: λ x . x {displaystyle lambda x.~x} , и в стиле Чёрча: λ x : α . x {displaystyle lambda x!:!alpha .~x} .

Правила редукции

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

( λ x : σ . M ) N → β M [ x := N ] {displaystyle (lambda x!:!sigma .~M)~N o _{eta } M[x:=N]} .

η {displaystyle eta } -редукция определяется так

λ x : σ . M x → η M {displaystyle lambda x!:!sigma .~M~x o _{eta } M} .

Для η {displaystyle eta } -редукции требуется, чтобы переменная x {displaystyle x} не была свободной в терме M {displaystyle M} .

Контексты типизации и утверждения типизации

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

f : ( β → γ ) , g : ( α → β ) , x : α {displaystyle f!:!(eta o gamma ),g!:!(alpha o eta ),x!:!alpha }

Контексты обычно обозначают прописными греческими буквами: Γ , Δ {displaystyle Gamma ,Delta } . В контекст можно добавить «свежую» для этого контекста переменную: если Γ {displaystyle Gamma } — допустимый контекст, не содержащий переменной x {displaystyle x} , то Γ , x : α {displaystyle Gamma ,x!:!alpha } — тоже допустимый контекст.

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

Γ ⊢ M : σ {displaystyle Gamma vdash M!:!sigma }

Это читается следующим образом: в контексте Γ {displaystyle Gamma } терм M {displaystyle M} имеет тип σ {displaystyle sigma } .

Правила типизации (по Чёрчу)

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

Аксиома. Если переменной x {displaystyle x} присвоен в контексте тип σ {displaystyle sigma } , то в этом контексте x {displaystyle x} имеет тип σ {displaystyle sigma } . В виде правила вывода:

Правило введения → {displaystyle ightarrow } . Если в некотором контексте, расширенном утверждением, что x {displaystyle x} имеет тип σ {displaystyle sigma } , терм M {displaystyle M} имеет тип τ {displaystyle au } , то в упомянутом контексте (без x {displaystyle x} ), лямбда-абстракция λ x : σ . M {displaystyle lambda x!:!sigma .~M} имеет тип σ → τ {displaystyle sigma o au } . В виде правила вывода:

Правило удаления → {displaystyle ightarrow } . Если в некотором контексте терм M {displaystyle M} имеет тип σ → τ {displaystyle sigma o au } , а терм N {displaystyle N} имеет тип σ {displaystyle sigma } , то применение M N {displaystyle M~N} имеет тип τ {displaystyle au } . В виде правила вывода:

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

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

x : α ⊢ x : α {displaystyle x!:!alpha vdash x!:!alpha } (аксиома) ⊢ ( λ x : α . x ) : ( α → α ) {displaystyle vdash (lambda x!:!alpha .~x)!:!(alpha o alpha )} (введение → {displaystyle ightarrow } ) f : ( β → γ → δ ) , y : β ⊢ ( f y ) : ( γ → δ ) {displaystyle f!:!(eta o gamma o delta ),y!:!eta vdash (f~y)!:!(gamma o delta )} (удаление → {displaystyle ightarrow } )

Свойства

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