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

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

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

λ-исчисление с зависимыми типами

maxim.krivchikov@gmail.com

Пример: чего мы хотим добиться?

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

Более амбициозная задача для проверки типов: контролировать нетривиальные свойства кода, например, определять при компиляции ошибки типа «выход за границы массива».

Пример: метод прогонки

// Tridiagonal algorithm (solution for the tridiagonal system of linear equations)
// (d, c, e) - matrix of the linear system
// n - matrix size
// d - diagonal elements
// c - subdiagonal elements
// e - superdiagonal elements
// a - superdiagonal gaussian elimination coefficients
// b - right hand side
// x - answer
void tridiagonal(int n, double* d, double* c, 
    double* e, double* a, double* b, int* x) {

    a[1] = -e[0] / d[0]; 
    b[1] = b[0]  / d[0];

    for (int i=1; i < n; i++) {
        double denominator = d[i] + c[i]*a[i];
        a[i+1] = -e[i]  / denominator;
        b[i+1] = (1. - c[i])*b[i] / denominator;
    }

    x[n] = (1. - c[n])*b[n]*(d[n] + c[n]*a[n]); 
    for (int j=n-1; j >=0; j--) {
        x[j] = a[j]*x[j+1] + b[j+1];
    }
}

Прогонка с простыми типами

Variable (int double DoubleArray IntArray : Type).
Variable (toInt : nat -> int) (toDouble : nat -> double).
Variable (set : DoubleArray -> int -> double -> unit)
  (get : DoubleArray -> int -> double)
  (add sub div mul : double -> double -> double)
  (neg : double -> double)
  (inc dec : int -> int)
  (loop : int -> int -> (int -> unit) -> unit).

Definition tridiagonal (n : int) (d c e a b : DoubleArray) (x : IntArray) := (
  set a (toInt 1) (div (neg (get e (toInt 0))) (get d (toInt 0))),
  set b (toInt 1) (div (get b (toInt 0)) (get d (toInt 0))),

  loop (toInt 1) n (fun i => let 
    denominator := (add (get d i) (mul (get c i) (get a i))) in
    let body := (
      set a (inc i) (div (get e i) denominator),
      set b (inc i) (div (mul (sub (toDouble 1) (get c i)) (get b i)) denominator)
    )
    in tt),

  set x n (mul (mul (sub (toDouble 1) (get c n)) (get b n)) (add (get d n) (mul (get c n) (get a n)))),
  loop (dec n) (toInt 0) (fun j =>  let
    body := set x j (add (get b (inc j)) (mul (get a j) (get x (inc i))))
  in tt)
).

Операторы над типами

Как определить тип абстрактного массива?

• λ (x : α). M — абстракция термов по термам λ (x : int). x

• Λ (α : *). M — абстракция термов по типам Λ (α : *) (β : *) . λ (p : α × β) . fst p

• Требуется — абстракция типов по типам

α — тип (type) * — вид (kind, «тип типов»)

Для абстракции типов по типам нужно «перенести» λ-исчисление с простыми типами на уровень выше («λ-исчисление с простыми видами»).

κ = * | κ₁ ⇒ κ₂

⇒ — временно обозначим «стрелку» между видами

Абстрактный массив: Array : * ⇒ * — конструктор типа Array · double : * — тип

Эквивалентность типов в λω

Типы α и (λ(t : *).t) · α должны быть эквивалентны.

Эквивалентность типов определяется в терминах нормализации. Пусть исчисление сильно нормализуемо (для λ-исчисления с простыми видами, это верно). Тогда два типа одного вида эквивалентны, если они приводятся β-редукцией к одинаковой нормальной форме.

Примеры типов в λω

Массив с операциями:

Array : * ⇒ *

new : ∀ (α : *). int -> Array · α

get : ∀(α : *). Array · α → int → α

set : ∀(α : *). Array · α → int → α → T

Прогонка в λω

Variable (int double : Type).
Variable (Array : Type -> Type)
    (set : forall {T : Type}, Array T -> int -> T -> unit)
    (get : forall {T : Type}, Array T -> int -> T).
Variable (toInt : nat -> int) (toDouble : nat -> double).
Variable 
  (add sub div mul : double -> double -> double)
  (neg : double -> double)
  (inc dec : int -> int)
  (loop : int -> int -> (int -> unit) -> unit).

Definition tridiagonal (n : int) (d c e a b : Array double) (x : Array int) := (
  set a (toInt 1) (div (neg (get e (toInt 0))) (get d (toInt 0))),
  set b (toInt 1) (div (get b (toInt 0)) (get d (toInt 0))),

  loop (toInt 1) n (fun i => let 
    denominator := (add (get d i) (mul (get c i) (get a i))) in
    let body := (
      set a (inc i) (div (get e i) denominator),
      set b (inc i) (div (mul (sub (toDouble 1) (get c i)) (get b i)) denominator)
    )
    in tt),

  set x n (mul (mul (sub (toDouble 1) (get c n)) (get b n)) (add (get d n) (mul (get c n) (get a n)))),
  loop (dec n) (toInt 0) (fun j =>  let
    body := set x j (add (get b (inc j)) (mul (get a j) (get x (inc j))))
  in tt)
).

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

Тип равенств между типами (тип идентичности по Лейбницу):

Eq = λ (α β : *). ∀ (φ : * ⇒ *). φ α → φ β

Свойство рефлексивности задаёт конструктор равенства («введение»):

refl : ∀(α : *). Eq α α

refl = Λ(α : *). Λ(φ : * ⇒ *) . λ (x : φ α) . x

Доказуемы свойства симметричности и транзитивности:

symm : ∀ (α β : *). Eq α β → Eq β α

trans : ∀ (α β γ : *) . Eq α β → Eq β γ → Eq α γ

Доказательства:

symm = Λ(α β : *). λ (e : Eq α β). e (λ (γ : *). Eq γ α) (refl α)

trans = Λ(α β γ : *). λ (s : Eq α β) (t : Eq β γ). t (Eq α) s

Свойство подстановки по равенству:

lift : ∀ (α β : * ). ∀ (φ : * ⇒ *). Eq α β → Eq (φ α) (φ β)

lift = Λ (α β : *). Λ (φ : * ⇒ *). λ (e : Eq α β). e (λ (γ : *). Eq (φ α) (φ γ)) (refl (φ α))

К зависимым типам

Мы определили следующие виды абстракции:

• λ (x : α). M — терм ↦ терм λ (x : int). x

• Λ (α : *). M — тип ↦ терм Λ (α : *) (β : *) . λ (p : α × β) . fst p

• λ (x : κ). A — тип ↦ тип Eq = λ (α β : *). ∀ (φ : * ⇒ *). φ α → φ β

Соответствие Карри-Говарда для рассмотренных систем позволяет представлять в виде термов исчисление высказываний и различные его расширения.

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

терм ↦ тип

λ-куб Барендрегта

Barendregt H.P. Introduction to generalized type systems // J. Funct. Program. 1991. Vol. 1, № 2. P. 125–154. Общая схема, примеры, ссылки на доказательства сильной нормализации для всех систем куба.

Зависимое произведение

Π(x : α). A

α и A — типы, вместо x подставляется терм.

Массив с контролем границ

Array : * ⇒ int ⇒ *

Array double 0

Array double 10

Функция, связывающая n и длину массива:

Π (n : int) (Array double n) → Array double n

λ (n : int). (d : Array double n). d

Парадокс

Hurkens A.J.C. A simplification of Girard’s paradox // Typed Lambda Calculi and Applications / ed. Dezani-Ciancaglini M., Plotkin G. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995. Vol. 902. P. 266–278.

Терм False не нормализуем.

http://liamoc.net/posts/2015-09-10-girards-paradox.html

Уровни универсумов

При проверке типов индексы строятся в виде ориентированного графа, рёбра которого помечены < и ⩽, а потом, например, алгоритмом Тарьяна, определяется, можно ли получить на основе этого графа требуемый порядок (можно, если нет ориентированного цикла с одним из рёбер, помеченных <).

Luo Z. ECC, an extended calculus of constructions // [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science. IEEE Comput. Soc. Press, 1989. P. 386–395.

Но в итоге всё равно получается, что объявления обобщённых типов это, фактически, схемы типов, полиморфные по индексам типов:

List T ≡ λ(T : Typeᵢ). Π(R : Typeⱼ). R → (T → R → R) → R

List : Π(T : Typeᵢ).Typeₖ, k > j.

Массив с контролем границ

Длина массива — неотрицательное целое число, это не то же самое, что int. Далее обозначаем ℕ (в Coq — nat, встроенный тип натуральных чисел с нулём).

S : ℕ → ℕ

· < · : ℕ → ℕ → Type

succ_lt : Π (n : ℕ). n < S n

Array : Type → ℕ → Type

Функция получения элемента: get : Π (T : Type). (n : ℕ). (a : Array T n). (i : ℕ). (i < n) → T

Массивы зависимой длины: λ (n : ℕ). (d : Array double (S n)). (c e : Array double n). (a b x : Array n). …

Разрешимые свойства

В некоторых случаях задавать какие-то ограничения на этапе компиляции затруднительно, лучше принимать решение в процессе исполнения.

Сравнение a < b можно представить в более типизированном и менее типизированном виде:

Менее типизированный: compare(a, b) : Bool

Более типизированный (разрешение свойства a<b): compare(a, b) : {a < b} + { b ⩽ a }

В последнем случае оператор удаления case может передать полученный тип далее. В языках с зависимыми типами использовать «менее типизированный» способ разрешения свойств почти никогда не имеет смысла.

Прогонка в λΠω

./07.v

Что осталось непроверенным

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

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

λΠ (λ-исчисление с простыми зависимыми типами)

Типы могут зависеть от значений; нет полиморфизма или конструкторов типов.

Можно связать с конструктивной логикой первого порядка (?).

λΠω (исчисление конструкций)

Можно связать с конструктивным исчислением предикатов второго порядка (?).

Есть пример, демонстрирующий эквивалентность исчисления конструкций и аксиоматики IZF (интуиционистская аксиоматика Цермело-Френкеля):

B. Barras. Sets in Coq, Coq in Sets.

Литература

1. Б. Пирс. Типы в языках программирования. 2010
2. Henk Barendregt, Wil Dekkers, Richard Statman. Lambda Calculus With Types. Cambridge University Press, 2010.
3. М. Кривчиков. Формальные модели и верификация свойств программ с использованием промежуточного представления.

Глава 1, раздел 2.1, подраздел 3.2.6.

https://istina.msu.ru/dissertations/10283583/

https://istina.msu.ru/download/10295218/1kk5zk:mNYCzzLrvKtV3M6NcjnCEr_L2tI/

Задачи

Задача 7.1 *

Записать тип равенства, его свойства и их доказательства в Coq так, чтобы они прошли проверку типов.

Задача 7.2 **

Записать парадокс, вызванный циклической иерархией универсумов, в Coq и убедиться, что он не проходит проверку типов. Тип ⊥ в Coq обозначается False.

Задача 7.3 **

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

Задачи

Задача 7.4 ***

Предложить способ описания в Coq (или в термах исчисления конструкций) спецификации неинициализированного массива:

Array : Type → ℕ → ?? → Type

new : Π (T : Type) (n : ℕ) . Array T n (все элементы не инициализированы)

get : Π (T : Type) (n : ℕ) (? : ??) (a : Array T n) (i : ℕ). (i < n) → (элемент i инициализирован) → T

set : Π (T : Type) (n : ℕ) (? : ??) (a : Array T n) (i : ℕ) (t : T). (i < n) → Array T n (? + элемент i инициализирован)