Apa yang dimaksud dengan semantik denotasional?

Pada utas lain , Andrej Bauer mendefinisikan semantik denotasional sebagai:

arti suatu program adalah fungsi dari makna bagian-bagiannya.

Yang menggangguku tentang definisi ini adalah bahwa ia tampaknya tidak memilih apa yang biasanya dianggap sebagai semantik denotasional dari apa yang biasanya dianggap sebagai semantik non-denotasional, yaitu semantik operasional struktural .

Lebih tepatnya, bahan utama di sini adalah modularitas , atau komposisionalitas , dari semantik, atau dengan kata lain, fakta bahwa mereka didefinisikan sesuai dengan struktur abstrak program.

Karena sebagian besar (semua?) Semantik formal saat ini cenderung struktural, apakah ini definisi yang diperlukan?

Jadi, pertanyaan saya adalah: Apa itu semantik denotasional?

Perbedaan yang saya buat secara pribadi antara semantik denotasional dan semantik adalah sesuatu seperti ini:

• semantik denotasional adalah matematika dan persamaan. Rincian masalah reduksi kurang dari hasil akhir, yang merupakan nilai abadi dalam beberapa ruang matematika.
• semantik operasional bersifat algoritmik. Itu terungkap dalam langkah-langkah individu dalam waktu. Proses adalah bagian dari maknanya, dan hasil akhirnya hanyalah langkah yang dibedakan dalam proses itu.

Perbedaannya kadang-kadang bisa sangat halus, dan bisa sulit untuk mengatakan apakah itu hanya perbedaan gaya, atau substansi.

Namun, kita dapat melihat bagaimana definisi komposisi Andrej mengikuti secara lebih alami dari definisi denotasional, dan kita juga dapat dengan mudah membayangkan semantik non-konfluen, non-komposisi yang masih memenuhi definisi operasional.

Jika saya menebak apa yang akan dikatakan Dana Scott, ia mungkin akan mengatakan bahwa semantik denotasional bersifat komposisional (seperti apa yang saya klaim) dan bahwa makna suatu program haruslah objek matematika asli, bukan entitas sintaksis atau formalis. Tentu saja, pandangan seperti itu menuntut seseorang untuk membedakan antara manipulasi formal sintaksis dan matematika "benar". Ini tentu merupakan perbedaan non-matematis.

Sebagai renungan, orang mungkin ingin maknanya mencukupi dalam arti bahwa dua program yang berbeda secara pengamatan tidak menerima makna yang sama. Tentu saja, kecukupan jenis ini tergantung pada apa yang orang akui sebagai "pengamatan".

Di bawah pandangan ini dapat dikatakan bahwa semantik operasional struktural bukan semantik denotasional karena menyamakan makna entitas sintaksis dengan entitas sintaksis lain (nilai atau urutan reduksi).

Saya setuju bahwa identifikasi A. Bauer tentang semantik denotasional dengan komposisionalitas (dalam Buku tentang semantik bahasa pemrograman ) tidak benar-benar menggambarkan dengan baik apa yang secara tradisional dimaksudkan oleh semantik denotasional, karena semantik operasional yang jelas serta logika program (semantik aksioma) adalah komposisi .

Saya menyarankan istilah ini paling baik dipahami secara sosio-historis, sebagai merujuk secara longgar pada tradisi teori tertentu (dimulai dengan sungguh-sungguh ketika Scott menghasilkan model kisi-teori dari lambda-kalkulus yang tidak diketik) dengan alat-alat tertentu yang disukai (teori pesanan, teorema fixpoint , topologi, teori kategori) dan bahasa target pilihan (murni fungsional dan berurutan). Saya membayangkan bahwa - terlepas dari kepentingan intelektual murni - semantik denotasional sebagian besar ditemukan karena:

1. Dulu sulit untuk alasan tentang semantik operasional.

2. Dulu sulit untuk memberikan semantik aksioma untuk bahasa non-sepele.

Saya berpendapat bahwa kedua masalah telah diperbaiki ke tingkat yang substansial, (1) misalnya dengan teknik berbasis bisimilasi yang berasal dari teori proses (yang dapat dilihat sebagai bentuk spesifik semantik operasional) atau misalnya Pitts bekerja pada semantik operasional dan program kesetaraan, dan (2) oleh pengembangan misalnya logika pemisahan atau logika Hoare yang diturunkan sebagai versi yang diketik dari logika Hennessy-Milner melalui embedded bahasa pemrograman dalam bahasa yang diketikkan -calculi.$\pi$

Jadi, secara ringkas, saya berpendapat bahwa istilah "semantik denotasional" menjadi kurang tepat, dan dengan demikian kurang bermanfaat. Mungkin bermanfaat bagi komunitas semantik untuk bertemu menuju terminologi yang lebih baik.

Saya senang dengan jawaban Adrej, tetapi saya ingin menelusuri lebih jauh.

Untuk mulai dengan, semantik denotasional ingin mengatakan sesuatu seperti "arti dari notasi ini adalah itu". Seorang semantikis sejati ingin membayangkan bahwa makna adalah apa yang ada dalam pikiran kita dan notasi hanyalah cara mengekspresikan makna itu. Persyaratan bahwa semantik denotasional harus bersifat komposisional mengikuti dari ini. Jika maknanya adalah primer dan notasi sekunder, maka kita tidak punya pilihan selain mendefinisikan makna notasi yang lebih besar sebagai fungsi dari makna konstituennya.

Jika kita menerima sudut pandang ini maka semantik denotasional yang baik perlu menangkap makna yang kita anggap kita miliki dalam pikiran kita. Semantik komposisi apa pun tidak selalu cocok dengan tagihan. Jika saya datang dengan definisi semantik komposisi dan tidak ada yang setuju bahwa itu menyatakan makna yang mereka miliki di kepala mereka, maka itu tidak ada gunanya. Game semantik saat ini ada dalam situasi ini. Ini adalah definisi komposisi dan secara teknis cukup kuat, tetapi sangat sedikit orang yang setuju bahwa itu ada hubungannya dengan makna yang mereka miliki dalam pikiran mereka.

Yang mengatakan, definisi komposisi apa pun memiliki berbagai keunggulan teknis. Kami dapat menggunakannya untuk memverifikasi persamaan atau properti lainnya dengan menginduksi sintaksis istilah. Kita dapat menggunakannya untuk memverifikasi kesehatan sistem bukti, sekali lagi dengan menginduksi sintaksis istilah. Kami dapat memverifikasi kebenaran kompiler atau teknik analisis program (yang, berdasarkan sifatnya, ditentukan oleh induksi pada sintaksis). Definisi semantik yang sepenuhnya abstrak bahkan memiliki lebih banyak keunggulan teknis. Anda dapat menggunakannya untuk menunjukkan bahwa dua program tidak setara, yang tidak dapat Anda lakukan dengan semantik komposisi semena-mena. Definisi semantik sepenuhnya dapat didefinisikan bahkan lebih baik. Di sini domain semantik memiliki apa yang dapat Anda ungkapkan dalam bahasa pemrograman (dengan beberapa ketentuan). Jadi, Anda dapat menghitung nilai dalam domain untuk melihat nilai apa yang ada, yang akan sulit dilakukan dengan notasi sintaksis. Atas dasar-dasar ini, skor semantik game sangat cemerlang.

Namun, definisi semantik komposisi telah kehilangan keunggulan mereka selama bertahun-tahun. Robin Milner dan Andy Pitts telah mengembangkan sejumlah teknik " penalaran operasional ", yang bekerja murni pada sintaksis tetapi menggunakan semantik operasional di mana pun diperlukan untuk membicarakan perilaku. Teknik penalaran operasional ini berteknologi rendah. Tidak ada matematika mewah. Tidak ada benda tak terbatas. Kita bisa mengajar mereka kepada mahasiswa dan siapa saja bisa menggunakannya. Jadi, banyak orang bertanya mengapa kita perlu semantik denotasional sama sekali. (Martin Berger mungkin di kamp ini.)

Secara pribadi, saya tidak punya masalah dengan memiliki banyak alat di kotak alat saya. Teknik denotasi mungkin menghasilkan skor yang lebih baik untuk beberapa masalah dan teknik operasional untuk orang lain. Para peneliti yang mengembangkan teori mungkin lebih baik untuk satu pendekatan atau yang lain. Cukup sering, kita dapat mengembangkan wawasan dalam satu pendekatan dan mentransfer wawasan tersebut ke pendekatan lain. (Banyak pekerjaan Andy Pitts dari jenis ini. Parametrisitas relasional dikembangkan dalam pengaturan denotasional tetapi dia mampu mengetahui bagaimana menyatakannya kembali sebagai alasan operasional. Ketika saya melihatnya, saya berkata "wow, saya tidak akan pernah berpikir itu akan mungkin. "Pemisahan Logika juga akan seperti ini. Steve Brookes memberikan bukti kesehatan 60 halaman untuk Concurrent Separation Logic menggunakan semantik denotasional.

Pendekatan operasional juga mendapat nilai cemerlang ketika bahasa pemrograman menjadi sangat mewah, dengan semua jenis tipe gila yang lebih tinggi. Kita mungkin tidak tahu bagaimana memodelkan hal-hal seperti itu secara matematis. Atau, model matematika standar mungkin berubah menjadi tidak konsisten di bawah tekanan kelengkungan. (Sebagai contoh, lihat "Polimorfisme tidak set-theoretik" oleh Reynolds.) Pendekatan operasional yang bekerja murni pada sintaksis dapat dengan rapi memandu semua masalah matematika ini.

Pendekatan lain yang merupakan perantara antara pendekatan operasional dan denotasional adalah realisasi . Alih-alih bekerja dengan istilah sintaksis seperti dalam pendekatan operasional, kami pergi sebagian denotasional dengan menggunakan beberapa bentuk lain dari perwakilan matematika. Perwakilan ini mungkin tidak memenuhi syarat sebagai "makna" denotasional nyata tetapi mereka setidaknya akan sedikit lebih abstrak daripada istilah sintaksis. Sebagai contoh, untuk kalkulus lambda polimorfik, pertama-tama kita dapat memberi makna pada istilah yang tidak diketik (dalam beberapa model kalkulus lambda yang tidak diketik) dan kemudian menggunakannya sebagai perwakilan ('realizers') untuk melakukan semacam "penalaran operasional" dengan sedikit tingkat yang lebih abstrak.

Jadi, biarlah ada persaingan sehat antara pendekatan denotasional, operasional, dan realisasi. Tidak ada salahnya.

Di sisi lain, mungkin ada juga persaingan "tidak sehat" yang tumbuh di antara berbagai pendekatan. Orang yang bekerja dengan satu pendekatan mungkin sangat dekat dengan itu sehingga mereka mungkin tidak melihat inti dari pendekatan lain. Idealnya kita semua harus menyadari kekuatan dan kelemahan dari pendekatan yang berbeda dan mengembangkan sikap ilmiah terhadap mereka bahkan jika mereka bukan favorit individu kita.

[Satu jawaban lagi. Mungkin tidak keren untuk menumpuk beberapa jawaban. Tapi, hei, ini adalah masalah yang dalam.]

Saya mengatakan bahwa saya setuju dengan jawaban Andrej, tetapi tampaknya saya tidak sepenuhnya setuju. Ada perbedaan.

Saya mengatakan bahwa semantik denotasional harus mengatakan "arti dari notasi ini adalah itu". Yang saya maksudkan adalah bahwa notasi harus diberi makna, yang merupakan beberapa bentuk entitas konseptual , bukan beberapa notasi lainnya. Sebaliknya, Andrej juga mensyaratkan, mengutip Scott, bahwa artinya harus berupa objek "matematis". Saya tidak percaya bahwa bit matematika diperlukan.

Sebagai contoh, itu akan baik-baik saja, dari sudut pandang saya, untuk arti notasi menjadi proses fisik. Setelah semua program komputer memakai rem di mobil Anda, menerbangkan pesawat, menjatuhkan bom, dan apa yang tidak. Ini adalah proses fisik, bukan elemen dalam ruang matematika. Anda tidak dapat menjatuhkan bom, melihat apakah itu membunuh seseorang, dan mengambilnya kembali jika tidak. Program komputer tidak bisa melakukan itu. Tetapi fungsi matematika bisa. (Mereka disebut operasi "snapback".) Jadi, sama sekali tidak jelas bahwa fungsi matematika akan membuat makna yang baik untuk program komputer.

Di sisi lain, kita benar-benar belum tahu bagaimana berbicara tentang proses fisik secara abstrak. Jadi, kita mungkin memang menggunakan beberapa deskripsi matematis tentang proses untuk mengartikulasikan ide-ide kita. Tetapi deskripsi matematis ini hanya akan menjadi "deskripsi". Itu bukan makna. Makna sebenarnya hanya proses fisik yang kita bayangkan secara konseptual.

Dalam pidato penerimaannya untuk penghargaan SIGPLAN (yang seharusnya ada di youtube dalam waktu dekat), Hoare mengatakan bahwa ACP menggunakan "pendekatan aljabar", CSP menggunakan "pendekatan denotasional" dan CCS menggunakan "pendekatan operasional" untuk menggambarkan proses. Ohad dan saya duduk bersama di sesi itu, kami saling memandang dan berkata "itu sangat menarik". Jadi, ada banyak ruang konseptual di sini yang sedang dieksplorasi. Saya pikir banyak pekerjaan Scott nanti, tentang sistem lingkungan dan sistem informasi dll, memang merupakan upaya untuk menjelaskan fungsi sebagai "proses" dari beberapa bentuk. Geometri interaksi Girard dan semantik permainan selanjutnya juga merupakan upaya untuk menjelaskan fungsi sebagai proses. Saya akan mengatakan bahwa mengembangkan teori proses yang solid bisa menjadi kontribusi besar yang dapat dibuat Ilmu Komputer untuk matematika abad ke-21. Saya tidak akan menerima kepercayaan bahwa matematika memiliki semua jawaban dan kita harus berusaha mengurangi fenomena komputasi menjadi konsep matematika untuk memahaminya.

Yang mengherankan saya adalah betapa indahnya penyembunyian informasi bekerja dalam perhitungan stateful (pemrograman imperatif serta proses kalkulus), sedangkan itu canggung dan rumit dalam formalisme matematika / fungsional. Ya, kami memiliki parametrik relasional, dan memungkinkan kami untuk mengatasi keterbatasan formalisme matematika dengan sangat baik. Tetapi itu tidak sesuai dengan kesederhanaan dan keanggunan pemrograman imperatif. Jadi, saya tidak percaya bahwa formalisme matematika adalah jawaban yang tepat, meskipun saya akan mengakui bahwa itu adalah jawaban terbaik yang kami miliki saat ini. Tetapi kita harus terus mencari. Ada teori bagus tentang proses di luar sana yang akan mengalahkan matematika tradisional dengan mudah.

[Semoga ini jawaban terakhir saya untuk pertanyaan ini!]

Pertanyaan awal Ohad adalah tentang bagaimana semantik denotasional berbeda dari semantik operasional struktural. Dia berpikir bahwa keduanya adalah komposisi. Sebenarnya itu tidak benar. Semantik operasional struktural diberikan sebagai urutan langkah. Setiap langkah diekspresikan secara komposisional (dan sangat luar biasa bagi Plotkin untuk membuat penemuan bahwa ini mungkin!), Tetapi seluruh perilaku tidak didefinisikan secara komposisional. Inilah yang dikatakan Plotkin dalam pengantarnya pada artikel SOS [penekanan ditambahkan]:

Dalam semantik denotasional seseorang mengikuti ideal komposisionalitas, di mana makna frase majemuk diberikan sebagai fungsi dari makna bagian-bagiannya. Dalam kasus semantik operasional, seseorang mempertimbangkan perilaku frasa program, yang hanya merupakan kumpulan transisi yang dapat dibuatnya. Perilaku ini, bagaimanapun, tidak komposisional ketika dianggap sebagai fungsi dari frase program. Namun aturan memberikannya secara struktural, yaitu, primitif secara rekursif, dalam sintaksis; ...

Fakta bahwa setiap langkah diekspresikan secara komposisional tidak berarti bahwa seluruh perilaku dinyatakan secara komposisional.

Ada artikel bagus oleh Carl Gunter yang disebut Bentuk Spesifikasi Semantik , di mana berbagai metode menentukan semantik dibandingkan dan dikontraskan. Banyak dari materi ini juga direproduksi dalam bab pertama teks "Semantics of Programming Languages". Semoga ini bisa memperjelas gambar.

Kata lain tentang "semantik operasional". Pada masa-masa awal, istilah "operasional" digunakan untuk merujuk pada definisi semantik yang merujuk pada langkah-langkah evaluasi terperinci. Baik semanticists denotasional dan pendukung aksiomatik memandang rendah semantik "operasional", menganggapnya sebagai level rendah dan berorientasi mesin. Saya pikir ini benar-benar didasarkan pada kepercayaan mereka bahwa deskripsi tingkat yang lebih tinggi dimungkinkan. Keyakinan ini hancur segera setelah mereka mempertimbangkan konkurensi. Proses de Bakker dan Zucker dan semantik konkuren konkuren memiliki bagian-bagian yang menarik ini:

Kami akan menggunakan metodologi semantik denotasional . "Denotasional" harus dikontraskan di sini dengan "operasional": Gagasan utama dari pendekatan sebelumnya adalah bahwa ekspresi dalam bahasa pemrograman menunjukkan nilai dalam domain matematika yang dilengkapi dengan struktur yang sesuai, sedangkan pada yang terakhir operasi seperti yang ditentukan oleh konstruksi bahasa adalah dimodelkan oleh langkah-langkah yang dilakukan oleh beberapa mesin abstrak ....

Model matematika berisi berbagai gagasan yang, meskipun denotasional dalam gaya, bersifat operasional [penekanan ditambahkan]. Ini termasuk fitur "sejarah" dari gagasan proses itu sendiri, dan penggunaan apa yang disebut gerakan diam dalam berurusan dengan sinkronisasi dan rekursi.

Di sini kita melihat penulis berjuang dengan dua pengertian "operasional", satu gagasan teknis - perilaku yang diekspresikan menggunakan manipulasi sintaksis, dan yang lainnya, gagasan konseptual - menjadi tingkat rendah dan rinci. Kredit sebagian besar jatuh ke Plotkin dan Milner untuk merehabilitasi semantik "operasional", menjadikannya setinggi mungkin dan menunjukkan bahwa itu bisa elegan dan berwawasan luas.

Terlepas dari semua ini, gagasan operasional proses masih sangat berbeda dari gagasan proses denotasional, yang belakangan dikembangkan oleh de Bakker dan Hoare dan tim mereka. Dan, saya pikir ada banyak yang misterius dan indah tentang konsep proses denotasional yang masih harus dipahami.

Tanggapan tambahan ini adalah untuk memperkuat titik bahwa model semantik denotasional dirancang untuk "menjelaskan" fenomena komputasi. Saya akan memberikan serangkaian contoh dari semantik bahasa pemrograman imperatif (juga disebut bahasa "mirip-Algol").

Pertama ada model semantik yang dirumuskan oleh Scott dan Strachey. (Lih. Gordon: Deskripsi denotasional bahasa pemrograman - favorit saya sepanjang masa atau buku Winskel.) Model ini menyatakan bahwa ada keadaan global , yang terdiri dari keadaan semua lokasi yang dialokasikan oleh suatu program. Setiap perintah ditafsirkan sebagai semacam fungsi dari negara global ke negara global.

Reynolds mengatakan bahwa itu tidak memodelkan disiplin tumpukan variabel lokal. Ketika ruang lingkup lokal dimasukkan, variabelnya dialokasikan, dan mereka tidak dialokasikan ketika ruang lingkup keluar. Pada dasarnya, ini adalah pertanyaan, "dalam arti apa variabel lokal bersifat lokal?" Bagaimana semantik menangkap lokalitas? Untuk menjelaskan ini, ia menemukan model functor-kategori. (Lih. Reynolds: Esensi dari Algol dan Tennent: Semantik bahasa pemrograman).

Tennent ingin memodelkan prinsip-prinsip penalaran yang dirumuskan dalam Logika Spesifikasi Reynolds (perpanjangan Hoare Logic untuk prosedur tingkat tinggi). Logika memiliki ide-ide seperti komputasi ekspresi (read-only), non-interferensi antara perintah-suka dan komputasi-seperti perhitungan, dan beberapa prinsip penalaran abstraksi data. Dia memperhalus model functor-kategori Reynolds untuk menemukan yang baru. Ini disebut model "SASL", juga tercakup dalam buku Tennent.

Meyer dan Sieber, dan juga O'Hearn dan Tennent, mencatat bahwa tidak satu pun dari model-model ini yang sepenuhnya menangkap lokalitas variabel lokal. Ketika dua implementasi dari tipe data abstrak atau kelas berbeda dalam variabel lokal mereka tetapi memanipulasinya dengan cara yang memiliki perilaku yang sama ketika dilihat dari luar, mereka setara secara observasi. Semantik denotasional harus menyamakan mereka. Untuk memodelkan ini, O'Hearn dan Tennent menambahkan parametrisitas relasional ke varian model functor-kategori Reynolds.

Ketika saya melihat masalah pada saat yang sama, saya tidak percaya pada pendekatan functor-kategori. Saya juga berpikir bahwa itu terlalu teknis dan percaya harus ada model yang lebih sederhana. Ini mendorong saya untuk menciptakan model "Keadaan global yang dianggap tidak perlu", yang agak mirip model jejak CSP, tetapi untuk bahasa tingkat tinggi. Sebagai bonus tambahan, model ini juga menangkap irreversibilitas perubahan negara, yang tidak ada pada model sebelumnya.

Model saya hanya berfungsi untuk subbahasa Algol yang berperilaku baik, yang disebut Kontrol Intertensi Sintaksis . Abramsky dan McCusker memperluas model saya menggunakan ide semantik game sehingga bisa bekerja untuk Algol penuh. Jadi, model mereka menjelaskan fenomena yang sama dengan saya, tetapi untuk bahasa yang lebih besar.

Dalam setiap kasus, kami dapat menunjukkan bahwa model baru menangkap kesetaraan pengamatan (atau bentuk lain dari rumus logis) yang menunjukkan fenomena komputasi yang disebutkan, yang tidak divalidasi oleh model sebelumnya. Jadi, ada pengertian yang sangat tepat di mana model-model ini "menjelaskan" fenomena komputasi.

[Semua pekerjaan yang saya sebutkan di sini dapat ditemukan dalam volume "Bahasa Algol-like Languages": tautan dan tautan ]