Kostka lambdy

Kostka lambda. Kierunek każdej strzałki jest kierunkiem włączenia.

W logice matematycznej i teorii typów , sześcian λ (również zapisany sześcian lambda ) jest strukturą wprowadzoną przez Henka Barendregta w celu zbadania różnych wymiarów, w których rachunek konstrukcji jest uogólnieniem prostego rachunku λ . Każdy wymiar sześcianu odpowiada nowemu rodzajowi zależności między terminami i typami. Tutaj „zależność” odnosi się do zdolności terminu lub typu do wiązania terminu lub typu. Odpowiednie wymiary sześcianu λ odpowiadają:

• oś x ( ${\ displaystyle \ rightarrow}$ ): typy, które mogą wiązać terminy, odpowiadające typom zależnym .
• oś y ( $:$ terminy, które mogą wiązać typy, odpowiadające polimorfizmowi .
• oś z ( $:$ typy, które mogą wiązać typy, odpowiadające (wiążącym) operatorom typów .

Różne sposoby łączenia tych trzech wymiarów dają 8 wierzchołków sześcianu, z których każdy odpowiada innemu rodzajowi systemu typowania. Sześcian λ można uogólnić na koncepcję systemu typu czystego .

Przykłady systemów

(λ→) Po prostu wpisany rachunek lambda

Najprostszym systemem znalezionym w kostce λ jest po prostu wpisany rachunek lambda , zwany także λ→. W tym systemie jedynym sposobem na skonstruowanie abstrakcji jest uzależnienie terminu od terminu , z regułą pisania

${\ Displaystyle {\ Frac {\ Gamma, x: \ sigma \; \ vdash \; t: \ tau} {\ Gamma \; \ vdash \; \ lambda xt: \ sigma \ do \ tau} }}$

(λ2) Układ F

W Systemie F (nazywanym również λ2 od „rachunku lambda wpisanego drugiego rzędu”) istnieje inny typ abstrakcji, zapisany za pomocą , który pozwala terminom zależeć od typów , z następującą regułą: ${\ displaystyle \ Lambda}$

$. \sigma }}\;{\text{ if }}\alpha {\text{ nie występuje swobodnie w }}\Gamma }$

Terminy zaczynające się na $literę$ nazywane polimorficznymi , ponieważ można je zastosować do różnych typów, aby uzyskać różne funkcje, podobnie jak funkcje polimorficzne w językach podobnych do ML . Na przykład tożsamość polimorficzna

    zabawa  x  ->  x 

OCaml ma typ

   '  a  ->  '  a 

co oznacza, że ​​może przyjąć argument dowolnego typu „a” i zwrócić element tego typu. Ten typ odpowiada w λ2 typowi ${\ Displaystyle \ Pi \ alfa. \ alfa \ do \ alfa}$ .

(λ ω ) Układ F ω

W Systemie wprowadzono konstrukcję typów dostaw zależnych $.$ innych Nazywa się to konstruktorem typu i umożliwia zbudowanie „funkcji z typem jako wartością ”. Przykładem takiego konstruktora typu jest ${\ Displaystyle {\ mathsf {TREE}}: = \ lambda A: *. \ Pi B. (A \ do B) \ do (B \ do B \ do B) \ do B}$ , gdzie „ ${\ displaystyle A:*}$ ” nieformalnie oznacza „ ${\ displaystyle A}$ jest typem”. Jest $ZA {$ funkcja, która przyjmuje parametr typu $A}$$zwraca$ typ s wartości typu . W programowaniu konkretnym funkcja ta odpowiada możliwości definiowania konstruktorów typów wewnątrz języka, a nie traktowania ich jako prymitywów. Poprzedni konstruktor typu z grubsza odpowiada następującej definicji drzewa z etykietowanymi liśćmi w OCaml:

                wpisz  „  drzewo  =  |  _  Liść  '  a  |  _  Węzeł  '  drzewa  *  '  drzewa  _  _  _ 

Ten konstruktor typów można zastosować do innych typów w celu uzyskania nowych typów. Np. aby otrzymać rodzaj drzew liczb całkowitych:

     wpisz  int_tree  =  int  drzewo 

System generalnie nie jest używany samodzielnie, ale jest przydatny do izolowania niezależnej funkcji $typów$

(λP) Lambda-P

W systemie λP , zwanym także ΛΠ, i blisko spokrewnionym z LF Logical Framework , istnieją tak zwane typy zależne . Są to typy, które mogą zależeć od warunków . Kluczową zasadą wprowadzenia systemu jest

${\ Displaystyle {\ Frac {\ Gamma, x: A \; \ vdash \; B: *} {\ Gamma \; \ vdash \;(\Pi x:AB):*}}}$

gdzie ${\ displaystyle *}$ reprezentuje prawidłowe typy. Konstruktor nowego typu odpowiada poprzez izomorfizm $jako$ -Howarda uniwersalnemu kwantyfikatorowi, a system λP jako całość odpowiada logice pierwszego rzędu z implikacją tylko łącznikiem. Przykładem tych typów zależnych w programowaniu konkretnym jest typ wektorów na określonej długości: długość jest terminem, od którego zależy typ.

(Fω) Układ Fω

System Fω łączy zarówno konstruktora Systemu F, jak i konstruktorów typów z Systemu fa . Λ $}}$$Lambda$ . W ten sposób System Fω zapewnia zarówno terminy zależne od typów, jak i typy zależne od typów .

(λC) Rachunek konstrukcji

W rachunku konstrukcji , oznaczonym jako λC w sześcianie lub jako λPω, te cztery cechy współistnieją, tak że zarówno typy, jak i wyrazy mogą zależeć od typów i wyrazów. Wyraźna granica, która istnieje w λ → między terminami i typami, jest nieco zniesiona, ponieważ wszystkie typy oprócz uniwersalnego $same$ terminami z typem.

Definicja formalna

Jak w przypadku wszystkich systemów opartych na prostym typie rachunku lambda, wszystkie systemy w kostce są podane w dwóch krokach: najpierw surowe terminy wraz z pojęciem β-redukcji, a następnie wpisanie reguł pozwalających na wpisanie tych wyrazów.

Zbiór $,$$zdefiniowany$ literę _ Istnieje również zestaw $reprezentowanych$ przez litery ${\ displaystyle x, y, \ kropki}$ . Surowe terminy ośmiu systemów sześcianu są podane w następującej składni:

${\ Displaystyle A: = x \ mid s \ mid A ~ A \ mid \ lambda x: AA \ mid \ Pi x: AA}$

i $_$$\ Displaystyle \ Pi x: AB}$ _ $B}$ , gdy nie występuje za darmo w $displaystyle$ .

Środowisko, jak to zwykle bywa w systemach typowanych, jest podane przez ${\ Displaystyle \ Gamma: = \ pusty zestaw \ mid \ Gamma, x: T}$

Pojęcie β-redukcji jest wspólne dla wszystkich układów w kostce. Jest napisane i podane przez zasady. ${\ displaystyle \ to _ {\ beta}}$

$${\ Displaystyle {\ Frac {} {(\ lambda x: AB) ~ C \ do _ {\ beta} B [C / x]}} }$$

$${\ Displaystyle {\ Frac {B \ do _ {\ beta} B '} {\ lambda x: AB \ do _ {\ beta} \ lambda x: AB'}}}$$

$${\ Displaystyle {\ Frac {A \ do _ {\ beta} A'} {\ lambda x: AB \ do _ {\ beta} \ lambda x: A'.B}}}$$

$${\ Displaystyle {\ Frac {B \ do _ {\ beta} B '} {\ Pi x: AB \ do _ {\ beta} \ Pi x: AB'}}}$$

$${\ Displaystyle {\ Frac {A \ do _ {\ beta} A'} {\ Pi x: AB \ do _ {\ beta} \ Pi x: A'.B}}}$$

Jego zwrotne, przechodnie zamknięcie jest zapisane ${\ displaystyle = _ {\ beta}}$ .

Następujące zasady wpisywania są również wspólne dla wszystkich systemów w kostce:

$${\ Displaystyle {\ Frac {} {\ vdash *: \ kwadrat}} \ quad {\ tekst {(aksjomat)}}}$$

$${\ Displaystyle {\ Frac {\ Gamma \ vdash A: s \ quad x {\ tekst {nie występuje w}} \Gamma }{\Gamma ,x:A\vdash x:A}}\quad {\text{(Start)}}}$$

$${\ Displaystyle {\ Frac {\ Gamma \ vdash A: B \ quad \ Gamma \ vdash C: s} {\ Gamma, x:C\vdash A:B}}\quad {\text{(osłabienie)}}}$$

$${\ Displaystyle {\ Frac {\ Gamma \ vdash C: \ Pi x: AB \ quad \ Gamma \ vdash a: A} {$$

$${\ Displaystyle {\ Frac {\ Gamma \ vdash A: B \ quad B = _ {\ beta} B ' \quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Konwersja)}}}$$

$są$ na parach sortowań, w następujących dwóch regułach

$${\ Displaystyle {\ Frac {\ Gamma \ vdash A: s_ {1} \ quad \ Gamma, x: A \ vdash B: s_ {2}} {\ Gamma \ vdash \ Pi x: AB:s_{2}}}\quad {\text{(Produkt)}}}$$

${\ Displaystyle {\ Frac {\ Gamma \ vdash A: s_ {1} \ quad \ Gamma, x: A \ vdash b: B \ quad \ Gamma, x: A \ vdash B: s_ {2}} {\ Gamma \vdash \lambda x:Ab:\Pi x:AB}}\quad {\text{(Abstrakcja)}}}$

zgodność między systemami a parami ${\ textstyle (s_ {1}, s_ {2})}$ jest następująca:

${\ Displaystyle (s_ {1}, s_ {2})}$	${\ Displaystyle (*, *)}$	${\ Displaystyle (*, \ kwadrat)}$	${\ Displaystyle (\ kwadrat, *)}$	${\ Displaystyle (\ kwadrat, \ kwadrat)}$
λ→
λP
λ2
λ ω
λP2
λP ω
λω
λC

Każdy kierunek sześcianu odpowiada jednej parze (z wyłączeniem pary współdzielonej przez wszystkie systemy $) , a$ zależności między terminami i

• ${\ textstyle (*,*)}$ pozwala terminom zależeć od warunków.
• ${\textstyle (*,\square)}$ pozwala typom zależeć od terminów.
• ${\ textstyle (\ kwadrat, *)}$ pozwala terminom zależeć od typów.
• ${\textstyle (\square, \square)}$ pozwala typom zależeć od typów.

Porównanie systemów

λ→

Typowe wyprowadzenie, które można uzyskać, to

$${\ Displaystyle \ alfa: * \ vdash \ lambda x: \ alfa .x: \ Pi x: \ alfa. \ alfa}$$

lub za pomocą skrótu strzałkowego

$${\ Displaystyle \ alfa: * \ vdash \ lambda x: \ alfa .x: \ alfa \ do \ alfa}$$

bardzo przypominający tożsamość (typu $zwykłego$ λ→. Zauważ, że wszystkie użyte typy muszą pojawić się w kontekście, ponieważ jedyne wyprowadzenie, które można wykonać w pustym kontekście, to ${\textstyle \vdash *:\square}$ .

Moc obliczeniowa jest dość słaba, odpowiada wielomianom rozszerzonym (wielomiany wraz z operatorem warunkowym).

λ2

W λ2 można otrzymać takie wyrazy jak

$${\ Displaystyle \ vdash (\ lambda \ beta: *. \ lambda x: \ bot .x \ beta): \ Pi \ beta: *. \ bot \ do \ beta}$$

gdzie ${\ textstyle \ bot = \ Pi \ alfa: *. \ alfa}$ . Jeśli ktoś odczytuje ${\ textstyle \ Pi}$ jako uniwersalną kwantyfikację, poprzez izomorfizm Curry'ego-Howarda, można to postrzegać jako dowód zasady eksplozji. Ogólnie rzecz biorąc, λ2 dodaje możliwość posiadania impredykacyjnych , takich jak ${\ textstyle \ bot}$ , czyli terminów kwantyfikujących wszystkie typy, w tym siebie.
Polimorfizm pozwala również na konstruowanie funkcji, które nie były konstruowalne w λ→. Dokładniej, funkcje możliwe do zdefiniowania w λ2 są funkcjami dającymi się udowodnić w arytmetyce Peano drugiego rzędu . W szczególności wszystkie prymitywne funkcje rekurencyjne są definiowalne.

λP

W λP możliwość posiadania typów zależnych od terminów oznacza, że ​​można wyrażać predykaty logiczne. Na przykład można wyprowadzić:

$${\ Displaystyle \ alfa: *, a_ {0}: \ alfa, p: \ alfa \ do *, q :*\vdash \lambda z:(\Pi x:\alpha .px\to q).\lambda y:(\Pi x:\alpha .px).(za_{0})(ya_{0}): (\Pi x:\alpha .px\do q)\do (\Pi x:\alpha .px)\do q}$$

co odpowiada, poprzez izomorfizm Curry'ego-Howarda, dowodowi ${\ Displaystyle (\ forall x: A, Px \ to Q)\do (\forall x:A,Px)\do Q}$ . Jednak z obliczeniowego punktu widzenia posiadanie typów zależnych nie zwiększa mocy obliczeniowej, a jedynie możliwość wyrażenia bardziej precyzyjnych właściwości typów.

Reguła konwersji jest bardzo potrzebna w przypadku typów zależnych, ponieważ umożliwia wykonywanie obliczeń na warunkach w typie. Na przykład, jeśli masz ${\ Displaystyle \ Gamma \ vdash A: P ((\ lambda xx) y)}$ i ${\ Displaystyle \ Gamma \ vdash B: \ Pi x: P (y). C}$${\ Displaystyle \ Gamma \ vdash A: P (y)},$ ZA móc pisać ${\ displaystyle \ Gamma \ vdash BA:C}$ .

λω

W λω następujący operator

$${\ Displaystyle I: = \ lambda \ alfa: *. \ lambda \ beta: *. \ Pi \ gamma: *. (\ alfa \ do \ beta \ do \ gamma) \ do \gamma}$$

⊢ ${\ Displaystyle \ vdash I: * \ do * \ do *$ . wyprowadzenie

$${\ Displaystyle \ alfa: *, \ beta: * \ vdash \ Pi \ gamma: *. (\ alfa \ do \ beta \ do \ gamma) \ do \ gamma: * }$$

można uzyskać już w λ2, jednak polimorfizm $zdefiniować tylko wtedy$ występuje również reguła ${\ textstyle (\ kwadrat, *)}$

Z obliczeniowego punktu widzenia λω jest niezwykle silne i zostało uznane za podstawę języków programowania.

λC

Rachunek konstrukcji ma zarówno wyrazistość predykatów λP, jak i moc obliczeniową λω, stąd λC jest również nazywany λPω, a więc jest bardzo potężny, zarówno po stronie logicznej, jak i obliczeniowej.

Stosunek do innych systemów

Z logicznego punktu widzenia system Automath jest podobny do λ2. Języki ML-podobne z punktu widzenia typowania leżą gdzieś pomiędzy λ→ a λ2, ponieważ dopuszczają ograniczony rodzaj typów polimorficznych, czyli typów w postaci normalnej prenex. Jednakże, ponieważ zawierają one pewne operatory rekurencji, ich moc obliczeniowa jest większa niż λ2. System Coq opiera się na rozszerzeniu λ C z liniową hierarchią wszechświatów, a nie tylko jednym nietypowalnym $na$ zdolności konstruowania typów indukcyjnych.

Systemy typu czystego można postrzegać jako uogólnienie sześcianu z dowolnym zestawem rodzajów, aksjomatów, iloczynów i reguł abstrakcji. I odwrotnie, systemy kostki lambda można wyrazić jako systemy typu czystego z dwoma rodzajami $\ textstyle$${$ aksjomatem i zbiór reguł $że$ , ${\ Displaystyle \ {(*, *, *) \ }\subseteq R\subseteq \{(*,*,*),(*,\kwadrat,\kwadrat),(\kwadrat,*,*),(\kwadrat,\kwadrat,\kwadrat)\}}$ .

Poprzez izomorfizm Curry'ego-Howarda istnieje zgodność jeden do jednego między systemami w kostce lambda a systemami logicznymi, a mianowicie:

Układ sześcianu	Układ logiczny
λ→	(Pierwszego rzędu) rachunek zdań
λ2	Rachunek zdań drugiego rzędu
λ ω	Słabo rachunek zdań wyższego rzędu
λω	Rachunek zdań wyższego rzędu
λP	(Pierwszy rząd) Logika predykatów
λP2	Rachunek predykatów drugiego rzędu
λP ω	Słaby rachunek predykatów wyższego rzędu
λC	Rachunek konstrukcji

${$ . jedynymi spójnikami są $}$ \ displaystyle $klin$ lub ${\ displaystyle \ neg }$ w sposób impredicative w logice drugiego i wyższego rzędu. W słabych logikach wyższego rzędu istnieją zmienne dla predykatów wyższego rzędu, ale nie można ich określić ilościowo.

Wspólne właściwości

Cieszą się wszystkie systemy w kostce

• Churcha -Rossera : jeśli ${\ Displaystyle M \ do _ {\ beta} N}$ i ${\ Displaystyle M \ do _ {\ beta} N'}$ to istnieje ${ \ Displaystyle N''}$ takie, że ${\ Displaystyle N \ do _ {\ beta} ^ {*} N''}$ i ${\ Displaystyle N '\ do _ {\ beta} ^ {*} N''}$ ;
• właściwość redukcji podmiotu $:$ i M $M'}$${ \displaystyle \Gamma \vdash M':T}$ to ;
• ${\ Displaystyle \ Gamma \ vdash A: B}$ ZA i ${\ Displaystyle \ Gamma \ vdash A: B'}$ b $\ Displaystyle B=_{\beta}B'}$ .

Wszystko to można udowodnić na ogólnych systemach typu czystego.

Każdy dobrze wpisany termin w systemie sześcianu jest silnie normalizujący, chociaż ta właściwość nie jest wspólna dla wszystkich systemów typu czystego. Żaden system w kostce nie jest kompletny w sensie Turinga.

Podtypowanie

Podtypowanie jednak nie jest reprezentowane w kostce, mimo że systemy takie jak , znane jako kwantyfikacja ograniczona wyższego rzędu, która łączy podtypowanie i polimorfizm, mają znaczenie praktyczne, fa < ${<:} ^ {\ omega}}$ i można go dalej uogólnić na operatory typu ograniczonego. Dalsze rozszerzenia pozwalają na definiowanie obiektów czysto funkcjonalnych; ${\ displaystyle F_ {<:} ^ {\ omega}}$ systemy te zostały ogólnie opracowane po opublikowaniu artykułu o kostkach lambda.

Pomysł sześcianu pochodzi od matematyka Henka Barendregta (1991). Struktura systemów typu czystego uogólnia kostkę lambda w tym sensie, że wszystkie rogi kostki, jak również wiele innych systemów, można przedstawić jako instancje tej ogólnej struktury. Ta struktura jest starsza niż kostka lambda o kilka lat. W swoim artykule z 1991 roku Barendregt definiuje również rogi sześcianu w tych ramach.

Zobacz też

• W swojej Habilitation à diriger les recherches Olivier Ridoux podaje wycięty szablon sześcianu lambda, a także podwójną reprezentację sześcianu jako ośmiościanu, w którym 8 wierzchołków zastąpiono twarzami, a także podwójną reprezentację jako dwunastościan , gdzie 12 krawędzi zastąpiono ścianami.
• Teoria typów homotopii

Dalsza lektura

• Peyton Jones, Szymon; Meijer, Erik (1997). „Henk: wpisany język pośredni” (PDF) . Microsoftu . Henk opiera się bezpośrednio na kostce lambda , ekspresyjnej rodzinie typowanych rachunków lambda.

Linki zewnętrzne

• Kostka Lambda Barendregta w kontekście systemów typu czystego autorstwa Rogera Bishopa Jonesa