Latar belakang :
Saya datang ke akhir gelar master saya di Matematika dan akan memulai PhD di bidang Logika pada bulan Agustus. Semakin banyak saya belajar logika, semakin banyak ilmu komputer teoritis saya terkena, misalnya teori rekursi, kalkulus lambda, tetapi CS yang mendasarinya disikat di bawah karpet. Bidang minat utama saya - teori himpunan dan teori kategori - juga memiliki aplikasi dalam ilmu komputer, tetapi sejauh ini saya hanya mempelajarinya dari sudut pandang matematika murni.
Masalah:
Kurangnya latar belakang ilmu komputer saya terkadang membuat saya sulit melihat motivasi atau intuisi di balik apa yang sedang terjadi, atau bagaimana hal itu bisa diterapkan. Saya bertahan, tetapi saya merasa akan lebih sehat untuk bercabang sedikit ... terpikir oleh saya bahwa, untuk kepentingan penelitian masa depan saya, saya harus belajar ilmu komputer.
Sebagian besar buku CS yang saya lihat belum cocok untuk tujuan saya, entah terlalu mendasar dan tidak teknis, atau mengandaikan jenis latar belakang CS yang tidak saya miliki. Mereka tampaknya ditujukan pada orang-orang yang cukup paham komputer tetapi yang memiliki sedikit di latar belakang matematika - situasi saya adalah sebaliknya.
Pertanyaan:
Apa buku atau sumber daya lain yang ada yang dapat membantu ahli matematika yang berubah menjadi ahli logika dalam tujuan mereka untuk mendapatkan pengetahuan kerja tentang ilmu komputer (teoretis)?
Saya mencari sesuatu yang lebih sehat daripada beberapa seminar seminar dan lebih mendalam daripada The New Turing Omnibus , tetapi saya tidak punya waktu atau sumber daya untuk melakukan gelar sarjana lainnya. (Mungkin aku meminta sesuatu yang tidak ada.)
Maaf jika pertanyaannya terlalu kabur atau tidak benar. Saya merasa lebih cocok di sini daripada di MSE tetapi saya akan senang untuk memigrasikannya jika perlu.
sumber
Jawaban:
Anda pada dasarnya meminta sumber daya yang akan memungkinkan Anda mengubah pengetahuan Anda tentang logika, teori rekursi, dan teori kategori menjadi pengetahuan tentang ilmu komputer teoretis. Saya akan menyarankan untuk melihat teori realisasi, terutama melalui hubungannya dengan teori topos dan teori bukti kategoris. .
Berikut ini beberapa saran; saran saya adalah memilih satu dan masuk ke kedalaman. Dengan pengecualian buku Taylor (yang menjelaskan hal ini), saran saya menganggap Anda telah cukup terpapar pada kalkulus lambda dan teori kategori untuk melihat interpretasi kategoris dari kalkulus lambda yang diketik sederhana.
Buku Paul Taylor, Yayasan Praktis Matematika
IMO, ini mungkin pengantar teknis tunggal terbaik untuk hubungan antara logika, teori kategori dan komputasi. Ini mengasumsikan hampir tidak ada prasyarat, tetapi masuk ke perairan yang cukup dalam dengan sangat cepat, dan pasti akan membebani (dan sangat meningkatkan) kematangan matematis Anda.
Catatan Wesley Phoa Pengantar Fibrations, Teori Topos, Topos Efektif, dan Set Sederhana
Ini adalah beberapa catatan kuliah yang ditulis oleh Wesley Phoa. Jika Anda benar-benar fasih, maka catatan ini menawarkan jalan yang sangat cepat untuk memahami beberapa konstruksi paling penting dalam teori realisasi dan topos (yaitu, pembangunan topos yang efektif).
Buku Bart Jacobs Categorical Logic and Type Theory
Ini adalah salah satu referensi definitif pada semantik kategoris teori tipe. Ini juga sangat besar.
Pada saat yang sama Anda membaca salah satu buku ini, saya akan menyarankan mengunduh dan belajar bagaimana menggunakan bahasa pemrograman Agda . Bahasa ini mengimplementasikan teori tipe canggih yang dijelaskan di atas, dan IMO akan sangat membantu untuk melihat bagaimana konstruksi semantik yang sangat halus menghasilkan teori tipe.
Andrej Bauer mungkin bisa memberi Anda nasihat yang lebih baik. Mungkin dia bisa dibujuk untuk memposting. :)
sumber
Dua buku yang muncul di pikiran adalah
Pengantar Teori Komputasi oleh Sipser
dan
Pengantar Algoritma oleh Cormen et al.
Saya setuju dengan usul yang mengatakan bahwa ilmu komputer teoretis adalah bidang yang luas dan kami dapat memberikan referensi yang lebih baik jika Anda lebih spesifik tentang apa yang ingin Anda pelajari.
sumber