Traitement théorique par catégorie des différences, des correctifs et des fusions?

Existe-t-il une catégorie de correctifs qui ressemble à peu près à ceci:

• Les objets sont des chaînes dans un alphabet de base
• Les morphismes sont des scripts d'édition ("diffs" ou "patches") entre les chaînes

Je m'intéresse à ces questions:

• Existe-t-il une notion catégorique de script d'édition minimal ? Peut-être que la catégorie des patchs est enrichie en PO-Sets?
• La fusion des correctifs est-elle un rejet catégorique?
• Comment généraliser cela des chaînes aux arbres (un système de fichiers ou un type de données algébrique)?

Comme l'a souligné Martin , il y a du travail sur la représentation catégorique des correctifs. "Une théorie catégorique des correctifs" de Mimram et Di Giusto étant l'approche catégorique la plus étendue pour les scripts d'édition tels qu'utilisés par le UNIX diff.

Dans leur sens, vous avez ce que vous voulez. Les objets sont des séquences finies de mots sur un alphabet $L$ , vu comme un mappage $A : [n] \rightarrow L$ , où $[n]$ désigne l'ensemble avec $n$ éléments. Une flèche entre $A : [n] \rightarrow L$ et $B : [m] \rightarrow L$ est une cartographie croissante partielle injective $f : [n] \rightarrow [m]$. L'injectivité et l'augmentation sont là pour indiquer que les copies ne se croisent jamais . Vous pouvez trouver tous les détails sur le papier .

Oui, la fusion est perçue comme la poussée sur la cocomplétion gratuite de la catégorie ci-dessus. Nous avons besoin de la complétion pour nous assurer d'ajouter des conflits de fusion à notre construction. Ce n'est pas le cas qu'une fusion existe toujours.

Sur votre deuxième question, il n'y a pas de notion catégorique de script d'édition minimal pour deux raisons principales.

1. Les scripts d'édition sont de toutes formes et de toutes formes. Certains auteurs considèrent les insertions, les suppressions et les copies, certains auteurs aiment aussi ajouter des substitutions comme opération. Lorsque vous généralisez des chaînes aux arbres, alors, une pléthore d'autres opérations deviennent réalisables.

2. $ab$$ba$

Il y a eu beaucoup de travail sur la généralisation des scripts d'édition aux arbres. Cela a été divisé en deux corps de travail principaux:

• Arbres non typés : pensez aux expressions s uniquement. La distance de modification d'arbre entre deux arbres est la distance de modification de chaîne entre la traversée en précommande desdits arbres. Vous pouvez consulter une bibliographie de Demaine et al. ou Pawlik et Augsten , par exemple.

• Arbres typés : correctifs sur les arbres de syntaxe abstraite garantissant la bonne typographie de l'objet, c'est-à-dire que l'application d'un correctif produira toujours un AST valide. Sous le parapluie tapé, il y a moins d'opérations d'édition que l'on peut considérer. La substitution, par exemple, n'a pas de sens. Néanmoins, il existe un diff sur la traversée en pré-commande des arbres par Lempsink et al. , qui a ensuite été étendu par Vassena . Je me concentre actuellement sur des approches qui se distancient des scripts d'édition pour les problèmes que j'ai signalés plus tôt, tels que nos derniers travaux ou certains travaux antérieurs qui tentent de tirer parti de la structure du type de valeurs "corrigées".

Dans aucun de ces cas, je n'ai vu d'interprétation catégorique précise des correctifs arborescents.

Il y a pas mal de travail dans cette direction. Vous pouvez commencer par regarder [1, 2], mais ils n'épuisent pas le sujet.

1. S. Mimram, C. Di Giusto, Une théorie catégorique des correctifs .

2. C. Angiuli, E. Morehouse, DR Licata, R. Harper, Homotopical Patch Theory .