Tengo la siguiente teoría escrita
|- 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)
con ecuaciones para todos los términos:
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))
Estoy buscando un procedimiento de semi-decisión que pueda probar ecuaciones en esta teoría dado un conjunto de ecuaciones hipotéticas. Tampoco está claro si existe un procedimiento de decisión completo o no: no parece haber ninguna forma de codificar el problema verbal para los grupos en él. Neel Krishnaswami mostró cómo codificar el problema verbal en esto, por lo que el problema general es indecidible. La subteoría de la asociatividad y la identidad se puede decidir fácilmente utilizando un modelo monoide de la teoría, mientras que el problema completo es más difícil que el cierre de la congruencia. ¡Cualquier referencia o puntero sería bienvenido!
Aquí hay un ejemplo explícito de algo que esperamos poder probar automáticamente:
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)
Una referencia: Pruebas de automatización en teoría de categorías de Dexter Kozen, Christoph Kreitz y Eva Richter.
fuente