3
$\begingroup$

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.

|cite|improve this question
$\endgroup$
  • $\begingroup$ In case anybody's wondering: I'm aware of the relation with cstheory.stackexchange.com/q/21534/989, and convinced this is no duplicate. $\endgroup$ – Blaisorblade Mar 6 '15 at 10:42
  • 4
    $\begingroup$ 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? $\endgroup$ – Martin Berger Mar 6 '15 at 13:02
  • $\begingroup$ @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 (cstheory.stackexchange.com/q/30712/989). $\endgroup$ – Blaisorblade Mar 6 '15 at 15:17
  • 1
    $\begingroup$ 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 ... $\endgroup$ – Martin Berger Mar 6 '15 at 15:53
  • $\begingroup$ cstheory.stackexchange.com/a/25325 $\endgroup$ – Kaveh Mar 13 '15 at 3:55
2
$\begingroup$

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?

|cite|improve this answer
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Blaisorblade Mar 13 '15 at 22:52
  • $\begingroup$ On the philosophical debate, I've grown up with the idea that the debate between formalism and alternatives is not settled. However, plato.stanford.edu/entries/formalism-mathematics seems to disagree, and I'll take a look. $\endgroup$ – Blaisorblade Mar 13 '15 at 23:11
  • 2
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Mar 14 '15 at 7:01
  • $\begingroup$ 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)? $\endgroup$ – Blaisorblade Mar 22 '15 at 19:07
  • 1
    $\begingroup$ I do not understand what you are asking. I was giving set theory as an example, and it is definitely not special. $\endgroup$ – Andrej Bauer Mar 23 '15 at 0:40
3
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
-1
$\begingroup$

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?).
  • 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.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.