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

20

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:

xx1x00x10x(S+T)xS+xTx(S×T)xS×T+S×xT

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.x00

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

Matthew Piziak
la source
5
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
1
Qu'entendez-vous par «égal»? Dans votre monde, est-ce que et ( S U ) × ( T U ) sont égaux? Que diriez-vous de N et L i s t ( N ) ? (S+T)U(SU)×(TU)NList(N)
Andrej Bauer
1
@AndrejBauer Le premier oui, le second non. est égal au produit itéré 1 + N + N × N + N × N × N + = n = 0 N n 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. List(N)1+N+N×N+N×N×N+=n=0Nn
Matthew Piziak
3
@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:

15

Considérons les multisets finis . Ses éléments sont donnés par { x 1 , , x n } cotés par permutations, de sorte que { x 1 , , x n } = { x π 1 , , x π n } pour tout π S n . Qu'est-ce qu'un contexte à un trou pour un élément dans une telle chose? Eh bien, nous devons avoir n > 0 pour sélectionner une position pour le trou, donc nous nous retrouvons avec les n -BunegX{x1,,xn}{x1,,xn}={xπ1,,xπn}πSnn>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 B a gn1 est donc a B a gBagX , et chaque B a gBagX peut apparaître comme tel. En pensant spatialement, la dérivée de B a gBagX doit être lui-même.BagX

Maintenant,

BagX=nNXn/Sn

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

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 P : s : S X ( PSP 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.

s:SX(Ps)

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

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é X . Un n- tuple non ordonné est donné par X n / n ! , et sa dérivée (lorsque n > 0 est un n - 1 non ordonnéX2/2XnXn/n!n>0n1 tuple ). Les sacs en prennent la somme. Nous pouvons jouer à des jeux similaires avec -tuples cycliques , X n / n , où le choix d'une position pour le trou cloue la rotation à un endroit, laissant X n -nXn/n , un tuple plus petit sans permutation.Xn1

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.)N2/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
3

Que diriez-vous de la somme infinie La dérivée est i , j N X i + + X i i + 1

i,jNXi?
i,jNXi++Xii+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.jNList(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
jeNN×Xje. En prenant le dérivé, nous obtenonsjeNje×N×Xje (avec le sens évident pour je). Maintenant, nous avons seulement besoinNje×N. Pour moi, cela ressemble un peu à (de manière très informelle)eX=jeXje/n!, sauf que les coefficients de la série de puissances sont choisis pour être + (c'est à dire, N), afin qu'ils puissent satisfaire unen=(n+1)unen+1dans un monde sans division.
chi
@MatthewPiziak Oups, j'ai écrit n au lieu de je, mais je pense que ce que je voulais dire est clair.
chi