ALONZO

Alonzo

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

Анотація

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