Czy dla tej teorii istnieją procedury półdecyzji?

Mam następującą teorię maszynową

|- 1_X : X -> X
f : A -> B, g : B -> C |- compose(g,f) : A -> C
F, f : A -> B |- apply(F,f) : F(A) -> F(B)

z równaniami dla wszystkich terminów:

f : A -> B, g : B -> C, h : C -> D |- compose(h,compose(f,g)) = compose(compose(h,f),g)
f : A -> B |- compose(f,1_A) = f
f : A -> B |- compose(1_B,f) = f
F |- apply(F,1_X) = 1_F(X)
f, f : A -> B, g : B -> C |- apply(F,compose(g,f)) = compose(apply(F,g),apply(F,f))

Szukam procedury półdecyzji, która będzie w stanie udowodnić równania w tej teorii, biorąc pod uwagę zestaw hipotetycznych równań. Nie jest również jasne, czy istnieje pełna procedura decyzyjna: Wydaje się, że nie ma sposobu na zakodowanie w niej problemu słownego dla grup. Neel Krishnaswami pokazał, jak zakodować w tym słowie problem, więc ogólny problem jest nierozstrzygalny. Pod-teorię asocjatywności i tożsamości można łatwo ustalić za pomocą monoidowego modelu teorii, podczas gdy pełny problem jest trudniejszy niż zamknięcie zgodności. Wszelkie referencje lub wskazówki będą mile widziane!

Oto wyraźny przykład czegoś, co chcielibyśmy automatycznie udowodnić:

f : X -> Y, F, G,
a : F(X) -> G(X), b : G(X) -> F(X),
c : F(Y) -> G(Y), d : G(Y) -> F(Y),
compose(a,b) = 1_F(X), compose(b,a) = 1_G(X),
compose(c,d) = 1_F(Y), compose(d,c) = 1_G(Y),
compose(c,apply(F,f)) = compose(apply(G,f),a)
|- compose(d,apply(G,f)) = compose(apply(F,f),b)

$X$$x,x' : X \to X$$x \circ x' = 1_X$$x' \circ x = 1_X$$x\circ y\circ z$$z' \circ y' \circ x'$

Jednak słowo problem jest rozwiązywalny dla wielu określonych grup, więc jeśli masz więcej szczegółów na temat problemu, może to pomóc. W szczególności jednym z pomysłów teorii grup, który może ci bardzo pomóc, jest to, że absolutne prezentacje skończonych grup są rozwiązywalne - nierówności mogą przycinać przestrzeń poszukiwań na tyle, aby teoria była rozstrzygalna.

EDYCJA: Jedną dodatkową myślą, którą myślałem, jest to, że dodanie irrelacji może być nadal przydatnym narzędziem, nawet jeśli konkretne modele, które są zainteresowane, potwierdzają równania. Wynika to z tego, że w sytuacjach kategorycznych często chcesz tylko „miłych” równań, dla pewnej wartości miłych, i możesz użyć nierówności, aby wykluczyć rozwiązania, które są dla ciebie zbyt złe. Twoja procedura decyzyjna może być nadal niekompletna, ale możesz uzyskać bardziej naturalną charakterystykę rozwiązań, które można znaleźć, niż „przeszukujemy możliwe drzewa próbne do głębokości 7”.

Powodzenia; ta funktor, którą robisz, wygląda całkiem fajnie!

Jeden odnośnik: Automatyzacja dowodów w teorii kategorii autorstwa Dextera Kozen'a, Christoph Kreitz i Evy Richter.