Co oznacza wiodący operator kołowrotu?

Wiem, że różni autorzy używają różnych notacji do reprezentacji semantyki języka programowania. W rzeczywistości Guy Steele rozwiązuje ten problem w ciekawym filmie .

Chciałbym wiedzieć, czy ktoś wie, czy wiodący operator bramki obrotowej ma dobrze rozpoznane znaczenie. Na przykład nie rozumiem wiodącego operatora na początku mianownika:$\vdash$

Czy ktoś może mi pomóc zrozumieć? Dzięki.

Po lewej stronie bramki znajduje się kontekst lokalny, skończona lista założeń dotyczących typów zmiennych.

Wyżej, może mieć wartość zero, co skutkuje ⊢ E : T . Oznacza to, że nie przyjęto żadnych założeń dotyczących zmiennych. Zwykle oznacza to, że E stanowi zamkniętą określenie (bez zmiennych wolnych) o typ T .$n$$\vdash e:T$$e$$T$

Często wspomniana reguła jest napisana w bardziej ogólnej formie, w której może być więcej hipotez niż wspomniana w pytaniu.

Tutaj reprezentuje dowolny kontekst, a Γ , x : T 1 reprezentuje jego rozszerzenie uzyskane przez dołączenie dodatkowej hipotezy x : T 1 do listy Γ . Często wymagane jest, aby $\Gamma$$\Gamma, x:T_1$$x:T_1$$\Gamma$$x$ nie pojawiał się w , aby rozszerzenie nie „kolidowało” z poprzednim założeniem.$\Gamma$

Jako uzupełnienie innych odpowiedzi należy zauważyć, że istnieją trzy poziomy „implikacji” w pisaniu pochodnych. Ta sama uwaga dotyczy logicznych pochodnych, ponieważ w rzeczywistości istnieje między nimi zgodność (zwana korespondencją Curry-Howarda).

Pierwszą implikacją jest strzałka pojawiająca się w formułach, która odpowiada logicznej implikacji w formule (lub typie funkcji dla kalkulatora).$\lambda$

Druga implikacja została zmaterializowana przez symbol bramki obrotowej i oznacza „przy założeniu, że każda formuła po lewej stronie ma formułę po prawej”. W szczególności reguła, którą podajesz, mówi, w jaki sposób należy udowodnić implikację: aby udowodnić , wówczas należy udowodnić B przy założeniu, że A ma. Pod względem λ- rachunek, aby udowodnić, że λ x . t ma typ A → B , należy wykazać, że t ma typ B , zakładając, że x jest zmienną typu$A \Rightarrow B$$B$$A$$\lambda$$\lambda x.t$$A \to B$$t$$B$$x$$A$ (patrz korespondencja?).

Trzeci poziom implikacji jest urzeczywistniany przez poziomy pasek i oznacza „jeśli każda przesłanka (elementy u góry) ma miejsce, wówczas wniosek (element u dołu) ma miejsce”. Możesz to powiązać z interpretacją reguły pisania dla podanego przez ciebie abstrakcji (zobacz wyjaśnienie w poprzednim akapicie).$\lambda$

W systemach kontroli typu ( ) reprezentuje trójskładnikową relację w środowiskach typów, wyrażeniach i typach: ⊢ E n v × E x p × T y $\vdash$$\vdash \texttt Env \times \texttt Exp \times \texttt Typ$ .

W twoim przykładzie wyrażenie jest wpisane jako typ T 2 wrt. w środowisku typu mającego odwzorowanie typu założeniu, T 1 do pewnego typu zmiennej $t_2$$T_2$ $T_1$$x$

W tym kontekście środowisko typów jest funkcją częściową, która przypisuje typy do zmiennych, zwykle oznaczonych gdzie Γ ∈ E n v : V a r ⇀ T y $\Gamma$$\Gamma \in \texttt Env : Var \rightharpoonup Typ$

Należy pamiętać, że operator zastrzega swoją funkcjonalność niezależnie od tego, gdzie się pojawi, zarówno w założeniu, jak i po zawarciu reguły.

W każdej sytuacji, które widziałem, oznacza, że istnieje dowód  Y zakładając, że X  trzyma. Jeśli X  jest pusty, oznacza to, że Y  jest tautologią: ma dowód bez potrzeby żadnych założeń.$X\vdash Y$$Y$$X$$X$$Y$