How to represent a directed acyclic graph in a way that makes it easy to conduct an inductive proof?

Question

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.

Answer 1

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)

Answer 2

Let $V_n := \{ 1, \dots, n \}$ for $n \in \mathbb{N}$, in particular $V_0 = \emptyset$.

Now a DAG with $n$ elements can be defined as an element of $\prod_{k < n} \mathcal{P}(V_k)$. In other words, a DAG with $n+1$ elements consists of a DAG on $n$ elements together with a subset of $V_n$, which indicates which nodes are reachable from the $n+1$th node.

But I don't think it is possible to represent this definition using BNF.