Po prostu wpisany rachunek lambda - Simply typed lambda calculus

Prostu wpisane rachunek lambda ( ), to forma teorii typów , jest wpisany interpretacja z rachunku lambda tylko jeden konstruktor typu ( ), która buduje typy funkcyjne . Jest to kanoniczny i najprostszy przykład typowanego rachunku lambda. Rachunek lambda z prostym typowaniem został pierwotnie wprowadzony przez Alonzo Church w 1940 roku jako próba uniknięcia paradoksalnych zastosowań rachunku lambda bez typowania i wykazuje wiele pożądanych i interesujących właściwości. ${\ Displaystyle \ lambda ^ {\ do}}$${\ Displaystyle \ do}$

Termin typ prosty jest również używany w odniesieniu do rozszerzeń prostego rachunku lambda, takich jak iloczyny , koprodukty lub liczby naturalne ( System T ) lub nawet pełna rekurencja (jak PCF ). W przeciwieństwie do tego, systemy, które wprowadzają typy polimorficzne (takie jak System F ) lub typy zależne (takie jak Logical Framework ) nie są uważane za po prostu typowane . Te pierwsze, poza pełną rekurencją, są nadal uważane za proste, ponieważ kościelne kodowanie takich struktur może być wykonane przy użyciu tylko i odpowiednich zmiennych typu, podczas gdy polimorfizm i zależność nie. ${\ Displaystyle \ do}$

Składnia

W tym artykule używamy i zmieniamy typy. Nieformalnie typ funkcji odnosi się do typu funkcji, które po podaniu danych wejściowych typu , generują dane wyjściowe typu . Zgodnie z konwencją, współpracownicy po prawej: czytamy jako . ${\displaystyle \sigma}$${\ Displaystyle \ tau}$ ${\ Displaystyle \ sigma \ do \ tau}$${\displaystyle \sigma}$${\ Displaystyle \ tau}$${\ Displaystyle \ do}$${\ Displaystyle \ sigma \ do \ tau \ do \ rho}$${\ Displaystyle \ sigma \ do (\ tau \ do \ rho)}$

Definiowanie typów zaczynamy od ustalenia zestawu typów bazowych , . Są one czasami nazywane typami atomowymi lub stałymi typu . Po naprawieniu składnia typów to: ${\ Displaystyle B}$

${\ Displaystyle \ tau :: = \ tau \ do \ tau \ średni T \ quad \ operatorname {gdzie} \ quad T \ w B}$.

Na przykład , generuje nieskończony zestaw typów zaczynających się od${\displaystyle B=\{a,b\}}$${\displaystyle a,b}$${\displaystyle a\do a}$${\displaystyle a\do b,b\do b,}$${\displaystyle b\do a}$${\displaystyle a\do (a\doa),\ldots,}$${\ Displaystyle (b\do a)\do (a\do b),\ldots}$

Ustalamy również zestaw stałych term dla typów podstawowych. Na przykład możemy założyć typ bazowy nat , a terminem stałe mogą być liczby naturalne. W oryginalnym przedstawieniu Church użył tylko dwóch typów podstawowych: dla „typu propozycji” i dla „typu jednostek”. Typ nie ma stałych terminowych, natomiast ma jedną stałą termiczną. Często bierze się pod uwagę rachunek różniczkowy z tylko jednym typem podstawowym, zwykle . ${\displaystyle o}$${\ Displaystyle \ iota }$${\displaystyle o}$${\ Displaystyle \ iota }$${\displaystyle o}$

Składnia prostego rachunku lambda jest zasadniczo składnią samego rachunku lambda. Piszemy, aby zaznaczyć, że zmienna jest typu . Składnia terminu w BNF to wtedy: ${\displaystyle x{\mathbin {:}}\tau}$${\displaystyle x}$${\ Displaystyle \ tau}$

${\ Displaystyle e:: = x \ mid \ lambda x {\ mathbin {:}} \ tau . e \ mid e \ e \ mid c}$

gdzie jest terminem stałym. ${\displaystyle c}$

Czyli referencja do zmiennej , abstrakcje , aplikacja i stała . Odwołanie do zmiennej jest powiązane, jeśli znajduje się wewnątrz powiązania abstrakcji . Termin jest zamknięty, jeśli nie ma niezwiązanych zmiennych. ${\displaystyle x}$${\displaystyle x}$

Porównaj to ze składnią rachunku lambda bez typu:

${\ Displaystyle e:: = x \ mid \ lambda xe \ mid e \ e}$

Widzimy, że w typowanym rachunku lambda każda funkcja ( abstrakcja ) musi określać typ swojego argumentu.

Zasady pisania

Aby zdefiniować zestaw dobrze wpisanych terminów lambda danego typu, zdefiniujemy relację typowania między terminami i typami. Najpierw wprowadzamy konteksty typowania lub środowiska typograficzne , które są zbiorami założeń typowania. Wpisując założenie ma formę , to znaczy ma typ . ${\ Displaystyle \ Gamma \ Delta \ kropki}$${\displaystyle x{\mathbin {:}}\sigma}$${\displaystyle x}$${\displaystyle \sigma}$

Związek typowania wskazuje, że to określenie typu kontekstu . W tym przypadku mówi się, że jest dobrze wpisany (mający typ ). Instancje relacji typowania nazywane są osądami typowania . Ważność sądu typograficznego jest pokazana przez dostarczenie wyprowadzenia typograficznego , skonstruowanego przy użyciu reguł typowania (gdzie przesłanki nad linią pozwalają nam wyprowadzić wniosek poniżej linii). Rachunek lambda o prostym typie używa następujących reguł: ${\ Displaystyle \ Gamma \ vdash e {\ mathbin {:}} \ sigma}$${\displaystyle e}$${\displaystyle \sigma}$${\ Displaystyle \ Gamma}$${\displaystyle e}$${\displaystyle \sigma}$

${\ Displaystyle {\ Frac {x {\ mathbin {:}} \ sigma \ w \ Gamma} {\ Gamma \ vdash x {\ mathbin {:}} \ sigma}}}$ (1)	${\displaystyle {\frac {c{\tekst{jest stałą typu}}T}{\gamma \vdash c{\mathbin {:}}T}}}$ (2)
${\displaystyle {\frac {\gamma,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau}{\gamma \vdash (\lambda x{\mathbin {:}}\ sigma .~e){\mathbin {:}}(\sigma \do \tau )}}}$ (3)	${\ Displaystyle {\ Frac {\ Gamma \ vdash e_ {1} {\ mathbin {:}} \ sigma \ do \ tau \ quad \ Gamma \ vdash e_ {2} {\ mathbin {:}} \ sigma} {\ Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}}$ (4)

W słowach,

1. Jeśli ma type w kontekście, wiemy, że ma type .${\displaystyle x}$${\displaystyle \sigma}$${\displaystyle x}$${\displaystyle \sigma}$
2. Stałe terminowe mają odpowiednie typy podstawowe.
3. Jeżeli w pewnym kontekście z konieczności typ , ma typ , to w tym samym kontekście, bez , ma typ .${\displaystyle x}$${\displaystyle \sigma}$${\displaystyle e}$${\ Displaystyle \ tau}$${\displaystyle x}$${\ Displaystyle \ lambda x {\ mathbin {:}} \ sigma. ~ e}$${\ Displaystyle \ sigma \ do \ tau}$
4. Jeśli w pewnym kontekście ma typ i ma typ , to ma typ .${\displaystyle e_{1}}$${\ Displaystyle \ sigma \ do \ tau}$${\displaystyle e_{2}}$${\displaystyle \sigma}$${\displaystyle e_{1}~e_{2}}$${\ Displaystyle \ tau}$

Przykłady terminów zamkniętych, tj. terminów typowalnych w pustym kontekście, to:

• Dla każdego typu termin (funkcja tożsamości/I-kombinator),${\ Displaystyle \ tau}$${\ Displaystyle \ lambda x {\ mathbin {:}} \ tau .x {\ mathbin {:}} \ tau \ do \ tau}$
• W przypadku typów termin (kombinator K) oraz${\displaystyle \sigma,\tau}$${\ Displaystyle \ lambda x {\ mathbin {:}} \ sigma \ lambda r {\ mathbin {:}} \ tau . x {\ mathbin {:}} \ sigma \ do \ tau \ do \ sigma}$
• W przypadku typów termin (kombinator S).${\ Displaystyle \ tau , \ tau ', \ tau ''}$${\ Displaystyle \ lambda x {\ mathbin {:}} \ tau \ do \ tau '\ do \ tau ''. \ lambda r {\ mathbin {:}} \ tau \ do \ tau '. \ lambda z {\ mathbin {:}}\tau .xz(yz):(\tau \do \tau '\do \tau '')\do (\tau \do \tau ')\do \tau \do \tau ''}$

Są to typizowane reprezentacje rachunku lambda podstawowych kombinatorów logiki kombinatorycznej .

Każdy typ ma przyporządkowane zamówienie, numer . Dla typów podstawowych ; dla typów funkcji, . Oznacza to, że kolejność typu mierzy głębokość strzałki najbardziej zagnieżdżonej w lewo. Stąd: ${\ Displaystyle \ tau}$${\displaystyle o(\tau)}$${\ Displaystyle o (T) = 0}$${\ Displaystyle o (\ sigma \ do \ tau) = {\ mbox {max}} (o (\ sigma) + 1, o (\ tau))}$

${\ Displaystyle o (\ jota \ do \ jota \ do \ jota ) = 1}$

${\ Displaystyle o ((\ jota \ do \ jota ) \ do \ jota ) = 2}$

Semantyka

Interpretacje wewnętrzne i zewnętrzne

Ogólnie rzecz biorąc, istnieją dwa różne sposoby przypisywania znaczenia po prostu wpisane do rachunku lambda, jak do wpisywanych języków bardziej ogólnie, czasami nazywany nieodłącznym vs. zewnętrzny lub Kościół -Style vs. Curry -Style . Semantyka wewnętrzna / w stylu kościelnym przypisuje znaczenie tylko dobrze napisanym terminom, a dokładniej, przypisuje znaczenie bezpośrednio pochodnym typowania. Skutkuje to tym, że terminom różniącym się tylko adnotacjami typu można jednak przypisać różne znaczenia. Na przykład termin tożsamości na liczbach całkowitych i termin tożsamości na wartości logiczne mogą oznaczać różne rzeczy. (Klasyczne zamierzone interpretacje to funkcja tożsamości na liczbach całkowitych i funkcja tożsamości na wartościach logicznych.) W przeciwieństwie do tego, semantyka zewnętrzna/w stylu Curry przypisuje znaczenie pojęciom niezależnie od typowania, tak jak byłyby one interpretowane w języku nieopisanym. W tym widoku i oznacza to samo ( tj. to samo co ). ${\ Displaystyle \ lambda x {\ mathbin {:}} {\ mathtt {int}}. ~ x}$${\ Displaystyle \ lambda x {\ mathbin {:}} {\ mathtt {bool}}. ~ x}$${\ Displaystyle \ lambda x {\ mathbin {:}} {\ mathtt {int}}. ~ x}$${\ Displaystyle \ lambda x {\ mathbin {:}} {\ mathtt {bool}}. ~ x}$${\ Displaystyle \ lambda x. ~ x}$

Rozróżnienie między wewnętrzną i zewnętrzną semantyką jest czasami związane z obecnością lub brakiem adnotacji w abstrakcjach lambda, ale ściśle mówiąc to użycie jest nieprecyzyjne. Możliwe jest zdefiniowanie semantyki w stylu Curry'ego na terminach z adnotacjami po prostu przez zignorowanie typów ( tj. poprzez wymazanie typu ), ponieważ możliwe jest nadanie semantyki w stylu kościelnym na terminach nieopatrzonych adnotacjami, gdy typy można wydedukować z kontekstu ( tj. , poprzez wnioskowanie o typie ). Zasadnicza różnica między podejściami wewnętrznymi i zewnętrznymi polega po prostu na tym, czy reguły typowania są postrzegane jako definiujące język, czy jako formalizm służący do weryfikacji właściwości bardziej prymitywnego języka bazowego. Większość różnych interpretacji semantycznych omówionych poniżej można zobaczyć z perspektywy Kościoła lub Curry'ego.

Teoria równań

Prosto typizowany rachunek lambda ma tę samą teorię równań równoważności βη, co nieopisany rachunek lambda , ale podlega ograniczeniom dotyczącym typu. Równanie redukcji beta

${\ Displaystyle (\ lambda x {\ mathbin {:}} \ sigma . ~ t) \ u = _ {\ beta} t [x: = u]}$

utrzymuje się w kontekście kiedykolwiek i , podczas gdy równanie redukcji eta${\ Displaystyle \ Gamma}$${\ Displaystyle \ Gamma, x {\ mathbin {:}} \ sigma \ vdash t {\ mathbin {:}} \ tau}$${\ Displaystyle \ Gamma \ vdash u {\ mathbin {:}} \ sigma}$

${\ Displaystyle \ lambda x {\ mathbin {:}} \ sigma. ~ t \, x = _ {\ eta} t}$

trzyma się zawsze i nie pojawia się jako wolny w . ${\ Displaystyle \ Gamma \ vdash t \!: \ sigma \ do \ tau}$${\displaystyle x}$${\displaystyle t}$

Semantyka operacyjna

Podobnie semantyka operacyjna rachunku lambda z prostym typem może być ustalona tak, jak w przypadku rachunku lambda bez typu, przy użyciu funkcji call by name , call by value lub innych strategii oceny . Podobnie jak w przypadku każdego języka maszynowego, bezpieczeństwo typów jest podstawową właściwością wszystkich tych strategii oceny. Ponadto opisana poniżej właściwość silnej normalizacji oznacza, że ​​każda strategia oceny zakończy się na wszystkich prostych warunkach.

Semantyka kategoryczna

Prosto wpisane rachunek Lambda (z -equivalence) jest wewnętrzny język z kartezjańskim zamknięte kategorie (CCCS), jak to po raz pierwszy zauważony przez Lambek . Przy jakimkolwiek określonym CCC, podstawowymi typami odpowiedniego rachunku lambda są tylko obiekty , a terminy to morfizmy . I odwrotnie, każdy prosty typ rachunku lambda daje CCC, którego obiektami są typy, a morfizmy są klasami równoważności terminów. ${\ Displaystyle \ beta \ eta}$

Aby korespondencja była jasna, do powyższego zazwyczaj dodawany jest konstruktor typu dla produktu kartezjańskiego . Aby zachować kategoryczność iloczynu kartezjańskiego , dodaje się reguły typu dla parowania , rzutowania i członu jednostkowego . Biorąc pod uwagę dwa terminy i , termin ma typ . Podobnie, jeśli mamy wyraz , to istnieją terminy i gdzie odpowiadają rzutom iloczynu kartezjańskiego. Termin jednostkowy typu 1 jest zapisywany i wymawiany jako 'nil', jest obiektem końcowym . Podobnie rozszerzono teorię równań, dzięki czemu: ${\displaystyle s{\mathbin {:}}\sigma}$${\displaystyle t{\mathbin {:}}\tau}$${\displaystyle (s,t)}$${\ Displaystyle \ sigma \ razy \ tau}$${\ Displaystyle u {\ mathbin {:}} \ tau _ {1} \ razy \ tau _ {2}}$${\ Displaystyle \ pi _ {1} (u) {\ mathbin {:}} \ tau _ {1}}$${\ Displaystyle \ pi _ {2} (u) {\ mathbin {:}} \ tau _ {2}}$${\ Displaystyle \ pi _ {i}}$${\ Displaystyle ()}$

${\displaystyle \pi_{1}(s{\mathbin {:}}\sigma,t{\mathbin {:}}\tau)=s{\mathbin {:}}\sigma}$

${\ Displaystyle \ pi _ {2} (s {\ mathbin {:}} \ sigma, t {\ mathbin {:}} \ tau) = t {\ mathbin {:}} \ tau}$

${\ Displaystyle (\ pi _ {1} (u {\ mathbin {:}} \ sigma \ razy \ tau), \ pi _ {2} (u {\ mathbin {:}} \ sigma \ razy \ tau )) =u{\mathbin {:}}\sigma \times \tau }$

${\ Displaystyle t {\ mathbin {:}} 1 = ()}$

To ostatnie jest czytane jako „ jeśli t ma typ 1, to redukuje się do zera ”.

Powyższe można następnie przekształcić w kategorię, biorąc typy jako obiekty . W morfizmami są równoważne klasy par , gdzie x oznacza zmienną (typu ), a T jest terminem (typu ), które nie mają wolnych zmienne w tym, z wyjątkiem (opcjonalnie) x . Zamknięcie uzyskuje się jak zwykle poprzez curry i aplikację . ${\ Displaystyle \ sigma \ do \ tau}$${\ Displaystyle (x {\ mathbin {:}} \ sigma, t {\ mathbin {:}} \ tau)}$${\displaystyle \sigma}$${\ Displaystyle \ tau}$

Dokładniej, między kategorią kartezjańskich kategorii zamkniętych a kategorią teorii lambda typu prostego istnieją funktory .

Powszechne jest rozszerzenie tego przypadku na zamknięte, symetryczne kategorie monoidalne, przy użyciu liniowego systemu typu . Powodem tego jest to, że CCC jest szczególnym przypadkiem zamkniętej symetrycznej kategorii monoidalnej, która jest zwykle uważana za kategorię zbiorów . Jest to dobre dla kładzenia podstaw teorii mnogości , ale bardziej ogólne toposy wydają się zapewniać lepsze podstawy.

Semantyka dowodowa

Rachunek lambda o prostym typowaniu jest ściśle powiązany z implikacyjnym fragmentem zdaniowej logiki intuicjonistycznej , tj. logiki minimalnej , poprzez izomorfizm Curry-Howarda : terminy odpowiadają dokładnie dowodom w dedukcji naturalnej , a typy zamieszkałe są dokładnie tautologiami logiki minimalnej.

Alternatywne składnie

Przedstawiona powyżej prezentacja nie jest jedynym sposobem zdefiniowania składni prostego rachunku lambda. Jedną z alternatyw jest całkowite usunięcie adnotacji typu (tak, aby składnia była identyczna z niewpisanym rachunkiem lambda), przy jednoczesnym upewnieniu się, że terminy są dobrze wpisane za pomocą wnioskowania o typie Hindley-Milner . Algorytm wnioskowania kończy się, brzmi i jest kompletny: za każdym razem, gdy termin można wpisać, algorytm oblicza jego typ. Dokładniej, to oblicza termin za główny typ , ponieważ często nieopisanych termin (jak ) może mieć więcej niż jeden typ ( , , itd., Które są wszystkie wystąpienia głównego typu ). ${\ Displaystyle \ lambda x. ~ x}$${\displaystyle {\mathtt {int}}\do {\mathtt {int}}}$${\displaystyle {\mathtt {bool}}\to {\mathtt {bool}}}$${\ Displaystyle \ alfa \ do \ alfa}$

Inna alternatywna prezentacja prostego typu rachunku lambda opiera się na dwukierunkowym sprawdzaniu typów , które wymaga więcej adnotacji typu niż wnioskowanie Hindleya-Milnera, ale jest łatwiejsze do opisania. System typów jest podzielony na dwa osądy, reprezentujące zarówno sprawdzanie, jak i syntezę , odpowiednio pisemny i pisemny . Operacyjnie wszystkie trzy składniki , , i są danymi wejściowymi do oceny sprawdzającej , podczas gdy ocena syntezy przyjmuje tylko dane wejściowe i jako dane wejściowe, tworząc typ jako dane wyjściowe. Te osądy są wyprowadzane według następujących zasad: ${\ Displaystyle \ Gamma \ vdash e \ Lewa strzałka \ tau}$${\ Displaystyle \ Gamma \ vdash e \ strzałka w prawo \ tau}$${\ Displaystyle \ Gamma}$${\displaystyle e}$${\ Displaystyle \ tau}$${\ Displaystyle \ Gamma \ vdash e \ Lewa strzałka \ tau}$${\ Displaystyle \ Gamma \ vdash e \ strzałka w prawo \ tau}$${\ Displaystyle \ Gamma}$${\displaystyle e}$${\ Displaystyle \ tau}$

${\ Displaystyle {\ Frac {x {\ mathbin {:}} \ sigma \ w \ gamma {\ gamma \ vdash x \ strzałka w prawo \ sigma}}}$ [1]	${\displaystyle {\frac {c{\tekst{jest stałą typu}}T}{\gamma \vdash c\rightarrow T}}}$ [2]
${\ Displaystyle {\ Frac {\ Gamma, x {\ mathbin {:}} \ sigma \ vdash e \ lewa strzałka \ tau }{\ gamma \ vdash \ lambda x. ~ e \ lewa strzałka \ sigma \ do \ tau }}}$ [3]	${\ Displaystyle {\ Frac {\ Gamma \ vdash e_ {1} \ strzałka w prawo \ sigma \ do \ tau \ quad \ gamma \ vdash e_ {2} \ strzałka w lewo \ sigma }{ \ gamma \ vdash e_ {1} ~ e_ { 2}\strzałka w prawo \tau }}}$ [4]
${\ Displaystyle {\ Frac {\ Gamma \ vdash e \ strzałka w prawo \ tau} {\ gamma \ vdash e \ strzałka w lewo \ tau}}}$ [5]	${\ Displaystyle {\ Frac {\ Gamma \ vdash e \ strzałka w lewo \ tau} {\ gamma \ vdash (e {\ mathbin {:}} \ tau) \ strzałka w prawo \ tau}}}$ [6]

Zauważ, że reguły [1]–[4] są prawie identyczne z regułami (1)–(4) powyżej, z wyjątkiem starannego wyboru sądów sprawdzających lub syntezujących. Te wybory można wyjaśnić w następujący sposób:

1. Jeśli jest w kontekście, możemy zsyntetyzować type for .${\displaystyle x{\mathbin {:}}\sigma}$${\displaystyle \sigma}$${\displaystyle x}$
2. Rodzaje stałych terminów są stałe i można je zsyntetyzować.
3. Aby sprawdzić, czy ma typ w jakimś kontekście, rozszerzamy kontekst o i sprawdzamy, czy ma typ .${\ Displaystyle \ lambda x. ~ e}$${\ Displaystyle \ sigma \ do \ tau}$${\displaystyle x{\mathbin {:}}\sigma}$${\displaystyle e}$${\ Displaystyle \ tau}$
4. Jeśli syntetyzuje typ (w pewnym kontekście) i sprawdza z typem (w tym samym kontekście), to syntetyzuje typ .${\displaystyle e_{1}}$${\ Displaystyle \ sigma \ do \ tau}$${\displaystyle e_{2}}$${\displaystyle \sigma}$${\displaystyle e_{1}~e_{2}}$${\ Displaystyle \ tau}$

Zauważ, że reguły syntezy są odczytywane od góry do dołu, podczas gdy reguły sprawdzania są odczytywane od dołu do góry. W szczególności zwróć uwagę, że nie potrzebujemy adnotacji na temat abstrakcji lambda w regule [3], ponieważ typ zmiennej związanej można wywnioskować z typu, w którym sprawdzamy funkcję. Na koniec wyjaśniamy reguły [5] i [6] w następujący sposób:

5. Aby sprawdzić , czy ma typ , wystarczy zsyntetyzować typ .${\displaystyle e}$${\ Displaystyle \ tau}$${\ Displaystyle \ tau}$
6. Jeśli sprawdzane jest z typem , termin wyraźnie oznaczony adnotacją jest syntetyzowany . ${\displaystyle e}$${\ Displaystyle \ tau}$${\ Displaystyle (e {\ mathbin {:}} \ tau)}$${\ Displaystyle \ tau}$

Dzięki tym dwóm ostatnim regułom, które nakładają się na syntezę i sprawdzanie, łatwo zauważyć, że każdy dobrze wpisany, ale nieopisany termin może być sprawdzony w systemie dwukierunkowym, o ile wstawimy „wystarczającą” adnotację typu. W rzeczywistości adnotacje są potrzebne tylko przy β-redeksach.

Generalne obserwacje

Biorąc pod uwagę standardową semantykę, po prostu typowany rachunek lambda jest silnie normalizujący : to znaczy, że dobrze wpisane terminy zawsze redukują się do wartości, tj . abstrakcji. Dzieje się tak, ponieważ rekurencja nie jest dozwolona przez reguły typowania: nie można znaleźć typów dla kombinatorów stałoprzecinkowych i terminu pętli . Rekurencję można dodać do języka, używając specjalnego operatora typu lub dodając ogólne typy rekurencyjne , chociaż oba eliminują silną normalizację. ${\ Displaystyle \ lambda}$${\ Displaystyle \ Omega = (\ lambda x. ~ x ~ x) (\ lambda x. ~ x ~ x)}$${\displaystyle {\mathtt {poprawka}}_{\alfa}}$${\ Displaystyle (\ alfa \ do \ alfa ) \ do \ alfa}$

Ponieważ jest to silnie normalizujące, rozstrzyga się, czy po prostu wpisany program rachunku lambda zatrzyma się, czy nie: w rzeczywistości zawsze się zatrzymuje. Możemy zatem wnioskować, że język nie jest zupełny pod względem Turinga .

Ważne wyniki

• Tait wykazał w 1967 roku, że -redukcja mocno się normalizuje . W konsekwencji równoważność jest rozstrzygalna . Statman wykazał w 1977 roku, że problem normalizacji nie jest elementarną rekurencją , co później uprościł Mairson (1992). Problem jest znany w zestawie z hierarchią Grzegorczyk . Czysto semantyczny dowód normalizacji (patrz normalizacja przez ocenę ) podali Berger i Schwichtenberg w 1991 roku.${\ Displaystyle \ beta}$${\ Displaystyle \ beta \ eta}$${\ Displaystyle {\ Mathcal {E}} ^ {4}}$
• Unifikacja problemem -equivalence jest nierozstrzygalny. Huet pokazał w 1973 roku, że unifikacja trzeciego rzędu jest nierozstrzygalna, co zostało ulepszone przez Baxtera w 1978 roku, a następnie przez Goldfarba w 1981 roku, pokazując, że unifikacja drugiego rzędu jest już nierozstrzygnięta. Dowód, że dopasowanie wyższego rzędu (unifikacja, w której tylko jeden termin zawiera zmienne egzystencjalne) jest rozstrzygalny, został ogłoszony przez Colina Stirlinga w 2006 roku, a pełny dowód opublikowano w 2009 roku.${\ Displaystyle \ beta \ eta}$
• Liczby naturalne możemy zakodować za pomocą terminów typu ( liczby kościelne ). Schwichtenberg wykazał w 1976 roku, że dokładnie rozszerzone wielomiany są reprezentowane jako funkcje nad cyframi kościelnymi; są to z grubsza wielomiany zamknięte operatorem warunkowym.${\ Displaystyle (o\do o)\do (o\do o)}$${\ Displaystyle \ lambda ^ {\ do}}$
• Pełny wzór od jest przez interpretacji podstawowych typów w zestawach i typów funkcji przez odbiornik-theoretic miejsca funkcyjnego . Friedman wykazał w 1975 roku, że ta interpretacja jest kompletna dla -równoważności, jeśli typy bazowe są interpretowane przez zbiory nieskończone. Statman wykazał w 1983 roku, że -równoważność to maksymalna równoważność, która jest zwykle niejednoznaczna , tj. zamknięta pod podstawieniami typów ( Typowe twierdzenie Statmana o niejednoznaczności ). Konsekwencją tego jest to, że zachodzi własność modelu skończonego , tj. zbiory skończone są wystarczające do rozróżnienia terminów, które nie są identyfikowane przez -równoważność.${\ Displaystyle \ lambda ^ {\ do}}$${\ Displaystyle \ beta \ eta}$${\ Displaystyle \ beta \ eta}$${\ Displaystyle \ beta \ eta}$
• Plotkin wprowadził relacje logiczne w 1973 roku, aby scharakteryzować elementy modelu, które można zdefiniować za pomocą terminów lambda. W 1993 roku Jung i Tiuryn ​​wykazali, że ogólna forma relacji logicznej (relacje logiczne Kripkego o zmiennej arności) dokładnie charakteryzuje definiowalność lambda. Plotkin i Statman wywnioskowali, że rozstrzyga się, czy dany element modelu wygenerowanego ze zbiorów skończonych jest definiowalny za pomocą wyrażenia lambda ( przypuszczenie Plotkina-Statmana ). Ta hipoteza okazała się fałszywa przez Loadera w 1993 roku.

Uwagi

Bibliografia

• A. Church: Sformułowanie prostej teorii typów , JSL 5, 1940
• WWTait : Intensjonalne interpretacje funkcjonałów typu skończonego I, JSL 32(2), 1967
• GD Plotkin: Definiowalność lambda i relacje logiczne, Raport techniczny, 1973
• GP Huet: Nierozstrzygalność unifikacji w informacji logicznej i kontroli trzeciego rzędu 22(3): 257-267 (1973)
• H. Friedman: Równość funkcjonałów . LogicColl. '73, strony 22-37, LNM 453, 1975.
• H. Schwichtenberg: Funkcje definiowalne w prostym rachunku lambda, Arch. Matematyka Logik 17 (1976) 113-114.
• R. Statman: Typowy rachunek lambda nie jest elementarnym rekurencyjnym FOCS 1977: 90-94
• WD Goldfarb: Nierozstrzygalność problemu unifikacji drugiego rzędu, TCS (1981), no. 13, 225-230.
• R. Statmana. -definiowalne funkcjonały i konwersja. Łuk. Matematyka. Logik, 23:21–26, 1983.${\ Displaystyle \ lambda}$${\ Displaystyle \ beta \ eta}$
• J. Lambek : Kartezjańskie kategorie zamknięte i typowane rachunki lambda . Kombinatory i języki programowania funkcjonalnego 1985: 136-175
• U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typeed lambda-calculus LICS 1991: 203-211
• H. Mairson: Prosty dowód twierdzenia Statmana , TCS 103(2):387-394, 1992.
• Jung, A., Tiuryn, J.: Nowa charakterystyka definiowalności lambda , TLCA 1993
• R. Loader: Nierozstrzygalność definiowania λ , ukazał się w Church Festschrift, 2001
• H. Barendregt, Lambda Calculi with Types , Handbook of Logic in Computer Science, tom II, Oxford University Press, 1993. ISBN  0-19-853761-1 .
• L. Baxter: Nierozstrzygalność problemu unifikacji diadów trzeciego rzędu , Informacja i kontrola 38(2), 170-178 (1978)

Zewnętrzne linki

• Ładowarka, Ralph (luty 1998). „Uwagi dotyczące prostego rachunku lambda” .
• Wpis „Church's Type Theory” w Stanford Encyclopedia of Philosophy