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)