Can we distinguish strictly syntactic and semantic methods in programming language?

Question

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods".

This brings me back to a more basic question: can we still distinguish syntactic and semantic constructions strictly, in the face of syntax-based models? What about term models for algebras, Henkin models for first-order logics? What about structural operational semantics? Since term models can be isomorphic to syntax, it seems hard to make a firm distinction.

Until I studied the difference between proof theory and model theory in logic, I was even baffled by the idea that "static type systems are a syntactic method". After all, a type system reasons about types, which are an abstraction of program behavior (and with dependent types, an arbitrarily precise one).

Answer 1

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense.

• Structural operational semantics is not denotational, because it is not a compositional method of giving semantics to a programming language.

• However, you can build denotational models out of a structural operational semantics by using a realizability or logical relations method. As an example, see Robert Harper's Constructing Type Systems over Operational Semantics.

• Term models are denotational, but generally semanticists are not satisfied with them. What they usually want is a category of models in which the term model is initial, which can be used to prove soundness and completeness results. (The soundness and completeness of the typed lambda calculus for cartesian closed categories is the paradigmatic example; see Alex Simpson's Categorical Completeness Results for the Simply-Typed $\lambda$-calculus for some details.)

• In the other direction, if you have a denotational semantics, you might want to figure out what the syntax for it is. Then you want to go and find a syntax and abstract machine whose term model can serve as an intitial object in a suitable category of models.

  For instance, game semantics began its life as a purely semantic construction, and eventually led to work on operational game semantics --- a recent example of which is Alexis Goyet's The lambda lambda-bar calculus: A dual calculus for unconstrained strategies.

• Overall, you can think of structural operational semantics as a way of specifying abstract machines, which we hope are easy to implement. A denotational semantics gives a compositional model of a language, which we hope is easy to reason about. If we have both, then we can both implement and reason about the language.

• Normalization theorems are an interesting ambiguous case. Usually, to prove normalization, you need a semantic model (typically a logical relation). However, once you know that normalization holds, many properties can now be proved by induction on normal forms, which is a purely syntactic argument.

  For weak logics (anything up to first-order logic without induction, roughly), you can prove normalization syntactically, using the technique of hereditary substitution. In these logics, the subformula property holds, and so you can prove normalization by induction on types. See Frank Pfenning's paper Structural Cut Elimination for an explanation of how this works.