How to prove that a nested composition of graphs is a graph?

Question

Sorry if this is naive or really obvious, but it's not obvious to me. I'm trying to see how to apply proof techniques to software modeling.

Basically, there is Graph Theory which has the definition of nodes and edges to make a graph. Then there is software formed out of bits into chains of bits, which is a graph. You then take these chains of bits and create special meaning behind them and then compose them into larger and larger object structures, until you have basically a database table. A database schema (set of tables) might look like this:

Table Book {
  chapters: [Chapter]
}

Table Chapter {
  paragraphs: [Paragraph]
}

Table Paragraph {
  sentences: [Sentence]
}

Table Sentence {
  words: [Word]
}

Table Word {
  letters: [Letter]
}

Table Letter {
  bits: [Bit]
}

Table Bit {

}

So basically, from [Bit] -> Book (Bit sequence to Book). If we model a sequence as a simple directed graph, then each letter is a sort of graph. If we combine the letters into words, where each letter is a node, we have a higher level graph. If we combine words into sentences, still a higher level graph. But my question is, how do we say "the sequence of words is actually a bit graph x" of some sort? How do we prove that the sequence of words can break down into the primitive "bit graph"?

Sorry if this isn't a fully formed question, I haven't tried to prove anything in years and I am trying to apply this to a real-world programming problem. Eventually with the goal of applying formal methods to programming.

If it's too involved for an answer, what instead then are the steps I would need to figure out to make such a proof?

Answer 1

What is there to prove? The scheme fits the definition of a directed graph. In particular, it is a tree, which is a specific type of graph. It contains more information than a graph does, but that extra information does not prevent it from being a graph. When talking about it as a graph, you just ignore the stuff that isn't graph-like (the term of art for this is a forgetful functor, since it "forgets" everything except the graph elements).

The nodes (aka "vertices") are the instances of your various tables. The links (aka "edges" - interesting how the "node-link" and "vertex-edge" terminologies get intermixed) are the parent instance - child instance relationships in your tables. That is all it takes to be a directed graph.

This graph is a tree because it has a "root": a single top level entry (the book - unless you want to add a "Library" table with multiple books), and there are no cycles. From any node there is only one path between that node and the root.