Connected components of a graph

[siddhartha-gadgil]

Given a finite graph, return

• partition into connected components
• for vertices in the same component, a path between them (with a proof that this is a path).
• proof that adjacent vertices are in the same component.

[rathivrunda]

How do we define a matrix in Idris ?

[anotherArka]

I think the book by Manning has one definition.

[siddhartha-gadgil]

Yes, it is in the book by Manning, and is one step beyond the definition of Vectors, which you can see at https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect.idr. So we define Mat:(rows: Nat) ->(cols: Nat) -> (elem: Type) -> Type where the entries have type elem

The idea is to fix the number of rows, i.e. the codomain of the natural transformation, and have constructors for

• the empty matrix with m rows (i.e. the linear transformation R^n -> 0 to the zero vector space, i.e. ZeroMat : (rows : Nat) -> (elem: Type) -> Mat(rows)(Z)(elem)
• Adding a column which is a vector, say at the beginning of the matrix `AddCol: (rows: Nat) -> (cols: Nat) -> (elem: Type) -> (firstCol: Data.Vect(rows)(elem) -> (mat : Mat(rows)(cols)(elem)) -> Mat(rows)(S cols)(elem)

By the way, if you are considering #12, it is worth doing the case of one equation over a field first, since there are cases with no solutions (and even with infinitely many)

[shafilmaheenn]

How exactly is a path defined? Can we repeat vertices and edges

[siddhartha-gadgil]

Yes, a path can have repeated vertices and edges. However, it is a theorem that there is a path between points p and q if and only if there is a simple path, i.e., one with no vertices or edges repeated. It may be worth proving this, i.e. mapping from a general path to a simple one with the same endpoints.

Note that first one must fix a definition of a graph. One way is with an incidence matrix. Another way, more common in at least topology related uses is to define a graph as

• A set (or type for us) of vertices V.
• A set (or type for us) of oriented edges E.
• An involution flip: E -> E that reverses the orientation of an edge.
• An initial vertex map i : E -> V

From these we can define a terminal vertex map t: E -> V. Then we can define a path from p to q as an inductive structure.

• A constant path at p.
• Given a path alpha from p to q and an edge e with i(e) = q a path from p to t(e) is obtained by appending the edge e.

In this case, it may (or may not) be easier to use an incidence matrix (or Boolean relation) or some other definition instead.