Можем ли мы различать строго синтаксические и семантические методы в языке программирования?

При обсуждении строгих доказательств нормализации этот комментарий противопоставляет «модель нормальных форм» «чисто синтаксическим методам».

Это возвращает меня к более основному вопросу: можем ли мы по-прежнему строго различать синтаксические и семантические конструкции перед лицом моделей, основанных на синтаксисе? А как насчет терминов для алгебр, моделей Хенкина для логик первого порядка? Как насчет структурной операционной семантики? Поскольку термины модели могут быть изоморфны синтаксису, кажется, трудно провести четкое различие.

Пока я не изучил различие между теорией доказательств и теорией моделей в логике, я даже был озадачен идеей, что «системы статического типа являются синтаксическим методом». В конце концов, система типов рассуждает о типах, которые являются абстракцией поведения программы (а с зависимыми типами - произвольно точными).

Нет, вы не можете строго отличать синтаксические от семантических методов, но это различие все же имеет смысл.

• Структурная операционная семантика не является денотационной, потому что это не композиционный метод предоставления семантики языку программирования.

• Однако вы можете построить денотационные модели из структурной операционной семантики с помощью метода реализуемости или логических отношений. В качестве примера см. Построение систем типа Роберта Харпера над операционной семантикой .

• $\lambda$ для некоторых деталей.)

• В другом направлении, если у вас есть денотационная семантика, вы можете выяснить, каков ее синтаксис. Затем вы захотите найти синтаксис и абстрактную машину, термин модели которой может служить начальным объектом в подходящей категории моделей.

  Например, игровая семантика начала свою жизнь как чисто семантическая конструкция и в конечном итоге привела к работе над операционной семантикой игры, недавним примером которой является Алексис Гойе « Лямбда-лямбда-исчисление: двойное исчисление для неограниченных стратегий» .

• В целом, вы можете рассматривать структурную операционную семантику как способ задания абстрактных машин, которые, как мы надеемся, легко реализовать. Денотационная семантика дает композиционную модель языка, о которой, мы надеемся, легко рассуждать. Если у нас есть и то и другое, то мы можем и реализовать, и рассуждать о языке.

• Теоремы о нормализации представляют собой интересный неоднозначный случай. Обычно, чтобы доказать нормализацию, вам нужна семантическая модель (обычно логическое отношение). Однако, как только вы узнаете, что нормализация справедлива, многие свойства теперь могут быть доказаны индукцией по нормальным формам, что является чисто синтаксическим аргументом.

  Для слабых логик (что угодно, вплоть до логики первого порядка без индукции, примерно), вы можете доказать синтаксическую нормализацию, используя технику наследственного замещения . В этих логиках свойство subformula выполнено, и вы можете доказать нормализацию по типам. См. Статью Фрэнка Пфеннинга « Устранение структурного разреза» для объяснения того, как это работает.