Система F

18.12.2020

Система F (полиморфное лямбда-исчисление, система λ 2 {displaystyle lambda 2} , типизированное лямбда-исчисление второго порядка) — система типизированного лямбда-исчисления, отличающаяся от просто типизированной системы наличием механизма универсальной квантификации над типами. Эту систему разработал в 1972 году Жан-Ив Жирар в контексте теории доказательств в логике. Независимо от него подобную систему предложил в 1974 году Джон Рейнольдс. Система F позволяет формализовать концепцию параметрического полиморфизма в языках программирования и служит теоретической основой для таких языков программирования как Haskell и ML.

Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды Λ {displaystyle Lambda } . Например, взяв терм λ x α .   x {displaystyle lambda x^{alpha }.~x} типа α → α {displaystyle alpha o alpha } и абстрагируясь по переменной типа α {displaystyle alpha } , получаем терм Λ α .   λ x α .   x {displaystyle Lambda alpha .~lambda x^{alpha }.~x} . Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами:

( Λ α .   λ x α .   x )   Bool   → β   λ x Bool .   x {displaystyle (Lambda alpha .~lambda x^{alpha }.~x)~{ exttt {Bool}} o _{eta } lambda x^{ exttt {Bool}}.~x} — терм типа Bool → Bool {displaystyle { exttt {Bool}} o { exttt {Bool}}} ; ( Λ α .   λ x α .   x )   Nat   → β   λ x Nat .   x {displaystyle (Lambda alpha .~lambda x^{alpha }.~x)~{ exttt {Nat}} o _{eta } lambda x^{ exttt {Nat}}.~x} — терм типа Nat → Nat {displaystyle { exttt {Nat}} o { exttt {Nat}}} .

Видно, что терм Λ α .   λ x α .   x {displaystyle Lambda alpha .~lambda x^{alpha }.~x} обладает полиморфным поведением, то есть задаёт общий интерфейс для различных типов данных. В Системе F этому терму приписывается тип ∀ α .   α → α {displaystyle forall alpha .~alpha o alpha } . Квантор всеобщности в типе подчёркивает возможность подстановки вместо переменной типа α {displaystyle alpha } любого допустимого типа.

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

Синтаксис типов

Типы Системы F конструируются из набора переменных типа с помощью операторов → {displaystyle o } и ∀ {displaystyle forall } . По традиции для переменных типа используют греческие буквы. Правила формирования типов таковы:

  • (Переменная типа) Если α {displaystyle alpha } — переменная типа, то α {displaystyle alpha } — это тип;
  • (Стрелочный тип) Если A {displaystyle A} и B {displaystyle B} являются типами, то ( A → B ) {displaystyle (A o B)} — это тип;
  • (Универсальный тип) Если α {displaystyle alpha } является переменной типа, а B {displaystyle B} — типом, то ( ∀ α .   B ) {displaystyle (forall alpha .~B)} — это тип.

Внешние скобки часто опускают, оператор → {displaystyle ightarrow } считают правоассоциативным, а действие оператора ∀ {displaystyle forall } продолжающимся вправо насколько это возможно. Например, ∀ α .   ∀ β .   α → β → α {displaystyle forall alpha .~forall eta .~alpha o eta o alpha } — стандартное сокращение для ( ∀ α .   ( ∀ β .   ( α → ( β → α ) ) ) ) {displaystyle (forall alpha .~(forall eta .~(alpha o (eta o alpha ))))} .

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

Термы Системы F конструируются из набора термовых переменных ( x {displaystyle x} , y {displaystyle y} , z {displaystyle z} и т.д.) по следующим правилам

  • (Переменная) Если x {displaystyle x} — переменная, то x {displaystyle x} — это терм;
  • (Абстракция) Если x {displaystyle x} является переменной, A {displaystyle A} — типом, а M {displaystyle M} — термом, то ( λ x A .   M ) {displaystyle (lambda x^{A}.~M)} — это терм;
  • (Применение) Если M {displaystyle M} и N {displaystyle N} являются термами, то ( M   N ) {displaystyle (M~N)} — это терм;
  • (Универсальная абстракция) Если α {displaystyle alpha } является переменной типа, а M {displaystyle M} — термом, то ( Λ α .   M ) {displaystyle (Lambda alpha .~M)} — это терм;
  • (Универсальное применение) Если M {displaystyle M} является термом, а A {displaystyle A} — типом, то ( M   A ) {displaystyle (M~A)} — это терм.

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

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

  • (Абстракция по Карри) Если x {displaystyle x} является переменной, а M {displaystyle M} — термом, то ( λ x .   M ) {displaystyle (lambda x.~M)} — это терм,

и отбросить два последних правила, то систему называют типизированной по Карри. Фактически, термы системы, типизированной по Карри, те же, что и в бестиповом лямбда-исчислении.

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

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

( λ a A .   M )   N   → β   M [ a := N ] {displaystyle (lambda a^{A}.~M)~N o _{eta } M[a:=N]}

в системе F в стиле Чёрча вводится дополнительное правило,

( Λ α .   M )   A   → β   M [ α := A ] {displaystyle (Lambda alpha .~M)~A o _{eta } M[alpha :=A]} ,

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

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

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

Γ = x 1 : A 1 , x 2 : A 1 , … , x n : A n {displaystyle Gamma =x_{1}!:!A_{1},x_{2}!:!A_{1},ldots ,x_{n}!:!A_{n}}

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

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

Γ ⊢ M : A {displaystyle Gamma vdash M!:!A}

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

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

В Системе F, типизированной по Чёрчу, приписывание типов термам осуществляется в соответствии со следующими правилами:

(Начальное правило) Если переменная x {displaystyle x} присутствует с типом A {displaystyle A} в контексте Γ {displaystyle Gamma } , то в этом контексте x {displaystyle x} имеет тип A {displaystyle A} . В виде правила вывода

(Правило введения → {displaystyle ightarrow } ) Если в некотором контексте, расширенном утверждением, что a {displaystyle a} имеет тип A {displaystyle A} , терм M {displaystyle M} имеет тип B {displaystyle B} , то в упомянутом контексте (без a {displaystyle a} ), лямбда-абстракция λ a A .   M {displaystyle lambda a^{A}.~M} имеет тип A → B {displaystyle A o B} . В виде правила вывода

(Правило удаления → {displaystyle ightarrow } ) Если в некотором контексте терм M {displaystyle M} имеет тип A → B {displaystyle A o B} , а терм N {displaystyle N} имеет тип A {displaystyle A} , то применение M   N {displaystyle M~N} имеет тип B {displaystyle B} . В виде правила вывода

(Правило введения ∀ {displaystyle forall } ) Если в некотором контексте терм M {displaystyle M} имеет тип A {displaystyle A} , то в этом контексте терм Λ α .   M {displaystyle Lambda alpha .~M} имеет тип ∀ α .   A {displaystyle forall alpha .~A} . В виде правила вывода

Это правило требует оговорки: переменная типа α {displaystyle alpha } не должна встречаться в утверждениях типизации контекста Γ {displaystyle Gamma } .

(Правило удаления ∀ {displaystyle forall } ) Если в некотором контексте терм M {displaystyle M} имеет тип ∀ α .   A {displaystyle forall alpha .~A} , и B {displaystyle B} — это тип, то в этом контексте терм M   B {displaystyle M~B} имеет тип A [ α := B ] {displaystyle A[alpha :=B]} . В виде правила вывода

Правила типизации по Карри

В Системе F, типизированной по Карри, приписывание типов термам осуществляется в соответствии со следующими правилами:

(Начальное правило) Если переменная x {displaystyle x} присутствует с типом A {displaystyle A} в контексте Γ {displaystyle Gamma } , то в этом контексте x {displaystyle x} имеет тип A {displaystyle A} . В виде правила вывода

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

(Правило удаления → {displaystyle ightarrow } ) Если в некотором контексте терм M {displaystyle M} имеет тип A → B {displaystyle A o B} , а терм N {displaystyle N} имеет тип A {displaystyle A} , то применение M   N {displaystyle M~N} имеет тип B {displaystyle B} . В виде правила вывода

(Правило введения ∀ {displaystyle forall } ) Если в некотором контексте терм M {displaystyle M} имеет тип A {displaystyle A} , то в этом контексте этому терму M {displaystyle M} может быть приписан и тип ∀ α .   A {displaystyle forall alpha .~A} . В виде правила вывода

Это правило требует оговорки: переменная типа α {displaystyle alpha } не должна встречаться в утверждениях типизации контекста Γ {displaystyle Gamma } .

(Правило удаления ∀ {displaystyle forall } ) Если в некотором контексте терм M {displaystyle M} имеет тип ∀ α .   A {displaystyle forall alpha .~A} , и B {displaystyle B} — это тип, то в этом контексте этому терму M {displaystyle M} может быть приписан и тип A [ α := B ] {displaystyle A[alpha :=B]} . В виде правила вывода

Пример. По начальному правилу:

x : ( ∀ α .   α → α ) ⊢ x : ( ∀ α .   α → α ) {displaystyle x!:!(forall alpha .~alpha o alpha )vdash x!:!(forall alpha .~alpha o alpha )}

Применим правило удаления ∀ {displaystyle forall } , взяв в качестве B {displaystyle B} тип ∀ α .   α → α {displaystyle forall alpha .~alpha o alpha }

x : ( ∀ α .   α → α ) ⊢ x : ( ∀ α .   α → α ) → ( ∀ α .   α → α ) {displaystyle x!:!(forall alpha .~alpha o alpha )vdash x!:!(forall alpha .~alpha o alpha ) o (forall alpha .~alpha o alpha )}

Теперь по правилу удаления → {displaystyle ightarrow } имеем возможность применить терм x {displaystyle x} сам к себе

x : ( ∀ α .   α → α ) ⊢ ( x   x ) : ( ∀ α .   α → α ) {displaystyle x!:!(forall alpha .~alpha o alpha )vdash (x~x)!:!(forall alpha .~alpha o alpha )}

и, наконец, по правилу введения → {displaystyle ightarrow }

⊢ ( λ x .   x   x ) : ( ∀ α .   α → α ) → ( ∀ α .   α → α ) {displaystyle vdash (lambda x.~x~x)!:!(forall alpha .~alpha o alpha ) o (forall alpha .~alpha o alpha )}

Это пример терма, типизируемого в Системе F, но не в просто типизированной системе.

Представление типов данных

Система F обладает достаточными выразительными средствами, для того чтобы напрямую реализовать многие типы данных, используемые в языках программирования. Будем работать в версии Чёрча системы F.

Пустой тип. Тип

⊥   ≡   ∀ α .   α {displaystyle ot equiv forall alpha .~alpha }

необитаем в системе F, то есть в ней отсутствуют термы с таким типом.

Единичный тип. У типа

⊤   ≡   ∀ α .   α → α {displaystyle op equiv forall alpha .~alpha o alpha }

в системе F имеется единственный находящийся в нормальной форме обитатель — терм

i d   ≡   Λ α .   λ x α .   x {displaystyle {mathtt {id}} equiv Lambda alpha .~lambda x^{alpha }.~x} .

Булев тип. В системе F задается так:

B o o l   ≡   ∀ α .   α → α → α {displaystyle {mathtt {Bool}} equiv forall alpha .~alpha o alpha o alpha } .

У этого типа ровно два обитателя, отождествляемых с двумя булевыми константами

t r u e   ≡   Λ α .   λ x α .   λ y α .   x {displaystyle {mathtt {true}} equiv Lambda alpha .~lambda x^{alpha }.~lambda y^{alpha }.~x} f a l s e   ≡   Λ α .   λ x α .   λ y α .   y {displaystyle {mathtt {false}} equiv Lambda alpha .~lambda x^{alpha }.~lambda y^{alpha }.~y}

Конструкция условного оператора

i f T h e n E l s e   ≡   Λ α .   λ b B o o l .   λ x α .   λ y α .   b α x y {displaystyle {mathtt {ifThenElse}} equiv Lambda alpha .~lambda b^{mathtt {Bool}}.~lambda x^{alpha }.~lambda y^{alpha }.~b,alpha ,x,y}

Эта функция удовлетворяет естественным требованиям

i f T h e n E l s e A t r u e M N = M {displaystyle {mathtt {ifThenElse}},A,{mathtt {true}},M,N=M}

и

i f T h e n E l s e A f a l s e M N = N {displaystyle {mathtt {ifThenElse}},A,{mathtt {false}},M,N=N}

для произвольного типа A {displaystyle A} и произвольных M : A {displaystyle M!:!A} и N : A {displaystyle N!:!A} . В этом легко убедиться, раскрыв определения и выполнив β {displaystyle eta } -редукции.

Тип произведения. Для произвольных типов A {displaystyle A} и B {displaystyle B} тип их декартова произведения

A × B   ≡   ∀ α .   ( A → B → α ) → α {displaystyle A imes B~equiv ~forall alpha .~(A o B o alpha ) o alpha }

населён парой

⟨ M ; N ⟩   ≡   Λ α .   λ f ( A → B → α ) .   f   M   N {displaystyle langle M;N angle ~equiv ~Lambda alpha .~lambda f^{(A o B o alpha )}.~f~M~N}

для каждых M : A {displaystyle M!:!A} и N : B {displaystyle N!:!B} . Проекции пары задаются функциями

f s t   ≡   Λ α .   Λ β .   λ p α × β .   p α ( λ x α . λ y β . x )   :   ∀ α .   ∀ β . α × β → α {displaystyle {mathtt {fst}} equiv Lambda alpha .~Lambda eta .~lambda p^{alpha imes eta }.~p,alpha ,(lambda x^{alpha }.,lambda y^{eta }.,x)~:~forall alpha .~forall eta .,alpha imes eta o alpha } s n d   ≡   Λ α .   Λ β .   λ p α × β .   p β ( λ x α . λ y β . y )   :   ∀ α .   ∀ β . α × β → β {displaystyle {mathtt {snd}} equiv Lambda alpha .~Lambda eta .~lambda p^{alpha imes eta }.~p,eta ,(lambda x^{alpha }.,lambda y^{eta }.,y)~:~forall alpha .~forall eta .,alpha imes eta o eta }

Эти функции удовлетворяют естественным требованиям f s t A B ⟨ M ; N ⟩ = M {displaystyle {mathtt {fst}},A,B,langle M;N angle =M} и s n d A B ⟨ M ; N ⟩ = N {displaystyle {mathtt {snd}},A,B,langle M;N angle =N} .

Тип суммы. Для произвольных типов A {displaystyle A} и B {displaystyle B} тип их суммы

A + B   ≡   ∀ α .   ( A → α ) → ( B → α ) → α {displaystyle A+B~equiv ~forall alpha .~(A o alpha ) o (B o alpha ) o alpha }

населён либо термом типа A {displaystyle A} , либо термом типа B {displaystyle B} , в зависимости от применённого конструктора

i n j L M   ≡   Λ α . λ f A → α . λ g B → α . f M {displaystyle {mathtt {injL}},M~equiv ~Lambda alpha .,lambda f^{A o alpha }.,lambda g^{B o alpha }.,f,M} i n j R N   ≡   Λ α . λ f A → α . λ g B → α . g N {displaystyle {mathtt {injR}},N~equiv ~Lambda alpha .,lambda f^{A o alpha }.,lambda g^{B o alpha }.,g,N}

Здесь M : A {displaystyle M!:!A} , N : B {displaystyle N!:!B} . Функция, осуществляющая разбор случаев (сопоставление с образцом), имеет вид

m a t c h   ≡   Λ α . Λ β . Λ γ . λ s α + β . λ f α → γ . λ g β → γ . s γ f g   :   ∀ α .   ∀ β .   ∀ γ .   α + β → ( α → γ ) → ( β → γ ) → γ {displaystyle {mathtt {match}}~equiv ~Lambda alpha .,Lambda eta .,Lambda gamma .,lambda s^{alpha +eta }.,lambda f^{alpha o gamma }.,lambda g^{eta o gamma }.,s,gamma ,f,g~:~forall alpha .~forall eta .~forall gamma .~alpha +eta o (alpha o gamma ) o (eta o gamma ) o gamma }

Эта функция удовлетворяет следующим естественным требованиям

m a t c h A B C ( i n j L M ) F G = F M {displaystyle {mathtt {match}},A,B,C,({mathtt {injL}},M),F,G=F,M}

и

m a t c h A B C ( i n j R N ) F G = G N {displaystyle {mathtt {match}},A,B,C,({mathtt {injR}},N),F,G=G,N}

для произвольных типов A {displaystyle A} , B {displaystyle B} и C {displaystyle C} и произвольных термов F : A → C {displaystyle F!:!A o C} и G : B → C {displaystyle G!:!B o C} .

Числа Чёрча. Тип натуральных чисел в системе F

N a t   ≡   ∀ α .   α → ( α → α ) → α {displaystyle {mathtt {Nat}} equiv forall alpha .~alpha o (alpha o alpha ) o alpha }

населён бесконечным количеством различных элементов, получаемых посредством двух конструкторов z e r o : N a t {displaystyle {mathtt {zero}}!:!{mathtt {Nat}}} и s u c c : N a t → N a t {displaystyle {mathtt {succ}}!:!{mathtt {Nat}} o {mathtt {Nat}}} :

z e r o   ≡   Λ α . λ z α . λ s α → α . z {displaystyle {mathtt {zero}} equiv Lambda alpha .,lambda z^{alpha }.,lambda s^{alpha o alpha }.,z} s u c c   ≡   λ n N a t . Λ α . λ z α . λ s α → α . s ( n α z s ) {displaystyle {mathtt {succ}} equiv lambda n^{mathtt {Nat}}.,Lambda alpha .,lambda z^{alpha }.,lambda s^{alpha o alpha }.,s,(n,alpha ,z,s)}

Натуральное число n {displaystyle n} может быть получено n {displaystyle n} -кратным применением второго конструктора к первому или, эквивалентно, представлено термом

n ¯   ≡   Λ α . λ z α . λ s α → α . s ( s ( s … ( s ⏟ n z ) … ) ) {displaystyle {overline {n}} equiv Lambda alpha .,lambda z^{alpha }.,lambda s^{alpha ightarrow alpha }.,underbrace {s(s(sldots (s} _{n},z)ldots ))}

Свойства

  • Просто типизированная система обладает свойством типовой безопасности: при β {displaystyle eta } -редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
  • В своей диссертации Жан-Ив Жирар показал, что Система F обладает свойством сильной нормализации: любой допустимый терм за конечное число β {displaystyle eta } -редукций приводится к единственной нормальной форме.
  • Система F является импредикативной системой, поскольку переменная типа, связываемая квантором всеобщности при определении универсального типа, может замещаться самим определяемым объектом. Например, терм id {displaystyle { exttt {id}}} единичного типа ⊤ ≡ ∀ α .   α → α {displaystyle op equiv forall alpha .~alpha o alpha } может быть применён к собственному типу, порождая терм типа ⊤ → ⊤ {displaystyle op o op } . Как показал Джо Уэллс в 1994 году, задача вывода типов для версии Карри Системы F неразрешима. Поэтому при практической реализации языков программирования обычно используют ограниченные, предикативные версии полиморфизма: пренекс-полиморфизм (полиморфизм в стиле ML), полиморфизм ранга 2 и т.п. В случае пренекс-полиморфизма областью определения переменных типа служат только типы без кванторов. В этих системах задача вывода типов разрешима, такой вывод базируется на алгоритме Хиндли — Милнера.
  • Соответствие Карри — Ховарда связывает Систему F с минимальной интуиционистской логикой высказываний второго порядка, формулы которой построены из пропозициональных переменных с помощью импликации и универсальной квантификации по высказываниям. При этом значения ⊤ {displaystyle op } (истина), ⊥ {displaystyle ot } (ложь), связки ¬ {displaystyle lnot } (отрицание), ∧ {displaystyle land } (конъюнкция) и ∨ {displaystyle lor } (дизъюнкция), а также ∃ {displaystyle exists } (квантор существования) могут быть определены так
⊤   ≡   ∀ α . α → α {displaystyle op ~equiv ~forall alpha .,alpha o alpha } ⊥   ≡   ∀ α . α {displaystyle ot ~equiv ~forall alpha .,alpha } ¬ A   ≡   A → ⊥ {displaystyle lnot A~equiv ~A o ot } A ∧ B   ≡   ∀ α . ( A → B → α ) → α {displaystyle Aland B~equiv ~forall alpha .,(A o B o alpha ) o alpha } A ∨ B   ≡   ∀ α . ( A → α ) → ( B → α ) → α {displaystyle Alor B~equiv ~forall alpha .,(A o alpha ) o (B o alpha ) o alpha } ∃ α . M [ α ]   ≡   ∀ γ . ( ∀ α . M [ α ] → γ ) → γ {displaystyle exists alpha .,M[alpha ]~equiv ~forall gamma .,(forall alpha .,M[alpha ] o gamma ) o gamma }

Отметим, что соответствие Карри — Ховарда ставит в соответствие истине — единичный тип, лжи — пустой тип, конъюнкции — произведение типов, а дизъюнкции — их сумму.


Имя:*
E-Mail:
Комментарий: