Apakah Chase Favorit Saya Akan Berhenti jika Evaluasi Conjunctive Query Berhenti? Ini Tidak Mudah Diputuskan

Aturan eksistensial (juga dikenal sebagai tuple-generating dependencies, TGDs) adalah formalisme sentral untuk memperkaya basis data dengan pengetahuan domain. Sebuah basis pengetahuan terdiri dari basis data $D$ dan himpunan aturan eksistensial $\Sigma$; penalaran berarti melakukan query terhadap model universal berhingga atau tak berhingga yang diperoleh dengan menerapkan prosedur chase. Namun, penalaran dengan aturan eksistensial sembarang tidak dapat diputuskan, bahkan untuk tugas dasar seperti entailment conjunctive query (CQ). Untuk mendapatkan kembali sifat dapat diputuskan, komunitas telah mengidentifikasi banyak kelas aturan dengan sifat-sifat yang berguna. Salah satu keluarga menonjol terdiri dari himpunan aturan yang padanya algoritma chase selalu berhenti, menjamin model universal berhingga. Keluarga lainnya adalah kelas bounded treewidth set (BTS), yang memastikan chase memiliki treewidth terbatas dan dengan demikian mendukung entailment CQ yang dapat diputuskan. Masalah yang berulang adalah bahwa kelas-kelas ini sering kali *abstrak*: diberikan himpunan aturan, mungkin tidak dapat diputuskan untuk memeriksa apakah himpunan itu termasuk dalam kelas tersebut. Karena kelas aturan eksistensial yang paling banyak dipelajari dirancang untuk penalaran basis data dan menjamin entailment CQ yang dapat diputuskan, penulis mengajukan pertanyaan alami: dalam kelas yang mendukung entailment query yang dapat diputuskan, apakah kelas abstrak yang biasa menjadi konkret? Dengan kata lain, jika kita membatasi perhatian pada himpunan aturan yang entailment CQ-nya dapat diputuskan, dapatkah kita memutuskan apakah chase berhenti (untuk berbagai varian) atau apakah himpunan itu BTS? Makalah ini menjawab pertanyaan ini secara negatif.

Penulis melakukan analisis keterputusan (decidability) terhadap masalah keanggotaan untuk kelas chase-termination dan kelas BTS, dengan asumsi bahwa kelas ambien sudah menikmati entailment conjunctive query yang dapat diputuskan. Studi ini mencakup semua varian chase klasik: oblivious chase, semi-oblivious chase, restricted chase, dan core chase. Untuk setiap varian, masalah terminasi menanyakan apakah, untuk himpunan berhingga aturan eksistensial $\Sigma$ yang diberikan, chase berhenti pada setiap basis data $D$ (atau pada basis data tertentu). Masalah keanggotaan BTS menanyakan apakah himpunan aturan tersebut merupakan bounded treewidth set. Pendekatan teknis mereduksi dari masalah-masalah yang diketahui tidak dapat diputuskan, seperti halting problem untuk mesin Turing atau Post correspondence problem, dengan mengodekan komputasi ke dalam himpunan aturan yang tetap berada dalam kelas entailment CQ yang dapat diputuskan. Reduksi-reduksi dirancang dengan hati-hati sehingga himpunan aturan yang dihasilkan memenuhi kondisi kelas ambien (misalnya, guardedness atau weak acyclicity) sekaligus menyimulasikan perilaku yang tidak dapat diputuskan. Hal ini menetapkan bahwa bahkan di bawah jaminan entailment CQ yang dapat diputuskan, masalah keanggotaan tetap tidak dapat diputuskan. Makalah ini juga memperjelas hubungan antara berbagai varian chase dan kelas BTS dalam pengaturan terbatas ini.