Consider a denotational semantics from simply-typed $\lambda$-calculus into dependent type theory. Is that actually a (trivial) term transformation into that dependent type theory? After all, type theory has a syntax.
In fact, even set theory has a syntax*! So how do we distinguish a denotational semantics from a compositional term transformation?
Now, let's generalize to less trivial program transformations — say, transformation to continuation-passing style (or store-passing style, environment passing style, ...). You can show the same idea through a non-standard semantics (here, a continuation-passing semantics) or a term transformation into a continuation-passing term, and they're distinguished by a binding-time shift. Again, isn't the non-standard semantics also a term transformation?
This is a concrete confusion which I've observed at least twice:
- In my work (on incremental computation) I've used a non-standard denotational semantics into type theory (a "change-passing" semantics). After a presentation of that, Gabriel Scherer remarked (kindly) that for him, that was a term transformation into a dependently typed language.
"F-ing modules" preempts this confusion — they defend their presentation of the syntax of semantic objects.
Semantic signatures. The syntax of semantic signatures is given in Figure 9. (And no, this is not an oxymoron, for in our setting the “semantic objects” we are using to model modules are merely pieces of Fω syntax.) [Emphasis added.]
*Apparently, some (non-formalists) claim that set theory is not "just syntax", but something ontologically different. I'll ignore this subtle philosophical issue; the only reference I know on it is Raymond Turner's Understanding Programming Languages.