Algebra of subgraphs
using Catlab.Graphs, Catlab.Graphics
using Catlab.Theories, Catlab.CategoricalAlgebra
Grph = ACSetCategory(Graph())
ACSetCategory(CSetCat(Graph), Dict{Symbol, Type}(:Cat => ConcreteCategory, :ACSHom => ACSetTransformation, :Hom => FinFunction, :Op => Union{}, :Sym => Symbol, :AttrType => Union{}, :Ob => FinSetInt, :Attr => Union{}, :ACS => ACSet, :Hetero => ConcreteHeteroMorphism…))
A subgraph of a graph is a monomorphism . Because the category of graphs is a presheaf topos, its subobjects have a rich algebraic structure, which we will explore in this vignette.
Throughout the vignette, we will work with subgraphs of the following graph.
G = @withmodel TypedCatWithCoproducts(Grph) (⊕) begin
cycle_graph(Graph, 4) ⊕ path_graph(Graph, 2) ⊕ cycle_graph(Graph, 1)
end
add_edge!(G, 3, add_vertex!(G))
to_graphviz(G, node_labels=true, edge_labels=true)
Meet and join
The basic operations of meet or intersection (), join or union (), top or maximum (), bottom or minimum () are all computed pointwise: separately on vertices and edges.
Consider the following two subgraphs.
(A = Subobject(G, V=1:4, E=[1,2,4])) |> to_graphviz
(B = Subobject(G, V=[2,3,4,7,8], E=[2,3,6,7])) |> to_graphviz
The join is defined as left adjoint to the diagonal, making it the least upper bound:
@withmodel Grph (∨) begin
A ∨ B
end |> to_graphviz
Dually, the meet is defined as right adjoint to the diagonal, making it the greatest lower bound:
@withmodel Grph (∧) begin
A ∧ B
end |> to_graphviz
Implication and negation
The other operations, beginning with implication () and negation () are more interesting because they do not have pointwise formulas.
Implication is defined as the right adjoint to the meet:
@withmodel Grph (⟹) begin
A ⟹ B
end |> to_graphviz
Negation is defined by setting in the above formula:
@withmodel Grph (¬) begin
¬A
end |> to_graphviz
Induced subgraph as a double negation
The logic of subgraphs, and of subobjects in presheaf toposes generally, is not classical. Specifically, subobjects form a Heyting algebra but not a Boolean algebra. This means that the law of excluded middle does not hold: in general, .
Applying the double negation to a discrete subgraph gives the subgraph induced by those vertices.
(C = Subobject(G, V=1:4)) |> to_graphviz
@withmodel Grph (¬) begin
¬(¬C)
end |> to_graphviz
Subtraction and non
The subojects also form co-Heyting algebra and hence a bi-Heyting algebra.
Subtraction is defined dually to implication as the left adjoint to the join:
@withmodel Grph (\) begin
A \ B
end |> to_graphviz
Non is defined by setting in the above formula:
@withmodel Grph (~) begin
~A
end |> to_graphviz
Boundary via non
A boundary operator can be defined using the non operator:
@withmodel Grph (∧, ~) begin
(A ∧ ~A)
end |> to_graphviz