Are there semi-decision procedures for this theory?

Question

I have the following typed theory

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

with equations for all terms:

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

I am looking for a semi-decision procedure that will be able to prove equations in this theory given a set of hypothetical equations. It is also not clear whether a complete decision procedure exists or not: There doesn't seem to be any way to encode the word problem for groups into it. Neel Krishnaswami showed how to encode the word problem into this, so the general problem is undecidable. The associativity and identity subtheory can easily be decided using a monoid model of the theory, while the full problem is harder than congruence closure. Any references or pointers would be most welcome!

---

Here is an explicit example of something we would hope to be able to automatically proved:

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)

Answer 1

It looks to me that you can encode the word problem for groups within the theory of categories in the following way. Pick an object $X$, and then for each generator of the group introduce two morphisms $x,x' : X \to X$, and assume the equalities $x \circ x' = 1_X$ and $x' \circ x = 1_X$. Then you can define the unit to be the identity map, the composition to be the group multiplication, and the negation of a string $x\circ y\circ z$ to be the reverse primed string $z' \circ y' \circ x'$. Hence this problem is undecidable.

However, the word problem is solvable for many specific groups, so if you have more details about the problem this may help. In particular, one idea from the theory of groups which might help you a lot is that absolute presentations of finitely generated groups are solvable -- the inequations can prune the search space enough to make the theory decidable.

EDIT: One additional thought I had is that adding irrelations might still be a useful tool for you, even if the concrete models you're interested validate the equations. This is because in categorical situations you often only want "nice" equations, for some value of nice, and you can use the inequations to rule out solutions that are too evil for you. Your decision procedure might still be incomplete, but you might get a more natural characterization of the solutions it can find than "we search possible proof-trees to a depth of 7".

Good luck; that functor thing you're doing looks pretty cool!

Answer 2

One reference: Automating Proofs in Category Theory by Dexter Kozen, Christoph Kreitz, and Eva Richter.