How to represent a directed acyclic graph in a way that makes it easy to conduct an inductive proof? Is there a good way to represent a directed acyclic graph in a way that makes it easy to conduct an inductive proof?  As an example of what I'm looking for, whenever I have something that follows a tree structure, I like to represent it using a grammar like BNF.  This lets allows us to use structural induction to understand what's going on.  More specifically, we can represent something like a tree with:
tree ::= leaf | branch(tree1,tree2)

and then define some kind of function on tree inductively.  For example, $f:tree \rightarrow \mathbb{N}$ where
$$
f(leaf)=1
$$
and
$$
f(branch(tree1,tree2))=1+f(tree1)+f(tree2)
$$
I like this representation since we can inductively define a function based on its structure and then we can inductively prove results about these functions.    Given that backdrop, is there a similar representation for a directed acyclic graph?  Yes, technically a tree is a DAG and BNF can represent tree structures, but I'd really like to represent any DAG with some kind of notation that allows a similar kind of methodology for inductively defining functions and proofs.
 A: I don't think it's possible,since there's no inductive definitions for DAG (Although you can argue that graph can be represented by the list of node and edge,and list is inductive, but it's not an direct definition)
A: It is possible, as long as you only want finite DAGs, i.e. DAGs with only finitely many points. The procedure is quite standard. The notation $L, T, DAG$ which I define here is not. Although the sets/concepts are.
For a set $X$ define for each $n \in ℕ$ the set $L(X, n)$ of lists of length $n$ with elements from $X$ recursively by $L(X, 0) := \{ \mathrm{nil} \}$ and $L(X, n+1) := X \times L(X, n)$. Here “nil” stands for an empty list. Other common notation for “nil” is “$\varepsilon$” or “[ ]”.
Now the set $L(X)$ of (finite) lists with elements from $X$ can be defined as $L(X) := \bigcup_{n \in ℕ} L(X, n)$.
Similarly, for a set $X$ we define for each $n \in ℕ$ the set $T(X, n)$ of finite trees of height $n$ with nodes labeled by elements from $X$ as
$$ T(X, 0) := X, \\ T(X, n+1) := X \times L(T(X, n)). $$
In the recursive "step" the left coordinate stands for the label of the current node, while the right is a list of branches which the current node sees.
Again, we can define a set $T(X)$ of finite trees with nodes labeled by elements from $X$ as $T(X) := \bigcup_{n\in ℕ} T(X, n)$.
Now an arbitrary (finite) directed acyclic graph can be written as a set/list of trees. I.e. if should $DAG(X)$ stands for the set of DAGs with nodes labeled in $X$, we can set $DAG(X) := L(T(X))$.
If you don't want your DAGs to be labeled, then consider $DAG(\{*\})$, for any object $*$.
We can do induction over these definitions, maybe this suffices.
On the spot, I do not know how to express the parametric $L(X)$ in BNF.
It is important, that the $X$ may vary here, as in different $T(X, n)$ we'd like to consider $L(X)$ for different $X$.
One can show, that the notion of DAG coincides with the notion of "finite directed acyclic graph" if a (directed) graph is considered as a set of vertices and edges.
