Consider an alphabet: $\{p,',(,),\land,\vee,\neg,\rightarrow \}$. A propositional atom is defined as $p$ followed by zero or more $'$s. A well-formed formula (wff) is defined recursively as
- Every propositional atom is a wff.
- If $W$ is a wff, so is $\neg W$
- If $W$ and $V$ are wffs, so are $(W \land V)$, $(W \vee V)$, and $(W \rightarrow V)$.
I want to formally define an algorithm that takes as input a wff and outputs a natural number which is the index, starting from $1$, of the main connective. (And for propositional atoms, the algorithm can output $0$.)
So, for example, given formulas $p''$, $\neg p$, $(p \land (p' \vee p'))$, and $((p \land p') \vee p')$, the algorithm would output $0$, $1$, $3$, and $8$, respectively. I do count the occurrences of the $'$ symbol, as you can see by the last example.