Substructures for structures without synecdoche

Stream: general

[Kyle Miller]

Most (if not all) algebraic objects in mathlib seem to take advantage of the usual synecdoche, for example a group G is the type containing the elements of the group -- recall, synecdoche is when you refer to a thing by one of its parts (a group is actually G along with a multiplication operation, an inverse operation, and axioms). Some algebraic objects, like modules, use two types, for example modules (the ring R and the abelian group M being acted upon), but we still can refer to M as if it were the module itself. This is OK because many times we want to talk about multiple rings acting upon M. So, the convention is that an algebraic object is referred to by a Type.

Because of this convention, there is a convenient way of dealing with subobjects of an algebraic object A. A subobject is a structure consisting of a carrier set of type set A along with some closure axioms. Mathlib takes advantage of Lean's automatic coercions to sort of make subobjects be objects in their own right by, for instance, defining instances group (↥G') for G' : subgroup G and [group G], where there is an instance has_coe_to_sort G' that gives the carrier set as a type.

However, some objects involve multiple types and you do not refer to the object by synecdoche. The particular case I have in mind are the various flavors of graphs. A graph G consists of a vertex set V and an edge set E. It's a term, not a type. So, if you were to define a subgraph structure (a subset of V, a subset of E, and some axioms), you cannot use the same coe_to_sort trick to give subgraphs the structure of a graph. You would have to do manual coercions everywhere, breaking the illusion that I feel we want to keep, that a subgraph is a graph. Also, a distinction between modules and graphs is that, in some ways, module structures are a partial function on the class of rings, but a graph consists of a fixed vertex and edge set -- it makes little sense varying either of them in this way.

Here is the main question: how should one design an interface for structures that lack synecdoche so that, for instance, subgraphs are graphs? I have one potential solution to this, but I'd like to know if anyone has explored any others.

Let's look at a way semigroups could have been defined (this is not a recommendation, just an illustration; I'd rather use an object people are familiar with in mathlib rather than getting into implementation details of graphs). Rather than giving individual types the structure of a semigroup, what if you declared that every term of a type is a semigroup? From a category theory perspective, perhaps this is declaring that a type is the object set of some category, and you are giving each of those objects some concrete interpretation.

The way this might look is the following (again, not a recommendation, just an illustration):

import tactic.basic

class {u v} semigroups (α : Type u) :=
(carrier : α → Type v)
(mul : Π (G : α), has_mul (carrier G))
(mul_assoc : Π (G : α),
  ∀ (a b c : carrier G), a * b * c = a * (b * c))

open semigroups

instance semigroup_to_sort (α : Type*) [semigroups α] : has_coe_to_sort α :=
⟨_, semigroups.carrier⟩

instance semigroup_coe_mul (α : Type*) [semigroups α] (G : α) : has_mul G :=
mul G

structure subsemigroup {α : Type*} [semigroups α] (G : α) :=
(carrier : set G)
(mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier)

instance (α : Type*) [semigroups α] (G : α) : semigroups (subsemigroup G) :=
{ carrier := λ G', subtype (subsemigroup.carrier G'),
  mul := λ G', ⟨λ a b, ⟨a.1 * b.1, subsemigroup.mul_mem' G' a.2 b.2⟩⟩,
  mul_assoc := λ G', λ a b c, begin
    cases a, cases b, cases c, simp [mul_assoc],
  end }

Notice how terms of subsemigroup G are semigroups themselves, without need for a coercion. (Note: the has_coe_to_sort is there to implement synecdoche from the other side: you can treat a semigroup as if it had terms. Graphs wouldn't have this instance.) (Another note: I used subtype in the last instance because I was having trouble using the coercion arrows and didn't want to spend time figuring out what's wrong.)

Hopefully this example makes it clear how this might apply to graphs. One would have a class that declares that every term in a type can be interpreted as being a graph. There would be graphs instances for the types of subgraphs and graph minors and so on. So, if G is a term from any type of graphs, you could write V G and E G to get its vertex and edge types.

Are there any other approaches that anyone has thought about? It seems that graphs might the first time this issue might have come up.

Using the semigroup example, an alternative could be using has_coe to give terms of a type a semigroup interpretation. However, because semigroup is parameterized by its carrier type, it seems you'd need an instance like

instance {α : Type*} (f : α → Type*) : has_coe α (semigroup (f α))

and then whenever you coerce, you would be obligated to specify the carrier type. A benefit of the semigroups approach is that a user of the API does not need to specify the carrier type: it is a function of the term at the class resolution level.

One other comment for this rather long message: it seems like you still might want semigroup around so that you can implement one-off semigroups. There's a tautological semigroups (semigroup α) instance. It seems weird, but maybe it's a consequence that semigroup is equivalent to semigroups pt where pt is a one-term type.

[Alex J. Best]

I didn't read your full message, so maybe you already answered this, feel free to ignore but: At one point there was a definition of graph floating around on Zulip where the vertices came from some fixed "universe" Type, but were a (fin)set of elements from that universe: I.e. something like

class graph (X : Type*) :=
(verts : set X)
(edges : set (X \times X))
(incidence : \forall e \in edges, e.fst \in verts \and e.snd \in verts)

What is your opinion of this approach?

[Patrick Massot]

Traditional link: Section 3 of https://hal.inria.fr/hal-00825074v1/document

[Kyle Miller]

@Alex J. Best I'm interested in particular about the "synecdoche problem" (or maybe it should be called the "subobject problem"?). I know this is in some ways an XY problem, since getting a good graph interface is an end goal, but it's probably worth figuring out some reasonable solution to it. It seems like something people must have thought about, but in my limited asking around I haven't found anything about it. I'm guessing it's because most things have a primary carrier type.

Anyway, regarding that graph definition, it is, essentially, the type of subgraphs of (directed) complete graphs. It seems to be a viable way of dealing with graphs without multi-edges, especially if you are interested in the lattice of subgraphs, though a downside is the vertices are a set rather than a type. Also, there will probably be some interest in defining the type of graph minors to prove theorems about excluded minors.

For multigraphs, though, you can't really do this trick because there's not really a natural universal multigraph that every other multigraph is a subgraph of. For simplicity, consider a common definition for multidigraphs:

structure multidigraph (V : Type*) :=
(E : Type*)
(ends : E → V × V)

You sort of want edges to be able to be "glued in" anywhere you'd like. A less natural approach that's analogous to the above graph definition would be something like

structure multidigraph (X Y : Type*) :=
(V : set X)
(edges : set (X × X × Y))
(incidence : ∀ e ∈ edges, e.1 ∈ V ∧ e.2.1 ∈ V)

where every multidigraph is a subgraph of the the one with edges between every pair of vertices indexed by Y. (It "solves" the subgraph problem, but I wouldn't want to work with this definition.)

[Kyle Miller]

@Patrick Massot Thanks, I'll take a look at that.

[Kyle Miller]

@Patrick Massot I'm trying to understand what I should be getting out of that link, since it seems to be about how subobjects work in mathlib. Is it that the way to solve this synecdoche problem is to define, for example, a directed multigraph to be a subgraph of a directed multigraph universe?

structure multidigraph_universe (V E : Type*) :=
(ends : E → V × V)

structure multidigraph {V E : Type*} (U : multidigraph_universe V E) :=
(V' : set V)
(E' : set E)
(compat : ∀ e ∈ E', (U.ends e).1 ∈ V' ∧ (U.ends e).2 ∈ V')

This is not exactly analogous to the paper, since the paper's group universe (a "graph type") is a type, but here a multidigraph_universe is a term.

[Patrick Massot]

I'm sorry about the cryptic message. This paper is not about mathlib at all, it's about the Coq library that contains the odd order theorem formalization. And it's not about graph, it's closer to your original message about subsemigroups. But I still hoped you would get useful information about how they solved this "subgroup of subgroup issue".

[Kyle Miller]

@Patrick Massot It was interesting to read regardless, and thank you for sharing it. I guess that even though it was Coq, it seemed like it might be what the design of mathlib was based on, except that mathlib has some different terminology and uses some typeclasses.

Maybe it was a mistake using subsemigroups as an example. The point was to translate an existing algebraic structure that relies on synecdoche (a semigroup "is" a type, and the additional structure is filled in by class resolution) into a form where objects are terms, and in this new form you could imagine adding more types to the structure. The example also showed how you could define subobjects in a way that doesn't rely on the automatic coercion trick for these to be treated as objects.

Perhaps I'll finally submit a PR with the multigraphs definition I've been working on that uses this technique. I've been hesitating because it's unlike other solutions in mathlib, but I think it's justified because these sorts of combinatorial objects are unlike algebraic objects in that they aren't referred to by synecdoche, so the typeclasses have to be structured in a different way. (And it feels natural using the interface, once you're used to saying a type consists of graphs and a graph is a term of that type. That's not so different from the paper you shared.)

[Kyle Miller]

I think I might have found an acceptable solution to this "synecdoche problem," and it seems sort of obvious in retrospect. Using simple graphs as an example, you can define a class that gives terms the structure of a simple graph:

class simple_graph {α : Type u} (G : α) :=
(V : Type v)
(adj : V → V → Prop)
(symm : symmetric adj)
(loopless : irreflexive adj)

Then you can define subgraphs and give them the structure of a simple graph:

structure subgraph {α : Type u} (G : α) :=
(V' : set (V G))
(E' : set (sym2 (V G)))
(edge_sub : E' ⊆ edge_set G)
(has_verts : ∀ (e ∈ E') (v ∈ e), v ∈ V')

instance subgraph.simple_graph (G' : subgraph G) : simple_graph G' := { ... }

Hence, subgraphs are graphs.

These are "abstract" simple graphs. You can form concrete ones using a sort of tautological instance:

structure from_rel (V : Type u) :=
(rel : V → V → Prop)
(symm : symmetric rel)
(irref : irreflexive rel)

instance (V : Type u) (G : from_rel V) : simple_graph G := { ... }

(I'm sort of unsure whether needing this tautological instance is ok.)

I have an implementation of this simple graph definition (a variation on #3458) along with the bounded lattice of subgraphs at https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph.lean

Does this seem like an acceptable design? We have #3458 in review without subgraphs; if this is a good idea, should we update it in this way? (Tagging @Johan Commelin)

Getting this interface right will inform how other combinatorial objects will work, since they tend to be referred to as terms rather than types, and they tend to have various kinds of derived objects like subobjects that you want to use as if they were objects.

[Kevin Buzzard]

I read this thread with interest, and was surprised that the category theory folk didn't weigh in, because what you are talking about is close to the "bundling objects" philosophy of category theory in Lean. @Scott Morrison do you have anything to say about this?

[Johan Commelin]

@Kyle Miller I don't understand why you have \alpha, G, and V...

[Johan Commelin]

The downside of turning graphs into classes is that you can't have multiple graph structures on the same set of vertices. Hence I wouldn't go that route...

[Kyle Miller]

Johan Commelin said:

The downside of turning graphs into classes is that you can't have multiple graph structures on the same set of vertices. Hence I wouldn't go that route...

This doesn't have that limitation, and in fact the design is purposefully trying to avoid this issue. The class is putting a graph structure on a term, and that term specifies the graph's vertex set. This lets you put graph structures on, for example, subgraphs, or really anything else that has a natural graph structure. The example instances I gave show that you can certainly have multiple graph structures on the same vertex type.

This use of classes is different from other algebraic structures, where the carrier type is given an instance (this is synecdoche: the carrier type is part of the algebraic object, but we refer to the type as if it were the object). Here, we refer to a term G and give it a graph structure with [simple_graph G], and then you can access its vertex type with V G. Like you said, vertex types might have multiple graph structures, which is one aspect of what I'm calling the "synecdoche problem." A graph is not referred to by any of its components.

[Patrick Massot]

Kyle Miller said:

I think I might have found an acceptable solution to this "synecdoche problem," and it seems sort of obvious in retrospect. Using simple graphs as an example, you can define a class that gives terms the structure of a simple graph:

class simple_graph {α : Type u} (G : α) :=
(V : Type v)
(adj : V → V → Prop)
(symm : symmetric adj)
(loopless : irreflexive adj)

Surely this is not what you mean. Alpha and G are not even used in fields.

[Patrick Massot]

Also a general note: having internal universe variables is asking for trouble.

[Kyle Miller]

This is what I mean. It is a partial function at the type class level that maps terms of α to graph structures. An alternative is to make it a total function, but I thought this was somewhat weird:

class simple_graphs (α : Type u) :=
(V : α → Type v)
(adj : Π (G : α), V G → V G → Prop)
(symm : Π (G : α), symmetric (adj G))
(loopless : Π (G : α), irreflexive (adj G))

You write (α : Type u) [simple_graphs α] (G : α) to get a graph in this form.

The hedetniemi branch used internal universe variables for directed multigraphs: https://github.com/leanprover-community/mathlib/blob/hedetniemi/src/graph_theory/basic.lean#L11

[Kyle Miller]

This is also similar to category_theory.has_hom, which has an internal universe variable.

[Kyle Miller]

(But categories are modeled differently from graphs. We refer to a category by its object type, if I understand the library correctly, but we don't refer to a graph by its vertex type.)

[Johan Commelin]

@Kyle Miller I've never seen such a class before, and it looks weird to me...
How would you write the complete graph on a type X using your proposal?

[Scott Morrison]

Kyle's implementation is an additional level of indirection which we've never used elsewhere. simple_graphs is a type class on \a that says "you can interpret terms of \a as particular simple graphs".

[Scott Morrison]

One might imagine an analogous typeclass polynomialish, which says that you can think of a type as representing a polynomial. You might provide instances on list R (for polynomials presented by a list of coefficients) and on nat \to\0 R (for our current implementation).

[Johan Commelin]

Right... and I would like to see how this works in practice.

[Scott Morrison]

Yeah, me too. It seems an interesting idea, but I'd want a big chunk of evidence that it is usable.

[Kyle Miller]

@Johan Commelin I suppose a point of this topic is that things like graphs seem to work differently from other objects, so it might take a solution that looks different from what we've seen before -- and I'd like to gather ideas that others might have to get an ergonomic API!

Here's complete graphs: https://github.com/leanprover-community/mathlib/blob/simple_graphs2/src/combinatorics/simple_graph.lean#L349 (I'm not particularly happy with the name from_rel. It's the "tautological" instance of a simple graph.)

@Scott Morrison I'd like more evidence, too. The linked branch, above, exercises at least some of the idea.

[Kyle Miller]

It's odd that the typeclass does not mention G within any of it's fields, of course. To do this sort of typeclass well, it will take some discipline to prove additional lemmas connecting properties of a term G of a particular type to the fields of simple_graph (or whatever combinatorial object we are defining).

[Johan Commelin]

@Kyle Miller Aha... I see. How about adj_rel instead of from_rel?

[Johan Commelin]

(Also, minor point: I think irrefl is the more common name, rather than irref.)

[Kyle Miller]

Thanks for the naming suggestions. I wonder if from_adj_rel might be good? If you don't open the namespace, then simple_graph.from_adj_rel r is what you'd see.

[Johan Commelin]

Yes, but maybe adj_rel in the root namespace also makes sense?

[Johan Commelin]

I don't know... maybe others have good ideas?

[Kyle Miller]

I think naming these things is getting outside my pay grade :smile: (Though, I'll throw in make_simple_graph.)