Анотація

Мова програмування — це внутрішня мова декартово-замкнених категорій, що реалізує функціональні обчислення через лямбда-абстракцію, аплікацію, стрілкові типи, одиничний тип та добутки. Вона забезпечує строгу типізацію та відповідає структурі CCC.

Синтаксис

Терми складаються зі змінних, зірки (тип типів), стрілкових типів, лямбда-абстракцій, аплікацій, одиничного типу, добутків, пар та їх проекцій. Мова підтримує строгі типи, забезпечуючи типобезпеку.

I = #identifier
STLC = I | Star | Arrow (STLC, STLC) | Lam (I, STLC, STLC)
       | App (STLC, STLC) | Unit | Prod (STLC, STLC)
       | Pair (STLC, STLC) | Pr1 STLC | Pr2 STLC

type term =
    | Var of string
    | Star
    | Arrow of term * term
    | Lam of string * term * term
    | App of term * term
    | Unit
    | Prod of term * term
    | Pair of term * term
    | Pr1 of term
    | Pr2 of term

Правила обчислень

Обчислення в базуються на бета-редукції для аплікацій та редукції для проекцій пар, з підтримкою eta-рівності.

App (Lam (x, A, t), u) → subst x u t        (* β-редукція *)
Pr1 (Pair (t,unofficial, u)) → t            (* π1-редукція *)
Pr2 (Pair (t, u)) → u                       (* π2-редукція *)
Lam (x, A, App (t, Var x)) → t              (* η-рівність *)

$β$

$π$

Правила типізації

Типізація в забезпечує, що кожен терм має коректний тип. Основні правила включають:

(* Контекст: Γ = список пар (x : A) *)
Var x : A                     (* якщо (x : A) ∈ Γ *)
Star : Star                   (* тип типів *)
Arrow (A, B) : Star          (* якщо A : Star, B : Star *)
Lam (x, A, t) : Arrow (A, B) (* якщо Γ ⊢ A : Star, Γ, x : A ⊢ t : B *)
App (t, u) : B               (* якщо t : Arrow (A, B), u : A *)
Unit : Star                   (* одиничний тип *)
Prod (A, B) : Star           (* якщо A : Star, B : Star *)
Pair (t, u) : Prod (A, B)    (* якщо t : A, u : B *)
Pr1 t : A                    (* якщо t : Prod (A, B) *)
Pr2 t : B                    (* якщо t : Prod (A, B) *)

Підстановка

Підстановка в замінює змінну на терм, зберігаючи типобезпеку.

let rec subst x s = function
    | Var y -> if x = y then s else Var y
    | Arrow (a, b) -> Arrow (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)
    | Prod (a, b) -> Prod (subst x s a, subst x s b)
    | Pair (t1, t2) -> Pair (subst x s t1, subst x s t2)
    | Pr1 t -> Pr1 (subst x s t)
    | Pr2 t -> Pr2 (subst x s t)
    | t -> t

Редукція

Редукція виконує бета-редукцію та редукцію проекцій для активних пар.

let rec reduce ctx t = match t with
    | App (Lam (x, _, b), a) -> subst x a b
    | App (f, a) -> App (reduce ctx f, reduce ctx a)
    | Pr1 (Pair (t1, _)) -> t1
    | Pr2 (Pair (_, t2)) -> t2
    | Pr1 t -> Pr1 (reduce ctx t)
    | Pr2 t -> Pr2 (reduce ctx t)
    | _ -> t

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

Нормалізація повторює редукцію до досягнення нормальної форми.

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

Внутрішня мова CCC

Доведення, що є внутрішньою мовою декартово-замкнених категорій:

Ці конструктори відповідають аксіомам CCC:

позначає об'єкти категорії (типи), моделює експоненціальний об'єкт , відповідає морфізму , реалізує оцінку , є термінальним об'єктом , для якого є унікальним, моделює декартовий добуток , створює пару , і є проекціями та , позначає об'єкти категорії.

Лямбда-абстракція та аплікація відповідають структурі CCC:

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

[1]. Church, A. A Formulation of the Simple Theory of Types. 1940
[2]. Guallart, N. An Overview of Type Theories. 2014
[3]. García, M. Category Theory and Lambda Calculus. 2020

Alonzo

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