Czy indukcja ścieżki jest konstruktywna?

17

Czytam poprzez książki hott i mam trudności z indukcją ścieżki.

Kiedy patrzę na typ w sekcji 1.12.1 : nie mam problemu ze zrozumieniem, co to znaczy (właśnie napisałem typ z pamięci, aby to sprawdzić).

{ind}_{=_{A}} : \prod_{C : \prod_{x, y : A} (x =_{A} y) \to U} ((\prod_{x : A} C (x, x, {refl}_{x})) \to \prod_{x, y : A} \prod_{p : x =_{A} y} C (x, y, p)),

$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}} \left( \left(\prod_{x:A}C(x,x,\text{refl}_x)\right) \to \prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p) \right),$

Mam problem z następną samą instrukcją: moje pierwsze wrażenie było takie, że to ostatnie wyrażenie nie definiuje wynikowej funkcji a jedynie podaje jej własność .

with the equality {ind}_{=_{A}} (C, c, x, x, {refl}_{x}) :\equiv c (x)

$\text{with the equality}\quad \text{ind}_{=_A}(C,c,x,x,\text{refl}_x):\equiv c(x)$

f : \prod_{x, y : A} \prod_{p : x =_{A} y} C (x, y, p),

$f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$

Jest to w przeciwieństwie do poprzednich przykładów zasad wprowadzających , lub - tam są zdefiniowaniu równania dla tych elementów - faktycznie wie, jak skonstruować wynikowy funkcję danego pomieszczenia. Co jest zgodne z „konstruktywnością” teorii typów reklamowaną w całym rozdziale. $\text{ind}_{A\times B}$ $\text{ind}_{A+B}$ $\text{ind}_\mathbb{N}$

Wracając do $\text{ind}_{=_A}$ , byłem podejrzliwy co do tego, że (wygląda jak) nie jest zdefiniowane. Stwierdzenie, że element $f$ właśnie istnieje, wydawało się niezgodne z resztą rozdziału. I rzeczywiście, sekcja 1.12.1 wydaje się podkreślać, że moje wrażenie jest błędne, a my faktycznie to zdefiniowaliśmy

... funkcja określa indukcji ścieżka z , który ponadto spełnia ... $f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$
$c:\prod_{x:A}C(x,x,\text{refl}_x)$
$f(x,x,\text{refl}_x):\equiv c(x)$

To sprawia, że jestem całkowicie zdezorientowany, ale mam wrażenie, że ten punkt jest bardzo ważny dla wszystkich dalszych zmian. Więc z którym z dwóch odczytów dla powinienem iść? A może brakuje mi ważnej subtelności, a odpowiedź brzmi „ani”? $\text{ind}_{=_A}$

induction dependent-types homotopy-type-theory

— Kostya
źródło

Nawiasem mówiąc, nie jest to tak naprawdę pytanie specyficzne dla HoTT, ale bardziej ogólne pytanie „typów zależnych”.

— cody

12

To złudzenie, że reguły obliczeniowe „definiują” lub „konstruują” obiekty, o których mówią. Prawidłowo zauważyłeś, że równanie dla nie „go definiuje”, ale nie zauważyłeś, że to samo dotyczy również innych przypadków. Rozważmy zasadę indukcji dla jednostki typu , która wydaje się szczególnie wyraźnie „określona”. Zgodnie z rozdziałem 1.5 książki HoTT mamy z równanie Czy to „definiuje” czy „konstruuje” w tym sensie, że nie pozostawia wątpliwości, co „robi”? Na przykład ustaw $\mathrm{ind}_{=_A}$ $1$

{i n d}_{1} : \prod_{C : 1 \to T y p e} C (⋆) \to \prod_{x : 1} P (x)

$\mathrm{ind}_1 : \prod_{C : 1 \to \mathtt{Type}} C(\star) \to \prod_{x : 1} P(x)$

{i n d}_{1} (C, c, ⋆) = c .

$\mathrm{ind}_1 (C, c, \star) = c.$

{i n d}_{1}

$\mathrm{ind}_1$

{i n d}_{1}

$\mathrm{ind}_1$

C (x) = N

$C(x) = \mathbb{N}$ i i zastanów się, co moglibyśmy powiedzieć o

a = 42

$a = 42$

{i n d}_{1} (C, 42, e)

$\mathrm{ind}_1(C, 42, e)$

e

$e$ typu . Twoja pierwsza myśl może być taka, że możemy zmniejszyć to do ponieważ „ jest jedynym elementem ”. Aby być bardziej precyzyjnym, równanie dla ma zastosowanie tylko wtedy, gdy pokażemy

1

$1$

42

$42$

⋆

$\star$

1

$1$

{i n d}_{1}

$\mathrm{ind}_1$

e \equiv ⋆

$e \equiv \star$ , co jest niemożliwe , na przykład, gdy jest zmienną. Możemy próbować poruszać się z tego i powiedzieć, że jesteśmy zainteresowani tylko w obliczeniach z zamkniętymi warunkach, tak powinny być zamknięte.

e

$e$

e

$e$

Czy nie jest tak, że każdy zamknięty termin typu jest w sensie sądowym równy $e$ $1$ $\star$ ? To zależy od nieprzyjemnych szczegółów i skomplikowanych dowodów normalizacji. W przypadku HoTT odpowiedź brzmi „nie”, ponieważ mogą zawierać instancje aksjomatu Univalence, i nie jest jasne, co z tym zrobić (jest to otwarty problem w HoTT). $e$

Możemy obejść problemy z univalance uznając wersję typu teorii, która robi dobre właściwości, tak aby każdy zamknięty określenie typu jest judgmentally równa . W takim przypadku można powiedzieć, że tak $1$ $\star$ wiem jak obliczyć z , ale: $\mathrm{ind}_1$

To samo dotyczy typu tożsamości, ponieważ każdy zamknięty termin typu tożsamości będzie sądowo równy pewnym , a więc równanie dla $\mathrm{refl}(a)$ $\mathrm{ind}_{=_A}$ będzie stwierdzić nas jak obliczyć.
Tylko dlatego, że wiemy, jak obliczyć z zamkniętymi terminami typu, nie oznacza to, że faktycznie coś zdefiniowaliśmy, ponieważ istnieje więcej niż typ zamknięty , jak próbowałem kiedyś wyjaśnić.

Na przykład teorię typów Martina-Löfa (bez typów tożsamości) można interpretować teoretycznie w domenie w taki sposób, że zawiera dwa elementy i , gdzie odpowiada a nieterminacji. Niestety, ponieważ w teorii typów nie ma sposobu, aby zapisać wyrażenie nie kończące się, nie można nazwać . W związku z tym, równanie ma nie $1$ $\bot$ $\top$ $\top$ $\star$ $\bot$ $\bot$ $\mathrm{ind}_1$ mówią nam, jak obliczyć na (dwa oczywiste wybory są „chętnie” i „leniwie”). $\bot$

Pod względem inżynierii oprogramowania powiedziałbym, że mamy pomieszanie specyfikacji i implementacji . Aksjomaty HoTT dla typów tożsamości są specyfikacją . Równanie nie mówi nam, jak obliczyć, ani jak zbudować , ale raczej, że jednak jest „zaimplementowany”, wymagamy, aby spełniał równanie. Osobnym pytaniem jest, czy taki można uzyskać w konstruktywny sposób. $\mathrm{ind}_{=_C}(C,c,x,x,\mathrm{refl}(x)) \equiv c(x)$ $\mathrm{ind}_{=_C}$ $\mathrm{ind}_{=_C}$ $\mathrm{ind}_{=_C}$

Wreszcie jestem trochę zmęczony tym, jak używasz słowa „konstruktywny”. Wygląda na to, że uważasz, że „konstruktywny” jest taki sam jak „zdefiniowany”. Zgodnie z tą interpretacją wyrocznia Halting jest konstruktywna, ponieważ jej zachowanie jest określone przez nałożony na nią wymóg (mianowicie, że generuje 1 lub 0 w zależności od tego, czy dana maszyna zatrzymuje się). Idealnie możliwe jest opisywanie obiektów, które istnieją tylko w niekonstruktywnym otoczeniu. I odwrotnie, można całkowicie konstruktywnie mówić o właściwościach i innych rzeczach, których w rzeczywistości nie można obliczyć. Oto jedna: relacja jest konstruktywna, tzn. Nie ma nic złego w tej definicji z konstruktywnego punktu widzenia. Tak się składa, że konstruktywnie nie można wykazać, że jest relacją całkowitą, $H \subseteq \mathbb{N} \times \{0,1\}$ zdefiniowana przez

H (n, d) ⟺ (d = 1 \Rightarrow n -th machine halts) \land (d = 0 \Rightarrow n -th machine diverges)

$H(n,d) \iff (d = 1 \Rightarrow \text{$n$-th machine halts}) \land (d = 0 \Rightarrow \text{$n$-th machine diverges})$

H

$H$

χ_{H} : N \times {0, 1} \to P r o p

$\chi_H : \mathbb{N} \times \{0,1\} \to \mathsf{Prop}$ nie uwzględnia przez , więc nie możemy „obliczyć” jego wartości.

b o o l

$\mathtt{bool}$

Uzupełnienie: Tytuł twojego pytania brzmi: „Czy indukcja ścieżki jest konstruktywna?” Po wyjaśnieniu różnicy między „konstruktywnym” a „zdefiniowanym” możemy odpowiedzieć na pytanie. Tak, wiadomo, że indukcja ścieżki jest konstruktywna w niektórych przypadkach:

Jeśli ograniczymy się do teorii typów bez Jedności, abyśmy mogli wykazać silną normalizację, wówczas indukcja ścieżki i wszystko inne jest konstruktywne, ponieważ istnieją algorytmy, które wykonują procedurę normalizacji.
Istnieją modele wykonalności teorii typów, które wyjaśniają, w jaki sposób każdy termin zamknięty w teorii typów odpowiada maszynie Turinga. Jednak te modele spełniają Axiom K Streichera, co wyklucza Univalence.
Istnieje tłumaczenie teorii typów (ponownie bez Univalence) na konstruktywną teorię zbiorów CZF. Po raz kolejny potwierdza to aksjomat K. Streichera
W modelach wykonalności znajduje się model grupoidalny, który pozwala nam interpretować teorię typów bez K. Streichera. To wstępna praca Steve'a Awodeya i mnie.

Naprawdę musimy ustalić konstruktywny status Univalence.

— Andrej Bauer
źródło

Wierzę, że ta odpowiedź jest (częściowo) nieaktualna

— WorldSEnder

Rzeczywiście, w międzyczasie teoria typu sześciennego dała pozytywną odpowiedź: istnieje konstruktywny model teorii typu Univalent.

— Andrej Bauer,

7

Nie jestem osobą HoTT, ale wrzucę moje dwa centy.

Załóżmy, że chcemy stworzyć funkcję Jak to zrobilibyśmy? Załóżmy, że otrzymaliśmy dowolne i dowód ich równości . Ponieważ nic nie wiem o dowolnym typie , nie wiem nic o „strukturze” . Wiem jednak coś o konkretnym typie równości: ma on jednego konstruktora, Stąd, for niektóre , ale wymusiłoby to . Dlatego jeśli mielibyśmy element dla dowolnego

f_{A} : \prod_{x, y : A} \prod_{p : x =_{A} y} C (x, y, p)

$f_A : \prod_{x,y : A}\prod_{p : x =_A y} C(x,y,p)$

x, y : A

$x,y : A$

p : x =_{A} y

$p : x =_A y$

A

$A$

x, y

$x,y$

{r e f l}_{a} : a =_{A} a, for any a : A

$\mathsf{refl}_a : a =_A a, \text{ for any } a : A$

p \equiv {r e f l}_{a}

$p \equiv \mathsf{refl}_a$

a : A

$a : A$

x = a = y

$x=a=y$

C (x, x, {r e f l}_{x})

$C(x,x,\mathsf{refl}_x)$

x : A

$x : A$ ; tzn. jeśli mielibyśmy funkcję (dla naszego konkretnego ), to naszą funkcję można zdefiniować w następujący sposób: .

b a s e_{C} : \prod_{x : A} C (x, x, {r e f l}_{x})

$base_C : \prod_{x:A}C(x,x,\mathsf{refl}_x)$

C

$C$

f_{A}

$f_A$

f_{A} (x, y, p) := b a s e_{C} (x, x, p)

$f_A(x,y,p) := base_C(x,x,p)$

Pozbycie się indeksów dolnych prowadzi do ogólnej definicji indukcyjnej.

Mam nadzieję, że to pomaga!

PS. Nie jestem facetem HoTT, więc zakładam „Axiom K”. Dokładniej, jestem przy założeniu, że element typu musi być wynikiem wielokrotnych zastosowań konstruktora . O ile mi wiadomo, HoTT, prawdopodobnie rozdział 2, odrzuca to pojęcie ... i to nie ma dla mnie żadnego sensu. $e$ $E$ $E$

— Musa Al-hassy
źródło

1

Być może możesz to zrozumieć, a przynajmniej martwić się o swoje obecne intuicje, sprawdzając math.andrej.com/2013/08/28/the-elements-of-an-inductive-typ, w którym próbuję wyjaśnić, dlaczego myślenie, że zamknięte terminy danego typu są dla danego typu szkodliwe, jest szkodliwe.

— Andrej Bauer,

2

r e f l

$\mathsf{refl}$

3

$A\times B$ $A\times B$

p a i r : A \to B \to A \times B

$\mathrm{pair}\ :\ A\rightarrow B\rightarrow A\times B$

f

$f$

A \times B

$A\times B$ , wystarczy opisać swoje działania na $\mathrm{pair}$

$\mathrm{pair}$ $f:A\times B\rightarrow C$ $A$ $B$

{fa}^{'} : ZA \to b \to do

$f':A\rightarrow B\rightarrow C$

f

$f$

A \times B

$A\times B$

(ZA \to b \to do) \to (ZA \times b \to do)

$(A\rightarrow B\rightarrow C)\rightarrow(A\times B\rightarrow C)$

{i n d}_{A \times B}

$\mathrm{ind}_{A\times B}$

$f$ $\mathrm{pair}(a,b)$ $f$ $f'$

fa (p za ja r (za, b)) : = {fa}^{'} za b

$f(\mathrm{pair}(a,b))\ :=\ f'\ a\ b$

{ja n re}_{ZA \times b} {fa}^{'} p za ja r (za, b) : = {fa}^{'} za b

$\mathrm{ind}_{A\times B}\ f'\ \mathrm{pair}(a,b)\ :=\ f'\ a\ b$

=

$=$

Widzicie więc, że definicja eliminatora typu indukcyjnego w danych konstruktorach składa się z 2 etapów:

$\mathrm{ind}$
$\mathrm{ind}$

$=_A$ $x,y:A$ $p:x=y$ $C$ $p$ $x=y$ $\mathrm{refl}(z)$ $z$

f : Π x, y : A, x = y \to C

$f:\Pi x, y:A, x=y\rightarrow C$

f^{'} : Π z : A, C

$f':\Pi z:A, C$

r e f l (z)

$\mathrm{refl}(z)$

C

$C$

$f$ $f'$

f z z r e f l (z) := f^{'} z

$f\ z\ z\ \mathrm{refl}(z):= f'\ z$

$A\times B$ $=_A$

— cody
źródło