Jakie są prawa równań dla typów zerowych?

Oświadczenie : chociaż dbam o teorię typów, nie uważam się za eksperta w dziedzinie teorii typów.

W prostym typie rachunku lambda typ zerowy nie ma konstruktorów i unikalnego eliminatora:

\frac{Γ ⊢ M : 0}{Γ ⊢ i n i t i a l (M) : A}

$\frac{\Gamma \vdash M \colon 0}{\Gamma \vdash initial (M) \colon A}$

Z denotacyjnego punktu widzenia równanie $initial (M_1) = initial(M_2)$ jest oczywiste (gdy typy mają sens).

Jednak z tej perspektywy mogę również wywnioskować, że gdy $M,M' \colon 0$ , to: $M = M'$ . Ta dedukcja wydaje się silniejsza, chociaż umyka mi konkretny model, który ją pokazuje.

(Mam jednak pewną intuicję teoretyczną: nie ma znaczenia, jakiej sprzeczności używasz w celu uzyskania mieszkańca, ale mogą istnieć różne dowody sprzeczności).

Więc moje pytania to:

Jakie są standardowe prawa równań dla typów zerowych?
Czy którekolwiek z nich są klasyfikowane jako prawa $\eta$ lub $\beta$ ?

pl.programming-languages type-theory lambda-calculus semantics Ohad Kammar
źródło

Odpowiedzi:

Standardowe reguły równań dla pustego typu to, jak się domyślacie, . Pomyśl o standardowym modelu teoretycznym, w którym zbiory są interpretowane według typów: typy sum są rozłącznymi związkami, a pusty typ jest pustym zbiorem. Tak więc dowolne dwie funkcje również muszą być równe, ponieważ mają wspólny wykres (mianowicie pusty wykres). . $\Gamma \vdash e = e' : 0$ $e,e' : \Gamma \to 0$
Pusty typ nie ma reguł , ponieważ nie ma dla niego żadnych formularzy wprowadzających. Jedyną regułą równania jest reguła . Jednak w zależności od tego, jak ściśle chcesz interpretować zasadę eta, możesz podzielić to na plus konwersję dojazdów do pracy. Ścisłe Regułę jest: $\beta$ $\eta$ $\eta$ $\eta$

$e = i n i t i a l (e)$ $e = \mathrm{initial}(e)$
Coversion dojazdów do pracy to:

$C [i n i t i a l (e)] = i n i t i a l (e)$ $C[\mathrm{initial}(e)] = \mathrm{initial}(e)$

EDYTOWAĆ:

Oto dlaczego dystrybucja w typie zerowym oznacza równość wszystkich map . $A \to 0$

Aby naprawić notację, napiszmy aby być unikalną mapą od do , i napiszmy aby była mapą od do . $!_A : 0 \to A$ $0$ $A$ $e : A \to 0$ $A$ $0$

Teraz warunek dystrybucji mówi, że występuje izomorfizm . Ponieważ obiekty początkowe są unikalne aż do izomorfizmu, oznacza to, że jest samym obiektem początkowym. Możemy teraz użyć tego, aby pokazać, że sam jest obiektem początkowym. $i : 0 \simeq A \times 0$ $A \times 0$ $A$

Ponieważ jest obiektem początkowym, znamy mapy i są równe. $A \times 0$ $\pi_1 : A \times 0 \to A$ $!_A \circ \pi_2$

Teraz, aby pokazać, że jest obiektem początkowym, musimy pokazać izomorfizm między nim a . Wybierzmy i jako składniki izomorfizmu. Chcemy pokazać, że i . $A$ $0$ $e : A \to 0$ $!_A : 0 \to A$ $e \circ !_A = id_0$ $!_A \circ e = id_A$

Pokazuje to jest natychmiastowe, ponieważ istnieje tylko jedna mapa typu i wiemy, że zawsze istnieje mapa tożsamości. $e \circ !_A = id_0$ $0 \to 0$

Aby pokazać inny kierunek, zwróć uwagę

\begin{array}{lcll} i d_{A} & = & π_{1} \circ (i d_{A}, e) & Product equations \\ = & !_{A} \circ π_{2} \circ (i d_{A}, e) & Since A \times 0 is initial \\ = & !_{A} \circ e & Product equations \end{array}

$\begin{array}{lcll} id_A & = & \pi_1 \circ (id_A, e) & \mbox{Product equations} \\ & = & !_A \circ \pi_2 \circ (id_A, e) & \mbox{Since $A\times 0$ is initial} \\ & = & !_A \circ e & \mbox{Product equations} \end{array}$

Stąd mamy izomorfizm , a więc jest obiektem początkowym. Dlatego mapy są unikalne, więc jeśli masz , to . $A \simeq 0$ $A$ $A \to 0$ $e,e' : A \to 0$ $e = e'$

EDYCJA 2: Okazuje się, że sytuacja jest ładniejsza niż początkowo myślałem. Nauczyłem się od Ulricha Bucholza, że jest oczywiste (w matematycznym znaczeniu „retrospektywnie oczywiste”), że każde biCCC ma charakter dystrybucyjny. Oto uroczy mały dowód: $\newcommand{\Hom}{\mathrm{Hom}}$

\begin{array}{lcl} H o m ((A + B) \times C, (A + B) \times C) & ≃ & H o m ((A + B) \times C, (A + B) \times C) \\ ≃ & H o m ((A + B), C \to (A + B) \times C) \\ ≃ & H o m (A, C \to (A + B) \times C) \times H o m (B, C \to (A + B) \times C) \\ ≃ & H o m (A \times C, (A + B) \times C) \times H o m (B \times C, (A + B) \times C) \\ ≃ & H o m ((A \times C) + (B \times C), (A + B) \times C) \end{array}

$\begin{array}{lcl} \Hom((A + B) \times C, (A + B) \times C) & \simeq & \Hom((A + B) \times C, (A + B) \times C) \\ & \simeq & \Hom((A + B), C \to (A + B) \times C) \\ & \simeq & \Hom(A , C \to (A + B) \times C) \times \Hom(B, C \to (A + B) \times C) \\ & \simeq & \Hom(A \times C, (A + B) \times C) \times \Hom(B \times C, (A + B) \times C) \\ & \simeq & \Hom((A \times C) + (B \times C), (A + B) \times C) \end{array}$

Neel Krishnaswami
źródło

Odnośnie 1: Myślę, że typ zerowy jest początkowym obiektem. Początkowe obiekty mogą mieć wiele strzałek do nich, ale może mieć tylko jedna strzałka się od nich. Innymi słowy, nie widzę od razu żadnego powodu, dla którego bycie bi-CCC sugeruje, że 0 jest subterminalne. Czy jest jeden

Ohad Kammar

Tak: fakt, że STLC z sumami wymaga rozdzielającego bi-CCC ( ), a także wyjątkowość dla 0 typ jest jego zerową wersją. (Spróbuj zapisać interpretację reguły eliminacji sum, a zobaczysz ją.)

(X \times A) + (X \times B) ≃ X \times (A + B)

$(X \times A) + (X \times B) \simeq X \times (A+B)$

Neel Krishnaswami

Nie podążam. Dystrybucja wynosi o odwrotności. Dlaczego to oznacza, że jest subterminalne?

i n i t i a l : 0 \to A \times 0

$initial : 0 \to A\times 0$

0

$0$

Ohad Kammar

Aha! Dzięki za ten dowód! I za cierpliwość!

Ohad Kammar

odnośnie do edycji 2: Lewe punkty pośrednie zachowują kolimity. Jeżeli kategoria jest zamknięty kartezjańskim, a pozostało sprzężona do tak jest suma .

(-) \times C

$(-)\times C$

(-)^{C}

$(-)^C$

(A + B) \times C

$(A+B)\times C$

A \times C + B \times C

$A\times C + B\times C$

Ohad Kammar

Równanie uchwyca tylko fakt, że ma najwyżej jeden element, więc nie sądzę, że Neel przechwytuje całą historię. Aksjatyzuję pusty typ w następujący sposób. $e = e' : 0$ $0$ $0$

Brak zasad wprowadzania. Reguła eliminacji toRównanie to gdzie i . W całym jest dowolny typ. Równanie jest motywowane następująco: jeśli udało ci się sformułować termin wówczas jest zamieszkane przez , ale jest to absurd, więc wszystkie równania są ważne. Zatem innym sposobem osiągnięcia tego samego efektu byłoby równania

\frac{e : 0}{{m a g i c}_{τ} (e) : τ} .

$\frac{e : 0}{\mathtt{magic}_\tau(e) : \tau}.$

{m a g i c}_{τ} (e) = e^{'} : τ

$\mathtt{magic}_\tau(e) = e' : \tau$

e : 0

$e : 0$

e^{'} : τ

$e' : \tau$

τ

$\tau$

{m a g i c}_{τ} (e)

$\mathtt{magic}_\tau(e)$

0

$0$

e

$e$

x : 0, Γ ⊢ e_{1} = e_{2} : τ

$x : 0, \Gamma \vdash e_1 = e_2 : \tau$ co może nie jest tak miłe, ponieważ majstruje w kontekście. Z drugiej strony pokazuje to wyraźniej, że stwierdzamy, że dowolne dwa morfizmy od do są równe ( jest rozproszeniem w CCC).

0

$0$

τ

$\tau$

Γ

$\Gamma$

Andrej Bauer
źródło

Cześć Andrej, równanie, które sugerujesz, można wyprowadzić z podanej przeze mnie konwersji dojazdowej. można uzyskać z , ponieważ tak naprawdę nie musi wystąpić na lewy termin. Analogia jest do , gdzie nieużywanie wyniku analizy przypadków jest w porządku, jeśli robisz to samo w obu gałęziach.

m a g i c (e) = e^{'}

$\mathtt{magic}(e) = e'$

C [m a g i c (e)] = m a g i c (e)

$C[\mathtt{magic}(e)] = \mathtt{magic}(e)$

m a g i c (e)

$\mathtt{magic}(e)$

C [c a s e (e, x . e^{'}, y . e^{″})] = c a s e (e, x . C [e^{'}], y . C [e^{″}])

$C[\mathtt{case}(e,x.\;e',y.\;e'')] = \mathtt{case}(e, x.\;C[e'], y.\;C[e''])$

Neel Krishnaswami

Powinienem jednak dodać, że bardziej podoba mi się prezentacja z kontekstami - myślę, że ogólnie jest najczystsza, jeśli w rzeczywistości pozwalasz na równania na wartościach sumarycznych w kontekście! Jest to o wiele ładniejsze w przypadku faktycznych dowodów niż gry z konwersjami dojazdów do pracy, IMO. (IIRC, jest to równoważne z dodaniem dodatkowego założenia o stabilnych koproduktach, ale dla wszystkich modeli rozsądnie widzę, że dba o to.)

Neel Krishnaswami

Ach tak, świetnie. Było za późno, aby pomyśleć o konwersjach dojazdowych, więc udawałem, że nie napisałeś tej części. Teraz Ohad może wybrać.

Andrej Bauer,

Sprawdzałem poprawność niektórych reguł strukturalnych ( , itp.) W klasie modeli. Chociaż wiem, że zestaw równań, które podałem, nie był kompletny (potrzebujesz CBPV ze złożonymi wartościami i stosami do tego), chciałem przynajmniej uchwycić standardowe równania, które zostaną wykorzystane do udowodnienia kompletności, jeśli będę miał wystarczającą liczbę równań. Innymi słowy, chciałem standardowych praw równań dla typów zerowych.

η

$\eta$

β

$\beta$

Ohad Kammar

Nie ma standardowych praw równań dla typów zerowych. Logicy zawsze bali się pustego wszechświata dyskursu, a informatycy zawsze bali się pustego typu. Nazwali nawet niepusty typ „void”, aby odmówić pustego typu.

Andrej Bauer,