Perbedaan Antara Semantik Operasional Kecil dan Besar

Apa perbedaan mendasar antara semantik operasional kecil dan besar?

Saya mengalami kesulitan memahami apa itu dan motivasi untuk memiliki keduanya.

Semantik langkah kecil mendefinisikan metode untuk mengevaluasi ekspresi satu langkah perhitungan pada satu waktu. Secara formal, semantik langkah kecil untuk bahasa ekspresi $E$ adalah relasi $\rightarrow : E \times E$ disebut relasi reduksi . Semantik langkah kecil menjelaskan apa yang terjadi pada ekspresi secara detail. Itu dapat memberikan akun yang tepat bahkan program non-terminasi, dengan rantai tak terbatas $e_0 \to e_1 \to e_2 \to \dots$ . Program terminating adalah program sedemikian rupa sehingga $e_0 \to e_1 \to \dots \to v$ $v$$\forall e' \in E, v \not\rightarrow e'$$\newcommand{\llbracket}{[\![} \newcommand{\rrbracket}{]\!]}$

Di ujung lain dari spektrum adalah semantik denotasional . Semantik denotasi memberikan "makna" untuk setiap ungkapan. Ini adalah fungsi dari ekspresi ke denotasi: ( disebut domain). Ruang denotasi dapat sepenuhnya tidak terkait dengan ruang sintaksis, misalnya dapat berupa ekspresi yang dievaluasi ke suatu angka dan dapat berupa sekumpulan angka seperti atau .$\llbracket \cdot \rrbracket : E \to D$$D$$E$$D$$\mathbb{N}$$\mathbb{R}$

Semantik langkah besar adalah jenis di tengah. Sebuah semantik besar-langkah pada bahasa ekspresi dan seperangkat nilai adalah hubungan . Ini mengaitkan ekspresi dengan nilainya (kemungkinan beberapa nilai jika bahasanya tidak deterministik). Seringkali, nilai khusus digunakan untuk ekspresi non-terminating.$E$$V$$\Downarrow : E \times V$$\bot$

Jadi mengapa kita memiliki ketiga konsep ini? Semua gagasan ini dapat saling memodelkan satu sama lain, tetapi model tersebut menambah tingkat kerumitan.

• Diberikan semantik langkah-kecil , Anda dapat menentukan semantik langkah-besar yang sesuai yang menghubungkan setiap ekspresi dengan nilainya (atau nilainya, jika reduksi tidak deterministik): jika jika ada rantai dan tidak dapat mengurangi lebih jauh. Perhatikan bahwa secara umum Anda tidak dapat merekonstruksi semantik langkah kecil dari semantik langkah besar. Misalnya, semua ekspresi non-terminating tidak dapat dibedakan di bawah semantik langkah besar.$\to$$e \Downarrow v$$e \to e_1 \to \dots \to v$$v$
• Mengingat besar-langkah semantik , Anda dapat mengatakan bahwa itu kecil-langkah semantik pada . Ini tidak terlalu berguna.$\Downarrow : E \times V$$E \cup V$
• Diberikan semantik langkah-kecil , Anda dapat menentukan semantik denotasi yang sesuai di mana denotasi ekspresi adalah himpunan rantai reduksi mulai dari itu. Ini memenuhi definisi formal, tetapi itu tidak terlalu berguna, karena menambahkan overhead teori set ke objek yang lebih mudah untuk dipikirkan dengan melihat langsung pada sintaks.$\to$
• Diberikan semantik denotasi , Anda dapat mendefinisikan semantik langkah kecil dengan menambahkan semua kemungkinan denotasi sebagai nilai dalam bahasa. Itu membutuhkan penciptaan nilai-nilai yang bukan bagian dari sintaks yang dapat ditulis oleh programmer, yang berarti bahwa beberapa hasil yang menarik harus menyatakan "untuk semua program yang dapat ditulis oleh programmer" daripada "untuk semua program". Yang ini juga sangat tidak berguna.$\llbracket \cdot \rrbracket$
• Diberikan semantik langkah besar , Anda dapat menentukan semantik denotasi terkait di mana domain adalah sekumpulan nilai: . Jika semantik langkah besar bersifat deterministik (setiap ekspresi dikurangi menjadi satu nilai), Anda dapat menentukan semantik denotasi sederhana di mana domain adalah himpunan nilai.$\Downarrow$$\llbracket e \rrbracket = \{v \mid e \Downarrow v\}$
• Sebaliknya, dengan semantik denotasional , Anda dapat menentukan semantik langkah besar . Sekali lagi yang ini tidak ada gunanya.$\llbracket \cdot \rrbracket$$E \Downarrow \llbracket \cdot \rrbracket$

Secara operasional, semantik langkah kecil sesuai dengan melihat setiap operasi yang dilakukan oleh penerjemah untuk bahasa tersebut. Semantik langkah besar hanya melihat nilai yang dihasilkan. Semantik denotasional melihat pada interpretasi matematis yang mungkin atau mungkin tidak ada hubungannya dengan apa yang terjadi pada komputer.

Semantik langkah kecil adalah yang paling jelas. Ini jelas memberikan informasi yang berguna tentang program yang tidak berakhir. Secara umum, ini memberikan informasi terperinci tentang perilaku program.

Semantik denotasional mengubah konstruksi sintaksis menjadi objek matematika yang arbitrer; ia dapat mengekspresikan apa pun yang diinginkan para ilmuwan (Anda dapat mendefinisikan denotasi ekspresi sebagai semua rantai reduksi yang mungkin darinya), tetapi dengan biaya menambahkan tingkat kerumitan. Ini digunakan ketika kita ingin memisahkan beberapa detail seperti bagaimana tepatnya ekspresi dievaluasi.

Semantik langkah besar ada di tengah: ia mengabstraksi rincian evaluasi tetapi mempertahankan sifat sintaksis hasilnya. Biasanya konsep ini digunakan ketika ada semantik langkah kecil yang mendasarinya, sebagai cara untuk mengekspresikan secara ringkas “ ”sebagai“ ”. Dalam konstruksi seperti itu, sementara konsepnya sangat berbeda (satu memungkinkan kita untuk berbicara tentang langkah-langkah perhitungan individu dan tentang program non-terminating, yang lain tidak), definisi akan terlihat sangat mirip, karena dalam kasus ini aturan yang menentukan semantik langkah besar pada dasarnya berbentuk “if dan… dan dan$\exists (e_1, \dots, e_n), e \to e_1 \to \dots e_n \text{ and } \not\exists e', e_n \to e'$$e \Downarrow e_n$$e_1 \to^* e_2$$e_n \to^* v$$v$adalah nilai maka ”.$e_1 \Downarrow v$