Gibt es Halbentscheidungsverfahren für diese Theorie?

Ich habe die folgende typisierte Theorie

|- 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)

mit Gleichungen für alle Begriffe:

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))

Ich suche nach einem Halbentscheidungsverfahren, mit dem Gleichungen in dieser Theorie anhand einer Reihe hypothetischer Gleichungen bewiesen werden können. Es ist auch nicht klar, ob ein vollständiges Entscheidungsverfahren existiert oder nicht: Es scheint keine Möglichkeit zu geben, das Wortproblem für Gruppen darin zu kodieren. Neel Krishnaswami hat gezeigt, wie man das Wort Problem in dieses kodiert, so dass das allgemeine Problem unentscheidbar ist. Die Assoziativitäts- und Identitätsuntertheorie kann leicht unter Verwendung eines Monoidmodells der Theorie entschieden werden, während das vollständige Problem schwieriger ist als der Kongruenzschluss. Alle Referenzen oder Hinweise wären sehr willkommen!

Hier ist ein explizites Beispiel für etwas, von dem wir hoffen, dass es automatisch bewiesen werden kann:

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'$

Das Wort Problem ist jedoch für viele bestimmte Gruppen lösbar. Wenn Sie also weitere Details zum Problem haben, kann dies hilfreich sein. Eine Idee aus der Gruppentheorie, die Ihnen sehr helfen könnte, ist insbesondere, dass absolute Darstellungen endlich erzeugter Gruppen lösbar sind - die Ungleichungen können den Suchraum so weit beschneiden, dass die Theorie entscheidbar wird.

EDIT: Ein weiterer Gedanke, den ich hatte, ist, dass das Hinzufügen von Irrelationen immer noch ein nützliches Werkzeug für Sie sein könnte, selbst wenn die konkreten Modelle, an denen Sie interessiert sind, die Gleichungen validieren. Dies liegt daran, dass Sie in kategorialen Situationen oft nur "nette" Gleichungen für einen gewissen Wert von "nett" wollen und die Ungleichungen verwenden können, um Lösungen auszuschließen, die für Sie zu böse sind. Ihr Entscheidungsverfahren ist möglicherweise noch unvollständig, aber Sie erhalten möglicherweise eine natürlichere Charakterisierung der Lösungen, die es finden kann, als "Wir suchen nach möglichen Beweisbäumen bis zu einer Tiefe von 7".

Viel Glück; Das, was du machst, sieht ziemlich cool aus!

Eine Referenz: Automatisierung von Beweisen in der Kategorietheorie von Dexter Kozen, Christoph Kreitz und Eva Richter.