Показать меню

Лямбда-куб

18.07.2021
29

Лямбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт. Дальнейшие обобщения лямбда-куба можно получить, рассматривая чистую систему типов.

Структура λ-куба

В системах λ-куба переменные относят к одному из двух сортов: ∗ {displaystyle ast } или ◻ {displaystyle Box } . Все допустимые выражения тоже разделяются по сортам. Утверждение о принадлежности выражения к сорту надстраивается над утверждением типизации, то есть высказывание A : B : C {displaystyle A:B:C} читается так: элемент A {displaystyle A} имеет тип B {displaystyle B} и принадлежит сорту C {displaystyle C} . Сорт ∗ {displaystyle ast } используется для обычных переменных и термов λ-исчисления, сорт ◻ {displaystyle Box } — для переменных и выражений типа. Поэтому в системах λ-куба типы сорта ∗ {displaystyle ast } и элементы сорта ◻ {displaystyle Box } рассматриваются как пересекающиеся. Например, тип терма ( λ x : α . x ) : ( α → α ) : ∗ {displaystyle (lambda x:alpha .,x):(alpha o alpha ):ast } может быть записан как элемент более «высокого» сорта ( α → α ) : ∗ : ◻ {displaystyle (alpha o alpha ):ast :Box } . Типы сорта ◻ {displaystyle Box } иногда называют родами.

Под зависимостью понимается возможность определять и использовать функции отображающие элементы одного сорта в другой (или тот же). Элементы сорта s 1 {displaystyle s_{1}} зависят от элементов сорта s 2 {displaystyle s_{2}} , если:

  • для допустимого выражения F [ x ] : τ : s 1 {displaystyle F[x]: au :s_{1}} , возможно содержащего переменную x : σ : s 2 {displaystyle x:sigma :s_{2}} , мы можем определить лямбда-абстракцию ( λ x : σ . F [ x ] ) : ( σ → τ ) : s 1 {displaystyle (lambda x:sigma .,F[x]):(sigma o au ):s_{1}} ;
  • для функции G : ( σ → τ ) : s 1 {displaystyle G:(sigma o au ):s_{1}} должно быть допустимо её применение к элементу Y : σ : s 2 {displaystyle Y:sigma :s_{2}} , при этом результат должен быть элементом типа τ {displaystyle au } сорта s 1 {displaystyle s_{1}} , то есть ( G Y ) : τ : s 1 {displaystyle (G,Y): au :s_{1}} .

Базовой вершиной куба служит система λ → {displaystyle lambda ^{ ightarrow }} , соответствующая просто типизированному лямбда-исчислению. Термы (элементы сорта ∗ {displaystyle ast } ) зависят от термов; типы (элементы сорта ◻ {displaystyle Box } ) в зависимостях не участвуют. Три оси, выходящие из базовой вершины, порождают следующие системы:

  • термы, зависящие от типов: система λ 2 {displaystyle lambda 2} (лямбда-исчисление с полиморфными типами, система F);
  • типы, зависящие от типов: система λ ω _ {displaystyle lambda {underline {omega }}} (лямбда-исчисление с операторами над типами);
  • типы, зависящие от термов: система λ P {displaystyle lambda P} (лямбда-исчисление с зависимыми типами).

Остальные системы представляют собой различные комбинации перечисленных зависимостей. Наиболее богатая система λ P ω {displaystyle lambda Pomega } (полиморфное лямбда-исчисление высшего порядка с зависимыми типами) фактически представляет собой исчисление конструкций.

Свойства систем λ-куба

Все системы лямбда-куба обладают свойством сильной нормализации: любой допустимый терм (и тип) за конечное число β-редукций приводится к единственной нормальной форме.

Поддержка в языках программирования

Различные функциональные языки поддерживают различное подмножество представленных в лямбда-кубе систем типов.

  • Haskell, ML — λ2 (система F)
  • В ограниченной форме Haskell (в реализации GHC начиная с последних версий) поддерживает λ ω _ {displaystyle lambda {underline {omega }}} с помощью «type families».
  • Coq, Agda — λ P ω {displaystyle lambda Pomega } (исчисление конструкций)
Еще по этой теме:
Лямбда-функция
13:00, 22 январь
Лямбда-функция
Термином «лямбда-функция» в точных науках может называться практически любая функция, обозначаемая греческой буквой «лямбда» (λ или Λ). Математика Примеры распространённых лямбда-функций:
Уравнения Чаплыгина
02:07, 18 декабрь
Уравнения Чаплыгина
Уравнения Чаплыгина — уравнения динамики неголономной системы. Получены С. А. Чаплыгиным в 1895 году. Позволяют упростить уравнения динамики неголономных систем путём исключения из уравнений динамики
Наращённый усечённый куб
22:54, 13 декабрь
Наращённый усечённый куб
Наращённый усечённый куб — один из многогранников Джонсона (J66, по Залгаллеру — М11+М5). Составлен из 22 граней: 12 правильных треугольников, 5 квадратов и 5 правильных восьмиугольников. Среди
Существенно особая точка
14:44, 12 декабрь
Существенно особая точка
Изолированная особая точка z 0 {displaystyle z_{0}} функции f (
Граф Кэли
19:23, 10 декабрь
Граф Кэли
Граф Кэли — граф, который строится по группе с выделенной системой образующих. Назван в честь Артура Кэли. Определение Пусть дана дискретная группа G
Максимальный тор
12:52, 03 декабрь
Максимальный тор
Максимальный тор связной вещественной группы Ли G {displaystyle G} — связная компактная коммутативная подгруппа Ли T
Комментарии:
Добавить комментарий
Ваше Имя:
Ваш E-Mail:
  • bowtiesmilelaughingblushsmileyrelaxedsmirk
    heart_eyeskissing_heartkissing_closed_eyesflushedrelievedsatisfiedgrin
    winkstuck_out_tongue_winking_eyestuck_out_tongue_closed_eyesgrinningkissingstuck_out_tonguesleeping
    worriedfrowninganguishedopen_mouthgrimacingconfusedhushed
    expressionlessunamusedsweat_smilesweatdisappointed_relievedwearypensive
    disappointedconfoundedfearfulcold_sweatperseverecrysob
    joyastonishedscreamtired_faceangryragetriumph
    sleepyyummasksunglassesdizzy_faceimpsmiling_imp
    neutral_faceno_mouthinnocent