HENK

Henk

Мінімальна мова з квантором узагальнення та нескінченною кількістю універсумів для послідовних обчислень в локальних декартово-замкнених категоріях

Анотація

Мова програмування — це залежно-типізоване лямбда-числення вищого порядку, розширення числення конструкцій (Кокан, Юе) з ієрархією предикативних і непредикативних універсумів.

Універсуми

Нескінченна ієрархія універсумів дозволяє уникати парадоксів (Жирара, Рассела, Гуркенса) у теорії типів (Мартіна-Льофа).

U₀ : U₁ : U₂ : U₃ : … U₀ — пропозиції U₁ — значення та множини U₂ — типи U₃ — сорти

Предикативні універсуми

Усі терми підкоряються рейтингу A у послідовності універсумів S, а складність R залежного терму дорівнює максимуму складності терму та його залежності. Система універсумів повністю описується наступною нотацією PTS (за Барендрегтом):

S (n : nat) = U n A₁ (n m : nat) = U n : U m де m > n — кумулятивні R₁ (m n : nat) = U m ⟶ U n : U (max m n) — предикативні

Зверніть увагу, що предикативні універсуми несумісні з кодуванням лямбда-термів за Чьорчем. Ви можете перемикатися між предикативними та непредикативними універсумами за допомогою параметра перевірки типів.

₁

₁

Непредикативні універсуми

Пропозиційний контрактний нижній простір — єдине доступне розширення предикативної ієрархії, яке не призводить до неконсистентності. Однак є інший варіант із нескінченною непредикативною ієрархією.

A₂ (n : nat) = U n : U (n + 1) — некумулятивні R₂ (m n : nat) = U m ⟶ U n : U n — непредикативні

₂

₂

Мова з єдиною аксіомою

Ця мова називається мовою з єдиною аксіомою (або чистою), оскільки елімінатор та введення спряжених функторів виводяться з правила формування типів. Єдиним правилом обчислення для типу Пі є бета-редукція.

Pi (A: U) (B: A -> U): U = (x: A) -> B x lambda (A: U) (B: A -> U) (b: Pi A B): Pi A B = \ (x: A) -> b x app (A: U) (B: A -> U) (f: Pi A B) (a: A): B a = f a beta (A: U) (B: A -> U) (a:A) (f: Pi A B): Equ (B a) (app A B (lambda A B f) a) (f a) =



Синтаксис

Терми складаються з nat-індексованих зірок, змінних, застосувань, абстракцій та універсальних кванторів. Ця мова називається Калькулем Конструкцій і існує в різних синтаксисах.

<> = #опція I = #ідентифікатор U = * < #число > PTS = U | I | PTS → PTS | ∀ ( I : PTS ) → PTS | PTS PTS | ( PTS ) | λ ( I : PTS ) → PTS

Еквівалентне кодування дерева HOAS для розпарсених термінів:

type term = | Var of string | Universe of int | Pi of string * term * term (* ∀ (x : a), b *) | Lam of string * term * term (* λ (x : a), b *) | App of term * term

Універсуми

let universe = function | Universe i -> i | _ -> raise (Failure ("Expected a universe"))

Підстановка

let rec subst x s = function | Var y -> if x = y then s else Var y | Pi (y, a, b) when x <> y -> Pi (y, subst x s a, subst x s b) | Lam (y, a, b) when x <> y -> Lam (y, subst x s a, subst x s b) | App (f, a) -> App (subst x s f, subst x s a) | t -> t

Рівність

let rec equal ctx t1 t2 = match t1, t2 with | Var x, Var y -> x = y | Universe i, Universe j -> i <= j | Pi (x, a, b), Pi (y, a', b') | Lam (x, a, b), Lam (y, a', b') -> equal ctx a a' && equal ((x,a) :: ctx) b (subst y (Var x) b') | Lam (x, _, b), t -> equal ctx b (App (t, Var x)) | t, Lam (x, _, b) -> equal ctx (App (t, Var x)) b | App (f, a), App (f', a') -> equal ctx f f' && equal ctx a a' | _ -> false

Редукція

and reduce ctx t = match t with | App (Lam (x, _, b), a) -> subst x a b | App (Pi (x, _, b), a) -> subst x a b | App (f, a) -> App (reduce ctx f, reduce ctx a) | _ -> t

Нормалізація

and normalize ctx t = let t' = reduce ctx t in if equal ctx t t' then t else normalize ctx t'

Перевірка типів

and infer ctx t = let res = match t with | Var x -> lookup x ctx | Universe i -> Universe (i + 1) | Pi (x, a, b) -> Universe (max (universe (infer ctx a)) (universe (infer ((x,a)::ctx) b))) | Lam (x, a, b) -> let _ = infer ctx a in Pi (x, a, infer ((x,a)::ctx) b) | App (f, a) -> match infer ctx f with | Pi (x, _, b) -> subst x a b | t -> raise (Failure "Requires a Pi type.") in normalize ctx res

Використання

Нормалізація

Терми в мові .

$ om show List/Cons λ (A: *) → λ (Head: A) → λ (Tail: ∀ (List: *) → ∀ (Cons: ∀ (Head: A) → ∀ (Tail: List) → List) → ∀ (Nil: List) → List) → λ (List: *) → λ (Cons: ∀ (Head: A) → ∀ (Tail: List) → List) → λ (Nil: List) → Cons Head (Tail List Cons Nil)

Стирання типів

Нетипізована лямбда-мова — найпростіша мова, що використовується в для генерації програм бекенду. Мова використовується як результат стирання типів.

I = #identifier O = I | ( O ) | O O | λ I -> O

Терми в чистій нетипізованій лямбда-мові .

$ om print fst erase a "#List/Cons" ( λ Head → ( λ Tail → ( λ Cons → ( λ Nil → ((Cons Head) ((Tail Cons) Nil)))))) ok

Бібліографія

[1]. Додаток I: Чиста система типів для Erlang
[2]. Деякі зауваження про залежну теорію типів