<p>I never found an explicit definition either, but I have inferred the folowing.</p>

<p>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.</p>

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

<p>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.</p>

<p>You could say all your expressions are one syntactic domain,</p>

<ul>
<li><strong>Exp</strong> contains all expressions, and will be mapped by a semantic function onto ${\mathbb Z} \cup {\mathbb B}$</li>
</ul>

<p>or you could decide to split them:</p>

<ul>
<li><strong>ExpBool</strong> contains boolean expressions, which will be mapped by a semantic function  onto ${\mathbb B}$</li>
<li><strong>ExpInt</strong> contains integer expressions, which will be mapped by a semantic function onto ${\mathbb Z}$</li>
</ul>

<p>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.</p>

CC BY-SA 3.0
2016-02-08T18:15:42.497Z
2016-02-17T19:34:18.700Z
2016-02-17T19:34:18.700Z
Jay
<p>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 <em>Theories of Programming Languages</em> has one of the more comprehensive explanations in its chapter 1, as does Robert Harper's <em>Practical Foundations of Programming Languages</em>.</p>

<p>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 <em>structural recursion</em>, and prove properties about them using <em>structural induction</em>: i.e., by case-analyzing all the different ways that a tree could be constructed. </p>

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

<pre><code>e ::= zero | succ(e)| add(e, e)
</code></pre>

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

<pre><code>eval : Expr -&gt; Int
eval zero     = 0
eval succ(e)  = 1 + eval e  
eval add(e, e') = eval e + eval e'*
</code></pre>

<p>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 <em>structural recursion</em>. </p>

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

<pre><code>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.
</code></pre>

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

<p>Now, it's a fact that one can define functions by structural recursion and prove properties by structural induction for <em>any</em> 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. </p>

<p>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. </p>

CC BY-SA 3.0
2016-02-18T20:18:13.547Z
If only we could use structural induction. Once a language has binders, things become more complicated.
Martin Berger
CC BY-SA 3.0
2016-02-18T10:09:58.873Z
2016-02-18T10:09:58.873Z
Neel Krishnaswami
<p>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 <em>syntactic categories</em>, or <em>syntactic domains</em>, I didn't find a rigorous and straightforward definition of those. Is there a standard definition, maybe in earlier works?</p>

<semantics><denotational-semantics><definitions>
Precise definition of syntatic categories / syntatic domains in abstract syntax
josh
# Precise definition of syntatic categories / syntatic domains in abstract syntax

(Asked by: username_0 on 2016-02-07)

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?

**Tags:** semantics, denotational-semantics, definitions

---

## 2 answers

### Answer by username_2 on 2016-02-18. Score: 7 | Accepted answer

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.

> **Comments:**
> **username_3**: If only we could use structural induction. Once a language has binders, things become more complicated.  

---

### Answer by username_1 on 2016-02-08. Score: 4

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.


---

