Semantik Operasional

Semantik operasional mendefinisikan makna suatu program dengan menentukan bagaimana program tersebut dieksekusi, menggunakan aturan inferensi yang menjelaskan langkah-langkah komputasi.

Definition

Semantik operasional menentukan makna suatu program sebagai urutan langkah komputasi yang dilakukannya, diberikan oleh relasi transisi yang didefinisikan secara induktif atas konfigurasi program.

Scope

Topik ini mencakup semantik operasional langkah-kecil (struktural) dan langkah-besar (natural), di mana relasi transisi atau evaluasi yang didefinisikan oleh aturan inferensi yang diarahkan sintaksis menjelaskan bagaimana program melakukan komputasi. Ini membahas strategi reduksi, mesin abstrak, dan bagaimana definisi operasional mendukung pembuktian kebenaran tipe (type soundness) dan kesetaraan program (program equivalence).

Core questions

• Bagaimana aturan inferensi menangkap langkah-langkah komputasi?
• Apa perbedaan antara semantik langkah-kecil dan langkah-besar?
• Bagaimana semantik operasional mendukung pembuktian kebenaran (soundness) dan kesetaraan (equivalence)?
• Bagaimana mesin abstrak berhubungan dengan definisi operasional berbasis aturan?

Key theories

Semantik operasional struktural

Plotkin mendefinisikan eksekusi dengan aturan transisi langkah-kecil yang terstruktur oleh sintaksis bahasa, memberikan penjelasan kompositif dan diarahkan sintaksis tentang bagaimana setiap konstruksi melakukan komputasi.

Semantik natural (langkah-besar)

Semantik natural Kahn menghubungkan suatu program secara langsung dengan hasil akhirnya melalui aturan evaluasi, mengabstraksi langkah-langkah perantara dan mempermudah pembuktian tertentu.

Clinical relevance

Semantik operasional merupakan alat standar untuk menentukan perilaku bahasa nyata dan membuktikan kebenaran kompiler dan interpreter. Gaya berbasis aturannya sangat sesuai dengan implementasi dan mendasari metateori bahasa yang diperiksa oleh mesin.

History

Ide-ide operasional muncul dalam definisi bahasa berbasis interpreter awal. Catatan Plotkin tahun 1981 di Aarhus menetapkan semantik operasional struktural sebagai kerangka kerja yang ketat dan diarahkan sintaksis, dan semantik natural Kahn tahun 1987 menawarkan alternatif langkah-besar. Bersama-sama, keduanya menjadi pendekatan dominan untuk mendefinisikan dan melakukan penalaran tentang bahasa pemrograman.

Debates

Formulasi langkah-kecil versus langkah-besar

Para semantisis memilih antara semantik langkah-kecil, yang mengekspos status perantara dan menangani non-terminasi serta konkurensi secara alami, dan semantik langkah-besar, yang ringkas tetapi kurang cocok untuk komputasi yang menyimpang atau saling terkait.

Key figures

• Gordon Plotkin
• Gilles Kahn
• Glynn Winskel
• Matthias Felleisen

Seminal works

• plotkin1981
• kahn1987
• winskel1993

Frequently asked questions

Apa perbedaan antara semantik langkah-kecil dan semantik langkah-besar?

Semantik langkah-kecil menjelaskan langkah-langkah komputasi individual dan status perantara di antaranya, sedangkan semantik langkah-besar menghubungkan suatu program secara langsung dengan nilai akhirnya, menyembunyikan langkah-langkah di antaranya.

Mengapa semantik operasional berguna untuk membuktikan kebenaran (soundness)?

Karena semantik ini membuat langkah-langkah eksekusi menjadi eksplisit, semantik ini berpasangan secara alami dengan metode kemajuan-dan-pemeliharaan (progress-and-preservation), yang melakukan penalaran tentang bagaimana pengetikan dipertahankan saat program mengambil setiap langkah.