Isomorphismes de la structure des données

Avertissement: je ne suis pas un théoricien CS.

Issu de l'algèbre abstraite, j'ai l'habitude de traiter des choses qui sont égales à un isomorphisme - mais j'ai du mal à traduire ce concept en structures de données. J'ai d'abord pensé que des morphismes bijectifs théoriques définis suffisaient, mais je suis tombé sur un mur assez rapidement - ce ne sont que des encodages et ne capturent pas l'essence informatique de la structure des données.

Existe-t-il une définition plus restrictive (mais plus utile)? (Ou sinon, pourquoi?) Existe-t-il une définition canonique de la catégorie des "structures de données construites"?

Il n'y a pas une telle catégorie canonique, pour la même raison il n'y a pas de catégorie canonique de calculs. Cependant, il existe des structures algébriques importantes et utiles sur les structures de données.

L'une des structures plus générales de ce type, qui reste néanmoins utile, est la théorie des espèces combinatoires. Une espèce est un foncteur , où est la catégorie des ensembles finis et des bijections entre eux. Vous pouvez considérer les espèces comme des familles de structures indexées par des ensembles abstraits d'emplacements. Cela explique la fonction sur - ces familles doivent être invariantes par rapport au changement de nom des étiquettes abstraites. Ensuite, le calcul des espèces rejoue essentiellement la génération de méthodes de fonction au niveau fonctorial, pour générer des ensembles de structures de données au lieu de décomptes.$F : B \to B$$B$$B$

Pour voir cette théorie implémentée dans un langage de programmation, vous pouvez lire l'article de Brent Yorgey's Haskell Symposium, Species and functors and types, oh my! . Je pense que Sage a également un paquet d'espèces, bien qu'il soit bien sûr orienté vers l'algèbre informatique plutôt que vers la programmation.

En effet, il existe une notion différente de l'isomorphisme qui est plus utile en programmation. Elle est appelée «équivalence comportementale» (parfois appelée «équivalence observationnelle») et elle est établie en donnant une «relation de simulation» entre les structures de données plutôt que des bijections. Les algèbres sont entrés et ont établi un domaine appelé "types de données algébriques" en informatique, où ils ont poussé les isomorphismes et les algèbres initiales pendant un certain temps. Finalement, les informaticiens ont réalisé qu'ils étaient induits en erreur. Un bon article qui parle de ces questions est "Sur l'équivalence observationnelle et la spécification algébrique" par Sannella et Tarlecki.

J'ai écrit une réponse à une autre question dans la théorie des relations logiques et des simulations qui parle de l'histoire plus générale des relations de simulation en informatique. Vous êtes invités à lire cela et à suivre les références qui y sont données. Le chapitre 5 de «Craft of Programming» de Reynolds est particulièrement instructif.

Un livre de texte sur la théorie des automates algébriques par Holcombe a la citation intéressante suivante (p. 42):

Il existe de nombreux autres résultats concernant les homomorphismes et les quotients ... Bien qu'ils présentent un intérêt algébrique indépendant, ils ne se sont pas encore révélés particulièrement utiles dans l'étude des automates et des domaines connexes. En fait, la théorie algébrique des machines diverge de la direction prise dans d'autres théories algébriques sur un point important ... Cependant, l'accent dans la théorie des automates n'est pas [sur] ce à quoi les machines "ressemblent" mais ce qu'elles "peuvent faire" . Nous considérerons deux machines comme étant très proches si elles peuvent toutes les deux "faire la même chose", elles peuvent cependant ne pas être algébriquement isomorphes!

Plutôt que de demander comment nous pouvons renforcer / affaiblir la notion d'isomorphisme, une autre possibilité consiste à se demander: quelle est la bonne notion d'équivalence entre les structures de calcul et quelle est la structure mathématique sous-jacente à cette notion.

Une grande famille de structures est constituée de houillères. Des structures telles que des listes, des arbres, des automates, à la fois de la variété finie et infinie, peuvent être décrites comme des houillères. On peut alors étudier l'homomorphisme ou l'isomorphisme entre les houillères.

Cependant, même les homomorphismes entre les houillères ne racontent pas toute l'histoire. Il peut être utile de rechercher des simulations, des bisimulations et d'autres relations logiques. Si vous préférez strictement une approche algébrique (par opposition à une approche relationnelle), les connexions Galois sont une option. Voici quelques points de départ.

• Relations logiques et connexions Galois par Backhouse et Backhouse.
• Coalgebra universelle: une théorie des systèmes par Jan Rutten

Avertissement: je ne suis pas sûr d'avoir compris votre question. Voulez-vous parler d'isomorphisme entre deux structures de données, ou entre deux "spécifications de structure de données"? (Ils sont parfois appelés types de données abstraits.)

Si vous considérez le modèle de sonde cellulaire, je pense qu'un concept d'isomorphisme apparaît facilement. En effet, le modèle de sonde cellulaire modélise le calcul par un arbre de décision, l'isomorphisme est donc facile à définir. Le modèle de sonde cellulaire aiderait, je pense, à la fois si vous considérez l'isomorphisme entre les implémentations de structure de données et si vous considérez les spécifications de structure de données.

Pour plus d'informations sur le modèle de sonde cellulaire, voir par exemple l'enquête de Miltersen. ( Complexité de la sonde cellulaire: enquête )

Si vous en dites plus sur les raisons pour lesquelles vous devez définir l'isomorphisme entre les structures de données, il pourrait être possible de fournir plus d'aide. N'hésitez pas à m'envoyer un message.