Математические модели вычислений

λ-исчисление с простыми типами

Расширения типизированного λ-исчисления

Полиморфное λ-исчисление

λ-исчисление с конструкторами типов

https://maxxk.github.io/formal-models/

λ-исчисление с простыми типами

τ≡ b | τ₁ → τ₂, b ∈ B.


Γ, x : α ⊦ x : α

c_α — постоянная типа α
Γ ⊦ c: α

Γ, x : σ ⊦ e : τ
Γ ⊦ (λ x_σ . e) : σ → τ

Γ ⊦ x : σ → τ Γ ⊦ y : σ
Γ ⊦ x · y : τ

Исчисление высказываний / соответствие Карри-Говарда

Типы можно рассматривать как импликативные суждения (α → β — импликация). Доказательства — термы, имеющие этот тип.

Импликативный фрагмент схем аксиом исчисления высказываний:

A → (B → A) — абстракция

a₁ ≡ λx_A.λy_B.x : A → (B → A) Комбинатор K (K x y = x)

Действие правила modus ponens:

Γ ⊦ z : A Γ ⊦ a₁ : A → (B → A)
Γ ⊦ a₁ · z : B → A

Редукция («упрощение доказательства»): a₁ · z ≡ (λx_A.λy_B.x) · z ⟶ λy_B.z

Исчисление высказываний / соответствие Карри-Говарда

(A → (B → C)) → ((A → B) → (A → C)) — «композиция»

a₂ ≡ λ g_A→(B→C) . λ f_A→B . λ x_A . g · x · (f · x)

a₂ : (A → (B → C)) → ((A → B) → (A → C))

Комбинатор S (S g f x = g x (f x))

Вывод типа a₂ : (A → (B → C)) → ((A → B) → (A → C))

Правило	Формула
T-Abs для g	Γ, g : A → (B → C) ⊦ λ f_A→B . λ x_A . g · x · (f · x) : (A → B) → (A → C)
T-Abs для f	Γ, g : A → (B → C), f : A → B ⊦ λ x_A . g · x · (f · x) : A → C
T-Abs для x	Γ, g : A → (B → C), f : A → B, x : A ⊦ g · x · (f · x) : A → C
T-App для g · x	Γ, g : A → (B → C) ⊦ g : A → (B → C) Γ, x : A ⊦ x : A g · x : B → C
T-App для f · x	(аналогично)
T-App для (g · x) · (f · x)	(аналогично)

Типы данных для λ-исчисления с простыми типами

Пустой тип

τ = … ⟂ …

Γ ⊦ x : ⊥
Γ ⊦ exfalso_α(x) : α

Отрицание:

не α ≡ α → ⟂

Тип из одного элемента

τ = … T …

Γ ⊦ () : T

Произведение (конъюнкция; кортеж)

τ = … α × β …

Введение:

Γ ⊦ x : α Γ ⊦ y : β
Γ ⊦ (x, y) : α × β

Удаление:

Γ ⊦ p : α × β
Γ ⊦ fst p : α

Γ ⊦ p : α × β
Γ ⊦ snd p : β

Редукция: fst (x, y) ⟶ x snd (x, y) ⟶ y

Операция каррирования: (α×β → γ) → α → β → γ

Можно сравнить с аксиомами исчисления высказываний для конъюнкции: https://maxxk.github.io/formal-models/presentations/04-Logics.html#%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5-%D0%B2%D1%8B%D1%81%D0%BA%D0%B0%D0%B7%D1%8B%D0%B2%D0%B0%D0%BD%D0%B8%D0%B9

Сумма (дизъюнкция; алгебраические типы данных)

τ = … α + β …

Введение:

Γ ⊦ x : α
Γ ⊦ inl_β x : α + b

Γ ⊦ y : β
Γ ⊦ inr_α y : α + b

Удаление:

Γ ⊦ x : α + β Γ ⊦ s : α → γ Γ ⊦ t : β → γ
Γ ⊦ switch_γ(x, s, t) : γ

Редукция:

switch_γ(inl_β a, s, t) ⟶ s · a switch_γ(inr_α b, s, t ) ⟶ t · b

Типы для простого императивного ЯП

Просто типизированное λ-исчисление можно использовать как основу для системы типов простого языка программирования (скорее Pascal-подобного, чем C-подобного).

extern int callback(int);
extern void set_callback(int (*cb)(int));

int main(int argc, StringArray argv) {
  double x;
  x = callback(0);
  set_callback(callback);
  return callback(argc);
}

Программу на простом императивном языке можно транслировать в просто типизированное λ-исчисление и получить средство проверки типов. Наборы аргументов — произведения. Если аргументов более двух, как правило, считаем произведение правоассоциативным:

int × StringArray × double × int = int × (StringArray × (double × int)). Доступ к аргументам тогда осуществляется с использованием последовательности термов snd.

λ callback_int→int. λ set_callback_{(int→int)→T}. λ main_args_{int×StringArray→int}. λ get_x_double. λ set_x_double→T. (set_x · (callback · 0), set_callback · callback, callback · fst main_args ) : T × T × int

Задачи анализа термов λ-исчисления

Задача проверки типов (Type Checking). Даны терм T и тип σ. Определить, имеет ли T тип σ (фактически — построить вывод в формальной системе).
Задача вывода типа (Type Inference). Дан терм T. Найти тип терма, если терм корректно типизирован, или указать на нарушение условий типизации.
Задача поиска доказательства (обитаемости типа, Type Inhabitation). Дан тип σ. Определить, существует ли терм, имеющий такой тип и, если он существует, предъявить такой терм.
Задача эквивалентности типов. Даны типы σ и τ. Определить, эквивалентны ли они.

Для λ-исчисления с простыми типами все эти задачи разрешимы, в частности, четвёртая — тривиальна.

(слайд по мотивам презентации по ссылке; сам курс Д.Н. Москвина можно рекомендовать как дополнительный источник по предыдущей, этой и, частично, следующей лекциям)

Двусторонний алгоритм проверки типов

Введём дополнительный терм «аннотация типов», подсказку для алгоритма проверки типов:

Определим две функции:

Вывод неизвестного типа

infer : Контекст → Терм → Тип?

infer(Γ, x) = τ ⇒ Γ ⊦ x : τ

infer(… ∪ x : τ ∪ …, x) ≡ τ

infer(Γ, c) = α, где c — константа типа α

infer(Γ, x · y) = 
  if infer(Γ, x) = α → β 
    and check(y, α) 
  then β 
  else fail

infer(Γ, (x : τ)) = 
  if check(x, τ) 
  then τ 
  else fail

infer(Γ, λ x_α . y) = α → infer(Γ ∪ x : α, y)

Γ ⊦ x : τ
Γ ⊦ (x : τ) : τ

Проверка известного типа

check : Контекст → Терм → Тип → 2

check(Γ, x, τ) = 1 ⇔ Γ ⊦ x : τ

check(Γ, λx.y, α → β) = check(Γ ∪ x : α, y, β)

check(Γ, x, τ) = infer(Γ, x) == τ

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

Подробнее можно поискать по запросу bidirectional typechecking и в каталоге code в репозитории с презентациями.

Метапеременные и унификация

В λ-исчислении с простыми типами (особенно в версии с аннотацией типов) приходится упоминать типы чаще, чем хотелось бы:

λ x_α→β. (λ y_{(α→β)→(γ→δ)}. y · x)

Разрешим вводить метапеременные типов — «прочерки», заполняемые в процессе проверки типов.

λ x_α→β . λ y_{1→(γ→δ)} . y · x

Задача унификации — для двух типов с метапеременными найти такую подстановку (набор значений метапеременных), что в результате подстановки типы будут эквивалентны.

1 ≡ α → β

Если эквивалентность типов тривиальна, то задача унификации разрешима.

Существует основанный на унификации более сложный алгоритм проверки типов (алгоритм Хиндли-Милнера), который не требует аннотаций. Описан, например, в курсе по ссылке.

Полиморфизм

Why no generics in λ→?

Аксиомы импликации A1 и A2 заданы в терминах λ-исчисления с простыми типами для фиксированных типов (высказываний) A, B, C. Для каждого нового типа (высказывания) нужно заново записывать эти аксиомы.

Функция идентичного преобразования id ≡ λx₁.x имеет отдельные несовместимые типы 1→1 для каждого типа x.

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

Пример: тип полиморфной функции сортировки: ∀ α . (α → α → 2) → List α → List α

Для определённых значений α: (int → int → 2) → List int → List int

Композиция: f ∘ g ≡ g(f(x)) ≡ λf.λg.λx. g · (f · x) : ∀ α β γ. (β → γ) → (α → β) → α → γ

Система F (λ2)

Жирар (1976), Рейнольдс (1974).

Тип τ ≡ α | α → β | ∀ α . τ (добавим переменные и полиморфный тип)

Термы M ≡ x | λ x : τ . M | M · N | Λ α . M | M · τ (добавим абстракцию и применение типов)

Редукция: β-редукция и аналогичная ей ɩ-редукция для типов: (Λα.M) · τ ⟶_ɩ M[α := τ].

В Coq ∀ записывается как forall, а между λ и Λ не делается различия.

Контексты

Для суждений типизации теперь нужно ввести понятие корректно сформированного (well-formed) контекста (т.е. контекста, в котором все переменные типов сначала объявляются, а затем уже используются):

Суждение Γ wf:


[] wf

Γ wf τ ∈ Γ
Γ, x : τ wf

Γ wf α не входит в типы в Γ
Γ, α wf

Для реализации проще обратиться к индексам де Брёйна для типов.

Существование типа (α : *) в корректно сформированном Γ:

Γ wf α ∈ Γ
Γ ⊦ α : *

Γ wf Γ ⊦ α : * Γ ⊦ β : *
Γ ⊦ α → β : *

Γ, α wf Γ, α ⊦ β : *
Γ ⊦ ∀α.β : *

Типизация

Правила типизации λ-исчисления с простыми типами (для абстракции и применения) входят в состав системы F, но только для корректно сформированных контекстов:

Γ, x : α wf
Γ ⊦ x : α

Правила типизации для полиморфных типов:

Γ ⊦ ∀ α . β : * Γ, α : * ⊦ M : β
Γ ⊦ Λα.M : ∀α . β

Γ ⊦ X : ∀α.β Γ ⊦ γ : *
Γ ⊦ X · γ : β[α := γ]

Свойства системы F

Для системы F выполняется свойство сильной нормализации (все корректно типизированные программы завершаются).
Задачи анализа типов (проверки типа, вывода типа, обитаемости типа) для системы F без явных аннотаций типов неразрешимы.
Эквивалентность типов разрешима.
На практике используют двустороннюю проверку типов с аннотациями типов. Если проверка типов не завершилась за некоторое «разумное» время, нужно добавить дополнительную аннотацию типа.

Типы данных в системе F

Типы данных, которые вводились для λ-исчисления с простыми типами в форме отдельных правил типизации, в λ2 представимы без отдельных правил, чаще всего — путём кодирования типа терма удаления.

Пустой тип

⊥ ≡ ∀α.α (exfalso)

Тривиальный тип

T ≡ ∀α. α → α (тип функции идентичности) 1 ≡ Λα.λx.x

Тип из двух элементов

2 ≡ ∀α.α → α → α true ≡ Λα. λ x y. x false ≡ Λα. λ x y . y

Типы данных в системе F

Условный оператор

if : ∀α. 2 → α → α → α if ≡ Λα. λ cond onTrue onFalse. cond · onTrue · onFalse

Произведение

A × B ≡ ∀α. (A → B → α) → α (a, b) ≡ Λα. λ f. f · a · b

Сумма

A + B ≡ ∀α. (A → α) → (B → α) → α inl a ≡ Λα.λf g. f · a inr b ≡ Λα.λf g. g · b

Типы данных в системе F

Нумерал Чёрча (натуральные числа)

ℕ ≡ ∀α. α → (α → α) → α

0 ≡ Λα. λz s. z

x+1 ≡ λx. Λα. λ z s. s · (n · α · z · s)

Натуральные числа задают понятие итерации.

Полиморфный список (!)

List β ≡ ∀β. ∀ α. α → (β → α → α) → α

[] ≡ Λα. λx. λf. x

head ; Tail ≡ Λβ. Λα. λ Tail_List β. λ headᵦ . λ x . λ f . Tail · x · (f · head · x)

Сравните определение нумералов и списка.

Аналогично — деревья и другие индуктивные структуры данных.

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

Исчисление высказываний представимо в системе F в терминах соответствия Карри-Говарда (аналогично λ-исчислению с простыми типами).

Дополнительно представимы кванторы по типам: ∀α.β

Квантор существования определяется следующим образом: ∃α.τ ≡ ∀β. (∀α . τ → β) → β

Задачи

Задача 6.1. *: Вывести в λ-исчислении с простыми типами, дополненном типами данных, аксиомы исчисления высказываний для конъюнкции, дизъюнкции и для отрицания, кроме аксиомы двойного отрицания или исключенного третьего.

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

Задача 6.2. *: Реализовать в системе F сортировку списка булевских значений 2.
Задача 6.3. **: Доказать, что аксиома двойного отрицания или аксиома исключённого третьего невыводима в λ-исчислении с простыми типами, дополненном типами данных.

Задачи

Для программ, которые являются решением задач 6.4, входом является пара строк — терм λ-исчисления, записанного в синтаксисе на ваш выбор (но в таком, чтобы можно было записать достаточно сложные примеры) и тип. Выходом является ответ «да» (терм имеет заданный тип) или «нет» (терм не имеет заданный тип). К решению должно прилагаться несколько нетривиальных примеров входов, как с положительным так и с отрицательным результатом проверки.

Задача 6.4а. **: Реализовать проверку типов для λ-исчисления с простыми типами, дополненного типами данных.
Задача 6.4б. ***: Реализовать проверку типов для системы F (полиморфного λ-исчисления).

Задачи

Задача 6.4в. ****: Реализовать проверку типов для системы F_ω (полиморфного λ-исчисления с конструкторами типов).

Бонусные ** к задачам 6.4 — реализовать транслятор из простого императивного языка программирования в набор термов и проверку типов для программ на таком языке.

PLAY