Bisakah kita membedakan metode sintaksis dan semantik dalam bahasa pemrograman?

Sementara diskusi menjadi bukti normalisasi yang kuat, komentar ini kontras dengan "model bentuk normal" dengan "metode sintaksis murni".

Ini membawa saya kembali ke pertanyaan yang lebih mendasar: dapatkah kita membedakan konstruksi sintaksis dan semantik secara ketat, di hadapan model berbasis sintaksis? Bagaimana dengan model istilah untuk aljabar, model Henkin untuk logika orde pertama? Bagaimana dengan semantik operasional struktural? Karena model jangka dapat isomorfis terhadap sintaksis, tampaknya sulit untuk membuat perbedaan tegas.

Sampai saya mempelajari perbedaan antara teori bukti dan teori model dalam logika, saya bahkan bingung oleh gagasan bahwa "sistem tipe statis adalah metode sintaksis". Lagi pula, sistem tipe beralasan tentang tipe, yang merupakan abstraksi dari perilaku program (dan dengan tipe dependen, yang tepat secara sewenang-wenang).

Tidak, Anda tidak dapat secara ketat membedakan sintaksis dari metode semantik, tetapi perbedaannya tetap masuk akal.

• Semantik operasional struktural bukan denotasional, karena itu bukan metode komposisi memberikan semantik ke bahasa pemrograman.

• Namun, Anda dapat membangun model denotasional dari semantik operasional struktural dengan menggunakan metode realisasi atau hubungan logis. Sebagai contoh, lihat Sistem Tipe Membangun Robert Harper atas Semantik Operasional .

• Model jangka adalah denotasional, tetapi umumnya para semantikis tidak puas dengan mereka. Apa yang biasanya mereka inginkan adalah kategori model di mana istilah model awal, yang dapat digunakan untuk membuktikan hasil kesehatan dan kelengkapan. (Tingkat kesehatan dan kelengkapan kalkulus lambda yang diketik untuk kategori tertutup kartesian adalah contoh paradigmatik; lihat Hasil Kelengkapan Kategorikal$\lambda$ Alex Simpson untuk λ -kalkulasi Cukup Ketik untuk beberapa detail.)

• Di arah lain, jika Anda memiliki semantik denotasional, Anda mungkin ingin mencari tahu apa sintaksisnya. Kemudian Anda ingin pergi dan menemukan mesin sintaks dan abstrak yang model jangkanya dapat berfungsi sebagai objek awal dalam kategori model yang sesuai.

  Sebagai contoh, semantik gim memulai kehidupannya sebagai konstruksi semantik murni, dan pada akhirnya mengarah ke mengerjakan semantik gim operasional --- sebuah contoh baru-baru ini yang merupakan kalkulus lambda-bar Alexis Goyet : Kalkulus lambda-bar lambda: Kalkulus ganda untuk strategi yang tidak dibatasi .

• Secara keseluruhan, Anda dapat menganggap semantik operasional struktural sebagai cara menentukan mesin abstrak, yang kami harap mudah diimplementasikan. Semantik denotasional memberikan model komposisi bahasa, yang kami harap mudah untuk dipikirkan. Jika kita memiliki keduanya, maka kita dapat mengimplementasikan dan alasan tentang bahasa.

• Teorisasi normalisasi adalah kasus ambigu yang menarik. Biasanya, untuk membuktikan normalisasi, Anda memerlukan model semantik (biasanya hubungan logis). Namun, begitu Anda tahu bahwa normalisasi berlaku, banyak properti sekarang dapat dibuktikan dengan induksi pada bentuk normal, yang merupakan argumen sintaksis murni.

  Untuk logika yang lemah (apa pun hingga logika tingkat pertama tanpa induksi, secara kasar), Anda dapat membuktikan normalisasi secara sintaksis, menggunakan teknik substitusi herediter . Dalam logika ini, properti subformula berlaku, dan Anda dapat membuktikan normalisasi dengan induksi pada jenis. Lihat makalah Frank Pfenning, Structural Cut Elimination untuk penjelasan tentang cara kerjanya.