What type of Tree/Graph/Multigraph is a syntax parse tree?

Question

Consider a string $((A\lor B)\lor A)$

We can make an (informally defined) parse tree for this expression whose nodes are subformulas. The root node would be the full formula $(A \lor B) \lor A$ which would have two children nodes $(A\lor B)$ and $A$ and the left branch would have two children: $A$ and $B$.

Say the root node appears at layer zero, $(A\lor B)$ and $A$ appear at layer 1 and $A$ and $B$ appear at layer 2.

But I'm trying to understand finer details about representing this structure as a mathematical graph. First of all, the two nodes at layer 1 must be ordered. That is $(A\lor B)$ comes before $A$. Second, the symbol $A$ appears at two positions in this informal tree. If we consider the elements of the nodes of the tree as living in a set then the edge pointing from $((A\lor B)\lor A)$ to $A$ would point to the same $A$ as the edge pointing from $(A\lor B)$ to $A$.

I don't think the graph needs to be totally ordered to handle the first issue. There need only be orderings amongst children of any node.

The second condition could somehow be handled by letting nodes be elements of a multiset rather than a set. I guess a labeled set.

It seems like the parse tree is in fact some sort of rooted ordered labeled directed tree, but I can't figure out sort of the minimal description.

If it's helpful I'm trying to formalize/develop a proof for the following. Say we have an alphabet with atomic symbols like $A, B, C, \ldots$ and connectives like $\lor, \land, \implies, \lnot$. Strings (elements of $\textbf{STR}$) are arbitrary concatenations of symbols but there are functions that take strings to connectivized strings like \begin{align} f_{\lor}: \textbf{STR} &\to \textbf{STR}\\ A, B &\mapsto (A\lor B) \end{align}

These functions ($f_{\lor}$, $f_{\land}$, $f_{\implies}$, $f_{\lnot}$) are collected in $\mathcal{F}$ and we call the set of all atomic symbols $\mathcal{A}\subset \textbf{STR}$. The "well-formed formulas" $\textbf{WFF} \subset \textbf{STR}$ can be defined as the inductive closure of $\mathcal{A}$ under $\mathcal{F}$ in $\textbf{STR}$. I would like to prove that the elements of $\textbf{WFF}$ defined as this inductive closure are exactly the elements of $\textbf{STR}$ that has a parse tree (1) whose root node is equal to the element of $\textbf{WFF}$ and (2) every node is either atomic (has no children) or is equal to one of the functions $f\in \mathcal{F}$ acting on the ordered tuple of its children. There may be some more conditions. But in any case, I'd like to formally define the "syntax parse tree" in such a way as to support this proof.

Disclaimer: I'm just wading into this field so there may be very obvious terminology definitions or references that I'm missing. All help is appreciated!

edit: I guess I see two possible approaches to my question.

• Use a rooted directed tree that is ordered and labeled, i.e. label each node with an integer such that the ordering of the integers is commensurate with the left/right ordering of sub-formulas in the string. A downside of this approach is that the ordering may not be unique. Conventions could maybe be chosen to enforce a conventional ordering.
• Use a rooted directed tree that is doubly labeled. Each node has one label to make it unique from other instances of that same formula within the tree (i.e. the string described above would have $A_1$, $A_2$, and $B_1$) and each node would have a second label indicated left/right ordering of children of a particular node. So the second label would induce a partial order on the set of 1st labeled nodes sufficient to resolve the ordering of the subformulas in the larger string.

The first approach is maybe simpler but a little bit overkill. The second approach gets more at the intuitive concepts being expressed but adds lots of structure.

These two ideas are only outlines of a formal structure in my mind, I would really appreciate if anyone could sharpen these definitions for me and even provide me terminology or references that treat syntax trees in the way I'm trying to here.

edit2: Yet a third approach:

• Abandon the tree concept but keep a directed graph. There will be a unique node that has no parents but children nodes can have multiple parents. Second we'll put labels on edges so that $(A\lor B)$ will have one edge labeled 1 pointing to $A$ and another labeled 2 pointing to $B$. We'll also allow a multigraph so that $(A\lor A)$ can be described by one node $(A\lor A)$ which points to $A$ with 2 edges labeled 1 and 2. The edge labelling assists in constructing the tuple that will be passed into the function $f_{\lor}$ to calculate the parent node. If we want to be even more explicit (to help with the proof sought above) we could label nodes by their primary connective in addition to just the string. That is the root node would become $((A\lor B), f_{\lor})$ and the leaves would be $(A, \mathcal{A})$ and $(B, \mathcal{A})$. I guess I would call this a rooted directed partially edge ordered multigraph.

Answer 1

Here's a stab at the definition of the structure at hand.

Suppose we have atomic symbols in the set $\textbf{ATOM} \subset \textbf{STR}$ and functions $\mathcal{F}$ for which $f\in \mathcal{F}$ means $f:\textbf{STR}^n \to \textbf{STR}$ for some $n\in \mathbb{N}$ (usually 1 or 2 in the case of usual first order logic, but we can consider more in general).

We try to define a parse tree as follows.

We have a set of nodes $N = [n] = \{0, \ldots, n-1\}$ for some $n\in \mathbb{N}$ so that $N\subset \mathbb{N}$. We then have a set of edges $E \subset \mathcal{P}(N\times N)$. Note that edges are ordered.

Let $\tilde{\mathcal{F}} = \mathcal{F}\cup \textbf{ATOM}$ Each node has a value represented by a function $V_N:N\to\tilde{\mathcal{F}}$ and each edge also has a value represented by a function $V_E:E\to \mathbb{N}$. The structure $G = (N, E, V_N, V_E)$ is a node and edge labeled directed graph.

We say $G$ is a parse tree if the following hold.

• There exists a root node $r\in N$ such that $r$ has no parents (i.e. no edges point to it)
• Each node $m$ satisfies one of
  • $V_N(m)\in \textbf{ATOM}$ and $m$ has no children or
  • $V_N(m) = f \in \textbf{F}$ and $f:\textbf{STR}^l \to \textbf{STR}$ for $l\in \mathbb{N}$. In this case the restriction of $V_E$ to the set of edges connecting $m$ to its children must be a bijection onto $[l] = \{0, \ldots, l-1\}$ (that is there must be $l$ children and the labels for the edges connecting to these children must be $\{0, \ldots, l-1\}$).

I'm not exactly sure of the fully formal details, but there must be a way using a structural recursion theorem to define a function that maps each node $m$ to a corresponding string in $\textbf{STR}$. A parse tree is then said to be a parse tree for a particular string $s\in \textbf{STR}$ if the value of this recursively defined function on the root node is equal to $s$.

So the underlying structure is indeed a plane (ordered) rooted tree. The added structure comes from the labels $V_N$ and $V_E$ for the nodes and edges.