1) Jaki, jeśli w ogóle, jest związek między pisaniem statycznym a gramatyką formalną?
2) Czy w szczególności byłoby możliwe, aby automat z ograniczeniem liniowym sprawdził, czy, powiedzmy, program C ++ lub SML był dobrze napisany? Automat zagnieżdżonego stosu?
3) Czy istnieje naturalny sposób na wyrażenie zasad pisania statycznego w formalnych terminach gramatycznych?
Odpowiedzi:
Automaty z ograniczeniami liniowymi nie są w stanie sprawdzić, czy programy w C ++ są mało prawdopodobne, a LBA sprawdzić, czy programy SML są dobrze napisane. C ++ ma system typu Turing-complete, ponieważ można kodować dowolne programy jako metaprogramy szablonów.
SML jest bardziej interesujący. Ma sprawdzalne sprawdzanie typu, ale problem jest zakończony WYŁĄCZNIE. Dlatego jest mało prawdopodobne, że LBA może to sprawdzić, chyba że nastąpi bardzo zaskakujące załamanie w hierarchii złożoności. Powodem tego jest to, że SML wymaga wnioskowania o typie, a istnieją rodziny programów, których rozmiar rośnie znacznie szybciej niż rozmiar programu. Jako przykład rozważmy następujący program:
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 *)
W przypadku systemów prostszych typów, takich jak C lub Pascal, uważam, że LBA może to sprawdzić.
Na początku badań nad językami programowania ludzie czasami używali gramatyki van Wingaarden ( zwanej także gramatyką dwupoziomową) do określania systemów typów dla języków programowania. Uważam, że Algol 68 został określony w ten sposób. Jednak powiedziano mi, że technika ta została porzucona z zasadniczo pragmatycznych powodów: okazało się, że pisanie gramatyk określających to, co według nich było trudne, okazało się dość trudne! (Zazwyczaj gramatyki, które napisali ludzie, generowały większe języki niż zamierzały).
W dzisiejszych czasach ludzie używają schematów wnioskowania w celu określenia systemów typów, co jest w zasadzie sposobem określania predykatów jako najmniej ustalonego punktu zbioru klauzul Horn. Satysfakcja z teorii Horn pierwszego rzędu jest ogólnie nierozstrzygalna, więc jeśli chcesz uchwycić wszystko, co robią teoretycy typu, to każdy formalizm gramatyczny, który wybierzesz, będzie silniejszy niż jest to naprawdę wygodne.
Wiem, że było trochę pracy nad wykorzystaniem gramatyki atrybutów do wdrożenia systemów typów. Twierdzą, że ten wybór ma pewne zalety inżynierii oprogramowania: mianowicie, gramatyka atrybutów kontroluje przepływ informacji bardzo ściśle, i powiedziano mi, że ułatwia to zrozumienie programu.
O ile mi wiadomo, poprawność typów jest zwykle nierozstrzygalna w interesujących przypadkach, więc gramatyki formalne nie są w stanie uchwycić każdego systemu typów, o którym myślisz.
Wiem, że główne generatory kompilatorów pozwalają na dowolne predykaty reguł, które uniemożliwiają wykonanie reguły, jeśli predykat nie oceni truenp
{ type(e1) == type(e2) } (expression e1) '+' (expression e2). Pojęcie to można łatwo sformalizować; odpowiednie ograniczenia dozwolonych predykatów mogą następnie dać rozstrzygalność przez LBA.