Co oznacza wiodący operator kołowrotu?

12

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$

\frac{x : {T.}_{1} ⊢ t_{2)} : {T.}_{2)}}{⊢ λ x : {T.}_{1} . t_{2)} : {T.}_{1} \to {T.}_{2)}}

$\frac{x:T_1 \vdash t_2:T_2}{\vdash \lambda x:T_1 . t_2 ~:~ T_1 \to T_2}$

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

type-theory denotational-semantics

— Jim Newton
źródło

Powiązane

— leftaroundabout

Wow, to pytanie ma ponad „1k” wyświetleń, co jest więcej niż sumą wyświetleń wszystkich pozostałych 29 nowych pytań! Jak sprawdziłem, ani znacznik „teoria typów”, ani znacznik „semantyka denotacyjna” nie należą do pierwszych 50 popularnych znaczników. Jestem ciekawy przyczyny tego zjawiska. Nie mam pojęcia. @DW? Czy mam pytanie meta?

— John L.

Jeśli się nie mylę, musisz przesunąć operator bramki (

), zgodnie z regułą, między

i

. Dodałbym również tag

⊢

$\vdash$

λ x : T_{1}

$\lambda x:T_1$

t_{2}

$t_2$ type-checking

— mchar

3

@ Apass.Jack Skończyło się na gorących pytaniach sieciowych, dlatego coraz więcej uwagi z tego powodu.

— JAB

20

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

x_{1} : {T.}_{1}, \dots, x_{n} : {T.}_{n} ⊢ mi : T.

$x_1:T_1, \ldots, x_n:T_n \vdash e:T$

Wyżej, może mieć wartość zero, co skutkuje . Oznacza to, że nie przyjęto żadnych założeń dotyczących zmiennych. Zwykle oznacza to, że stanowi zamkniętą określenie (bez zmiennych wolnych) o typ . $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.

\frac{Γ, x : {T.}_{1} ⊢ t : {T.}_{2)}}{Γ ⊢ (λ x : {T.}_{1} . t) : {T.}_{1} \to {T.}_{2)}}

$\dfrac{ \Gamma, x:T_1 \vdash t : T_2 }{ \Gamma\vdash (\lambda x:T_1. t) : T_1\to T_2 }$

Tutaj reprezentuje dowolny kontekst, a reprezentuje jego rozszerzenie uzyskane przez dołączenie dodatkowej hipotezy 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$

— chi
źródło

7

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ć przy założeniu, że ma. Pod względem rachunek, aby udowodnić, że ma typ , należy wykazać, że ma typ , zakładając, że 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$

— Rodolphe Lepigre
źródło

3

W systemach kontroli typu ( ) reprezentuje trójskładnikową relację w środowiskach typów, wyrażeniach i typach: $\vdash$ $\vdash \texttt Env \times \texttt Exp \times \texttt Typ$ .

W twoim przykładzie wyrażenie jest wpisane jako typ wrt. w środowisku typu mającego odwzorowanie typu założeniu, 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 $\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.

— Mchar
źródło

-1

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

— David Richerby
źródło

1

ale jeśli to, co mówisz, jest prawdą, jest to dziwne, ponieważ to również oznacza poziomy pasek, prawda? Że jeśli szczyt jest prawdziwy, to dół jest prawdziwy. W efekcie

oznaczałoby, że jeśli

jest prawdziwe, to

jest bezwarunkowo prawdziwe.

\frac{X}{⊢ Y}

$\frac{X}{\vdash Y}$

X

$X$

Y

$Y$

— Jim Newton,

1

Poziomy pasek oznacza, że rzecz na dole jest natychmiastową dedukcją od rzeczy na górze. Chociaż zgadzam się, że w twoim przykładzie wygląda to bardzo dziwnie, że bezwarunkowa prawda wywodzi się z warunkowej ...

— David Richerby

Teoria typów nie jest logiką. Jest to oczywiście powiązane na wiele sposobów i (do pewnego stopnia celowo) używa podobnej notacji, ale z pewnością nie ma związku a priori ze stosowalnością dowodową, a często też nie ma związku a posteriori (przynajmniej nie z rozsądnie logiczną logiką). Jak napisano, odpowiedź jest co najmniej myląca, ponieważ sugeruje, że „

” jest formułą, której praktycznie nigdy nie ma w teorii typów, np. Język zawierający formuły takie jak

ogół nie jest opisany i często jest niemożliwy w standardowej meta-logice, np. w przypadku liniowego rachunku lambda.

x : T_{1}

$x:T_1$

(x : T_{1}) \lor (y : T_{2})

$(x:T_1)\lor(y:T_2)$

— Derek Elkins opuścił SE

@DerekElkins To system dowodowy, a systemy dowodowe to logika.

jest właśnie twierdzeniem, a

jest niczym innym jak stwierdzeniem, które twierdzenie zawiera, gdy

ma. Fakt, że rozróżnienia zdań nie są formułami, jest po prostu ograniczeniem składni logiki.

x : T

$x\colon T$

Γ ⊢ x : T

$\Gamma\vdash x\colon T$

Γ

$\Gamma$

— David Richerby,

To nie tylko rozłączenie. Żadne z

,

lub

jest formułami. A może mówisz, że to logika, która ma tylko twierdzenia atomowe? Jako przykład podałem logikę liniową. W uporządkowanej logice liniowej bardzo łatwo może się zdarzyć, że

utrzyma się podczas

\neg (x : A)

$\neg (x:A)$

(x : A) \land (y : B)

$(x:A)\land(y:B)$

(x : A) \to (y : B)

$(x:A)\to(y:B)$

x : A, y : B ⊢ t : C

$x:A,y:B\vdash t:C$

nie. Co spójniki zrobić przecinek i

odpowiadać podjąć „wartości Prawda”

,

i

i produkują powyższy zachowanie? Istnieje opcja, jeśli meta-logika jest również uporządkowaną logiką liniową, ale wtedy niczego nie wyjaśniamy.

y : B, x : A ⊢ t : C

$y:B,x:A\vdash t:C$

⊢

$\vdash$

x : A

$x:A$

y : B

$y:B$

t : C

$t:C$

— Derek Elkins opuścił SE