<p>In general semantics is a mapping $[\![ {-} ]\!]$ of syntax to mathematical objects of some sort. The objects may be syntactic in nature, in which case it is perhaps better to speak of a <em>translation</em>.</p>

<p>Some kinds of semantics are clearly not syntax. For example, if you interpret the simply typed $\lambda$-calculus into set theory, then it is not reasonable to claim that this is just a translation of one kind of syntax into another. For instance, in the set-theoretic semantics any set may act as a type, even a non-definable one, and even some definable types will have uncountable cardinality (consider $\mathtt{nat} \to \mathtt{nat}$) –– it would be absurd to claim that these are just syntax.</p>

<p>One should not confuse semantics with how we express the semantic function. Of course, <em>anything</em> you express in mathematics is "just a bunch of expressions". But it's been a long time since we learned the difference between a word and its meaning. If you are going to defend the position that "it's all just formalism all the way down" then we have a different issue to discuss, namely: are you a formalist?</p>

CC BY-SA 3.0
2015-03-13T22:52:16.290Z
I don't know whether I'm a formalist. I've seen that paper in a seminar, and it claims that Strachey's Platonism is not philosophically justified. Through your answer one can avoid the problem: Since (IIUC) set theory has a syntax, there is a translation into the syntax of set theory, that can be composed with the semantics of set theory itself to get the semantics you discuss. That's into uncountable sets that are clearly different, at least inside the theory which declares them uncountable. Because the model might be countable, this does not settle the philosophical debate, but that's fine.
Blaisorblade
CC BY-SA 3.0
2015-03-13T23:11:43.317Z
On the philosophical debate, I've grown up with the idea that the debate between formalism and alternatives is not settled.
However, http://plato.stanford.edu/entries/formalism-mathematics/ seems to disagree, and I'll take a look.
Blaisorblade
CC BY-SA 3.0
2015-03-14T07:01:56.740Z
I would put it differently: the set-theoretic semantics of $\lambda$-calculus maps syntax *directly* into sets. To each type corresponds a *set*, not a symbol which denotes a set. But *when you write this on paper* you will use symbols to explain what you mean. The "countable model" problem is irrelevant because it confuses internal and external points of view. *Inside* the model (which is where we are when we give semantics) uncountable sets are uncountable setes, no magic. Stop thinking in terms of "everything is a model" because then you keep switching to a meta-level at the wrong moment.
Andrej Bauer
CC BY-SA 3.0
2015-03-22T19:07:02.693Z
Thanks for clarifying countable models. On the "translation to set theory", I take your answer as "nobody cares about it", so we can ignore it. Is set theory somehow special, or can I also have a type-theoretic semantics mapping simply-typed $\lambda$-calculus into the ambient type theory (say, some suitable variants of MLTT)?
Blaisorblade
CC BY-SA 3.0
2015-03-23T00:40:30.260Z
I do not understand what you are asking. I was giving set theory as an example, and it is definitely not special.
Andrej Bauer
CC BY-SA 3.0
2015-03-23T02:42:37.087Z
Thanks for your patience and sorry for the unclarity. Your answers have been helpful.
Blaisorblade
CC BY-SA 3.0
2015-03-13T17:21:07.380Z
2015-03-13T17:21:07.380Z
Andrej Bauer
<p>I think I understand your difficulties, indeed if you consider just a programming language both a denotational semantics and a term transformation (into another language) are nothing but mappings of syntactic elements of the given language in mathematical objects (elements of a domain in the first case, terms of the language in the second case).</p>

<p>Notheless differences between these two semantics start to arise if you put an operational semantics in your programming language and so you want that the denotational semantics and term transformations are compatible with this operational semantic.</p>

<p>In the first case you would like that denotation of terms/programs that compute the same results have the same denotation, hence the denotational semantics should associates to <em>operational convertible</em> terms the same denotation.</p>

<p>In the second case you would simply like that the term transformation maps terms/programs in such a way to preserve the derivations (if you reguard terms and reduction/derivations respectively as objects and morphisms of a category you can say that a term transformation should be a functor).
In the first case we lost information about the reduction between terms in the second case we preserve it. </p>

<p>In the first case <em>semantically equivalent terms</em> are mapped in the same denotation in the second they are mapped just in <em>operationally equivalent terms</em> but the term translation does not guaratee that equivalent terms are mapped in the same term (and usually that's not the case).</p>

<p>Denotational semantics  allows to <em>easily</em> find different terms, supposing that the denotation-mapping is easily computable, in order to distinguish two programs we just need to compute the denotation an see if they are different values.
Nonetheless in this way we lost information about the reductions (computations of our operational semantics) which are instead preserved by the term transformations. </p>

<p>I hope this helps.</p>

CC BY-SA 3.0
2015-03-12T11:42:57.170Z
2015-03-12T11:42:57.170Z
Giorgio Mossa
<p>There's at least one important difference between a (compositional) term transformation and a semantics — the output of a term transformation is written in the syntax of an object language, the output of a semantics is written in the syntax of the <em>metalanguage</em>. While a metalanguage has a syntax, you needn't deal with that additional complexity any more — the metatheory takes care of that.</p>

<p>Consider for instance proving $f(a) = f(b)$ from $a = b$.</p>

<ul>
<li>In a syntactic framework, to do the corresponding thing (go from $a = b$ to $f(a) = f(b)$) you need to apply (in some form) a substitution lemma to the terms $a$, $b$, $f(x)$. EDIT: Also, you need to pick an appropriate equality (usually observational equivalence, but see <a href="https://cstheory.stackexchange.com/q/30712/989">For what languages is there already a theory of observational equivalence?</a>).</li>
<li>In a semantic framework, you just go from $a = b$ to $f(a) = f(b)$, because $f$ is a "function" and thus takes equals to equals, and because = has been defined appropriately. That's because the metatheory already proved that "functions" satisfy the <em>specification</em> of functions.</li>
</ul>

<p>According to many, the specification of functions is <em>category theory</em>. I'm tempted to conclude: "One can ignore the syntax of the metalanguage because somebody else proved that the metalanguage operations model the axioms of categories" — but I'm ignoring all the subtle issues for languages bigger than simply-typed $\lambda$-calculus, and I'm not sure that's a good idea.</p>

CC BY-SA 3.0
2015-03-06T10:10:33.340Z
2015-03-06T15:11:25.220Z
2017-04-13T12:32:28.053Z
Blaisorblade
<p>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.</p>

<p>In fact, even set theory has a syntax*! So how do we distinguish a denotational semantics from a compositional term transformation?</p>

<p>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 <em>non-standard</em> 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?</p>

<p>This is a concrete confusion which I've observed at least twice:</p>

<ul>
<li>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.</li>
<li><p>"F-ing modules" preempts this confusion — they defend their presentation of the syntax of semantic objects.</p>

<blockquote>
  <p>Semantic signatures. The syntax of semantic signatures is given in Figure 9. (<em>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.</em>) [Emphasis added.]</p>
</blockquote></li>
</ul>

<p>*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 <a href="https://github.com/reflectionalist/DS-PhPL/blob/master/Articles/Raymond-Turner_UnderstandingProgrammingLanguages_2007.pdf" rel="nofollow">Understanding Programming Languages</a>.</p>

CC BY-SA 3.0
2015-03-06T10:42:55.970Z
In case anybody's wondering: I'm aware of the relation with http://cstheory.stackexchange.com/q/21534/989, and convinced this is no duplicate.
Blaisorblade
CC BY-SA 3.0
2015-03-06T13:02:55.607Z
Why is it so important for you to distinguish denotational semantics from a compositional term transformation? The term "denotational semantics" doesn't have a clear-cut boundary, and  it makes sense to say that a compositional term transformation, but maybe not an interesting one?
Martin Berger
CC BY-SA 3.0
2015-03-06T15:17:09.870Z
@MartinBerger: you're right, the question might be a bit pointless for the semantic itself (and we've already been over that). I'll have to clarify. Reasoning on the result of the semantic is a different matter though — see my answer below, and the linked question (http://cstheory.stackexchange.com/q/30712/989).
Blaisorblade
CC BY-SA 3.0
2015-03-06T15:53:08.020Z
I'm still not sure what you mean. If you have a mapping $f$ -- compositional or otherwise, form a language $\cal{L}$ to a language $\cal{L'}$, and you want to reason about a $\cal{L}$-program $P$ by considering $f(P)$, then you need to ensure that $f$ has the right properties so you can 'push back to $\cal{L}$ the insight you've gained about $f(P)$. What conditions on $f$ you'd need to impose depends on the properties you want to transport via $f$ and $f^{-1}$. Not sure that is relevant for your question ...
Martin Berger
CC BY-SA 3.0
2015-03-13T03:55:50.007Z
http://cstheory.stackexchange.com/a/25325/
Kaveh
CC BY-SA 3.0
2015-03-13T17:13:59.117Z
Is there a question here?
Andrej Bauer
CC BY-SA 3.0
2015-03-22T19:07:52.693Z
@AndrejBauer: indeed, the one you're answering.
Blaisorblade
<lo.logic><pl.programming-languages><big-picture>
Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains
Blaisorblade
# Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains

(Asked by: username_0 on 2015-03-06)

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](https://github.com/reflectionalist/DS-PhPL/blob/master/Articles/Raymond-Turner_UnderstandingProgrammingLanguages_2007.pdf).

**Tags:** lo.logic, pl.programming-languages, big-picture
> **Comments:**
> **username_0**: In case anybody's wondering: I'm aware of the relation with http://cstheory.stackexchange.com/q/21534/989, and convinced this is no duplicate.  
> **username_1**: Why is it so important for you to distinguish denotational semantics from a compositional term transformation? The term "denotational semantics" doesn't have a clear-cut boundary, and  it makes sense to say that a compositional term transformation, but maybe not an interesting one?  
> **username_0**: @MartinBerger: you're right, the question might be a bit pointless for the semantic itself (and we've already been over that). I'll have to clarify. Reasoning on the result of the semantic is a different matter though — see my answer below, and the linked question (http://cstheory.stackexchange.com/q/30712/989).  
> **username_1**: I'm still not sure what you mean. If you have a mapping $f$ -- compositional or otherwise, form a language $\cal{L}$ to a language $\cal{L'}$, and you want to reason about a $\cal{L}$-program $P$ by considering $f(P)$, then you need to ensure that $f$ has the right properties so you can 'push back to $\cal{L}$ the insight you've gained about $f(P)$. What conditions on $f$ you'd need to impose depends on the properties you want to transport via $f$ and $f^{-1}$. Not sure that is relevant for your question ...  
> **username_2**: http://cstheory.stackexchange.com/a/25325/  
> **username_3**: Is there a question here?  
> **username_0**: @AndrejBauer: indeed, the one you're answering.  

---

## 3 answers

### Answer by username_3 on 2015-03-13. Score: 2 | Accepted answer

In general semantics is a mapping $[\![ {-} ]\!]$ of syntax to mathematical objects of some sort. The objects may be syntactic in nature, in which case it is perhaps better to speak of a *translation*.

Some kinds of semantics are clearly not syntax. For example, if you interpret the simply typed $\lambda$-calculus into set theory, then it is not reasonable to claim that this is just a translation of one kind of syntax into another. For instance, in the set-theoretic semantics any set may act as a type, even a non-definable one, and even some definable types will have uncountable cardinality (consider $\mathtt{nat} \to \mathtt{nat}$) –– it would be absurd to claim that these are just syntax.

One should not confuse semantics with how we express the semantic function. Of course, *anything* you express in mathematics is "just a bunch of expressions". But it's been a long time since we learned the difference between a word and its meaning. If you are going to defend the position that "it's all just formalism all the way down" then we have a different issue to discuss, namely: are you a formalist?

> **Comments:**
> **username_0**: I don't know whether I'm a formalist. I've seen that paper in a seminar, and it claims that Strachey's Platonism is not philosophically justified. Through your answer one can avoid the problem: Since (IIUC) set theory has a syntax, there is a translation into the syntax of set theory, that can be composed with the semantics of set theory itself to get the semantics you discuss. That's into uncountable sets that are clearly different, at least inside the theory which declares them uncountable. Because the model might be countable, this does not settle the philosophical debate, but that's fine.  
> **username_0**: On the philosophical debate, I've grown up with the idea that the debate between formalism and alternatives is not settled. However, http://plato.stanford.edu/entries/formalism-mathematics/ seems to disagree, and I'll take a look.  
> **username_3**: I would put it differently: the set-theoretic semantics of $\lambda$-calculus maps syntax *directly* into sets. To each type corresponds a *set*, not a symbol which denotes a set. But *when you write this on paper* you will use symbols to explain what you mean. The "countable model" problem is irrelevant because it confuses internal and external points of view. *Inside* the model (which is where we are when we give semantics) uncountable sets are uncountable setes, no magic. Stop thinking in terms of "everything is a model" because then you keep switching to a meta-level at the wrong moment.  
> **username_0**: Thanks for clarifying countable models. On the "translation to set theory", I take your answer as "nobody cares about it", so we can ignore it. Is set theory somehow special, or can I also have a type-theoretic semantics mapping simply-typed $\lambda$-calculus into the ambient type theory (say, some suitable variants of MLTT)?  
> **username_3**: I do not understand what you are asking. I was giving set theory as an example, and it is definitely not special.  
> **username_0**: Thanks for your patience and sorry for the unclarity. Your answers have been helpful.  

---

### Answer by username_4 on 2015-03-12. Score: 3

I think I understand your difficulties, indeed if you consider just a programming language both a denotational semantics and a term transformation (into another language) are nothing but mappings of syntactic elements of the given language in mathematical objects (elements of a domain in the first case, terms of the language in the second case).

Notheless differences between these two semantics start to arise if you put an operational semantics in your programming language and so you want that the denotational semantics and term transformations are compatible with this operational semantic.

In the first case you would like that denotation of terms/programs that compute the same results have the same denotation, hence the denotational semantics should associates to *operational convertible* terms the same denotation.

In the second case you would simply like that the term transformation maps terms/programs in such a way to preserve the derivations (if you reguard terms and reduction/derivations respectively as objects and morphisms of a category you can say that a term transformation should be a functor).
In the first case we lost information about the reduction between terms in the second case we preserve it.

In the first case *semantically equivalent terms* are mapped in the same denotation in the second they are mapped just in *operationally equivalent terms* but the term translation does not guaratee that equivalent terms are mapped in the same term (and usually that's not the case).

Denotational semantics allows to *easily* find different terms, supposing that the denotation-mapping is easily computable, in order to distinguish two programs we just need to compute the denotation an see if they are different values.
Nonetheless in this way we lost information about the reductions (computations of our operational semantics) which are instead preserved by the term transformations.

I hope this helps.


---

### Answer by username_0 on 2015-03-06. Score: -1

There's at least one important difference between a (compositional) term transformation and a semantics — the output of a term transformation is written in the syntax of an object language, the output of a semantics is written in the syntax of the *metalanguage*. While a metalanguage has a syntax, you needn't deal with that additional complexity any more — the metatheory takes care of that.

Consider for instance proving $f(a) = f(b)$ from $a = b$.

* In a syntactic framework, to do the corresponding thing (go from $a = b$ to $f(a) = f(b)$) you need to apply (in some form) a substitution lemma to the terms $a$, $b$, $f(x)$. EDIT: Also, you need to pick an appropriate equality (usually observational equivalence, but see [For what languages is there already a theory of observational equivalence?](https://cstheory.stackexchange.com/q/30712/989)).
* In a semantic framework, you just go from $a = b$ to $f(a) = f(b)$, because $f$ is a "function" and thus takes equals to equals, and because = has been defined appropriately. That's because the metatheory already proved that "functions" satisfy the *specification* of functions.

According to many, the specification of functions is *category theory*. I'm tempted to conclude: "One can ignore the syntax of the metalanguage because somebody else proved that the metalanguage operations model the axioms of categories" — but I'm ignoring all the subtle issues for languages bigger than simply-typed $\lambda$-calculus, and I'm not sure that's a good idea.


---

