Czy istnieje nietrywialny typ, który jest równy jego własnej pochodnej?

Artykuł zatytułowany The Derivative of a Regular Type to Type One-Hole Contexts pokazuje, że „zamek błyskawiczny” typu - jego konteksty z jedną dziurą - są zgodne z regułami różnicowania w algebrze typów.

Mamy:

\begin{aligned} \partial_{x} x & \mapsto 1 \\ \partial_{x} 0 & \mapsto 0 \\ \partial_{x} 1 & \mapsto 0 \\ \partial_{x} (S + T) & \mapsto \partial_{x} S + \partial_{x} T \\ \partial_{x} (S \times T) & \mapsto \partial_{x} S \times T + S \times \partial_{x} T \end{aligned}

$\begin{align} \partial_x x &\mapsto 1 \\ \partial_x 0 &\mapsto 0 \\ \partial_x 1 &\mapsto 0 \\ \partial_x (S + T) &\mapsto \partial_x S + \partial_x T \\ \partial_x (S\times T) &\mapsto \partial_xS \times T + S \times \partial_x T \end{align}$

Możemy użyć tego modelu do ustalenia, że pochodna jednostki jest nieważna, że pochodna listy jest iloczynem dwóch list (sufiks razy prefiks) i tak dalej.

Naturalne pytanie, które należy zadać, to: „jaki rodzaj ma własną pochodną?” Oczywiście mamy już , co mówi nam, że pustka (typ niezamieszkany) jest własną pochodną, ale nie jest to bardzo interesujące. Jest to analogiczny fakt, że pochodna zera wynosi zero w zwykłym rachunku nieskończenie małym. $\partial_x 0 \mapsto 0$

Czy istnieją inne rozwiązania równania ? W szczególności, czy istnieje algebra typu ? Dlaczego lub dlaczego nie? $\partial_x T \mapsto T$ $\partial_x e^x = e^x$

type-theory algebra

— Matthew Piziak
źródło

Istnieje teoria gatunków kombinatorycznych i odpowiada ona gatunkom zbiorów (skończonych), ale to nie odpowiada typowi danych algebraicznych.

— Derek Elkins opuścił SE

Co rozumiesz przez „równy”? Czy w twoim świecie

równe? Jak o

and

(S + T) \to U

$(S + T) \to U$

(S \to U) \times (T \to U)

$(S \to U) \times (T \to U)$

N

$\mathbb{N}$

L i s t (N)

$\mathsf{List}(\mathbb{N})$

— Andrej Bauer

@AndrejBauer Pierwsze tak, drugie nie.

jest w moim umyśle równe iloczynowi iloczynu

. To powiedziawszy, nie mam w głowie rygorystycznego modelu równości typów, a jeśli masz model, możesz mnie wskazać, chętnie go przeczytam.

L i s t (N)

$\mathsf{List}(\mathbb{N})$

1 + N + N \times N + N \times N \times N + \dots = \sum_{n = 0}^{\infty} N^{n}

$1 + \mathbb{N} + \mathbb{N} \times \mathbb{N} + \mathbb{N} \times \mathbb{N} \times \mathbb{N} + \ldots = \sum_{n=0}^{\infty} \mathbb{N}^{n}$

— Matthew Piziak

@DerekElkins, jak to się dzieje, kolejny artykuł McBride'a, zatytułowany Clowns to the Left of me, Jokers to the Right zauważa, że: „W przypadku struktur skończonych [iteracja operatora na zamkach błyskawicznych] prowadzi do sformułowania szeregów mocy typów danych bezpośrednio, znajdując wszystkie elementy od lewej do prawej ... Istnieje zatem znaczący związek z pojęciem gatunków kombinatorycznych ". Nie zdziwiłbym się zatem, gdyby gatunki kombinatoryczne miały jakąś interesującą rolę do odegrania również w kontekście tego pytania.

— Matthew Piziak

@MatthewPiziak Zdecydowanie tak. Brent Yorgey dużo o tym mówił . Zobacz także jego pracę magisterską .

— Derek Elkins opuścił SE

Odpowiedzi:

Rozważ skończone multisety . Jego elementy są podane przez wyrażone przez permutacje, tak że dla dowolnego . Jaki jest kontekst z jednym otworem dla elementu w takiej rzeczy? Cóż, musieliśmy mieć aby wybrać pozycję dla otworu, więc pozostało nam pozostałe $\mathbf{Bag}\:X$ $\{x_1,\ldots,x_n\}$ $\{x_1,\ldots,x_n\}=\{x_{\pi 1},\ldots,x_{\pi n}\}$ $\pi\in\mathbf{S}_n$ $n>0$ elementy, ale nie jesteśmy mądrzejsi o tym, gdzie jest. (To w przeciwieństwie do list, w których wybór pozycji dołka wycina jedną listę na dwie sekcje, a druga pochodna wycina zaznacza jedną z tych sekcji i tnie ją dalej, jak „punkt” i „zaznacz” w edytorze, ale dygresję. ) Kontekst z jednym otworem w $n-1$ jest zatem $\mathbf{Bag}\:X$ i każdy $\mathbf{Bag}\:X$ może powstać jako taki. Myśląc przestrzennie, pochodna $\mathbf{Bag}\:X$ powinien być sobą. $\mathbf{Bag}\:X$

Teraz,

B a g X = \sum_{n \in N} X^{n} / S_{n}

$\mathbf{Bag}\:X = \sum\limits_{n\in\mathbb{N}}X^n/\mathbf{S}_n$

wybór krotki , z krotką elementów do grupy permutacji rzędu , co daje nam dokładnie rozszerzenie szeregu mocy . $n$ $n$ $n!$ $e^x$

Naiwnie możemy scharakteryzować typy kontenerów za pomocą zestawu kształtów i zależnej od kształtu rodziny pozycji : $S$ $P$ tak, że kontener jest wybierany przez wybór kształtu i mapy od pozycji do elementów. Z torbami i tym podobnymi dodatkami.

\sum_{s : S} X^{(P s)}

$\sum\limits_{s:S}X^{(P\,s)}$

„Kształt” torby to trochę ; „pozycje” to , skończony zestaw wielkości , ale mapa od pozycji do elementów musi być niezmienna w permutacjach z . Nie powinno być możliwości uzyskania dostępu do torby, która „wykrywa” rozmieszczenie jej elementów. $n\in\mathbb{N}$ $\{1,\ldots,n\}$ $n$ $\mathbf{S}_n$

Konsorcjum East Midlands Container Consortium pisało o takich strukturach w Konstruowaniu programów polimorficznych z typami ilorazowymi dla Matematyki Budowy Programów 2004. Kontenery ilorazowe rozszerzają naszą zwykłą analizę struktur o „kształty” i „pozycje”, umożliwiając grupie automorfizmów działanie na pozycjach , pozwalając rozważyć struktury, takie jak para nieuporządkowana , z pochodnej . Nieuporządkowana liczba jest podana przez , i jej pochodna (gdy jest nieuporządkowanym $X^2/2$ $X$ $n$ $X^n/n!$ $n>0$ $n-1$ krotka). Torby biorą ich sumę. Możemy grać w podobne gry z cyklicznymi kropkami, , w których wybranie pozycji dla otworu powoduje obrót obrotu w jednym miejscu, pozostawiając , krotkę mniejszą bez permutacji. $n$ $X^n/n$ $X^{n-1}$

„Podział typów” jest ogólnie trudny do zrozumienia, ale iloraz według grup permutacyjnych (jak w gatunkach kombinatorycznych) ma sens i jest przyjemny do zabawy. (Ćwiczenie: formułuje zasadę indukcji strukturalną nieuporządkowanych pary liczb, i użyć go do realizacji dodawania i mnożenia, tak że są przemienne o budowie). $\mathbb{N}^2/2$

Charakterystyka „kształtów i pozycji” pojemników nie narzuca skończoności żadnemu. Gatunki kombinatoryczne mają tendencję do organizowania się według wielkości , a nie kształtu, co sprowadza się do zbierania terminów i obliczania współczynnika dla każdego wykładnika. Ilorazowe pojemniki z zestawami pozycji skończonych i gatunki kombinatoryczne to w zasadzie różne spiny tej samej substancji.

— hodowca świń
źródło

Pojawia się oryginalny autor! Dziękujemy za przybycie i pokazanie nam tego pięknego wyniku.

— Matthew Piziak

A co z nieskończoną sumą Pochodna to która jest równa oryginałowi przez asocjatywność i przemienność sum.

\sum_{i, j \in N} X^{i} ?

$\sum_{i, j \in \mathbb{N}} X^i ?$

\sum_{i, j \in N} \underset{i + 1}{\underset{⏟}{X^{i} + \dots + X^{i}}}

$\sum_{i, j \in \mathbb{N}} \underbrace{X^i + \cdots + X^i}_{i+1}$

Ponadto, nieskończona suma jest równa ), więc możemy spróbować obliczyć pochodną za pomocą list. $\sum_{j \in \mathbb{N}} \mathsf{List}(X)$

— Andrej Bauer
źródło

Pochodną listy jest para list (sufiks razy prefiks). Według reguły sumowania pochodną listy list jest lista par list. Czy lista par list jest izomorficzna z listą list?

— Matthew Piziak

\sum_{i \in N} N \times X^{i}

$\sum_{i\in \mathbb{N}} \mathbb{N}\times X^i$

\sum_{i \in N} i \times N \times X^{i}

$\sum_{i\in \mathbb{N}} i\times \mathbb{N}\times X^i$

i

$i$

N ≃ i \times N

$\mathbb{N}\simeq i\times \mathbb{N}$

e^{x} = \sum_{i} x^{i} / n!

$e^x = \sum_i x^i/n!$

+ \infty

$+\infty$

N

$\mathbb{N}$

a_{n} = (n + 1) \cdot a_{n + 1}

$a_{n} = (n+1) \cdot a_{n+1}$

n

$n$

i

$i$