Precise definition of syntatic categories / syntatic domains in abstract syntax

Question

I have read the introductory parts of a couple of books on programming language semantics (Gordon, Winskel, Nielson & Nielson, Allison, Stump, Schmidt), and while I do understand what they mean by syntactic categories, or syntactic domains, I didn't find a rigorous and straightforward definition of those. Is there a standard definition, maybe in earlier works?

Answer 1

Most people avoid giving precise descriptions of what a syntactic category is, because if you do it properly with all the details, the ratio of insight to necessary mathematical sophistication ends up being very, very low. John Reynolds' book Theories of Programming Languages has one of the more comprehensive explanations in its chapter 1, as does Robert Harper's Practical Foundations of Programming Languages.

The intuition you should have is that a syntactic category is the set of trees generated by a context free grammar. Given such a definition for a set of trees, you can define functions on this set using structural recursion, and prove properties about them using structural induction: i.e., by case-analyzing all the different ways that a tree could be constructed.

For example, suppose that we have a language of arithmetic operations given by the following grammar:

e ::= zero | succ(e)| add(e, e)

Then, we can define an interpretation function eval which takes a term and gives you an integer, by cases on the ways we can construct a term:

eval : Expr -> Int
eval zero     = 0
eval succ(e)  = 1 + eval e  
eval add(e, e') = eval e + eval e'*

Note that we have completely defined this function by giving one clause for each possible way we could have generated an expression from the grammar. The fact that this is a complete definition of a function is called the principle of structural recursion.

We can also prove properties about this function by using structural induction -- by doing an inductive analysis for each case. For example, we can prove that for every e, eval e ≥ 0.

Proof. By structural induction on e.
- Case e = zero:
  By the definition of eval, eval zero = 0. 
  We know 0 ≥ 0 by reflexivity of ≥.    

- Case e = succ(e'):     
  By induction, we know that eval e' ≥ 0 
  So we also know that 1 + eval e' ≥ eval e'.
  By transitivity, 1 + eval e' ≥ 0. 
  But eval succ(e') = 1 + eval e'.
  So eval succ(e') ≥ 0.

- Case e = add(e', e'').
  By induction, we know that eval e' ≥ 0.
  By induction, we know that eval e'' ≥ 0.
  By properties of addition, we know that eval e' + eval e'' ≥ 0.
  By the definition of eval, eval add(e',e'') = eval e' + eval e''.
  So eval add(e',e'') ≥ 0.

The fact that considering just the cases for how expressions could be formed constitutes a proof is called the principle of structural induction.

Now, it's a fact that one can define functions by structural recursion and prove properties by structural induction for any grammar. However, proving this rigorously requires a certain amount of category theory; you need to formalize syntactic categories as initial algebras of a certain class of functors, and then prove that such initial algebras always exist for that class.

This is really heavyweight tooling for proving such an "obvious" result, and so I recommend just trusting your intuition about how structural definitions work, and then only bothering with their detailed semantics if you decide to become a professional logician.

Answer 2

I never found an explicit definition either, but I have inferred the folowing.

As I understand, you split the language into syntactic domains; with the addition that syntactic domains must be fully generated by single different symbols, when you write down the grammar. So a syntactic domain is a subset of your language, and each domain is generated by one single symbol.

(I did not say you should partition the language, because then an identifier "$x$" would not be allowed to be in both "integer expressions" and "boolean expressions", for example)

Note that using this definition, you can have different syntactic categories when defining abstract syntax of a language (that is, the abstrat syntax may not be unique). A simple example: suppose you need to specify the abstract syntac for expressions, both integer and boolean. Call ${\mathbb Z}$ the set of integers and ${\mathbb B}=\{T,F\}$ the set of boolean values.

You could say all your expressions are one syntactic domain,

• Exp contains all expressions, and will be mapped by a semantic function onto ${\mathbb Z} \cup {\mathbb B}$

or you could decide to split them:

• ExpBool contains boolean expressions, which will be mapped by a semantic function onto ${\mathbb B}$
• ExpInt contains integer expressions, which will be mapped by a semantic function onto ${\mathbb Z}$

So, as far as I understand the exact syntactic domains to be used is a design issue (I mean a decision you make when designing the abstract syntax for your language). But they are certainly subsets of your language, and each syntactic domain must be generated by a different symbol.