Jalan menuju metode formal

Sudah lazim untuk melihat siswa memulai PhD mereka dengan hanya latar belakang yang terbatas dalam matematika dan aspek formal ilmu komputer. Jelas akan sangat sulit bagi siswa tersebut untuk menjadi ilmuwan komputer teoretis, tetapi akan lebih baik jika mereka dapat menjadi paham dengan menggunakan metode formal dan membaca makalah yang berisi metode formal.

Apa jalur jangka pendek yang baik yang dapat diikuti oleh mahasiswa PhD untuk mendapatkan paparan yang diperlukan agar mereka membaca makalah yang melibatkan metode formal dan akhirnya menulis makalah yang menggunakan metode formal seperti itu?

Dalam hal konteks, saya lebih memikirkan Teori B dan verifikasi formal sebagai hal-hal yang harus mereka pelajari, tetapi juga topik TCS klasik seperti teori automata.

Dalam kata pengantar bukunya “Penemuan Matematika, Tentang Pemahaman, Pembelajaran, dan Pemecahan Masalah Pengajaran” George Pólya menulis:

Memecahkan masalah adalah seni praktis, seperti berenang, atau bermain ski, atau bermain piano: Anda dapat mempelajarinya hanya dengan meniru dan berlatih. Buku ini tidak dapat menawarkan Anda sebuah kunci ajaib yang membuka semua pintu dan menyelesaikan semua masalah, tetapi buku ini menawarkan contoh-contoh bagus untuk meniru dan banyak kesempatan untuk berlatih: jika Anda ingin belajar berenang, Anda harus pergi ke air, dan jika Anda ingin menjadi pemecah masalah Anda harus menyelesaikan masalah.

Saya pikir tidak ada jalan pendek, terutama untuk mencapai keadaan menulis makalah. Itu membutuhkan latihan, banyak.

Beberapa petunjuk:

Jika "latar belakang terbatas dalam matematika dan aspek formal" berarti "tidak pernah menyusun bukti dan menuliskannya" maka sesuatu seperti ini mungkin merupakan awal.

Jika sesuatu pada Cheat Sheet Ilmu Komputer Teoritis membuat siswa merasa tidak nyaman, maka kursus penyegaran dari cabang matematika yang sesuai akan disarankan.

Ada banyak sumber untuk penulisan matematis: Catatan kuliah mata kuliah 1978 Stanford University CS209 mungkin. Atau artikel ini oleh Paul Halmos.

Metode formal seperti Z, B, TLA, CafeObj sangat bergantung pada teori himpunan, logika, teori kategori, kalkulus lambda, dan automata untuk pemodelan konsep tipe, data, dan perhitungan.

Anda dapat melompat ke monograf yang komprehensif seperti Logika Bahasa Spesifikasi, oleh Dines Bjørner dan Martin C. Henson eds., Monografi dalam Ilmu Komputer Teoretis, Springer Verlag, 2008 dan belajar sesuai kebutuhan Anda, dan menggunakan referensi yang dikutip di sana. Atau pelajari satu topik sekaligus:

1. Tetapkan teori
2. Logika matematika
3. Logika temporal
4. Aljabar universal
5. Kalkulus Lambda
6. Teori kategori

Saya benar-benar berpikir metode "formal" bukan ide yang sangat bagus untuk tujuan pendidikan. Untuk itu, pemrograman komputer adalah metode "formal". Apakah ini berhasil sebagai alat pendidikan?

Yang dibutuhkan adalah pemahaman, intuisi, dan kemampuan untuk menghadapi abstraksi. Metode formal menghalangi semua itu. Sebaliknya, mereka mempromosikan trial and error, peretasan, pencocokan pola, imitasi, fokus pada sintaksis. Daftar ini terus berlanjut.

Setiap bagian dari matematika yang ketat akan mengajarkan orang bagaimana bernalar dengan benar. Semakin sederhana domain, semakin baik itu. Semua yang saya pelajari tentang penalaran saya pelajari di sekolah menengah ketika saya mengerjakan Euclidean Geometry dengan serius. Kalkulus dan aljabar linier di Universitas mengerjakan sisanya.

Alternatif lain yang menarik adalah logika filosofis, di mana mereka mengajarkan orang bagaimana berpikir tentang pernyataan dan memahami apa isi informasi dan apa konsekuensi dari apa. Mereka melakukan itu tanpa menenggelamkan siswa dalam simbol.

Jika Anda mencatat semua Ilmuwan Komputer papan atas, Anda akan kagum betapa banyak dari mereka memiliki pelatihan formal dalam bidang filsafat. Kami kehilangan semua itu sekarang karena mahasiswa filsafat sekarang menganggap Ilmu Komputer sebagai subjek yang biasa. Membuat siswa kami untuk belajar beberapa filosofi dapat melawan itu sampai batas tertentu. Dapatkan mereka untuk bekerja melalui Sejarah Filsafat Barat Bertrand Russell . Itu akan melakukan keajaiban.

Jika mereka bekerja dalam teori bahasa pemrograman, Anda juga dapat meminta mereka membaca Quine, yang saya anggap sebagai "bapak tuhan" semantik denotasional. (Quine pada dasarnya melakukan semantik denotasi bahasa alami di Word and Object , yang merupakan sumber inspirasi besar bagi Christopher Strachey. Tetapi buku ini cukup sulit.) Koleksi yang diedit Quintessence adalah sumber ide Quine yang bagus untuk seorang pemula.

[Catatan ditambahkan: Salah satu keuntungan filosofi dibandingkan matematika adalah bahwa siswa dapat melihat debat , yaitu, mereka dapat melihat argumen "benar" dan argumen "salah" dan melihat para ahli menghancurkan yang salah. Dalam matematika, seseorang tidak akan pernah melihat argumen yang salah, yang membatasi nilai pendidikannya.]