Bagaimana bahasa pemrograman dan dasar matematika terkait?

Pada dasarnya saya mengetahui tiga dasar untuk matematika

1. Tetapkan teori
2. Jenis teori
3. Teori kategori

Jadi dalam hal apa bahasa pemrograman dan dasar matematika terkait?

EDIT

Pertanyaan aslinya adalah "Memprogram bahasa berdasarkan dasar matematika"

dengan paragarph ditambahkan

Dan implementasi teori
1. Ketikkan teori dalam Coq
2. Set teori dalam SETL
3. Kategori teori dalam Haskell

Berdasarkan saran ini diubah menjadi "Bagaimana bahasa pemrograman dan dasar-dasar matematika terkait"

Karena ini adalah salah satu dari pertanyaan-pertanyaan itu jika saya tidak cukup tahu tentang apa yang saya tanyakan tetapi ingin belajar sesuatu, saya memodifikasi pertanyaan itu agar lebih berharga untuk dipelajari dan yang lain, namun meninggalkan detailnya agar tidak membuat jawaban saat ini oleh Andrej Bauer tampaknya keluar dari topik.

Terima kasih atas semua komentar dan jawabannya sejauh ini, saya belajar dari mereka.

[Catatan: paragraf ini sudah usang.] Judul pertanyaan Anda berisi asumsi yang tidak beralasan, yaitu bahwa bahasa pemrograman "berdasarkan pada dasar matematika". Ini umumnya tidak terjadi, meskipun kedua bidang memiliki hubungan yang penting. Pernyataan yang lebih akurat adalah bahwa (beberapa) bahasa pemrograman dirancang menggunakan teknik-teknik dasar. Pertanyaan yang lebih baik untuk ditanyakan adalah "bagaimana bahasa pemrograman dan dasar-dasar matematika terkait?"

Koneksi yang paling umum diwujudkan dalam slogan proof-as-programs , yang dapat dibuat bekerja dengan beberapa cara. The Curry-Howard korespondensi adalah yang paling jelas satu. Dengan itu kita berhubungan sekaligus mengetik teori, logika, dan pemrograman. Tetapi harus ditekankan bahwa korespondensi Curry-Howard tidak bekerja dengan baik di hadapan rekursi umum (karena setiap jenis menjadi dihuni), yang didukung oleh setiap bahasa pemrograman tujuan umum.

Cara yang lebih halus untuk membuat slogan proof-as-programs berfungsi adalah dengan menggunakan realizability . Di sini kita juga menghubungkan bukti dan program, tetapi sekarang arahnya beralih dari bukti ke program: setiap bukti memberikan program, tetapi tidak setiap program selalu merupakan bukti.

Contoh utama bahasa pemrograman berdasarkan pada yayasan adalah Agda , yang hanya merupakan implementasi dari teori tipe dependen. Namun, Agda bukan bahasa pemrograman untuk tujuan umum karena tidak mendukung rekursi umum. Setiap fungsi di Agda adalah total, dan ada fungsi yang dapat dihitung yang tidak dapat diimplementasikan di Agda. Dalam praktiknya programmer tidak akan memperhatikan ini, tetapi mereka akan melihat bahwa Agda tidak mengizinkan nilai yang tidak ditentukan, misalnya loop tak terbatas

Coq adalah tidak bahasa pemrograman melainkan seorang asisten bukti. Namun, ia juga memiliki kemampuan ekstraksi yang memberikan program dari bukti. Asisten pembuktian dan bahasa pemrograman tidak boleh bingung satu sama lain.

Kita tidak boleh lupa bahwa prolog dan bahasa pemrograman logika lainnya mengambil inspirasi mereka dari gagasan bahwa perhitungan adalah pencarian bukti . Ini tentu saja berkaitan erat dengan logika.

Haskell adalah bahasa pemrograman untuk tujuan umum yang didasarkan pada teori domain . Dengan kata lain, semantiknya adalah teori-domain karena harus memperhitungkan fungsi dan rekursi parsial. Komunitas Haskell telah mengembangkan sejumlah teknik yang diilhami oleh teori kategori, yang mana monad paling terkenal tetapi tidak boleh dikacaukan dengan monad . Secara lebih umum, fitur pemrograman tingkat lanjut biasanya diperlakukan dengan kombinasi teori domain dan teori kategori, tetapi ini bukan sesuatu yang mahir oleh programmer Haskell. Apa yang disebut "kategori sintaksis" dari tipe-tipe Haskell adalah pandangan orang awam tentang bagaimana Haskell dan teori kategori berhubungan satu sama lain.

Teori himpunan (klasik atau konstruktif) tampaknya menginspirasi ide-ide dalam bahasa pemrograman ke tingkat yang lebih rendah. Tentu saja, teori himpunan konstruktif memiliki koneksi ke pemrograman melalui logika konstruktif. Satu aplikasi penting dari teori himpunan intuitionistic untuk bahasa pemrograman diberikan oleh Alex Simpson yang menggunakannya untuk membuat teori domain sintetik bekerja. Tapi ini hal yang cukup maju, mungkin lihat slide ini . Jean-Louis Krivine telah mengembangkan merek realisasi yang sangat menarik untuk teori himpunan klasik. Ini tampaknya cara yang baik untuk menghubungkan teori himpunan klasik dan pemrograman.

Singkatnya, teori bahasa pemrograman menggunakan teknik dasar. Ini tidak mengherankan, karena kami menganggap komputasi sebagai konsep mendasar. Tetapi terlalu naif untuk mengatakan bahwa bahasa pemrograman "berdasarkan" pada fondasi tertentu. Sebenarnya, trikotomi yayasan "teori himpunan - teori tipe - teori kategori" sekali lagi hanyalah pengamatan tingkat tinggi yang berguna yang dapat dibuat akurat secara matematis dalam berbagai cara, tetapi tidak ada yang perlu tentang hal itu. Itu adalah kecelakaan bersejarah.

ini adalah topik yang sangat kompleks dan ada banyak buku hebat tentang masalah ini, yang baru-baru ini disebut Turings Cathedral, asal-usul alam semesta digital dan juga Mesin logika, ahli matematika, dan asal-usul komputer .

bahasa komputer telah berkembang selama beberapa dekade, tetapi percaya atau tidak ada dua bahasa pemrograman asli yang menunjukkan bahwa matematika dan ilmu komputer saling terkait:

• Makalah Turing 1936 tentang masalah penghentian . konstruksi teoretis untuk menyelesaikan masalah yang diajukan oleh hilbert pada pergantian abad, Entscheidungsproblem , yaitu prosedur otomatis untuk memecahkan masalah matematika!

• Kalkulus lambda Gereja yang dikembangkan pada saat yang sama masih bertahan dalam bahasa seperti cisp dan skema

ada dua tokoh kunci yang melintasi batas matematika dan ilmu komputer wrt "bahasa pemrograman":

• teori informasi yang dipelopori oleh Shannon menunjukkan hubungan yang mendalam antara matematika dan ilmu komputer

• tokoh kunci lain yang melintasi antara matematika dan ilmu komputer adalah Von Neumann . ia menemukan arsitektur von neumann untuk menyimpan program dalam memori.

"bahasa pemrograman" yang lebih awal:

• kata bahasa Inggris "komputer" pada awalnya berarti sesuatu yang lebih seperti "kalkulator" yang menggunakan operasi matematika pada angka dan artinya telah bergeser secara substansial ke konsep pemrograman tujuan umum saat ini. jadi ada koneksi antara bahasa pemrograman dan kalkulator awal.
• kartu punch yang digunakan dalam menenun alat tenun dari akhir abad 19 dan awal 20 adalah "bahasa pemrograman" untuk pola tenun. perhatikan bahwa kartu punch banyak digunakan untuk pemrograman mainframe pada 1960-an. ini awalnya dilihat sebagai "mesin hitung" (menggunakan matematika!) tidak begitu modern, komputer tujuan umum.
• Babbage dan Ada Lovelace mengembangkan konsep awal yang belum sempurna dari "bahasa pemrograman" pada pertengahan 1800-an dengan "mesin penghitung"
• aljabar boolean awalnya merupakan konsep matematika murni yang ditemukan oleh Boole
• sempoa kuno (milenia lama) untuk perhitungan matematika dipandang sebagai cikal bakal komputer modern. tetapi dapat dikatakan bahwa operasi untuk memanipulasinya adalah semacam "bahasa pemrograman" (diikuti oleh manusia)

Namun, dalam bahasa pemrograman modern karena abstraksi telah meningkat dan ditingkatkan, koneksi yang jelas dan langsung ke matematika agak menurun selama beberapa dekade, tetapi selalu menjadi sangat intrinsik dan dalam beberapa hal, itu telah menguat. misalnya bahasa seperti Java dengan tipe ketatnya memiliki koneksi ke matematika, dan pada mulanya pada akhir ~ 1990an bahasa komputer utama (misalnya c ++, Java, Ruby dll) mulai secara eksplisit mengimplementasikan banyak objek tingkat tinggi matematika sebagai primitif dekat dalam bahasa seperti set, tree (misalnya Btrees atau hashmaps), dll.