Teoretyczne traktowanie różnic, łat i łączenia?

Czy istnieje kategoria łatek, która wygląda mniej więcej tak:

• Obiekty są ciągami znaków w pewnym alfabecie podstawowym
• Morfizmy to skrypty edycyjne („diffs” lub „łatki”) między ciągami

Interesują mnie następujące pytania:

• Czy istnieje kategoryczne pojęcie minimalnego skryptu edycji? Może kategoria łatek jest wzbogacona w zestawy PO?
• Czy łączenie łat jest kategorycznym wypychaniem?
• Jak uogólnić to na ciągi znaków na drzewa (system plików lub algebraiczny typ danych)?

Jak zauważył Martin , jest trochę pracy nad kategorycznym przedstawieniem łat. „A Categorical Theory of Patches” Mimrama i Di Giusto jest najbardziej rozbudowanym kategorycznym podejściem do skryptów edycyjnych używanych przez UNIX diff.

W ich znaczeniu masz to, czego chcesz. Obiekty są skończonymi sekwencjami słów nad alfabetem $L$ , postrzeganym jako odwzorowanie $A : [n] \rightarrow L$ , gdzie $[n]$ oznacza zbiór z $n$ elementami. Strzałka między $A : [n] \rightarrow L$ i $B : [m] \rightarrow L$ to częściowe mapowanie iniekcyjne częściowo : $f : [n] \rightarrow [m]$. Zastrzyki i wzrost mają na celu wskazanie, że kopie nigdy się nie krzyżują . Możesz znaleźć wszystkie szczegóły na papierze .

Tak, łączenie jest postrzegane jako wypychanie w zakresie bezpłatnego ukończenia powyższej kategorii. Potrzebujemy uzupełnienia, aby mieć pewność, że dodamy konflikty scalania do naszej konstrukcji. Nie zawsze jest tak, że scalenie istnieje.

W drugim pytaniu nie ma kategorycznego pojęcia minimalnego skryptu edycji z dwóch głównych powodów.

1. Skrypty edycji występują we wszystkich kształtach i formach. Niektórzy autorzy rozważają wstawianie, usuwanie i kopiowanie, niektórzy autorzy lubią także dodawać podstawienia jako operację. Kiedy uogólnisz od strun do drzew, wtedy wykonalne stanie się mnóstwo innych operacji.

2. $ab$$ba$

Dużo pracy nad uogólnieniem skryptów edycyjnych na drzewach. Zostało to podzielone na dwa główne obszary prac:

• Untyped Trees : Pomyśl tylko o wyrażeniach s. Odległość edycji drzewa między dwoma drzewami jest odległością edycji łańcucha między przejściem przed drzewem tych drzew. Możesz sprawdzić bibliografię Demaine i in. lub Pawlik i Augsten , na przykład.

• Typowane drzewa : łatki nad abstrakcyjnymi składniami Drzewa, które gwarantują zachowanie poprawnego typowania obiektu, tj. Zastosowanie poprawki zawsze da prawidłową wartość AST. Pod wpisanym parasolem można rozważyć mniej operacji edycji. Na przykład podstawienie nie ma sensu. Niemniej jednak istnieje rozbieżność w stosunku do przedwczesnego przechodzenia drzew przez Lempsink i in. , który został później rozszerzony przez Vassenę . Obecnie koncentruję się na podejściach, które dystansują się od skryptów edycji w odniesieniu do problemów, które wcześniej wskazałem, takich jak nasza najnowsza praca lub niektóre wcześniejsze prace, które próbują wykorzystać strukturę typu „łatanych” wartości.

W żadnym z tych przypadków nie widziałem dokładnej kategorycznej interpretacji łat o strukturze drzewa.

W tym kierunku jest sporo pracy. Możesz zacząć od spojrzenia na [1, 2], ale nie wyczerpują one tematu.

1. S. Mimram, C. Di Giusto, Kategoryczna teoria łat .

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