henk.pug

include header

html
    head
        meta(property='og:title'       content='HENK')
        meta(property='og:description' content='Чиста система типів CoC')
        meta(property='og:url'         content='https://henk.groupoid.space/')

block title
    title HENK

block content
    +header('', 'Henk', 'Мінімальна мова з квантором узагальнення та зліченою кількістю універсумів для послідовних обчислень в локальних декартово-замкнених категоріях')
    article.main
        .exe
            section
                h1 Анотація
            aside Намдак Тонпа
                time ДАТА: 10 ЖОВТНЯ 2016
            section
                +tex.
                    Мова програмування $\mathbf{Henk}$ — це залежно-типізоване лямбда-числення вищого порядку,
                    розширення числення конструкцій (Кокан, Юе) зі зліченою ієрархією предикативних і непредикативних універсумів.

        .semantics
            section
                h2#nat Універсуми
                p.
                    Нескінченна ієрархія універсумів дозволяє уникати парадоксів (Жирара, Рассела, Гуркенса)
                    у теорії типів (Мартіна-Льофа).
                code.
                    U₀ : U₁ : U₂ : U₃ : …

                    U₀ — пропозиції
                    U₁ — значення та множини
                    U₂ — типи
                    U₃ — сорти
                br
                +tex(true).
                    $$
                      \begin{equation}
                      \tag{S}
                      \dfrac
                      {o : Nat}
                      {Type_o}
                      \end{equation}
                    $$

                h2#axioms Предикативні універсуми
                p.
                    Усі терми підкоряються рейтингу <b>A</b> у послідовності універсумів <b>S</b>,
                    а складність <b>R</b> залежного терму дорівнює максимуму складності терму та його залежності.
                    Система універсумів повністю описується наступною нотацією PTS (за Барендрегтом):
                code.
                    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) — предикативні
                br.
                p.
                    Зверніть увагу, що предикативні універсуми несумісні з кодуванням лямбда-термів за Чьорчем.
                    Ви можете перемикатися між предикативними та непредикативними універсумами за допомогою параметра перевірки типів.
                +tex(true).
                    $$
                    \begin{equation}
                    \tag{A₁}
                    \dfrac
                    {i: Nat,\ \ \ \ j: Nat,\ \ \ \ i < j}
                    {Type_i : Type_{j}}
                    \end{equation}
                    $$
                +tex(true).
                    $$
                    \begin{equation}
                    \tag{R₁}
                    \dfrac
                    {i : Nat,\ \ \ \ j : Nat}
                    {Type_i \rightarrow Type_{j} : Type_{max(i,j)}}
                    \end{equation}
                    $$

                h2#axioms Непредикативні універсуми
                p.
                    Пропозиційний контрактний нижній простір — єдине доступне розширення предикативної ієрархії,
                    яке не призводить до неконсистентності. Однак є інший варіант із нескінченною
                    непредикативною ієрархією.
                code.
                    A₂   (n : nat) = U n : U (n + 1) — некумулятивні
                    R₂ (m n : nat) = U m ⟶ U n : U n — непредикативні
                br.
                +tex(true).
                    $$
                    \begin{equation}
                    \tag{A₂}
                    \dfrac
                    {i: Nat}
                    {Type_i : Type_{i+1}}
                    \end{equation}
                    $$
                +tex(true).
                    $$
                    \begin{equation}
                    \tag{R₂}
                    \dfrac
                    {i : Nat,\ \ \ \ j : Nat}
                    {Type_i \rightarrow Type_{j} : Type_{j}}
                    \end{equation}
                    $$

                h2#ast Мова з єдиною аксіомою
                p.
                    Ця мова називається мовою з єдиною аксіомою (або чистою), оскільки елімінатор
                    та введення спряжених функторів виводяться з правила формування типів.
                    Єдиним правилом обчислення для типу Пі є бета-редукція.
                code.
                    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) =
                br.
                +tex(true).
                    \begin{equation}
                    \tag{$\Pi$-formation}
                    \dfrac
                    {x:A \vdash B : Type}
                    {\Pi\ (x:A) \rightarrow B : Type}
                    \end{equation}
                +tex(true).
                    \begin{equation}
                    \tag{$\Pi$-intro}
                    \dfrac
                    {x:A \vdash b : B}
                    {\lambda\ (x:A) \rightarrow b : \Pi\ (x: A) \rightarrow B }
                    \end{equation}
                br.
                +tex(true).
                    $$
                    \begin{equation}
                    \tag{$\Pi$-application}
                    \dfrac
                    {f: (\Pi\ (x:A) \rightarrow B)\ \ \ a: A}
                    {f\ a : B\ [a/x]}
                    \end{equation}
                    $$
                +tex(true).
                    $$
                    \begin{equation}
                    \tag{$\beta$-rule}
                    \dfrac
                    {x:A \vdash b: B\ \ \ a:A}
                    {(\lambda\ (x:A) \rightarrow b)\ a = b\ [a/x] : B\ [a/x]}
                    \end{equation}
                    $$
                br.

                h2#ast Синтаксис
                +tex.
                    Терми $\mathbf{Henk}$ складаються з <b>nat</b>-індексованих зірок, змінних, застосувань,
                    абстракцій та універсальних кванторів. Ця мова називається Калькулем Конструкцій
                    і існує в різних синтаксисах.
                code.
                    <>  = #опція
                    I   = #ідентифікатор
                    U   = * < #число >
                    PTS = U | I | PTS → PTS | ∀ ( I : PTS ) → PTS
                        | PTS PTS | ( PTS ) | λ ( I : PTS ) → PTS
                p.
                    Еквівалентне кодування дерева HOAS для розпарсених термінів:
                code.
                    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
                br.

                h2 Універсуми
                code.
                    let universe = function
                        | Universe i -> i
                        | _ -> raise (Failure ("Expected a universe"))
                br.

                h2 Підстановка
                code.
                    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
                br.

                h2 Рівність
                code.
                    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
                br.

                h2 Редукція
                code.
                    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
                br.

                h2 Нормалізація
                code.
                    and normalize ctx t =
                        let t' = reduce ctx t in
                        if equal ctx t t' then t else normalize ctx t'
                br.

                h2 Перевірка типів
                code.
                    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
                br.

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

                h2#normal Нормалізація
                +tex.
                    Терми в мові $\mathbf{Henk}$.
                code.
                    $ 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)
                br.

                h2#erased Стирання типів
                +tex.
                    Нетипізована лямбда-мова $\mathbf{Joe}$ — найпростіша мова, що використовується в
                    $\mathbf{Henk}$ для генерації програм бекенду. Мова $\mathbf{Joe}$ використовується
                    як результат стирання типів.
                code.
                    I = #identifier
                    O = I | ( O ) | O O | λ I -> O
                +tex.
                    Терми в чистій нетипізованій лямбда-мові $\mathbf{Joe}$.
                code.
                    $ om print fst erase a "#List/Cons"
                    ( λ Head
                    → ( λ Tail
                    → ( λ Cons
                    → ( λ Nil
                    → ((Cons Head) ((Tail Cons) Nil))))))
                    ok
                br.

            section
                h1 Бібліографія
                p(style="font-size:16px;").
                    [1]. <a href="https://groupoid.space/books/vol3/henk.pdf">Issue XI: Pure Type System</a><br>
                    [2]. <a href="https://www.cse.chalmers.se/~coquand/v1.pdf">Деякі зауваження про залежну теорію типів</a><br>

include footer