home

author: niplav, created: 2025-07-10, modified: 2025-09-29, language: english, status: in progress, importance: 3, confidence: likely

P→(V∪P)^2 , the rest is commentary.

Contents

Pergraphs

I am afflicted by a strange curse, which condemns me to be creative enough to find and explore new mathematical structures, but too dumb to prove anything interesting about them.

A drawing with the letter 'A' on the left side, the letter 'B' on the right side. A red arrow goes from 'A' to 'B'. A blue arrow goes from the middle of the red arrow to 'A'.

On a meditation retreat in 2022 I remembered a post by Scott Garrabrant and doodled the above image in my notebook, together with some other drawings of networks where edges can have edges as sources and sinks.

Formalizing

Recently, I got thinking about those kinds of graphs again, researched a bit and think I've discovered they've not been looked at in detail yet. I'll call those kinds of graphs or networks "pergraphs".

In this post I'll go a double track where I'll first and foremost draw pretty pictures to give the reader a visual sense of what they should be thinking about, and also provide Lean 4 code for definitions, theorems and proofs, as a barbell strategy in terms of rigour.

Basic Definitions

Intuition 1: Intuitively, a pergraph is a finite mathematical structure consisting of nodes and edges (which I'll also equivalently call "peredges"), where each edge needs to have a source and a sink. The source and the sink of an edge can be any node or edge, including itself.

Definition 1 (Lean): Given:

  1. A finite set of vertices V and
  2. A finite set of peredges P (where a peredge is simply a label),

A pergraph is the tuple (V, P, e: P \rightarrow (V \cup P) \times (V \cup P)) , where e is a function that assigns each peredge a source and a sink.

Remark 1: A pergraph is more specifically a directed multi-pergraph, since peredges are directed, and two peredges can have the same source and the same sink. We will use the term "pergraph" for directed multi-pergraphs, and specify deviations from such.

Theorem 1 (Proof): Every quiver is also a pergraph, that is the pergraphs contain the quivers as a subset.

Intuition 1: Take any quiver Q=(V, P, s: P→V, t: P→V) . We can then construct a pergraph by assigning the V to the vertex pernodes, P to the peredges, and constructing e by declaring e(p)=(s(p), t(p)) for p \in P . Congrats! You've now constructed a pergraph from your quiver.

Remark 2: Since every directed graph is a quiver, all directed graphs are also pergraphs.

Definition 2 (Lean): A uni-pergraph is a pergraph with the additional constraint that no two peredges have the same source and the same sink, mathematically \lnot \exists p_1, p_2 \in P: p_1 \not=p_2 \land e(p_1)=e(p_2) .

Definition 3 (Lean): An undirected pergraph is a a pergraph with undirected peredges, i.e. a pergraph where e has the type signature P \rightarrow {V \cup P \choose 2} .

Some Pergraph Concepts

Definition 4 (Lean): The source of a peredge is the vertex or peredge it comes from, the sink of a peredge is the thing it points to.

Definition 5 (Lean): A source-path is a sequence of edges so that each edge has as its source the previous edge; a sink-path is a sequence of edges so that each edge has as its sink the following edge. A pure path is a sequence of edges that is both a source-path and a sink-path.

Definition 6 (Lean): Two vertices v_1, v_2 are connected via a source-path if the source of the first edge is v_1 and the sink of the last edge is v_2 , and similar for sink-paths.

Definition 7 (Lean): A mixed source-path is a source-path with vertices mixed in, a mixed sink-path is a sink-path with vertices mixed in.

Definition 8: A source-cycle is a source-path that connects a vertex v to v or an edge p to p . One can define a sink-cycle, a pure cycle, a mixed source cycle, and a mixed sink-cycle similarly.

Remark 3: There's a variant of vertexless pure cycles that I like to call "keltic knots", where, if of any edge p_1 the sink is p_2 , the source of p_2 is p_1 .

Definition 9: A sub-pergraph S of a pergraph A=(V, P, e) is a pergraph where the vertices are subsets of V and the edges are a subset of P . As is custom, a proper sub-pergraph of A is a sub-pergraph of A that isn't equal to A ; an induced sub-pergraph S_i of a pergraph A is a sub-pergraph of A where, for any pair of vertices or edges, all edges between those two components are also edges of S_i , similarly to induced subgraphs.

Definition Ratking (Lean): A ratking is a pergraph without vertices.

Definition 10: A rhizome is a pergraph without a proper sub-pergraph.

Theorem 2: Every rhizome is either a single vertex or a ratking.

Intuition: A pergraph that has at least a vertex is either a single vertex or contains a single vertex as a proper sub-pergraph.

Remark 4: There are non-rhizomatic ratkings.

Remark 5: Ratkings, ordered by whether they are sub-pergraphs, form a lattice where the minimal elements are rhizomes.

Remark 6: Pergraphs, ordered by whether are sub-pergraphs, form a lattice where the minimal elements are rhizomes and a single vertex.

Theorem 3: There are countably infinitely many finite pergraphs.

Intuition: There are finitely many pergraphs of size n for any natural number, order by natural number, then for each natural number, order the pergraphs of that size however you like. You now have a bijection to the natural numbers.

Pseudo-vertex cycles, source-semi-ratkings, sink-semi-ratkings…

Pergraph isomorphism, sub-pergraph detection, pergraph rewrite rules (ratking collapse, flip equivalence (flipping peredges results in the same pergraph)).

Euler cycles and Hamilton cycles, decomposing into rhizomes, enforcing some kind of hierarchy/partial hierarchy? Generating pergraphs from a simpler set with simpler rules?

Bijection/injection with the directed graphs? Needs to blow up the directed graphs.

Counting

Unlabeled pergraphs are counted up to isomorphism for renamings of vertices and peredges.

One can count equence of pergraphs with n=|V|+|P| constituents, starting at n=0:

1, 2, 15, 180, 3638, …

This sequence is not yet in the OEIS.

Code for computing the first terms of the sequence here.

The sequence that that counts the number of unlabeled undirected pergraphs, up to isomorphism, starting at n=0:

1, 2, 10, …

Here's the undirected pergraphs with two components:

As a variant one could ditch the vertex entirely, and replace them self-sourced and self-sinked peredges. I think that one has different combinatorial behavior.

Questions

  1. When does reversing the peredges of a pergraph result in an isomorphic pergraph?
  2. Is there some canonical injection into directed graphs?
  3. How computationally expensive is isomorphism-checking?
    1. Sub-pergraph detection?
  4. In general, what graph theory concepts could be ported over?
    1. Planarity? Strongly/weakly connected components?
  5. Has really nobody looked at these before?
    1. What's the closest most specific but more general mathematical object that includes pergraphs as a special case?
  6. What could these possibly be useful for?

Situating Pergraphs

Pergraphs are a generalization of directed graphs (i.e. every directed graph is a pergraph), but I don't know what known mathematical structure they're a special case of. Claude Opus 4.1 suggests it might be a special case of 2-categories, but I don't think that's true85%.

Random Remarks

  1. Pergraphs aren't recursive in any meaningful sense of the word. They are "sort of" self-referential, if you squint, but really it's only the edges that can be self-referential.
    1. There no way in which a peredge can point at an entire pergraph that contains that peredge.
      1. Hey, there's an idea!
      2. So you'd have a graph a→b , and an edge from a to the entire subgraph a→b …
      3. …Wow that seems really expressive.
      4. Anyway.
    2. I include this point because when I talk about the concept with LLMs, they almost always claim that pergraphs are recursive.
  2. I find pergraphs really pretty to draw.
  3. I also find them very natural, so I'm surprised by why they haven't been studied before.
    1. It could be that I'm missing why they're some trivial aspect of some other known object.
    2. It could be that pergraphs are too general or too expressive to contain interesting structure.
    3. It could be that they're not useful for any other mathematics, and not pratically useful.
  4. Vaguely gesturing at an intuition, pergraphs could be useful for modeling systems where a transition happening causes something.
    1. E.g. in Garrabrant's original post, an agent performs an action because performing the action will transition to a different state.
    2. This doesn't justify things like edges having themselves as sources and sinks.

Axes Along Which to Categorize Different Graph Concepts

{directed, undirected} edges×{allows, disallows} multi-edges×{allows, disallows} loops×{allows, disallows} hyperedges×{allows, disallows} edges between other edges×{allows, disallows} edges from/to themselves×{allows, disallows} edges between arbitrary sets of vertices.

Prior Art

Pergraphs are distinct from hypergraphs, as they don't allow for an edge between more than two nodes; they are not multigraphs, because pergraphs allow for edges from/to edges (similar to multigraphs, they allow for multiple edges between the same two nodes); they are distinct from higraphs, as they don't allow for nested vertices; they are different from Petri nets, because they don't have movable tokens; they are not the same as metagraphs, because they again allow for edges between (nested) collections of nodes. They are probably different from categories and n-categories, because they don't require composition and don't enforce any kind of hierarchy, but I don't know enough category theory to confirm that.

The closest I've found to this concept is in this unsourced section on the Wikipedia article on hypergraphs:

Alternately, edges can be allowed to point at other edges, irrespective of the requirement that the edges be ordered as directed, acyclic graphs. This allows graphs with edge-loops, which need not contain vertices at all. For example, consider the generalized hypergraph consisting of two edges e_{1} and e_{2} , and zero vertices, so that e_{1}=\{e_{2}\} and e_{2}=\{e_{1}\} . As this loop is infinitely recursive, sets that are the edges violate the axiom of foundation. In particular, there is no transitive closure of set membership for such hypergraphs. Although such structures may seem strange at first, they can be readily understood by noting that the equivalent generalization of their Levi graph is no longer bipartite, but is rather just some general directed graph.

The generalized incidence matrix for such hypergraphs is, by definition, a square matrix, of a rank equal to the total number of vertices plus edges. Thus, for the above example, the incidence matrix is simply

\begin{pmatrix} 0 & 1 \cr 1 & 0 \cr \end{pmatrix}

The concept appears under-developed, and slightly different from what I'm pointing at.

Acknowledgements

Many thanks to Claude 4 Sonnet and Claude 4 Opus for several long conversations which fleshed out the concept, talked through the pergraphs with n=2 , help with learning Lean, and help with writing the Rust code for the enumeration.

See Also

Appendix A: Lean Definitions and Proofs

I provide Lean 4 definitions and proofs for pergraphs, related structures, and the theorems in this text.

Definition 1

inductive PerNode (V E : Type) : Type
  | vertex : V → PerNode V E
  | edge : E → PerNode V E

structure Pergraph (V E : Type) where
  e : E → PerNode V E × PerNode V E

Proof 1

def Quiver.toPergraph {V : Type} [Quiver V] :
  Pergraph (V ⊕ (Σ (a b : V), a ⟶ b)) (Σ (a b : V), a ⟶ b) where
  e := fun arr@⟨a, _b, _h⟩ => (PerNode.vertex (Sum.inl a), PerNode.vertex (Sum.inr arr))

That function is injective:

theorem quiver_to_pergraph_injective {V : Type} [Quiver V] :
  Function.Injective (@Quiver.toPergraph V _).e := by
  intros e₁ e₂ h_eq
  simp [Quiver.toPergraph] at h_eq
  -- simp already gives us e₁ = e₂, so we're done
  exact h_eq.2

Definition 2

def UniPergraph (V E : Type) : Type :=
  { p : Pergraph V E // Function.Injective p.e }

Definition 3

structure UndirectedPergraph (V E : Type) where
  e : E → Sym2 (PerNode V E)

Definition 4

def source (G : Pergraph V E) (edge : E) : PerNode V E :=
  (G.e edge).1

def sink (G : Pergraph V E) (edge : E) : PerNode V E :=
  (G.e edge).2

Definition 5

def SourcePath (G : Pergraph V E) : List E → Prop
  | [] => True
  | [_] => True
  | e₁ :: e₂ :: rest => G.source e₂ = PerNode.edge e₁ ∧ SourcePath G (e₂ :: rest)

def SinkPath (G : Pergraph V E) : List E → Prop
  | [] => True
  | [_] => True
  | e₁ :: e₂ :: rest => G.sink e₁ = PerNode.edge e₂ ∧ SinkPath G (e₂ :: rest)

Definition 6

def connectedViaSourcePath (G : Pergraph V E) (start finish : PerNode V E) (path : List E) : Prop :=
  SourcePath G path ∧
  (path.head?.map G.source = some start) ∧
  (path.getLast?.map G.sink = some finish)

def connectedViaSinkPath (G : Pergraph V E) (start finish : PerNode V E) (path : List E) : Prop :=
  SinkPath G path ∧
  (path.head?.map G.source = some start) ∧
  (path.getLast?.map G.sink = some finish)

Definition 7

inductive MixedPath (G : Pergraph V E) (dir : Pergraph V E → E → PerNode V E) (codir : Pergraph V E → E → PerNode V E) : List (PerNode V E ⊕ E) → Prop
  | empty : MixedPath G dir codir []
  | single_vertex (v : PerNode V E) : MixedPath G dir codir [Sum.inl v]
  | single_edge (e : E) : MixedPath G dir codir [Sum.inr e]
  | vertex_then_edge (v : PerNode V E) (e : E) (rest : List (PerNode V E ⊕ E)) :
      dir G e = v →
      MixedPath G dir codir (Sum.inr e :: rest) →
      MixedPath G dir codir (Sum.inl v :: Sum.inr e :: rest)
  | edge_then_edge (e₁ e₂ : E) (rest : List (PerNode V E ⊕ E)) :
      dir G e₂ = PerNode.edge e₁ →
      MixedPath G dir codir (Sum.inr e₂ :: rest) →
      MixedPath G dir codir (Sum.inr e₁ :: Sum.inr e₂ :: rest)
  | edge_then_vertex (e : E) (v : PerNode V E) (rest : List (PerNode V E ⊕ E)) :
      codir G e = v →
      MixedPath G dir codir (Sum.inl v :: rest) →
      MixedPath G dir codir (Sum.inr e :: Sum.inl v :: rest)

def MixedSourcePath (G : Pergraph V E) : List (PerNode V E ⊕ E) → Prop :=
  MixedPath G source sink

def MixedSinkPath (G : Pergraph V E) : List (PerNode V E ⊕ E) → Prop :=
  MixedPath G sink source

Definition Ratking

def isRatking (G : Pergraph V E) : Prop :=
  IsEmpty V