# Do the following concepts belong to syntax or semantics?

I am not very sure about the difference between syntax and semantics.

Does each of the following concepts belong to syntax or semantics?

• terms
• values: terms that are possible ﬁnal results of evaluation.
• types
• (typing) context
• evaluation (rules)
• typing (relation)?

Here are two examples from Types and Programming Languages by Pierce.

For example, I thought evaluation (rules) belongs to operational semantics, so values should also belong to operational semantics, by the definition of values. Why does the book list "values" under "Syntax"?

• Do not post pictures of formulas, please. – Andrej Bauer Sep 2 '19 at 5:57
• Sorry, I don't know how to reproduce the two figures, and I think It is better to have them than not at all. – Tim Sep 2 '19 at 12:00

It's not really a good idea to try to divide everything in PL into "syntax" and "semantics". Often we mix things. Nevertheless, as for your question, we normally divide things up like this:

• terms, values and types are syntactic entities, as each of them is described by grammatical rules, so these are syntax
• a typing context is syntax in simple cases, when we can describe contexts using grammatical rules
• the typing relation is considered to be part of static semantics, i.e., the typing relation is determined by the structure of the terms (as opposed to their operational behavior),
• the evaluation relation is part of dynamic semantics, i.e., the evaluation rules explain the operational (dynamic) behavior of terms.

You did not mention denotational semantics, which gives mathematical meaning to terms and types. It is considered to be a separate thing of its own.

• Thanks. (1) values are special terms which are the final results of evaluating other terms. Which term is a vealue depends on evaluation rules, so I guess value belongs to semantics, just as evaluation rule does. Or am I wrong? (2) How do you "describe typing contexts using grammatical rules"? Typing context seem to be used together with typing relation, so I guess typing context belongs to semantics, just as typing relation does. Or am I wrong? – Tim Sep 2 '19 at 12:06
• Re (1): No. Values are defined separately from evaluation rules using grammatical rules. It is a theorem that evaluation always terminates in a value. Such a theorem guarantees that your computations never get "stuck" at terms that are not values. – Andrej Bauer Sep 2 '19 at 14:10
• Re (2): for simple type theory a context is just a list of types, or possibly a list of pairs x : A where x is a variable. This can be desribed by a grammar easily enough. For complicated theories (say, dependent type theory), contexts are complicated and one needs to make a judgement form for "is a well-formed context". But you are not asking about such complicated cases. – Andrej Bauer Sep 2 '19 at 14:12
• Thanks. (1) "It is a theorem that evaluation always terminates in a value." In the untyped lambda calculus, evaluation of term (lambda x. x x) (lambda x. x x) doesn't terminate in a value, see p65 of the book. Does the book mention something like "Values are defined separately from evaluation rules using grammatical rules"? From p34 of the book, I saw that values are defined as special terms which are the final results of evaluating other terms, so I think it implies that which term is a "value" is derived from evaluation rules. – Tim Sep 2 '19 at 14:24
• There are several possible notions of value: head-normal, weak head-normal, normal form. These are all syntactic, as they say things like "there is no subexpression of the form $(\lambda x . M) N$". So this is still a syntactic criterion. – Andrej Bauer Sep 2 '19 at 17:04