Apa dasar teori pemrograman imperatif?

Pemrograman fungsional memiliki dasar teoritis dalam kalkulus lambda dan logika kombinatorik . Sebagai seseorang yang terlibat dalam komputasi statistik, saya menemukan konsep-konsep ini sangat berguna untuk pemodelan.

Apakah ada dasar matematika yang setara dengan pemrograman imperatif , atau apakah itu hanya tumbuh dari aplikasi perangkat keras praktis dalam bahasa mesin dan pengembangan FORTRAN selanjutnya ?

Secara umum, ketika matematika digunakan untuk mempelajari beberapa X , yang pertama membutuhkan model X , dan kemudian mengembangkan teori, satu set hasil tentang model itu. Saya kira teori yang dapat dikatakan sebagai "dasar teoritis" untuk X . Sekarang atur X = perhitungan. Ada banyak model perhitungan, banyak yang melibatkan "negara". Setiap model memiliki "teori" sendiri dan kadang-kadang mungkin untuk "menerjemahkan" antar model. Saya percaya sulit untuk mengatakan model mana yang lebih "dasar" --- mereka hanya dirancang dengan tujuan yang berbeda dalam pikiran.

Mesin Turing dirancang untuk menentukan apa yang dapat dihitung . Jadi mereka membuat model yang bagus jika Anda peduli apakah ada algoritma untuk masalah tertentu. Model ini kadang-kadang disalahgunakan untuk mempelajari efisiensi algoritma atau kekerasan masalah, dengan dalih bahwa itu cukup baik, setidaknya jika Anda hanya peduli pada polinomial / non-polinomial. Model RAM lebih dekat ke komputer nyata dan oleh karena itu lebih baik jika Anda menginginkan analisis algoritma yang tepat. Untuk menempatkan batas bawah pada kekerasan masalah, lebih baik tidakgunakan model yang mirip dengan komputer saat ini karena Anda ingin mencakup berbagai komputer yang mungkin, namun tetap lebih tepat daripada hanya polinomial / non-polinomial. Dalam konteks ini, saya melihat misalnya model sel-probe yang digunakan.

Jika Anda peduli tentang kebenaran , maka masih ada model lain yang bermanfaat. Di sini Anda memiliki semantik operasional (yang saya katakan adalah analog dari kalkulus lambda untuk perhitungan penuh negara), semantik aksiomatik (dikembangkan pada 1969 oleh Hoare berdasarkan pernyataan induktif Floyd dari 1967, yang dipopulerkan oleh Knuth dalam The Art of Computer Programming , volume 1), dan lainnya.

Untuk meringkas, saya pikir Anda mencari model perhitungan. Ada banyak model seperti itu, yang dikembangkan dengan berbagai tujuan dalam pikiran, dan banyak yang menyatakan, sehingga mereka sesuai dengan pemrograman imperatif. Jika Anda ingin tahu apakah sesuatu dapat dihitung, maka lihatlah mesin Turing. Jika Anda peduli efisiensi, lihat model RAM. Jika Anda peduli tentang kebenaran, lihat model yang diakhiri dengan "semantik", seperti semantik operasional.

Akhirnya, izinkan saya menyebutkan bahwa ada buku besar online hanya tentang Models of Computation oleh John Savage. Sebagian besar tentang efisiensi. Untuk bagian yang benar saya sarankan Anda mulai dengan karya-karya klasik Floyd (1967) , Hoare (1969) , Dijkstra (1975) , dan Plotkin (1981) . Mereka semua sangat keren.

Model teoritis paling sederhana dari program imperatif adalah mesin turing itu sendiri. Ini memiliki kedua komponen penting dari program imperatif: keadaan yang dapat dimodifikasi tanpa batas dan mesin negara yang beroperasi di atasnya.

Anda juga dapat memasukkan pemrograman imperatif ke pemrograman fungsional dengan mempertimbangkan program sebagai komposisi operasi monadik yang lulus dan mengembalikan versi modifikasi dari negara global, seperti yang dilakukan dalam bahasa pemrograman Haskell.

Singkatnya, saya akan mengatakan bahwa pemrograman imperatif berevolusi dari bahasa mesin dan praktik pemrograman. Di sisi lain, monads menyediakan kerangka kerja semantik yang sesuai untuk menggambarkan semantik fitur bahasa pemrograman yang penting. Makalah Makalah tentang perhitungan dan monad oleh Moggi mendirikan yayasan formal. Phil Wadler mempopulerkan ide itu dan berkontribusi secara signifikan pada hal itu menjadi cara kunci untuk memasukkan fitur-fitur penting ke dalam bahasa pemrograman Haskell. Karya terbaru oleh Plotkin dan Power Notions of Computation Menentukan Monads sebaliknya menyatakan bahwa beberapa, tetapi tidak semua, gagasan perhitungan (imperatif) benar-benar memberikan monad, yang berarti bahwa dalam cara yang sangat esensial, monad berhubungan dengan gagasan imperatif (dan lainnya) tentang perhitungan.

Jika Anda mencari perlakuan matematika yang ketat dari bahasa pemrograman imperatif, buku Winskel "The Semantics Resmi Bahasa Pemrograman" (1993) adalah contohnya.

Dalam buku itu, ia mendefinisikan bahasa pemrograman imperatif yang disebut IMP dan menyediakan semantik operasional, denotasional, dan aksiomatis.

Saya datang ke pertanyaan ini terlambat, tetapi ini adalah pertanyaan yang menarik. Jadi, inilah pandangan saya.

Ketika saya masih sarjana, kami memiliki profesor Matematika yang hebat, yang biasa memberi kami kuliah tentang sejarah dan perkembangan matematika. Menurutnya, matematika berkembang dalam gelombang "ekspansi" dan "konsolidasi". Selama fase ekspansi, ide-ide baru yang sebelumnya tidak diketahui dipertimbangkan dan diselidiki. Kemudian, selama fase konsolidasi, teori-teori baru diintegrasikan ke dalam tubuh pengetahuan yang ada. Namun, pada abad ke-20, katanya, ekspansi dan konsolidasi sedang berlangsung secara paralel.

Pemrograman imperatif saat ini merupakan kegiatan ekspansi untuk matematika. Sebelumnya "tidak dikenal". (Itu mungkin tidak sepenuhnya benar. Hoare memberi tahu kita bahwa Euclid melakukan sesuatu seperti pemrograman imperatif dalam Geometri-nya. Tetapi matematika kehilangan minat di dalamnya, baik atau buruk.) Matematikawan masih tidak tertarik pada pemrograman imperatif. Begitu banyak kerugian bagi mereka. Tapi saya menganggap semua Ilmu Komputer sebagai cabang matematika dalam arti abstrak. Kami sedang mempelajarinya, memperluas matematika dalam proses.

Jadi, saya tidak akan peduli terutama apakah ada dasar teori apriori untuk pemrograman imperatif. Jika tidak ada, mari kita pergi dan menemukannya. Apa yang kita ketahui sudah memberi tahu kita bahwa pemrograman imperatif sangat dalam dan indah. Pemrograman fungsional artinya jika dibandingkan. Tetapi, kami memiliki banyak pekerjaan yang harus dilakukan untuk membawa semua teori ini kepada orang-orang.

Pemrograman fungsional memiliki dasar yang jelas dalam matematika karena bahasa pemrograman fungsional berkembang secara paralel dengan matematika yang relevan dan perancang mereka biasanya memegang matematika dalam hal yang tinggi. Hubungan yang kuat dan langsung adalah ramalan yang terpenuhi dengan sendirinya.

Pemrograman imperatif memiliki sejarah yang jauh lebih berantakan yang terkait lebih erat dengan masalah bisnis dan teknik dan secara historis jauh lebih peduli dengan kinerja kompiler dan kode yang mereka hasilkan daripada dengan menghormati formalisme matematika.

Banyak orang telah berusaha menjelaskan pemrograman imperatif dalam istilah fungsional (tradisional). Ini mungkin yang paling dekat dengan apa yang Anda cari, tetapi upaya ini selalu canggung, membosankan, forensik. Saya cukup yakin saya lebih suka merobek mata saya dari wajah saya daripada membaca bukti kemajuan / pelestarian untuk CLR.

Biasanya jika Anda mendekati akhir dari buku teks pl yang layak (mis. Jenis dan Bahasa Pemrograman Pierce), Anda akan mulai melihat pemodelan formal fitur bahasa imperatif. Ini mungkin menarik bagi Anda.

An Axiomatic Basis for Computer Programming oleh CAR HOARE

Dalam makalah ini dilakukan upaya untuk mengeksplorasi dasar-dasar logis pemrograman komputer dengan menggunakan teknik yang pertama kali diterapkan dalam studi geometri dan kemudian diperluas ke cabang matematika lainnya. Ini melibatkan penjelasan set aksioma dan aturan inferensi yang dapat digunakan sebagai bukti sifat-sifat program komputer. Contoh diberikan dari aksioma dan aturan seperti itu, dan bukti formal dari teorema sederhana ditampilkan. Akhirnya, dikemukakan bahwa keuntungan penting, baik teoritis dan praktis, dapat mengikuti dari pengejaran topik ini.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Saya mendukung apa yang dikatakan Alexandre, bahwa mesin Turing memberikan dasar teori asli untuk pemrograman imperatif. Sejauh organisasi bahasa pemrograman imperatif mencerminkan arsitektur mesin, saya pikir karya John Von Neumann juga akan menjadi bagian penting dari fondasi teoretis mereka.

Apakah ada dasar matematika yang setara dengan pemrograman imperatif, atau apakah itu hanya tumbuh dari aplikasi perangkat keras praktis dalam bahasa mesin dan pengembangan FORTRAN selanjutnya?

Jika yang Anda maksud "dasar" dalam arti historis, saya pikir tidak ada "dasar matematika yang setara". Namun, meskipun pemrograman imperatif tumbuh dari keprihatinan praktis, ada beberapa cara untuk secara komprehensif mengkarakterisasi makna pemrograman imperatif dengan cara yang mungkin Anda temukan "berguna untuk pemodelan", seperti logika Hoare .

posting yang menyebutkan logika hoare dan logika pemisahan adalah yang benar dalam hal ini. Logika hoare memungkinkan Anda menyatakan properti dari seluruh konfigurasi heap suatu program, dan logika separasi adalah relatif lebih modern yang memungkinkan Anda menggunakan "separating conjunction" yang memungkinkan Anda menyatakan sebagai kondisi pra dan posting ke segmen kode untuk properti yang dipegang oleh properti bagian dari heap yang akan dimanipulasi oleh segmen program sambil menghitung sisa heap.

Jawaban mengenai monad tidak sepenuhnya akurat, karena dalam haskell monad digunakan hanya karena itu adalah abstraksi yang memungkinkan pengkodean urutan kendala evaluasi dan pelacakan eksplisit dari properti "mungkin menggunakan IO".

Patut ditunjukkan bahwa logika hoare / separasi dapat dipandang sebagai monad, dan bahwa ada sejumlah proyek kontemporer seperti proyek ynot di harvard yang mengeksplorasi topik-topik ini.

penelitian dalam logika pemisahan adalah bidang yang sedang berlangsung dan aktif.

Saya datang ke pertanyaan ini bahkan kemudian, tetapi saya sama-sama terpesona olehnya.

Mengapa teori pemrograman imperatif dianggap kurang mantap daripada teori pemrograman fungsional membuat saya terhindar. Mungkin mulai serius dengan Scott dan de Bakker pada tahun 1969 dengan analisis mereka tentang makna rekursi dalam bahasa imperatif sederhana [1]. Ketika bahasa imperatif memperoleh fitur, cerita menjadi sedikit berantakan tetapi itu hanya harga yang harus dibayar untuk menjadi lebih dekat dengan logam. Untuk menyebutkan salah satu upaya yang lebih komprehensif, pada tahun 1980, de Bakker, de Bruin, dan Zucker menulis monograf tentang masalah ini [2]. Yang lain disebutkan di atas. Referensi ini tentu saja logika pemisahan pra-tanggal tetapi [2] tetap menangani array dan prosedur yang saling rekursif.

[1]: tidak diterbitkan pada tahun 1969 tetapi muncul sebagai Jaco W. de Bakker dan Dana S. Scott. A Theory of Programs , halaman 1-30. Dalam Klop et al. JW de Bakker, 25 tahun semantiek. CWI, Amsterdam, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: Teori matematika tentang kebenaran program. Prentice Hall 1980.

Tak lama setelah Anda mengajukan pertanyaan, Mark Bender dari McMaster University merilis tesis: Assignment Calculus: A Pure Imperative Reasoning Language (2010 Sep 8). Tesis ini menjelaskan bahasa imperatif sederhana yang terkait dengan kalkulus lambda.

Tugas kalkulus hanya terdiri dari empat konstruksi dasar, penugasan X:=t, urutan t;u, pembentukan ¡tprosedur dan pemanggilan prosedur !t. Tiga interpretasi diberikan untuk AC: semantik operasional, semantik denotasi, dan sistem penulisan ulang istilah. Ketiganya terbukti setara.

Tesis Mark Bender melanjutkan untuk mengeksplorasi varian diperpanjang dengan evaluasi malas, mundur, komposisi prosedur. Ini mirip dengan eksplorasi kalkulus lambda dengan menggunakan ekstensi kecil.

Secara keseluruhan, tesis ini memberikan jawaban yang relatif langsung terhadap pertanyaan OP.