Precise definition of syntatic categories / syntatic domains in abstract syntax I have read the introductory parts of a couple of books on programming language semantics (Gordon, Winskel, Nielson &amp; 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?
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 -&gt; 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.