I przysięgam, że kiedyś T-shirt na sprzedaż gościnnie nieśmiertelne słowa:

W jakiej części

ty nie rozumiesz?

W moim przypadku odpowiedź brzmiałaby ... wszystko!

W szczególności często widzę taką notację w dokumentach Haskella, ale nie mam pojęcia, co to wszystko znaczy. Nie mam pojęcia, jaką to powinna być gałąź matematyki.

Rozpoznaję oczywiście litery greckiego alfabetu i symbole takie jak „∉” (co zwykle oznacza, że ​​coś nie jest elementem zestawu).

Z drugiej strony nigdy wcześniej nie widziałem „⊢” ( Wikipedia twierdzi, że może to oznaczać „partycję” ). Nie jestem również zaznajomiony z użyciem winculum tutaj. (Zwykle oznacza ułamek, ale nie wydaje się , że tak jest w tym przypadku.)

Gdyby ktoś mógł mi przynajmniej powiedzieć, od czego zacząć szukać zrozumienia tego morza symboli, byłoby to pomocne.

• Do poziomego paska oznacza, że „[powyżej] implikuje [poniżej]”.
• Jeśli istnieje wiele wyrażeń w [powyżej], a następnie rozważyć ich anded razem; wszystkie [powyższe] muszą być prawdziwe, aby zagwarantować [poniżej].
• :oznacza ma typ
• ∈oznacza jest w . (Podobnie ∉oznacza „nie ma”).
• Γjest zwykle używany w odniesieniu do środowiska lub kontekstu; w tym przypadku można go traktować jako zestaw adnotacji typu, łącząc identyfikator z jego typem. Oznacza x : σ ∈ Γto, że środowisko Γobejmuje fakt, że xma typ σ.
• ⊢można odczytać jako dowody lub ustalenia. Γ ⊢ x : σoznacza, że ​​środowisko Γokreśla xtyp σ.
• ,to sposób uwzględnienia konkretnych dodatkowych założeń w środowisku Γ.
  Oznacza Γ, x : τ ⊢ e : τ'to, że środowisko Γ, przy dodatkowym, nadrzędnym założeniu, że xma typτ , udowadnia, że ema typ τ'.

Zgodnie z życzeniem: pierwszeństwo operatora, od najwyższej do najniższej:

• Infix i mixfix operatorzy specyficzne dla języka, takie jak λ x . e, ∀ α . σi τ → τ', let x = e0 in e1i spacji do stosowania funkcji.
• :
• ∈ i ∉
• , (lewostronny)
• ⊢
• białe znaki oddzielające wiele zdań (asocjacyjne)
• poziomy pasek

Ta składnia, choć może wydawać się skomplikowana, jest w rzeczywistości dość prosta. Podstawowa idea pochodzi z logiki formalnej: całe wyrażenie jest implikacją, a górna połowa to założenia, a dolna połowa to wynik. Oznacza to, że jeśli wiesz, że górne wyrażenia są prawdziwe, możesz stwierdzić, że dolne wyrażenia również są prawdziwe.

Symbolika

Należy także pamiętać, że niektóre litery mają tradycyjne znaczenie; w szczególności Γ oznacza „kontekst”, w którym się znajdujesz - to znaczy, jakie są rodzaje innych rzeczy, które widziałeś. Więc coś w stylu Γ ⊢ ...oznacza „wyrażenie, ...gdy znasz typy każdego wyrażenia w Γ.

Ten ⊢symbol oznacza, że ​​możesz coś udowodnić. Podobnie Γ ⊢ ...jest ze stwierdzeniem: „Mogę udowodnić ...w kontekście Γ. Te stwierdzenia nazywane są również osądami typu.

Kolejna rzecz, o której należy pamiętać: w matematyce, podobnie jak ML i Scala, x : σoznacza, że xma typ σ. Możesz przeczytać tak jak u Haskella x :: σ.

Co oznacza każda reguła

Tak więc, wiedząc o tym, pierwszy wyraz staje się łatwe do zrozumienia: jeśli wiemy, że x : σ ∈ Γ(to jest, xma jakiś typ σw pewnym kontekście Γ), to wiemy, że Γ ⊢ x : σ(to jest w Γ, xma typ σ). Tak naprawdę, to nie mówi ci niczego super interesującego; po prostu mówi ci, jak korzystać z kontekstu.

Inne zasady są również proste. Na przykład weź [App]. Ta reguła ma dwa warunki: e₀jest funkcją od pewnego typu τdo jakiegoś typu τ'i e₁jest wartością typu τ. Teraz wiesz, co wpisać dostaniesz stosując e₀się e₁! Mam nadzieję, że to nie jest niespodzianka :).

Następna reguła ma jeszcze nową składnię. W szczególności Γ, x : τoznacza tylko kontekst Γi osąd x : τ. Tak więc, jeśli wiemy, że zmienna xma typ, τa wyrażenie ema typ τ', znamy również typ funkcji, która przyjmuje xi zwraca e. To po prostu mówi nam, co zrobić, jeśli ustaliliśmy, jaki typ funkcja przyjmuje i jaki typ zwraca, więc nie powinno to być zaskakujące.

Następny mówi po prostu, jak obsługiwać letinstrukcje. Jeśli wiesz, że jakieś wyrażenie e₁ma typ τtak długo, jak xma typ σ, wówczas letwyrażenie, które lokalnie wiąże xsię z wartością typu, σsprawi, że będzie e₁miało typ τ. Naprawdę, to po prostu mówi ci, że instrukcja let pozwala zasadniczo rozszerzyć kontekst o nowe powiązanie - co dokładnie letdziała!

[Inst]Zasada dotyczy sub-pisania. Mówi, że jeśli masz wartość typu σ'i jest ona podtypem σ( ⊑reprezentuje relację częściowego uporządkowania), to wyrażenie jest również typu σ.

Ostatnia zasada dotyczy typów uogólnionych. Krótko na bok: wolna zmienna jest zmienną, która nie jest wprowadzana przez wyrażenie let ani lambda wewnątrz jakiegoś wyrażenia; Wyrażenie to zależy teraz od wartości zmiennej wolnej od kontekstu. Reguła mówi, że jeśli istnieje jakaś zmienna, αktóra nie jest „wolna” w jakimkolwiek kontekście, to można powiedzieć, że każde wyrażenie, którego typ znasz e : σbędzie miał ten typ dla dowolnej wartości α.

Jak korzystać z reguł

Teraz, kiedy rozumiesz symbole, co robisz z tymi zasadami? Cóż, możesz użyć tych reguł, aby dowiedzieć się, jakie są różne wartości. Aby to zrobić, spójrz na swoje wyrażenie (powiedzmy f x y) i znajdź regułę, która ma konkluzję (dolna część) pasującą do twojego wyrażenia. Nazwijmy rzecz, którą próbujesz znaleźć, „celem”. W takim przypadku spójrz na regułę, która kończy się na e₀ e₁. Kiedy to znajdziesz, musisz znaleźć reguły potwierdzające wszystko powyżej linii tej reguły. Te rzeczy zasadniczo odpowiadają typom podwyrażeń, więc zasadniczo rekurencyjnie powtarzasz niektóre części wyrażenia. Po prostu rób to, dopóki nie skończysz drzewa dowodu, co daje dowód rodzaju wyrażenia.

Tak więc wszystkie te reguły określają dokładnie - i w zwykłym matematycznie pedantycznym szczególe: P - jak rozróżnić rodzaje wyrażeń.

Teraz powinno to brzmieć znajomo, jeśli kiedykolwiek używałeś Prologa - w zasadzie obliczasz drzewo dowodu jak ludzki tłumacz Prolog. Istnieje powód, dla którego Prolog nazywa się „programowaniem logicznym”! Jest to również ważne, ponieważ pierwszy sposób, w jaki zapoznałem się z algorytmem wnioskowania HM, to wdrożenie go w Prologu. Jest to w rzeczywistości zaskakująco proste i wyjaśnia, co się dzieje. Z pewnością powinieneś spróbować.

Uwaga: Prawdopodobnie popełniłem kilka błędów w tym wyjaśnieniu i bardzo by mi się podobało, gdyby ktoś je wskazał. Za kilka tygodni zajmę się tym na zajęciach, więc będę bardziej pewny niż: P.

gdyby ktoś mógł mi przynajmniej powiedzieć, od czego zacząć szukać zrozumienia tego morza symboli

Zobacz „ Praktyczne podstawy języków programowania ”, rozdziały 2 i 3, na temat logiki opartej na osądach i pochodnych. Cała książka jest teraz dostępna na Amazon.

Rozdział 2

Definicje indukcyjne

Definicje indukcyjne są niezbędnym narzędziem w nauce języków programowania. W tym rozdziale opracujemy podstawowe ramy definicji indukcyjnych i podamy przykłady ich zastosowania. Definicja indukcyjna składa się z zestawu zasad dotyczących wydawania osądów lub twierdzeń o różnych formach. Wyroki są stwierdzeniami na temat jednego lub większej liczby obiektów składniowych określonego rodzaju. Przepisy określają niezbędne i wystarczające warunki dla ważności wyroku, a tym samym w pełni określają jego znaczenie.

2.1 Orzeczenia

Zaczynamy od pojęcia wyroku lub twierdzenia o obiekcie składniowym. Będziemy korzystać z wielu form osądu, w tym takich przykładów:

• n nat - n jest liczbą naturalną
• n = n1 + n2 - n jest sumą n1 i n2
• τ typ - τ jest typem
• e : τ - wyrażenie e ma typ τ
• e ⇓ v - wyrażenie e ma wartość v

Wyrok stwierdza, że ​​jeden lub więcej obiektów składniowych ma właściwość lub stoi w pewnym stosunku do siebie. Sama własność lub relacja nazywana jest formą osądu , a osąd, że przedmiot lub przedmioty mają tę własność lub stanowisko w tej relacji, jest uważany za przykład takiej formy osądu. Forma osądu jest również nazywana orzeczeniem , a przedmioty stanowiące instancję są jej podmiotami . Piszemy o J o wyroku twierdząc, że J ładowniach . Kiedy podkreślenie przedmiotu wyroku nie jest ważne (tekst ucina się tutaj)

Jak rozumiem zasady Hindleya-Milnera?

Hindley-Milner jest zbiorem reguł w postaci rachunku sekwencyjnego (a nie naturalnej dedukcji), który pokazuje, że możemy wywnioskować (najbardziej ogólny) typ programu z jego konstrukcji bez wyraźnych deklaracji typu.

Symbole i notacja

Najpierw wyjaśnijmy symbole i omówmy pierwszeństwo operatora

• 𝑥 jest identyfikatorem (nieformalnie nazwa zmiennej).
• : oznacza to rodzaj (nieformalnie, instancja lub „jest-a”).
• 𝜎 (sigma) to wyrażenie, które jest zmienną lub funkcją.
• tak więc 𝑥: 𝜎 jest czytane „ 𝑥 is-a 𝜎 ”
• ∈ oznacza „jest elementem”
• 𝚪 (Gamma) to środowisko.
• ⊦ (znak potwierdzający) oznacza stwierdzenia (lub dowodzi, ale kontekstowo „zapewnia” czyta lepiej).
• 𝚪 ⊦ 𝑥 : 𝜎 jest zatem czytane „𝚪 potwierdza, że ​​𝑥, jest-a 𝜎 ”
• 𝑒 jest faktyczną instancją (elementem) typu 𝜎 .
• 𝜏 (tau) to typ: podstawowy, zmienny ( 𝛼 ), funkcjonalny 𝜏 → 𝜏 ' lub produkt 𝜏 × 𝜏' (produkt nie jest tutaj używany)
• 𝜏 → 𝜏 ” jest typem funkcjonalnym, w którym 𝜏 i 𝜏” są potencjalnie różnymi typami.

• 𝜆𝑥.𝑒 oznacza, że 𝜆 (lambda) to anonimowa funkcja, która przyjmuje argument 𝑥 i zwraca wyrażenie 𝑒 .

• niech 𝑥 = 𝑒₀ w 𝑒₁ oznacza w wyrażeniu 𝑒₁ , zamień 𝑒₀ gdziekolwiek pojawia się 𝑥 .

• ⊑ oznacza, że ​​poprzedni element jest podtypem (nieformalnie - podklasa) tego drugiego elementu.

• 𝛼 jest zmienną typu.
• ∀ 𝛼.𝜎 jest typem, ∀ (dla wszystkich) zmiennych argumentu, 𝛼 , zwracające 𝜎 wyrażenie
• ∉ wolny (𝚪) nie oznacza elementu zmiennych typu swobodnego 𝚪 zdefiniowanych w kontekście zewnętrznym. (Zmienne powiązane są zastępowalne).

Wszystko powyżej linii jest przesłanką, wszystko poniżej jest wnioskiem ( Per Martin-Löf )

Pierwszeństwo na przykładzie

Wziąłem niektóre bardziej złożone przykłady z reguł i wstawiłem zbędne nawiasy, które pokazują pierwszeństwo:

• 𝑥: 𝜎 ∈ 𝚪 można zapisać (𝑥: 𝜎) ∈ 𝚪

• 𝚪 ⊦ 𝑥 : 𝜎 można zapisać 𝚪 ⊦ ( 𝑥 : 𝜎 )

• 𝚪 ⊦ niech 𝑥 = 𝑒₀ w 𝑒₁ : 𝜏 jest równoważnie 𝚪 ⊦ (( niech ( 𝑥 = 𝑒₀ ) w 𝑒₁ ): 𝜏 )

• 𝚪 ⊦ 𝜆𝑥.𝑒 : 𝜏 → 𝜏 ' jest równoważnie 𝚪 ⊦ (( 𝜆𝑥.𝑒 ): ( 𝜏 → 𝜏' ))

Następnie duże spacje oddzielające stwierdzenia asertywne i inne warunki wstępne wskazują zestaw takich warunków wstępnych, a na koniec pozioma linia oddzielająca przesłankę od zakończenia przybliża koniec kolejności pierwszeństwa.

Zasady

Poniżej znajdują się angielskie interpretacje zasad, po których następuje luźne przekształcenie i wyjaśnienie.

Zmienna

Biorąc pod uwagę, że 𝑥 jest rodzajem 𝜎 (sigma), elementem 𝚪 (gamma),
wniosek 𝚪 zapewnia 𝑥 jest 𝜎.

Innymi słowy, w 𝚪 wiemy, że 𝑥 jest typu 𝜎, ponieważ 𝑥 jest typu 𝜎 w 𝚪.

Jest to w zasadzie tautologia. Nazwa identyfikatora to zmienna lub funkcja.

Zastosowanie aplikacji

Biorąc pod uwagę, że 𝚪 zapewnia 𝑒₀ jest typem funkcjonalnym, a 𝚪 zapewnia 𝚪 jest 𝑒₁
wnioskiem 𝚪 zapewnia, że ​​zastosowanie funkcji 𝑒₀ do 𝑒₁ jest rodzajem 𝜏 ”

Aby ponownie sformułować regułę, wiemy, że aplikacja funkcji zwraca typ 𝜏 ', ponieważ funkcja ma typ 𝜏 → 𝜏' i otrzymuje argument typu 𝜏.

Oznacza to, że jeśli wiemy, że funkcja zwraca typ, i zastosujemy ją do argumentu, wynikiem będzie instancja typu, o którym wiemy, że zwraca.

Abstrakcja funkcji

Biorąc pod uwagę, że 𝚪 i 𝑥 typu 𝜏 zapewnia 𝑒 jest typem, 𝜏 „
zawrzeć ” zapewnia anonimową funkcję, 𝜆 zwracającego wyrażenie, 𝑒 jest typu 𝜏 → 𝜏 ”.

Ponownie, gdy widzimy funkcję, która przyjmuje 𝑥 i zwraca wyrażenie 𝑒, wiemy, że jest ona typu 𝜏 → 𝜏 ', ponieważ 𝑥 (a 𝜏) twierdzi, że 𝑒 jest 𝜏 ”.

Jeśli wiemy, że 𝑥 jest typu 𝜏, a zatem wyrażenie 𝑒 jest typu 𝜏 ', to funkcja 𝑥 zwracającego wyrażenie 𝑒 jest typu 𝜏 → 𝜏'.

Niech zmienna deklaracja

Biorąc pod uwagę 𝚪 zapewnia 𝑒₀, typu 𝜎 oraz 𝚪 i 𝑥, typu 𝜎, zapewnia 𝑒₁ typu 𝜏
wnioskuje 𝚪 zapewnia let𝑥 = 𝑒₀ in𝑒₁ typu 𝜏

Luźno 𝑥 jest związany z 𝑒₀ w 𝑒₁ (a 𝜏), ponieważ 𝑒₀ jest 𝜎, a 𝑥 jest 𝜎, który twierdzi, że 𝑒₁ jest 𝜏.

Oznacza to, że jeśli mamy wyrażenie 𝑒₀, które jest 𝜎 (będące zmienną lub funkcją), i jakąś nazwę, also, również 𝜎 i wyrażenie 𝑒₁ typu 𝜏, wówczas możemy zastąpić 𝑒₀ zamiast 𝑥 wszędzie tam, gdzie pojawia się w środku z 𝑒₁.

Instancja

Biorąc pod uwagę 𝚪 twierdzenia 𝑒 typu 𝜎 ”i 𝜎” jest podtypem 𝜎
wniosku 𝚪 twierdzenia 𝑒 jest typu 𝜎

Wyrażenie 𝑒 jest typu nadrzędnego 𝜎, ponieważ wyrażenie 𝑒 jest podtypem 𝜎 ', a 𝜎 jest rodzicielskim typem 𝜎 ”.

Jeśli instancja jest typu, który jest podtypem innego typu, to jest to również instancja tego nadtypu - bardziej ogólnego typu.

Uogólnienie

Biorąc pod uwagę, że 𝚪 aserts 𝑒 jest 𝜎 i 𝛼 nie jest elementem wolnych zmiennych 𝚪,
wnioskuj 𝚪 asserts 𝑒, wpisz wszystkie wyrażenia argumentowe 𝛼 zwracając 𝜎 wyrażenie

Ogólnie rzecz biorąc, typ jest wpisywane 𝜎 dla wszystkich zmiennych argumentów (𝛼) zwracających 𝜎, ponieważ wiemy, że a jest 𝜎, a variable nie jest zmienną wolną.

Oznacza to, że możemy uogólnić program, aby akceptował wszystkie typy argumentów, które nie są jeszcze powiązane w zawierającym zakresie (zmienne, które nie są lokalne). Te powiązane zmienne są zastępowalne.

Kładąc wszystko razem

Biorąc pod uwagę pewne założenia (takie jak brak wolnych / niezdefiniowanych zmiennych, znane środowisko), znamy typy:

• elementy atomowe naszych programów (zmienne),
• wartości zwracane przez funkcje (Aplikacja funkcji),
• konstrukty funkcjonalne (funkcja abstrakcyjna),
• let bindings (Let Variable Declarations),
• typy nadrzędne instancji (tworzenie instancji) oraz
• wszystkie wyrażenia (uogólnienie).

Wniosek

Łącznie te reguły pozwalają nam udowodnić najbardziej ogólny typ zapewnianego programu, bez wymagania adnotacji typu.

Notacja pochodzi z naturalnej dedukcji .

⊢ symbol nazywa się kołowrót .

6 zasad jest bardzo łatwe.

Var reguła jest raczej trywialną regułą - mówi, że jeśli typ identyfikatora jest już obecny w twoim środowisku typowym, to aby wywnioskować typ, po prostu zabierz go ze środowiska bez zmian.

AppReguła mówi, że jeśli masz dwa identyfikatory e0i e1możesz wywnioskować ich typy, możesz wywnioskować rodzaj aplikacji e0 e1. Reguła brzmi następująco: jeśli wiesz o tym e0 :: t0 -> t1i e1 :: t0(to samo t0!), To aplikacja jest dobrze napisana, a typ jest t1.

Absi Letsą zasadami wnioskowania o typach dla abstrakcji lambda i let-in.

Inst reguła mówi, że możesz zastąpić typ mniej ogólnym.

Istnieją dwa sposoby myślenia o e: σ. Jeden to „wyrażenie e ma typ σ”, drugi to „uporządkowana para wyrażenia e i typ σ”.

Zobacz Γ jako wiedzę o typach wyrażeń, zaimplementowaną jako zestaw par wyrażeń i typów, e: σ.

Bramka ⊢ oznacza, że ​​z wiedzy po lewej stronie możemy wywnioskować, co jest po prawej stronie.

Można zatem odczytać pierwszą zasadę [Var]:
jeśli nasza wiedza Γ zawiera parę e: σ, to możemy wywnioskować z Γ, że e ma typ σ.

Drugą zasadę [App] można odczytać:
jeśli my z Γ możemy wywnioskować, że e_0 ma typ τ → τ ', a my z Γ możemy wywnioskować, że e_1 ma typ τ, to z Γ możemy wywnioskować, że e_0 e_1 ma wpisz τ ”.

Często pisze się write, e: σ zamiast Γ ∪ {e: σ}.

Trzecią zasadę [Abs] można zatem odczytać:
jeśli z Γ rozszerzonej o x: τ możemy wywnioskować, że e ma typ τ ', to z Γ możemy wywnioskować, że λx.e ma typ τ → τ'.

Czwarta zasada [Let] pozostawia się jako ćwiczenie. :-)

Piątą zasadę [Inst] można odczytać:
jeśli możemy z Γ wywnioskować, że e ma typ σ ', a σ' jest podtypem σ, to z Γ możemy wywnioskować, że e ma typ σ.

Szóstą i ostatnią zasadę [Gen] można odczytać:
jeśli możemy z Γ wywnioskować, że e ma typ σ, a α nie jest zmienną dowolnego typu w żadnym z typów w Γ, wówczas z Γ możemy wywnioskować, że e ma typ ∀α σ.