Existe-t-il un type non trivial qui est égal à sa propre dérivée?

Un article intitulé The Derivative of a Regular Type is its Type of One-Hole Contexts montre que la "fermeture à glissière" d'un type - ses contextes à un trou - suit les règles de différenciation en algèbre de type.

Nous avons:

\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}$

Nous pouvons utiliser ce modèle pour déduire que la dérivée d'unité est nulle, que la dérivée de liste est un produit de deux listes (préfixe fois suffixe), et ainsi de suite.

Une question naturelle à poser est: "quel type est son propre dérivé?" Bien sûr, nous avons déjà , ce qui nous dit que le vide (le type inhabité) est sa propre dérivée, mais ce n'est pas très intéressant. C'est l'analogue du fait que la dérivée de zéro est zéro dans le calcul infinitésimal ordinaire. $\partial_x 0 \mapsto 0$

Y a-t-il d'autres solutions à l'équation ? En particulier, existe-t-il un analogue de dans l'algèbre de type? Pourquoi ou pourquoi pas? $\partial_x T \mapsto T$ $\partial_x e^x = e^x$

type-theory algebra Matthew Piziak
la source

Il y a dans la théorie des espèces combinatoires, et là cela correspond aux espèces d'ensembles (finis), mais cela ne correspond pas à un type de données algébrique.

Derek Elkins a quitté le SE

Qu'entendez-vous par «égal»? Dans votre monde, est-ce que

égaux? Que diriez-vous de

(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 Le premier oui, le second non.

est égal au produit itéré

dans mon esprit. Cela dit, je n'ai pas de modèle rigoureux d'égalité des types dans mon esprit, et si vous en avez un, vous pouvez me le signaler, je serais heureux de le lire.

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 en l'occurrence, un autre article de McBride, intitulé Clowns to the Left of me, Jokers to the Right, souligne que "pour les structures finies, [l'itération d'un opérateur sur les fermetures à glissière] donne lieu à une formulation en série de puissance de types de données directement, trouver tous les éléments de gauche à droite ... Il y a donc un lien significatif avec la notion d'espèce combinatoire ". Je ne serais donc pas surpris que les espèces combinatoires aient un rôle intéressant à jouer dans le contexte de cette question également.

Matthew Piziak

@MatthewPiziak Ils le font certainement. Brent Yorgey en a beaucoup parlé . Voir aussi sa thèse .

Derek Elkins a quitté le SE

Réponses:

Considérons les multisets finis . Ses éléments sont donnés par cotés par permutations, de sorte que pour tout . Qu'est-ce qu'un contexte à un trou pour un élément dans une telle chose? Eh bien, nous devons avoir pour sélectionner une position pour le trou, donc nous nous retrouvons avec les $\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$ éléments, mais nous ne savons pas qui est où. (C'est différent des listes, où le choix d'une position pour le trou coupe une liste en deux sections, et la deuxième coupe dérivée sélectionne l'une de ces sections et la coupe plus loin, comme "point" et "marque" dans un éditeur, mais je m'égare. ) Un contexte à un trou dans un $n-1$ est donc a $\mathbf{Bag}\:X$ , et chaque $\mathbf{Bag}\:X$ peut apparaître comme tel. En pensant spatialement, la dérivée de $\mathbf{Bag}\:X$ doit être lui-même. $\mathbf{Bag}\:X$

Maintenant,

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$

un choix de taille de tuple , avec un tuple de éléments jusqu'à un groupe de permutation d'ordre , ce qui nous donne exactement l'expansion en série de puissance de . $n$ $n$ $n!$ $e^x$

Naïvement, nous pouvons caractériser les types de conteneurs par un ensemble de formes et une famille de positions dépendantes de la forme : $S$ $P$ pour qu'un conteneur soit donné par un choix de forme et une carte des positions aux éléments. Avec des sacs et autres, il y a une touche supplémentaire.

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

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

La "forme" d'un sac est quelque ; les "positions" sont , l'ensemble fini de taille , mais la carte des positions aux éléments doit être invariante sous les permutations de . Il ne devrait y avoir aucun moyen d'accéder à un sac qui "détecte" la disposition de ses éléments. $n\in\mathbb{N}$ $\{1,\ldots,n\}$ $n$ $\mathbf{S}_n$

Le East Midlands Container Consortium a écrit sur ces structures dans Constructing Polymorphic Programs with Quotient Types , for Mathematics of Program Construction 2004. Les conteneurs de quotients étendent notre analyse habituelle des structures par des "formes" et des "positions" en permettant à un groupe d'automorphisme d'agir sur les positions , ce qui nous permet d'envisager des structures telles que des paires non ordonnées , avec un dérivé . Un tuple non ordonné est donné par , et sa dérivée (lorsque est un non ordonné $X^2/2$ $X$ $n$ $X^n/n!$ $n>0$ $n-1$ tuple ). Les sacs en prennent la somme. Nous pouvons jouer à des jeux similaires avec -tuples cycliques , , où le choix d'une position pour le trou cloue la rotation à un endroit, laissant $n$ $X^n/n$ , un tuple plus petit sans permutation. $X^{n-1}$

La "division de type" est difficile à comprendre en général, mais le quotient par groupes de permutation (comme dans les espèces combinatoires) a du sens et est amusant à jouer avec. (Exercice: formuler un principe d'induction structurelle pour des paires de nombres non ordonnées, , etutiliser pour mettreœuvreaddition etmultiplication afin qu'ils soient commutative par construction.) $\mathbb{N}^2/2$

La caractérisation des formes et des positions des conteneurs n'impose ni fin ni fin. Les espèces combinatoires ont tendance à s'organiser par taille , plutôt que par forme, ce qui revient à collecter des termes et à calculer le coefficient pour chaque exposant. Les conteneurs de quotients avec des ensembles de positions finies et les espèces combinatoires sont essentiellement des spins différents sur la même substance.

travailleur du porc
la source

L'auteur original apparaît! Merci d'être venu nous montrer ce beau résultat.

Matthew Piziak

Que diriez-vous de la somme infinie La dérivée est

\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}$ qui est égale à l'original par associativité et commutativité des sommes.

De plus, la somme infinie est égale à ), nous pourrions donc essayer de calculer la dérivée à l'aide de listes. $\sum_{j \in \mathbb{N}} \mathsf{List}(X)$

Andrej Bauer
la source

Le dérivé d'une liste est une paire de listes (préfixe fois suffixe). Par la règle de somme, la dérivée d'une liste de listes est une liste de paires de listes. Une liste de paires de listes est-elle isomorphe à une liste de listes?

Matthew Piziak

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

$\sum_{i\in \mathbb{N}} \mathbb{N}\times X^i$ . En prenant le dérivé, nous obtenons

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

$\sum_{i\in \mathbb{N}} i\times \mathbb{N}\times X^i$ (avec le sens évident pour

i

$i$ ). Maintenant, nous avons seulement besoin

N ≃ i \times N

$\mathbb{N}\simeq i\times \mathbb{N}$ . Pour moi, cela ressemble un peu à (de manière très informelle)

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

$e^x = \sum_i x^i/n!$ , sauf que les coefficients de la série de puissances sont choisis pour être

+ \infty

$+\infty$ (c'est à dire,

N

$\mathbb{N}$ ), afin qu'ils puissent satisfaire

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

$a_{n} = (n+1) \cdot a_{n+1}$ dans un monde sans division.

chi

@MatthewPiziak Oups, j'ai écrit

n

$n$ au lieu de

i

$i$ , mais je pense que ce que je voulais dire est clair.

chi