0
$\begingroup$

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 final 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"?

enter image description here

enter image description here

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ Do not post pictures of formulas, please. $\endgroup$
    – Andrej Bauer
    Commented Sep 2, 2019 at 5:57
  • 1
    $\begingroup$ Sorry, I don't know how to reproduce the two figures, and I think It is better to have them than not at all. $\endgroup$
    – Tim
    Commented Sep 2, 2019 at 12:00

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
14
  • $\begingroup$ 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? $\endgroup$
    – Tim
    Commented Sep 2, 2019 at 12:06
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Sep 2, 2019 at 14:10
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Sep 2, 2019 at 14:12
  • $\begingroup$ 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. $\endgroup$
    – Tim
    Commented Sep 2, 2019 at 14:24
  • 1
    $\begingroup$ Even if in some text you saw someone defined values as "final results of evaluation", I am telling you that (a) it's better to avoid this and define values separately (for several reasons that we cannot go into here), and (b) in most cases values are defined by a syntactic criterion so that they are recognizable by inspection. $\endgroup$
    – Andrej Bauer
    Commented Sep 2, 2019 at 17:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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