<p>I think the key problem here is not understanding how inductive definitions of syntax work. Here are three approaches to understanding what a BNF grammar means.</p>

<p>Consider a simple grammar:</p>

<p>$$ t ::= \mathtt{true} ~~|~~ \mathtt{false} ~~|~~ 0 ~~|~~ \mathtt{succ}\ t ~~|~~ \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t$$</p>

<p>Following <a href="http://rads.stackoverflow.com/amzn/click/0262162091" rel="nofollow">Pierce's <em>Types and Programming Languages</em></a> pages 26-27, the set of terms defined by this grammar is given by the following three equivalent ways.</p>

<p><strong>Inductively</strong></p>

<p>The set of terms is the smallest set $\mathcal{T}$ such that:</p>

<ol>
<li>$\{\mathtt{true},\mathtt{false},0\}\subseteq\mathcal{T}$.  </li>
<li>if $t_1\in\mathcal{T}$, then $\mathtt{succ}\ t_1\in\mathcal{T}$.</li>
<li>if $t_1,t_2,t_3\in\mathcal{T}$, then $\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3\in\mathcal{T}$.</li>
</ol>

<p><strong>By Inference Rules</strong></p>

<p>The set of terms is defined by the following rules:</p>

<p>$$\mathtt{true}\in\mathcal{T} \qquad
\mathtt{false}\in\mathcal{T} \qquad 0\in\mathcal{T}$$</p>

<p>$$\dfrac{t_1\in\mathcal{T}}{\mathtt{succ}\ t_1\in\mathcal{T}}
\qquad 
\dfrac{t_1\in\mathcal{T}\quad t_2\in\mathcal{T}\quad t_3\in\mathcal{T}}{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3\in\mathcal{T}}$$</p>

<p><strong>Concretely</strong></p>

<p>For each natural number $i$, define set $S_i$ as follows:</p>

<ol>
<li>$S_0=\emptyset$.</li>
<li>$S_{i+1}=\{\mathtt{true},\mathtt{false},0\}\cup\{\mathtt{succ}\ t_1\mid t_1\in S_i\} \cup \{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \mid t_1,t_2,t_3\in S_i\}$</li>
</ol>

<p>Finally,     $S=\bigcup_i S_i$ is the set of all terms.</p>

CC BY-SA 3.0
2013-01-17T18:22:14.070Z
Thanks a lot - such a clean answer (+1). And it does say SMALLEST set :)
DaveBall aka user750378
CC BY-SA 3.0
2013-01-17T18:31:02.007Z
Suppose you state: $t ::= 0~|~ 0 w$ with $w \in \mathcal{L}$, the language currently being defined. Is this still a BNF? Or does only the inductive way apply? If only the inductive way applies, you do need to state that $\mathcal{L}$ must be the smallest such set. That's what the discussion with Vijay D was about...
DaveBall aka user750378
CC BY-SA 3.0
2013-01-17T19:06:14.370Z
You cannot refer to the language currently being defined like that in BNF. Of course, you can refer to the top non-terminal instead of $w$ to achieve the same effect. I do need to say the smallest set in the inductive definition above; that's what makes it inductive.  If I allowed any other set, then there could be other junk in $\mathcal{T}$.
Dave Clarke
CC BY-SA 3.0
2013-01-17T23:39:35.843Z
I'm jealous. That's a beautifully clear answer that I could not produce.
Vijay D
CC BY-SA 3.0
2013-01-18T05:15:12.577Z
@VijayD: The credit should go to Pierce. I just knew were to find this description.
Dave Clarke
CC BY-SA 3.0
2013-01-17T16:40:40.170Z
2013-01-17T19:01:20.983Z
2013-01-17T19:01:20.983Z
Dave Clarke
<p>The formula in your statement</p>

<blockquote>
  <p>Obviously E(A(F1)) with F1=E(A(F1)) is not well-defined for some Büchi automata. So what does inductively defined exactly mean in this case?</p>
</blockquote>

<p>cannot arise if you built ECTL* inductively. This means, in standard academic parlance, we would present a syntax definition of the form below.</p>

<p>Let $Prop$ be a set of propositions and $p$ range over $Prop$. If $\varphi_1, \ldots, \varphi_n$ are formulae of ECTL* let $\mathcal{A}[\varphi_1, \ldots, \varphi_n]$ denote an automaton $\mathcal{A}$ over the alphabet $\mathcal{P}(\{\varphi_1, \ldots, \varphi_n\})$ of subsets of the $n$ formulae shown.  </p>

<p>$ \varphi ::= p ~\mid~ \varphi \land \varphi ~\mid~ \neg \varphi ~\mid~ \mathsf{E}(\mathcal{A}[\varphi_1, \ldots, \varphi_n])$</p>

<p>I believe there is some confusion in how you may be reading the presentation above. In academic terms this qualifies as BNF. I see that the Wikipedia page gives a slightly different presentation. 
However, the definition above
is <em>equivalent</em> to the BNF grammar you give below. It is not a "relaxed BNF" to use your terminology. It is just an inductive definition where some BNF is used where convenient.</p>

<blockquote>
  <p><strong>BNF</strong>: $\langle\text{sf}\rangle::=\;   \langle\text{atomic prop}\rangle\;\big\vert\; \langle\text{sf}\rangle \vee
\langle\text{sf}\rangle\;\big\vert
\neg\langle\text{sf}\rangle\;\big\vert\; \text{E }\langle
\text{Buechi}\;\mathcal{A}\rangle
(\langle\text{sf}\rangle,\dots,\langle\text{sf}\rangle); $</p>
</blockquote>

<p>Academic writing mixes English and BNF when we make inductive definitions because it is convenient. To see the need for convenience, consider your grammar. It does not inform the reader what $\langle\mathrm{atomic~prop}\rangle$ and what $\langle \mathrm{sf}\rangle$ are. You have chosen an intuitive naming convention, so one can guess the first represents atomic propositions. But in general, we want to have short symbols in our papers, so we prefer a one-time cost of verbose English, which is why we write something like "where $\varphi$ is an ECTL* formula". This text does not in any way change the language being defined.</p>

<p>To your specific question:
Your formula $F$ with $F = E(A(F))$ is not a formula of ECTL*. This type of formula cannot arise as the result of an inductive of the form above. This impossibility has nothing to do with the difference in presentation between BNF as you write it and inductive definitions in papers. To derive your formula, you need some atomic propositions, and a sequence of syntactic compositions to build up the more complex formula.</p>

<p>Now about fixed points. There is some confusion here too. BNF grammars are specific ways to present certain inductive definitions. They are not the only way and they do not cover all inductive definitions. Inductive definitions are a more general class and can be presented in many ways. Least fixed points are a strict generalisation of inductive definitions. Below I will only give an example of how both the BNF grammar above and the inductive definition I gave define a least fixed point. I emphasise that both definitions give rise to the same least fixed point.</p>

<p>Let's assume that $Prop = \{q,r,s\}$ is a set of atomic propositions and $p$ ranges over $Prop$. Consider a lattice $L$ which contains all sets of sequences of symbols appearing in the definitions above. The formulae of ECTL* are one specific element of this lattice. Consider a function $G:L \to L$, which is generated by the definitions above. </p>

<p>$G(\emptyset) = Props$, which accounts for $q$, $r$ and $s$ being formulae, or for the instantiation of $\langle \mathrm{atomic~prop}\rangle$ in BNF.</p>

<p>$G(G(\emptyset)) = G(Props)$, which is the set containing elements, $q \land r$, $q \land s$, $r \land s$, $\neg q$, $\neg s$, $\neg r$, $E(\mathcal{A}(\{q\}))$, $E(\mathcal{A}(\{r\}))$, $E(\mathcal{A}(\{s\}))$, $E(\mathcal{A}(\{q,r\}))$, $E(\mathcal{A}(\{q,s\}))$, $E(\mathcal{A}(\{r,s\}))$, $E(\mathcal{A}(\{q,r,s\}))$.
This is equivalent to applying the formation rules $\langle \mathrm{sf} \rangle \lor \langle \mathrm{sf} \rangle$, $\neg \langle \mathrm{sf} \rangle $ and the others with $\langle \mathrm{sf} \rangle$ being replaced by $\langle \mathrm{atomic~prop}\rangle$. Alternatively, this is equivalent to one unwinding of the inductive definition where we say, if $\varphi_1$ and $\varphi_2$ are atomic propositions, then $\varphi_1 \land \varphi_2$, $\neg \varphi_1$, $E(\mathcal{A}(\{\varphi_1, \varphi_2\}))$, etc are formulae.</p>

<p>The set $G(G(G(\emptyset)))$ contains $q \land r\land  s$, $r \land \neg s$, $\neg (q \land s)$, $\neg E(\mathcal{A}(\{r\}))$,  $E(\mathcal{A}(\{q \land s, \neg r\}))$ and so on.</p>

<p>The set of ECTL* formulae is the least fixed point of the function $G$ above. Note that I have not explicitly defined it, but this is possible to do and might be an insightful exercise to work out the details. Equivalently, you can obtain exactly the same fixed point by the BNF grammar or the inductive definition I give.</p>

<p>The kind of formula you suggest will occur in a fixed point that is not a least fixed point. I emphasise that both the BNF grammar and the inductive definition I give generate the same function $G$, hence they have the same least fixed point and the same set of fixed points. So, if the inductive definition allows for a certain formula, your BNF must allow for the at formula, and vice versa.</p>

CC BY-SA 3.0
2013-01-15T10:59:03.277Z
Thanks for the answer (+1). I've updated my question. Is my syntax definition correct? Is it a direct consequence of "inductively defined"? Because what confuses me in Mads Dam's and your text is "let f_i be formulae". Do you have any reference where ECTL*'s syntax is defined rigorously? Thx.
DaveBall aka user750378
CC BY-SA 3.0
2013-01-15T22:27:13.063Z
Thanks a lot for your thorough update. It explains the BNF I have given in my update, doesn't it?
DaveBall aka user750378
CC BY-SA 3.0
2013-01-15T22:31:44.210Z
I am having difficulty understanding your comment. My expansion is for the grammar *I* gave. Maybe I am used to the way BNF is used in the academic literature, while you are reading it slightly differently. How can the grammar I gave admit the formula you wrote?
Vijay D
CC BY-SA 3.0
2013-01-15T22:37:45.487Z
Let $\varphi_1:=E(A(\varphi_1))$. Then $\varphi_1$ is a fixpoint of your BNF, thus you could argue it is in ECTL*. This problem does not arise in my definition where all syntactic elements are created by the BNF, without using $F_i \in$ ECTL*.
DaveBall aka user750378
CC BY-SA 3.0
2013-01-15T22:40:15.823Z
Can you show me other academic literature where a language $L$ is defined by a BNF that uses $F_i \in L$ (as opposed to non-terminal symbols creating that syntactic element)?
DaveBall aka user750378
CC BY-SA 3.0
2013-01-15T22:47:33.133Z
The BNF is typically understood to define the least fixed point. Even in your definition, you can have the formula in your comment as a fixed point.
Vijay D
CC BY-SA 3.0
2013-01-15T22:54:35.090Z
Interesting. I thought only by "going outside of the BNF" as in your definition, you could have $\varphi_1 = E(A(\varphi_i))$, whereas in the pure BNF, the closest thing you can generate is a finite $\varphi_1 = E(A(E(A(....T))))$ with $\varphi_1 \not\in subformula(T)$ - just like you described in your update.
DaveBall aka user750378
CC BY-SA 3.0
2013-01-16T11:28:16.437Z
I have suggested a change to your answer to include this discussion (how I understood it). Is it ok? If so, I'll remove the BNF part in my question and accept your answer. It would still be interesting to have a reference to a visible book/paper where such relaxed BNFs are being used...
DaveBall aka user750378
CC BY-SA 3.0
2013-01-16T18:38:37.287Z
http://en.wikipedia.org/wiki/Computation_tree_logic#Syntax_of_CTL  I do not like the edit. I do not understand what 'relaxed' means. My grammar is just BNF. If the subscripts are distracting, you can remove them.
Vijay D
CC BY-SA 3.0
2013-01-16T18:55:45.707Z
Or Section 4.1 www.math.unipd.it/~ranzato/papers/jlc07.pdf
Vijay D
CC BY-SA 3.0
2013-01-16T21:23:15.773Z
Again: In pure DNF, you only have non-terminals and a fixed set of terminals on the ride hand side, and the replacement rules already disallow my recursive formula. In a relaxed DNF, you also have elements of the very language you are defining on the right hand side and have to demand the least fixpoint to rule out my recursive formula.
DaveBall aka user750378
CC BY-SA 3.0
2013-01-17T06:58:38.007Z
What is relaxed DNF/BNF?
Dave Clarke
CC BY-SA 3.0
2013-01-17T19:12:08.697Z
Thanks a lot Vijay D for all your work and thorough answers. Since I see it more like Dave Clarke does, I accepted his answer, though I considered yours, too.
DaveBall aka user750378
CC BY-SA 3.0
2013-01-17T23:40:43.063Z
No worries. His answer is the better one. But I think you should spend more time really understanding inductive definitions.
Vijay D
CC BY-SA 3.0
2013-01-14T20:20:59.680Z
2013-01-17T03:58:33.330Z
2013-01-17T03:58:33.330Z
Vijay D
<p>In <a href="http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-217/" rel="nofollow">[1]</a>, the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi automaton whose alphabet is $2^{\{F_1,..,F_n\}}$ for some ECTL* formulas $F_1,..F_n$. </p>

<p>Obviously E($A(F_1)$) with $F_1=$E$(A(F_1)$) is not well-defined for some Büchi automata. So <strong>what does inductively defined exactly mean in this case?</strong> </p>

<p>Maybe that no $F_1,..,F_n$ may use $F_1,..,F_n$ in their respective Büchi automata, but the Büchi automata may occur recursively if the alphabet is correctly exchanged. Or may, e.g., $F_1$ use $F_2,..,F_n$, as long as there is no mutual recursion between the $F_i$?</p>

<hr>

<p>Update: Does the following define ECTL*'s syntax?</p>

<p>$\langle\text{sf}\rangle::=\;
  \langle\text{atomic prop}\rangle\;\big\vert\;
\langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert
\neg\langle\text{sf}\rangle\;\big\vert\; \text{E
}\langle \text{Buechi}\;\mathcal{A}\rangle (\langle\text{sf}\rangle,\dots,\langle\text{sf}\rangle);
$</p>

<p>(as opposed to 
$\langle\text{sf}\rangle::=\;
  \langle\text{atomic prop}\rangle\;\big\vert\;
\langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert
\neg\langle\text{sf}\rangle\;\big\vert\; \text{E
}\langle \text{Buechi}\;\mathcal{A}\rangle (F_1,\dots,F_n);
$ where the $F_i$ are ECTL* formulas).</p>

<hr>

<h3> In detail,</h3>

<p><a href="http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-217/" rel="nofollow">[1]</a> says </p>

<blockquote>
  <p>Formulas of ECTL* are inductively defined as usual and built from
  propositional variables using boolean connectives and containing the
  formula $E(A)$ for each Büchi automaton $A$ over an alphabet
  $2^{\{F_1,..,F_n\}}$ where the $F_i$ are ECTL* formulas.</p>
</blockquote>

<hr>

<p>[1] <a href="http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-217/" rel="nofollow">CTL* and ECTL* as fragements of the modal $\mu$-calculus by Mads Dam</a></p>

CC BY-SA 3.0
2013-01-14T15:22:17.710Z
Probably the first you say, i.e., that each $F_i$ is defined by some BNF and thus cannot refer to any other $F_j$.
John K.
CC BY-SA 3.0
2013-01-15T19:52:09.193Z
Do you mean CTL* or ECTL* syntax?
Vijay D
CC BY-SA 3.0
2013-01-15T22:28:00.893Z
I would choose the first definition you give. The two are equivalent to me, but if your confusion is notational, I would stick with the first one.
Vijay D
<lo.logic><automata-theory><model-checking><temporal-logic>
Inductive definition of ECTL*: how are recursive formulas forbidden?
DaveBall aka user750378
# Inductive definition of ECTL*: how are recursive formulas forbidden?

(Asked by: username_0 on 2013-01-14)

In [[1]](http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-217/), the extended computation tree logic ECTL\* is inductively defined as the propositional formulas over all E($A(F\_1,..F\_n)$), where E is the existential path quantifier and $A$ some Büchi automaton whose alphabet is $2^{\{F\_1,..,F\_n\}}$ for some ECTL\* formulas $F\_1,..F\_n$.

Obviously E($A(F\_1)$) with $F\_1=$E$(A(F\_1)$) is not well-defined for some Büchi automata. So **what does inductively defined exactly mean in this case?**

Maybe that no $F\_1,..,F\_n$ may use $F\_1,..,F\_n$ in their respective Büchi automata, but the Büchi automata may occur recursively if the alphabet is correctly exchanged. Or may, e.g., $F\_1$ use $F\_2,..,F\_n$, as long as there is no mutual recursion between the $F\_i$?

---

Update: Does the following define ECTL\*'s syntax?

$\langle\text{sf}\rangle::=\;
\langle\text{atomic prop}\rangle\;\big\vert\;
\langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert
\neg\langle\text{sf}\rangle\;\big\vert\; \text{E
}\langle \text{Buechi}\;\mathcal{A}\rangle (\langle\text{sf}\rangle,\dots,\langle\text{sf}\rangle);
$

(as opposed to
$\langle\text{sf}\rangle::=\;
\langle\text{atomic prop}\rangle\;\big\vert\;
\langle\text{sf}\rangle \vee \langle\text{sf}\rangle\;\big\vert
\neg\langle\text{sf}\rangle\;\big\vert\; \text{E
}\langle \text{Buechi}\;\mathcal{A}\rangle (F\_1,\dots,F\_n);
$ where the $F\_i$ are ECTL\* formulas).

---

### In detail,

[[1]](http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-217/) says

> Formulas of ECTL\* are inductively defined as usual and built from
> propositional variables using boolean connectives and containing the
> formula $E(A)$ for each Büchi automaton $A$ over an alphabet
> $2^{\{F\_1,..,F\_n\}}$ where the $F\_i$ are ECTL\* formulas.

---

[1] [CTL\* and ECTL\* as fragements of the modal $\mu$-calculus by Mads Dam](http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-217/)

**Tags:** lo.logic, automata-theory, model-checking, temporal-logic

> **Comments:**
> **username_1**: Probably the first you say, i.e., that each $F_i$ is defined by some BNF and thus cannot refer to any other $F_j$.  
> **username_2**: Do you mean CTL* or ECTL* syntax?  
> **username_2**: I would choose the first definition you give. The two are equivalent to me, but if your confusion is notational, I would stick with the first one.  

---

## 2 answers

### Answer by username_3 on 2013-01-17. Score: 5 | Accepted answer

I think the key problem here is not understanding how inductive definitions of syntax work. Here are three approaches to understanding what a BNF grammar means.

Consider a simple grammar:

$$ t ::= \mathtt{true} ~~|~~ \mathtt{false} ~~|~~ 0 ~~|~~ \mathtt{succ}\ t ~~|~~ \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t$$

Following [Pierce's *Types and Programming Languages*](http://rads.stackoverflow.com/amzn/click/0262162091) pages 26-27, the set of terms defined by this grammar is given by the following three equivalent ways.

**Inductively**

The set of terms is the smallest set $\mathcal{T}$ such that:

1. $\{\mathtt{true},\mathtt{false},0\}\subseteq\mathcal{T}$.
2. if $t\_1\in\mathcal{T}$, then $\mathtt{succ}\ t\_1\in\mathcal{T}$.
3. if $t\_1,t\_2,t\_3\in\mathcal{T}$, then $\mathtt{if}\ t\_1\ \mathtt{then}\ t\_2\ \mathtt{else}\ t\_3\in\mathcal{T}$.

**By Inference Rules**

The set of terms is defined by the following rules:

$$\mathtt{true}\in\mathcal{T} \qquad
\mathtt{false}\in\mathcal{T} \qquad 0\in\mathcal{T}$$

$$\dfrac{t\_1\in\mathcal{T}}{\mathtt{succ}\ t\_1\in\mathcal{T}}
\qquad
\dfrac{t\_1\in\mathcal{T}\quad t\_2\in\mathcal{T}\quad t\_3\in\mathcal{T}}{\mathtt{if}\ t\_1\ \mathtt{then}\ t\_2\ \mathtt{else}\ t\_3\in\mathcal{T}}$$

**Concretely**

For each natural number $i$, define set $S\_i$ as follows:

1. $S\_0=\emptyset$.
2. $S\_{i+1}=\{\mathtt{true},\mathtt{false},0\}\cup\{\mathtt{succ}\ t\_1\mid t\_1\in S\_i\} \cup \{\mathtt{if}\ t\_1\ \mathtt{then}\ t\_2\ \mathtt{else}\ t\_3 \mid t\_1,t\_2,t\_3\in S\_i\}$

Finally, $S=\bigcup\_i S\_i$ is the set of all terms.

> **Comments:**
> **username_0**: Thanks a lot - such a clean answer (+1). And it does say SMALLEST set :)  
> **username_0**: Suppose you state: $t ::= 0~|~ 0 w$ with $w \in \mathcal{L}$, the language currently being defined. Is this still a BNF? Or does only the inductive way apply? If only the inductive way applies, you do need to state that $\mathcal{L}$ must be the smallest such set. That's what the discussion with username_2 was about...  
> **username_3**: You cannot refer to the language currently being defined like that in BNF. Of course, you can refer to the top non-terminal instead of $w$ to achieve the same effect. I do need to say the smallest set in the inductive definition above; that's what makes it inductive.  If I allowed any other set, then there could be other junk in $\mathcal{T}$.  
> **username_2**: I'm jealous. That's a beautifully clear answer that I could not produce.  
> **username_3**: @VijayD: The credit should go to Pierce. I just knew were to find this description.  

---

### Answer by username_2 on 2013-01-14. Score: 6

The formula in your statement

> Obviously E(A(F1)) with F1=E(A(F1)) is not well-defined for some Büchi automata. So what does inductively defined exactly mean in this case?

cannot arise if you built ECTL\* inductively. This means, in standard academic parlance, we would present a syntax definition of the form below.

Let $Prop$ be a set of propositions and $p$ range over $Prop$. If $\varphi\_1, \ldots, \varphi\_n$ are formulae of ECTL\* let $\mathcal{A}[\varphi\_1, \ldots, \varphi\_n]$ denote an automaton $\mathcal{A}$ over the alphabet $\mathcal{P}(\{\varphi\_1, \ldots, \varphi\_n\})$ of subsets of the $n$ formulae shown.

$ \varphi ::= p ~\mid~ \varphi \land \varphi ~\mid~ \neg \varphi ~\mid~ \mathsf{E}(\mathcal{A}[\varphi\_1, \ldots, \varphi\_n])$

I believe there is some confusion in how you may be reading the presentation above. In academic terms this qualifies as BNF. I see that the Wikipedia page gives a slightly different presentation.
However, the definition above
is *equivalent* to the BNF grammar you give below. It is not a "relaxed BNF" to use your terminology. It is just an inductive definition where some BNF is used where convenient.

> **BNF**: $\langle\text{sf}\rangle::=\; \langle\text{atomic prop}\rangle\;\big\vert\; \langle\text{sf}\rangle \vee
> \langle\text{sf}\rangle\;\big\vert
> \neg\langle\text{sf}\rangle\;\big\vert\; \text{E }\langle
> \text{Buechi}\;\mathcal{A}\rangle
> (\langle\text{sf}\rangle,\dots,\langle\text{sf}\rangle); $

Academic writing mixes English and BNF when we make inductive definitions because it is convenient. To see the need for convenience, consider your grammar. It does not inform the reader what $\langle\mathrm{atomic~prop}\rangle$ and what $\langle \mathrm{sf}\rangle$ are. You have chosen an intuitive naming convention, so one can guess the first represents atomic propositions. But in general, we want to have short symbols in our papers, so we prefer a one-time cost of verbose English, which is why we write something like "where $\varphi$ is an ECTL\* formula". This text does not in any way change the language being defined.

To your specific question:
Your formula $F$ with $F = E(A(F))$ is not a formula of ECTL\*. This type of formula cannot arise as the result of an inductive of the form above. This impossibility has nothing to do with the difference in presentation between BNF as you write it and inductive definitions in papers. To derive your formula, you need some atomic propositions, and a sequence of syntactic compositions to build up the more complex formula.

Now about fixed points. There is some confusion here too. BNF grammars are specific ways to present certain inductive definitions. They are not the only way and they do not cover all inductive definitions. Inductive definitions are a more general class and can be presented in many ways. Least fixed points are a strict generalisation of inductive definitions. Below I will only give an example of how both the BNF grammar above and the inductive definition I gave define a least fixed point. I emphasise that both definitions give rise to the same least fixed point.

Let's assume that $Prop = \{q,r,s\}$ is a set of atomic propositions and $p$ ranges over $Prop$. Consider a lattice $L$ which contains all sets of sequences of symbols appearing in the definitions above. The formulae of ECTL\* are one specific element of this lattice. Consider a function $G:L \to L$, which is generated by the definitions above.

$G(\emptyset) = Props$, which accounts for $q$, $r$ and $s$ being formulae, or for the instantiation of $\langle \mathrm{atomic~prop}\rangle$ in BNF.

$G(G(\emptyset)) = G(Props)$, which is the set containing elements, $q \land r$, $q \land s$, $r \land s$, $\neg q$, $\neg s$, $\neg r$, $E(\mathcal{A}(\{q\}))$, $E(\mathcal{A}(\{r\}))$, $E(\mathcal{A}(\{s\}))$, $E(\mathcal{A}(\{q,r\}))$, $E(\mathcal{A}(\{q,s\}))$, $E(\mathcal{A}(\{r,s\}))$, $E(\mathcal{A}(\{q,r,s\}))$.
This is equivalent to applying the formation rules $\langle \mathrm{sf} \rangle \lor \langle \mathrm{sf} \rangle$, $\neg \langle \mathrm{sf} \rangle $ and the others with $\langle \mathrm{sf} \rangle$ being replaced by $\langle \mathrm{atomic~prop}\rangle$. Alternatively, this is equivalent to one unwinding of the inductive definition where we say, if $\varphi\_1$ and $\varphi\_2$ are atomic propositions, then $\varphi\_1 \land \varphi\_2$, $\neg \varphi\_1$, $E(\mathcal{A}(\{\varphi\_1, \varphi\_2\}))$, etc are formulae.

The set $G(G(G(\emptyset)))$ contains $q \land r\land s$, $r \land \neg s$, $\neg (q \land s)$, $\neg E(\mathcal{A}(\{r\}))$, $E(\mathcal{A}(\{q \land s, \neg r\}))$ and so on.

The set of ECTL\* formulae is the least fixed point of the function $G$ above. Note that I have not explicitly defined it, but this is possible to do and might be an insightful exercise to work out the details. Equivalently, you can obtain exactly the same fixed point by the BNF grammar or the inductive definition I give.

The kind of formula you suggest will occur in a fixed point that is not a least fixed point. I emphasise that both the BNF grammar and the inductive definition I give generate the same function $G$, hence they have the same least fixed point and the same set of fixed points. So, if the inductive definition allows for a certain formula, your BNF must allow for the at formula, and vice versa.

> **Comments:**
> **username_0**: Thanks for the answer (+1). I've updated my question. Is my syntax definition correct? Is it a direct consequence of "inductively defined"? Because what confuses me in Mads Dam's and your text is "let f_i be formulae". Do you have any reference where ECTL*'s syntax is defined rigorously? Thx.  
> **username_0**: Thanks a lot for your thorough update. It explains the BNF I have given in my update, doesn't it?  
> **username_2**: I am having difficulty understanding your comment. My expansion is for the grammar *I* gave. Maybe I am used to the way BNF is used in the academic literature, while you are reading it slightly differently. How can the grammar I gave admit the formula you wrote?  
> **username_0**: Let $\varphi_1:=E(A(\varphi_1))$. Then $\varphi_1$ is a fixpoint of your BNF, thus you could argue it is in ECTL*. This problem does not arise in my definition where all syntactic elements are created by the BNF, without using $F_i \in$ ECTL*.  
> **username_0**: Can you show me other academic literature where a language $L$ is defined by a BNF that uses $F_i \in L$ (as opposed to non-terminal symbols creating that syntactic element)?  
> **username_2**: The BNF is typically understood to define the least fixed point. Even in your definition, you can have the formula in your comment as a fixed point.  
> **username_0**: Interesting. I thought only by "going outside of the BNF" as in your definition, you could have $\varphi_1 = E(A(\varphi_i))$, whereas in the pure BNF, the closest thing you can generate is a finite $\varphi_1 = E(A(E(A(....T))))$ with $\varphi_1 \not\in subformula(T)$ - just like you described in your update.  
> **username_0**: I have suggested a change to your answer to include this discussion (how I understood it). Is it ok? If so, I'll remove the BNF part in my question and accept your answer. It would still be interesting to have a reference to a visible book/paper where such relaxed BNFs are being used...  
> **username_2**: http://en.wikipedia.org/wiki/Computation_tree_logic#Syntax_of_CTL  I do not like the edit. I do not understand what 'relaxed' means. My grammar is just BNF. If the subscripts are distracting, you can remove them.  
> **username_2**: Or Section 4.1 www.math.unipd.it/~ranzato/papers/jlc07.pdf  
> **username_0**: Again: In pure DNF, you only have non-terminals and a fixed set of terminals on the ride hand side, and the replacement rules already disallow my recursive formula. In a relaxed DNF, you also have elements of the very language you are defining on the right hand side and have to demand the least fixpoint to rule out my recursive formula.  
> **username_3**: What is relaxed DNF/BNF?  
> **username_0**: Thanks a lot username_2 for all your work and thorough answers. Since I see it more like username_3 does, I accepted his answer, though I considered yours, too.  
> **username_2**: No worries. His answer is the better one. But I think you should spend more time really understanding inductive definitions.  

---

