Tidak mungkin untuk automata terikat linier untuk memeriksa apakah program C ++, dan tidak mungkin untuk dan LBA untuk memeriksa apakah program SML diketik dengan baik. C ++ memiliki sistem tipe Turing-complete, karena Anda dapat mengkode program yang sewenang-wenang sebagai metaprogram templat.
SML lebih menarik. Itu memang memiliki pengecekan tipe decidable, tetapi masalahnya adalah EXPTIME-complete. Oleh karena itu tidak mungkin LBA dapat memeriksanya, kecuali ada keruntuhan yang sangat mengejutkan dalam hierarki kompleksitas. Alasan untuk ini adalah bahwa SML memerlukan inferensi tipe, dan ada keluarga program yang ukurannya tumbuh jauh lebih cepat daripada ukuran program. Sebagai contoh, pertimbangkan program berikut:
fun delta x = (x, x) (* this has type 'a -> ('a * 'a), so its return value
has a type double the size of its argument *)
fun f1 x = delta (delta x) (* Now we use functions to iterate this process *)
fun f2 x = f1 (f1 x)
fun f3 x = f2 (f2 x) (* This function has a HUGE type *)
Untuk sistem tipe yang lebih sederhana, seperti C atau Pascal, saya percaya dimungkinkan bagi LBA untuk memeriksanya.
Pada hari-hari awal penelitian bahasa pemrograman, orang kadang-kadang menggunakan tata bahasa van Wingaarden (alias tata bahasa dua tingkat) untuk menentukan sistem tipe untuk bahasa pemrograman. Saya percaya Algol 68 ditentukan dengan cara ini. Namun, saya diberitahu bahwa teknik ini ditinggalkan karena alasan pragmatis: ternyata cukup sulit bagi orang untuk menulis tata bahasa yang menentukan apa yang mereka pikir mereka tentukan! (Biasanya, tata bahasa yang ditulis orang menghasilkan bahasa yang lebih besar dari yang dimaksudkan.)
Saat ini orang menggunakan aturan inferensi skematik untuk menentukan sistem tipe, yang pada dasarnya merupakan cara menetapkan predikat sebagai titik paling tidak tetap dari koleksi klausa Horn. Kepuasan untuk teori Horn orde pertama tidak dapat diputuskan secara umum, jadi jika Anda ingin menangkap semua yang dilakukan oleh tipe teori, maka formalisme gramatikal apa pun yang Anda pilih akan lebih kuat daripada yang benar-benar nyaman.
Saya tahu ada beberapa pekerjaan menggunakan tata bahasa atribut untuk mengimplementasikan sistem tipe. Mereka mengklaim ada beberapa manfaat rekayasa perangkat lunak untuk pilihan ini: yaitu, tata bahasa atribut mengontrol aliran informasi dengan sangat ketat, dan saya diberitahu ini membuat pemahaman program lebih mudah.
