Czy potrafimy rozróżnić metody ściśle składniowe i semantyczne w języku programowania?

Chociaż dyskusje dowodzą silnych dowodów na normalizację, komentarz ten kontrastuje „model form normalnych” z „metodami czysto składniowymi”.

To sprowadza mnie z powrotem do bardziej podstawowego pytania: czy nadal możemy dokładnie rozróżniać konstrukcje składniowe i semantyczne w obliczu modeli opartych na składni? Co z modelami terminów dla algeb, modelami Henkina dla logiki pierwszego rzędu? Co z strukturalną semantyką operacyjną? Ponieważ modele terminów mogą być od izomorficzne do składni, trudno jest wprowadzić wyraźne rozróżnienie.

Dopóki nie przestudiowałem różnicy między teorią dowodów a teorią modeli w logice, byłem nawet zdumiony pomysłem, że „statyczne systemy typu są metodą składniową”. W końcu system typów uzasadnia typy, które są abstrakcją zachowania programu (a z typami zależnymi - arbitralnie precyzyjnymi).

Nie, nie można ściśle odróżnić metod składniowych od metod semantycznych, ale rozróżnienie wciąż ma sens.

• Strukturalna semantyka operacyjna nie jest denotacyjna, ponieważ nie jest to kompozycyjna metoda nadawania semantyce języka programowania.

• Można jednak budować modele denotacyjne ze strukturalnej semantyki operacyjnej za pomocą metody wykonalności lub relacji logicznych. Jako przykład zobacz Robert Harper's Constructing Type Systems over Operational Semantics .

• $\lambda$

• Z drugiej strony, jeśli masz semantykę denotacyjną, możesz dowiedzieć się, jaka jest jej składnia. Następnie chcesz znaleźć maszynę składni i abstrakcję, której termin model może służyć jako obiekt początkowy w odpowiedniej kategorii modeli.

  Na przykład semantyka gier zaczęła swoje życie jako konstrukcja czysto semantyczna i ostatecznie doprowadziła do pracy nad semantyką gier operacyjnych - najnowszym przykładem jest rachunek lambda lambda-bar Alexisa Goyeta : Rachunek podwójny dla strategii nieograniczonych .

• Ogólnie rzecz biorąc, można myśleć o strukturalnej semantyce operacyjnej jako sposobie określania abstrakcyjnych maszyn, które, mamy nadzieję, są łatwe do wdrożenia. Semantyka denotacyjna daje model kompozycyjny języka, który, mamy nadzieję, jest łatwy do uzasadnienia. Jeśli mamy jedno i drugie, możemy zarówno wdrożyć, jak i uzasadnić język.

• Twierdzenia o normalizacji są interesującym niejednoznacznym przypadkiem. Zwykle, aby udowodnić normalizację, potrzebny jest model semantyczny (zwykle relacja logiczna). Jednak gdy już wiadomo, że normalizacja się utrzymuje, wiele właściwości można teraz udowodnić przez indukcję w postaciach normalnych, co jest argumentem czysto syntaktycznym.

  W przypadku słabej logiki (w przybliżeniu do logiki pierwszego rzędu bez indukcji, z grubsza), możesz udowodnić normalizację składniowo, stosując technikę dziedzicznej substytucji . W tych logikach zachowuje się właściwość podformuły, dzięki czemu można udowodnić normalizację przez indukcję typów. Zobacz artykuł Franka Pfenninga Structural Cut Elimination, aby uzyskać wyjaśnienie, jak to działa.