Definisi tepat dari kategori sintaksis / domain sintaksis dalam sintaksis abstrak

Saya telah membaca bagian pengantar dari beberapa buku tentang semantik bahasa pemrograman (Gordon, Winskel, Nielson & Nielson, Allison, Stump, Schmidt), dan sementara saya mengerti apa yang dimaksud dengan kategori sintaksis , atau domain sintaksis , saya tidak t menemukan definisi yang tegas dan langsung dari mereka. Apakah ada definisi standar, mungkin di karya sebelumnya?

Kebanyakan orang menghindari memberikan deskripsi yang tepat tentang apa kategori sintaksis, karena jika Anda melakukannya dengan benar dengan semua detail, rasio wawasan terhadap kecanggihan matematika yang diperlukan berakhir menjadi sangat, sangat rendah. Buku John Reynolds ' Theories of Programming Languages memiliki salah satu penjelasan yang lebih komprehensif dalam bab 1, seperti yang dilakukan oleh Robert Harper, Yayasan Praktis Bahasa Pemrograman .

Intuisi yang harus Anda miliki adalah bahwa kategori sintaksis adalah kumpulan pohon yang dihasilkan oleh tata bahasa bebas konteks. Dengan definisi seperti itu untuk satu set pohon, Anda dapat mendefinisikan fungsi-fungsi pada set ini menggunakan rekursi struktural , dan membuktikan sifat-sifatnya menggunakan induksi struktural : yaitu, dengan menganalisis semua cara yang berbeda tentang sebuah pohon yang dapat dibangun.

Misalnya, anggaplah kita memiliki bahasa operasi aritmatika yang diberikan oleh tata bahasa berikut:

e ::= zero | succ(e)| add(e, e)

Kemudian, kita dapat mendefinisikan fungsi interpretasi evalyang mengambil istilah dan memberi Anda bilangan bulat, berdasarkan kasus pada cara kita dapat membangun istilah:

eval : Expr -> Int
eval zero     = 0
eval succ(e)  = 1 + eval e  
eval add(e, e') = eval e + eval e'*

Perhatikan bahwa kita telah mendefinisikan fungsi ini sepenuhnya dengan memberikan satu klausa untuk setiap cara yang mungkin kita dapat menghasilkan ekspresi dari tata bahasa. Fakta bahwa ini adalah definisi lengkap dari suatu fungsi disebut prinsip rekursi struktural .

Kami juga dapat membuktikan properti tentang fungsi ini dengan menggunakan induksi struktural - dengan melakukan analisis induktif untuk setiap kasus. Sebagai contoh, kita dapat membuktikan bahwa untuk setiap e, eval e ≥ 0.

Proof. By structural induction on e.
- Case e = zero:
  By the definition of eval, eval zero = 0. 
  We know 0 ≥ 0 by reflexivity of ≥.    

- Case e = succ(e'):     
  By induction, we know that eval e' ≥ 0 
  So we also know that 1 + eval e' ≥ eval e'.
  By transitivity, 1 + eval e' ≥ 0. 
  But eval succ(e') = 1 + eval e'.
  So eval succ(e') ≥ 0.

- Case e = add(e', e'').
  By induction, we know that eval e' ≥ 0.
  By induction, we know that eval e'' ≥ 0.
  By properties of addition, we know that eval e' + eval e'' ≥ 0.
  By the definition of eval, eval add(e',e'') = eval e' + eval e''.
  So eval add(e',e'') ≥ 0.

Fakta bahwa mempertimbangkan kasus-kasus bagaimana ekspresi dapat dibentuk merupakan bukti disebut prinsip induksi struktural .

Sekarang, fakta bahwa seseorang dapat mendefinisikan fungsi dengan rekursi struktural dan membuktikan sifat dengan induksi struktural untuk tata bahasa apa pun . Namun, untuk membuktikan hal ini dengan ketat membutuhkan sejumlah teori kategori; Anda perlu memformalkan kategori sintaksis sebagai aljabar awal dari kelas fungsi tertentu, dan kemudian membuktikan bahwa aljabar awal seperti itu selalu ada untuk kelas itu.

Ini adalah alat kelas berat untuk membuktikan hasil yang "jelas", dan jadi saya sarankan hanya memercayai intuisi Anda tentang bagaimana definisi struktural bekerja, dan kemudian hanya mengganggu dengan semantik terperinci mereka jika Anda memutuskan untuk menjadi ahli logika profesional.

Saya juga tidak pernah menemukan definisi eksplisit, tetapi saya telah menyimpulkannya.

Seperti yang saya mengerti, Anda membagi bahasa menjadi domain sintaksis; dengan tambahan bahwa domain sintaksis harus sepenuhnya dihasilkan oleh simbol tunggal yang berbeda, ketika Anda menuliskan tata bahasa. Jadi domain sintaksis adalah bagian dari bahasa Anda, dan setiap domain dihasilkan oleh satu simbol tunggal.

$x$

${\mathbb Z}$${\mathbb B}=\{T,F\}$

Anda bisa mengatakan semua ekspresi Anda adalah satu domain sintaksis,

• ${\mathbb Z} \cup {\mathbb B}$

atau Anda dapat memutuskan untuk membaginya:

• ${\mathbb B}$
• ${\mathbb Z}$

Jadi, sejauh yang saya mengerti domain sintaksis yang tepat untuk digunakan adalah masalah desain (maksud saya keputusan yang Anda buat saat mendesain sintaksis abstrak untuk bahasa Anda). Tetapi mereka pasti himpunan bagian dari bahasa Anda, dan setiap domain sintaksis harus dihasilkan oleh simbol yang berbeda.