Membuktikan Persamaan Matematika Menggunakan Diagram

Struktur data e-graph atau equality graph semakin menarik perhatian dalam ranah ilmu komputer teoritis dan penalaran persamaan. Struktur yang pertama kali diperkenalkan oleh Nelson dan Oppen pada 1980 ini kembali populer setelah Willsey dan timnya mengembangkan pustaka perangkat lunak egg, yang menggabungkan e-graph dengan teknik equality saturation untuk melakukan penalaran persamaan secara cepat dan adaptif.

Semantik Kategori dan Perkembangan E-Graph

Perkembangan struktur data ini berlanjut melalui perangkat penerusnya, egglog, yang dimanfaatkan dalam proyek CatColab untuk menalar kategori bersaji terhingga. Baru-baru ini, dua kelompok peneliti—Biondo, Castelnovo, dan Gadducci serta Tiurin dan rekan-rekan—mengajukan semantik kategori untuk e-graph dengan mendefinisikan e-hypergraph sebagai hipergraf berlabel yang dilengkapi struktur kesetaraan.

Dalam memodelkan pemrosesan e-graph secara kategoris dan operasional, pembuktian persamaan dapat diawali dengan mengamati bagaimana diagram dimanipulasi. Konsep kunci yang menjadi landasan manipulasi ini adalah funktor inisial. Pada tahap awal, pembahasan difokuskan pada kategori polos tanpa struktur tambahan, yang setara dengan penggunaan simbol fungsi unary.

Definisi Diagram dan Funktor Inisial

Dalam teori kategori, persamaan antar-morfisme umumnya digambarkan menggunakan diagram komutatif. Sebuah diagram dalam suatu kategori didefinisikan sebagai funktor dari kategori indeks bentuk diagram tersebut. Diagram dikatakan bebas jika bentuknya dihasilkan oleh sebuah graf, bersaji terhingga jika kategorinya bersaji terhingga, serta komutatif jika setiap pasangan morfisme dengan domain dan kodomain yang sama menghasilkan pemetaan yang identik pada kategori target.

Untuk mengubah suatu diagram menjadi diagram lain tanpa mengubah himpunan solusi persamaan, diperlukan funktor khusus yang disebut funktor inisial. Sebuah funktor dikatakan inisial apabila penarikan kembali (pullback) sepanjang funktor tersebut mempertahankan limit diagram, atau secara kualitatif membuat kategori koma (comma category) selalu terhubung dan tidak kosong untuk setiap objek.

Manfaat utama dari funktor inisial adalah kemampuannya mempertahankan himpunan solusi dari sistem persamaan yang diwakili oleh diagram. Terdapat beberapa pola transformasi dasar menggunakan funktor inisial, antara lain introduksi operasi, reduksi kongruensi, dan introduksi persamaan.

Penerapan dalam Pembuktian Persamaan

Penerapan funktor inisial dapat dilihat pada pembuktian hukum penempelan persegi komutatif (pasting law for commutative squares). Ketika dua persegi komutatif berdampingan pada satu sisi, keduanya dapat digabungkan membentuk satu persegi panjang komutatif melalui serangkaian langkah mekanis yang memanfaatkan penarikan kembali dan reduksi kongruensi.

Contoh lainnya terjadi pada pembuktian penyajian monoid dengan elemen f yang memenuhi persamaan f^3 = id = f^5. Melalui penerapan reduksi kongruensi secara berulang (congruence closure), diagram awal dapat disederhanakan hingga menghasilkan persamaan akhir f = id. Hal ini membuktikan bahwa monoid yang disajikan tersebut sebenarnya merupakan monoid trivial, sejalan dengan contoh klasik yang pernah dipaparkan oleh Nelson dan Oppen.

Pengembangan teori ini akan dilanjutkan pada pembahasan berikutnya dengan memperluas formalisme ke kategori yang memiliki produk terhingga (finite products) untuk menghubungkannya secara lebih erat dengan struktur e-graph.