Saya telah belajar beberapa bit dari teori kategori. Tentunya cara pandang yang berbeda. (Ringkasan yang sangat kasar bagi mereka yang belum melihatnya: teori kategori memberikan cara untuk mengekspresikan semua jenis perilaku matematika hanya dalam hal hubungan fungsional antara objek. Misalnya, hal-hal seperti produk Cartesian dari dua set didefinisikan sepenuhnya dalam hal bagaimana fungsi-fungsi lain berperilaku dengannya, bukan dalam hal elemen apa yang menjadi anggota set.)
Saya memiliki pemahaman yang samar-samar bahwa teori kategori berguna pada bahasa pemrograman / logika ("Teori B"), dan saya bertanya-tanya berapa banyak algoritma dan kompleksitas ("Teori A") yang dapat memperoleh manfaat. Mungkin bisa membantu saya turun, jika saya tahu beberapa aplikasi yang kuat dari teori kategori dalam Teori B. (Saya sudah secara implisit mengasumsikan tidak ada aplikasi dalam Teori A yang ditemukan sejauh ini, tetapi jika Anda memiliki beberapa di antaranya, itu bahkan lebih baik untuk saya!)
Dengan "aplikasi solid", maksud saya:
(1) Aplikasi sangat bergantung pada teori kategori sehingga sangat sulit untuk dicapai tanpa menggunakan mesin.
(2) Aplikasi ini memanggil setidaknya satu teorema kategori non-sepele (misalnya lemma Yoneda).
Bisa jadi itu (1) menyiratkan (2), tapi saya ingin memastikan ini adalah aplikasi "nyata".
Walaupun saya memiliki latar belakang "Teori B", itu sudah lama, jadi de-jargonisasi akan sangat dihargai.
(Tergantung pada jawaban apa yang saya dapatkan, saya mungkin mengubah pertanyaan ini menjadi wiki komunitas nanti. Tapi saya benar-benar menginginkan aplikasi yang bagus dengan penjelasan yang bagus, jadi sepertinya memalukan untuk tidak memberi hadiah kepada penjawab dengan sesuatu.)
sumber
Komputasi Quantum
Satu bidang yang sangat menarik adalah penerapan berbagai kategori monoid untuk perhitungan kuantum. Beberapa bisa berpendapat bahwa ini juga fisika, tetapi pekerjaannya dilakukan oleh orang-orang di departemen ilmu komputer. Sebuah makalah awal di bidang ini adalah semantik kategoris protokol kuantum oleh Samson Abramsky dan Bob Coecke; banyak makalah baru-baru ini oleh Abramsky dan Coecke dan lainnya terus bekerja ke arah ini.
Dalam tubuh kerja protokol kuantum ini dixiomatiskan sebagai (jenis tertentu) kategori tertutup rapat. Kategori tersebut memiliki bahasa grafis yang indah dalam hal diagram string (dan pita). Persamaan dalam kategori sesuai dengan gerakan tertentu dari string, seperti meluruskan string yang kusut tetapi tidak diikat, yang pada gilirannya sesuai dengan sesuatu yang bermakna dalam mekanika kuantum, seperti teleportasi kuantum.
Pendekatan kategoris menawarkan pandangan logis tingkat tinggi tentang apa yang biasanya melibatkan perhitungan tingkat sangat rendah.
Teori Sistem
Coalgebra telah digunakan sebagai kerangka kerja umum untuk memodelkan sistem (aliran, automata, sistem transisi, sistem probabilistik). Teorinya berakar pada teori kategori, yang didasarkan pada gagasan coalgebra , di mana adalah functor yang menggambarkan struktur sistem transisi. Dengan demikian, jenis sistem berubah dengan functor yang mendasarinya, tetapi banyak teori, seperti gagasan bisimulasi, dapat diterapkan untuk semua functors. Teori kategori juga memungkinkan konstruksi modular dari modal logika untuk alasan tentang sistem yang digambarkan sebagai coalgebras.F F
Transformasi Grafik
Transformasi grafik dapat diekspresikan dengan cukup baik dalam bahasa teori kategori. Ini telah menemukan aplikasi, misalnya, dalam transformasi model (seperti dalam model UML) dan formalisme pemodelan visual lainnya. Pendekatan berlangsung dalam kategori grafik dan grafik homomorfisme. Pertama, pushout dapat dilihat sebagai konstruksi perekatan: Diberikan dua grafik . Grafik dan dua morfisme dan menunjukkan bagian-bagian yang memiliki dua grafik. Pushout menyatukan bagian-bagian ini, menambahkan bagian dan , pada dasarnya, menempelkan dan bersama-sama di sepanjangG1, G2 P e1: P→ G1 e2: P→ G2 G1 G2 G1 G2 P .
Sebuah pushout ganda digunakan untuk menggambarkan transformasi grafik. Aturan diwakili oleh tuple , di mana menunjukkan prasyarat aturan, menunjukkan kondisi pasak aturan, dan menunjukkan bagian grafik untuk menerapkan aturan. Ada peta dari dan , salah satunya akan digunakan untuk mencocokkan bagian dari grafik asli, yang lain untuk membuat grafik yang dihasilkan. menjelaskan bagian grafik yang akan dihapus. menjelaskan bagian yang akan dibuat. Peta dari ke dalam konteks( L , K, R ) L. R K l : K→ L r : K→ R L ∖ K R ∖ K d K grafik perlu disediakan, dan pushout dari dan peta perlu sama dengan grafik yang menarik . Pushout dari dan
kemudian memberikan hasil melakukan transformasi.D d l G d k
Bahasa Pemrograman (via MathOverflow)
Ada banyak aplikasi teori kategori dalam desain bahasa pemrograman dan teori bahasa pemrograman. Jawaban luas dapat ditemukan di MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory ) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory .
Bigraphs - Kalki Proses
Akhirnya, ada bigraph Milner , kerangka umum untuk menggambarkan dan bernalar tentang sistem agen yang berinteraksi. Ini dapat dilihat sebagai kerangka kerja umum untuk penalaran tentang proses aljabar dan teori struktural dan perilaku mereka. Pendekatan ini juga didasarkan pada pushout.
sumber
Pemahaman saya adalah bahwa teori spesies Joyal digunakan secara relatif luas dalam kombinatorik enumeratif, sebagai generalisasi fungsi-fungsi pembangkit yang juga memberi tahu Anda cara mengubah hal-hal di samping jumlah yang ada.
Pippenger telah menerapkan Batu dualitas untuk menghubungkan bahasa dan varietas semi-grup reguler. Jeandel telah memperkenalkan automata topologi menerapkan ide-ide ini untuk memberikan akun terpadu (dan bukti!) Untuk kuantum, probabilistik, dan automata biasa.
Roland Backhouse telah memberikan karakterisasi abstrak dari algoritma serakah melalui koneksi Galois dengan semiring tropis.
Dalam nada yang jauh lebih spekulatif, Noam menyebutkan model-model berkas. Ini secara abstrak mencirikan teknik sintaksis hubungan logis, yang mungkin merupakan salah satu teknik paling kuat dalam semantik. Kami sebagian besar menggunakannya untuk membuktikan hasil yang tidak dapat diekspresikan dan konsistensi, tetapi itu harus menarik untuk teori kompleksitas karena ini adalah contoh yang bagus dari teknik bukti non-alami (dalam arti Razborov / Rudich) yang praktis. (Namun, hubungan logis biasanya dirancang dengan sangat hati-hati untuk menjamin bahwa mereka relativisasi - sebagai perancang bahasa, kami ingin dapat meyakinkan pemrogram bahwa panggilan fungsi adalah kotak hitam!)
EDIT: Saya akan terus berspekulasi, atas permintaan Ryan. Seperti yang saya pahami, bukti alami kira-kira satu di sepanjang garis mencoba mendefinisikan invarian induktif dari struktur sirkuit, tunduk pada berbagai kondisi yang masuk akal. Gagasan serupa (tidak mengejutkan) cukup umum dalam bahasa pemrograman juga, ketika Anda mencoba mendefinisikan invarian yang dikelola secara induktif oleh istilah lambda-calculus (misalnya, untuk membuktikan keamanan jenis). 1
Namun, teknik ini sering rusak pada tipe yang lebih tinggi (yaitu, fungsi). Sebagai contoh, kalkulus lambda yang diketik sederhana adalah total - setiap program yang tertulis di dalamnya berakhir. Namun, upaya langsung untuk membuktikan kecenderungan ini cenderung pada masalah fungsi kelas satu: itu tidak cukup untuk membuktikan bahwa setiap istilah tipe berakhir. Karena kita juga dapat menerapkan argumen pada fungsi, kita tidak hanya perlu memastikan bahwa setiap istilah tipe berhenti, kita juga perlu memastikan bahwa properti ini memiliki "secara turun-temurun" - kita juga perlu tahu bahwa dengan jangka waktu berapa pun tipe , aplikasi juga akan berhenti.A → B AA→B A→B A
Inilah yang dilakukan hubungan logis. Alih-alih mendefinisikan satu invarian induktif tunggal, kami mendefinisikan seluruh keluarga predikat dengan rekursi atas struktur (biasanya) tipe. Kemudian, kami membuktikan bahwa setiap istilah yang dapat ditentukan terletak pada predikat yang sesuai, yang memungkinkan kami menetapkan apa yang kami cari. Jadi untuk terminasi, kita akan mengatakan bahwa nilai-nilai yang baik dari tipe dasar adalah nilai-nilai dari tipe dasar, dan nilai-nilai yang baik dari tipe adalah nilai-nilai dari tipe ini yang, jika diberi nilai , dievaluasi menjadi nilai yang baik. dariA BA→B A B . Perhatikan bahwa tidak ada satu pun invarian induktif - kami mendefinisikan seluruh keluarga invarian dengan rekursi pada struktur input, dan menggunakan cara lain untuk menunjukkan bahwa semua istilah ada di dalam invarian ini. Bukti-teoritis, ini adalah teknik yang jauh lebih kuat, dan itulah sebabnya itu memungkinkan Anda membuktikan hasil konsistensi.
Koneksi ke berkas berkas muncul dari fakta bahwa kita sering perlu alasan tentang istilah terbuka (yaitu, istilah dengan variabel bebas), dan karenanya perlu membedakan antara macet karena kesalahan dan macet karena perlu mengurangi variabel. Berkas gandum muncul dari mempertimbangkan pengurangan kalkulus lambda sebagai mendefinisikan morfisme kategori yang istilahnya adalah objek (yaitu, urutan parsial yang diinduksi oleh reduksi), dan kemudian mempertimbangkan functors dari kategori ini ke dalam set (yaitu, predikat). Jean Gallier menulis beberapa makalah yang bagus tentang ini pada awal 2000-an, tetapi saya ragu mereka dapat dibaca kecuali Anda sudah mengasimilasi kalkulus lambda dalam jumlah yang wajar.
sumber
Ada banyak contoh, yang pertama terlintas dalam pikiran adalah penggunaan teori kategori oleh Alex Simpson untuk membuktikan sifat-sifat bahasa pemrograman, lihat misalnya " Kecukupan Komputasi untuk Jenis Rekursif dalam Model Teori Set Intuitionistic ", Sejarah Logika Murni dan Terapan , 130: 207-275, 2004. Walaupun judulnya menyebutkan teori himpunan, tekniknya adalah kategori-teoretik. Lihat beranda Alex untuk lebih banyak contoh.
sumber
Saya pikir Anda mengajukan dua pertanyaan tentang penerapan, tipe A dan tipe B secara terpisah.
Seperti yang Anda perhatikan, ada banyak aplikasi substantif dari teori kategori untuk topik tipe B: semantik bahasa pemrograman (monad, kategori tertutup kartesius), logika dan kemampuan (topoi, varietas logika linier).
Namun, tampaknya ada sedikit aplikasi substantif untuk teori A (algoritma atau kompleksitas).
Ada beberapa kegunaan dalam objek dasar, seperti menggambarkan kategori automata atau objek kombinatorial (grafik, sekuens, permutasi, dll). Tetapi ini sepertinya tidak menjelaskan pemahaman yang lebih dalam tentang teori atau algoritma bahasa.
Secara spekulatif, ini bisa menjadi ketidakcocokan antara strategi saat ini dari teori kategori dan teori A:
Strategi utama teori kategori berhadapan dengan kesetaraan (ketika semuanya sama dan ketika mereka berbeda dan bagaimana mereka saling memetakan).
Untuk teori kompleksitas, strategi utama adalah reduksi dan menetapkan batas (orang akan berpikir pengurangan adalah seperti panah, tapi saya tidak berpikir apa pun di luar kesamaan dangkal ini telah dipelajari).
Untuk algoritma, tidak ada strategi menyeluruh untuk itu selain pemikiran kombinatorial cerdas ad hoc. Untuk domain tertentu, saya berharap bisa ada eksplorasi yang bermanfaat (algoritma untuk aljabar?) Tapi saya belum melihatnya.
sumber
Aplikasi "TCS-A" yang muncul di benak saya adalah spesies kombinatorial Joyal (generalisasi seri daya ke functors sehingga dapat menggambarkan objek kombinatorial seperti pohon, set, multiset, dll.) Dan formalisasi kriptografi "permainan-hopping" menggunakan relasional, logika Hoare probabilistik (Easycrypt, Certicrypt, karya Andreas Lochbihler). Sementara kategori tidak secara langsung muncul dalam yang terakhir mereka berperan dalam pengembangan logika yang mendasarinya (misalnya monad).
PS: Karena nama saya disebutkan dalam jawaban pertama: penggunaan fibrations dari groupoids untuk menunjukkan nonderivability dari aksioma tertentu dalam teori tipe Martin-Löf oleh Thomas Streicher dan saya sendiri juga dapat dianggap sebagai penggunaan teori kategori yang “solid” (walaupun dalam logika atau "TCS-B").
sumber
Buku yang lebih baru Seven Sketches in Compositionality mencantumkan beberapa aplikasi teori kategori dalam sains dan teknik komputer. Bab penting tentang basis data di mana penulis menggambarkan kueri, penggabungan, migrasi, dan pengembangan basis data berdasarkan model kategorikal. Penulis mengambil ini lebih jauh dan mengembangkan Categorical Query Language (CQL) dan lingkungan pengembangan terintegrasi (IDE) berdasarkan pada model kategorikal dari basis data.
sumber