Apakah ada prosedur semi-keputusan untuk teori ini?

Saya memiliki teori yang diketik berikut

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

dengan persamaan untuk semua istilah:

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

Saya mencari prosedur semi-keputusan yang akan dapat membuktikan persamaan dalam teori ini diberikan seperangkat persamaan hipotetis. Juga tidak jelas apakah prosedur pengambilan keputusan lengkap ada atau tidak: Tampaknya tidak ada cara untuk menyandikan kata masalah bagi kelompok ke dalamnya. Neel Krishnaswami menunjukkan bagaimana menyandikan kata masalah ke dalam masalah ini, sehingga masalah umum tidak dapat diputuskan. Subtory associativitas dan identitas dapat dengan mudah diputuskan dengan menggunakan model teori monoid, sementara masalah penuh lebih sulit daripada penutupan kongruensi. Referensi atau petunjuk apa pun akan sangat diterima!

Berikut adalah contoh eksplisit dari sesuatu yang kami harapkan dapat dibuktikan secara otomatis:

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

Namun, kata problem dapat dipecahkan untuk banyak grup tertentu, jadi jika Anda memiliki detail lebih lanjut tentang masalah ini dapat membantu. Secara khusus, satu ide dari teori grup yang mungkin banyak membantu Anda adalah bahwa presentasi absolut dari grup yang dihasilkan dapat dipecahkan - ketidaksetaraan dapat memangkas ruang pencarian yang cukup untuk membuat teori dapat diputuskan.

EDIT: Satu pemikiran tambahan yang saya miliki adalah bahwa menambahkan irrelasi mungkin masih menjadi alat yang berguna untuk Anda, bahkan jika model konkret yang Anda minati memvalidasi persamaan. Ini karena dalam situasi kategoris Anda sering hanya menginginkan persamaan "baik", untuk beberapa nilai bagus, dan Anda dapat menggunakan persamaan untuk mengesampingkan solusi yang terlalu jahat bagi Anda. Prosedur keputusan Anda mungkin masih belum lengkap, tetapi Anda mungkin mendapatkan karakterisasi yang lebih alami dari solusi yang dapat ditemukan daripada "kami mencari kemungkinan pohon bukti hingga kedalaman 7".

Semoga berhasil; hal functor yang Anda lakukan terlihat sangat keren!

Satu referensi: Mengotomasi Bukti dalam Kategori Teori oleh Dexter Kozen, Christoph Kreitz, dan Eva Richter.