Graphs : weight for a walk

Stream: new members

[Christopher Schmidt]

Hello everyone,
I am trying to define a weight for a walk as the product of the weights of the edges the walk visits.

universe u

@[ext]
structure directed_simple_graph (V : Type u) := (adj : V → V → Prop)

namespace directed_simple_graph
variables {V : Type u}
variables (G : directed_simple_graph V)

@[ext, derive decidable_eq]
structure dart extends V × V :=
(is_adj : G.adj fst snd)

def dart.edge (d : G.dart) : V × V := d.to_prod

@[derive decidable_eq]
inductive directed_walk : V → V → Type u
| nil {u : V} : directed_walk u u
| cons {u v w: V} (h : G.adj u v) (p : directed_walk v w) : directed_walk u w

namespace directed_walk
variables {u v : Type V}

def darts : Π {u v : V}, G.directed_walk u v → list G.dart
| u v nil := []
| u v (cons h p) := ⟨(u, _), h⟩ :: p.darts

def edges {u v : V} (p : G.directed_walk u v) : list (V × V) := p.darts.map (dart.edge G)

def edges_set {u v : V} : G.directed_walk u v → set (V × V) :=
λ p, {x : V × V | [(x.1, x.2)] ⊆ p.edges }

constant walk_edge_weight : p.edges_set → ℝ

def edges_mult_set {u v : V} : G.directed_walk u v → set ((V × V) × ℕ) :=
λ p, {x : (V × V) × ℕ | (x.1.1,x.1.2) ∈ p.edges_set ∧ x.2 =  (p.edges).count (x.1.1,x.1.2) }

def walk_weight {u v : V} : G.directed_walk u v → ℝ := sorry

The issue, I have, is :
First, I need to introduce a weight function that sends the edge of a walk to a real number. I would like to have a function

f : p.edges \to \R

however this does not seem to work. Therefore, I defined a set, "edges_set", instead of a list (V \times V), "edges". Now, I can introduce the weight function, "walk_edge_weight". However, wanting to introduce a weight fot the walk, I must not lose duplicates. Thats why I came up with "edges_mult_set". Now I am trying to map the walk to a real number by

Product_{e=(e1,e1,e3) in edges_set_mult} walk_edge_weight (e1,e2) * e3

But I dont know, how to implement that or whether there is a way more convenient way of achieving the goal of a weight for a walk. Any help is appreciated.

[Kyle Miller]

This is untested, but this might be something like what you're looking for:

def walk_weight (wt : G.edge_set → ℝ) : Π {u v : V}, G.directed_walk u v → ℝ
| u v nil := 1
| u v (cons h p) := wt ⟨_, h⟩ * walk_weight p

[Kyle Miller]

That's a function that takes a weight function on the edges of a graph and a directed walk and outputs a real number. I might have gotten wt ⟨_, h⟩ wrong. You might also do something like

def walk_weight (wt : V → V → ℝ) : Π {u v : V}, G.directed_walk u v → ℝ
| u v nil := 1
| u v (@cons _ x _ h p) := wt u x * walk_weight p

[Kyle Miller]

It generally is OK to allow larger domains for things, like wt in this case taking in arbitrary pairs of vertices. You can always put "junk" values for non-edges

[Christopher Schmidt]

Kyle Miller schrieb:

It generally is OK to allow larger domains for things, like wt in this case taking in arbitrary pairs of vertices. You can always put "junk" values for non-edges

Thanks for helping me, again :smile:. This most likely is what I have been looking for. I still find the "nil cons recursive way" of defining stuff quite unintuitive.

How do I define a junk value ? I mean it could be defined as 0, but is there a way to make the output an error and not an element in \R ?

By the way, has anyone worked on similar stuff already ? I also plan on introducing a path system and the weight of such. (The goal is to work on the Lindstrom Gessel Viennot Lemma.)

[Sky Wilshaw]

You can use arbitrary \R for your junk value. It turns out to be equal to 0, but it's marked @[irreducible] so it's not easy to accidentally rely on this behaviour.

[Sky Wilshaw]

docs#arbitrary

[Christopher Schmidt]

@Sky Wilshaw Thanks.

[Christopher Schmidt]

Kyle Miller schrieb:

This is untested, but this might be something like what you're looking for:

def walk_weight (wt : G.edge_set → ℝ) : Π {u v : V}, G.directed_walk u v → ℝ
| u v nil := 1
| u v (cons h p) := wt ⟨_, h⟩ * walk_weight p

Both of those definition did not seem to work. So I modified the second one to

def walk_weight2 (wt : V → V → ℝ) : Π {u v : V}, G.directed_walk u v → ℝ
| u v nil := 1
| u v (@cons V G _ x _ h p) := wt u x * walk_weight2 p

and alternatively formulated :

def walk_weight3 (wt : V → V → ℝ) : Π {u v : V}, G.directed_walk u v → ℝ
| u v nil := 1
| u v (@cons V G _ x _ h p) := by {have r1 := wt u x, have r2 := walk_weight3 p, exact (r1 * r2)}

Are both equivalent ?

[Kyle Miller]

Ah, right, I forgot the V and G arguments.

Yes, the two definitions are equivalent. The first is preferred since tactics can obscure the precise expressions used in a definition. Just so you know about it (and I'm not suggesting you use it here), you can use let expressions. Again untested, but rather than by {have r1 := wt u x, have r2 := walk_weight3 p, exact (r1 * r2)} you should be able to do let r1 := wt u x, r2 := walk_weight3 p in r1 * r2

[Christopher Schmidt]

Kyle Miller schrieb:

Ah, right, I forgot the V and G arguments.

Yes, the two definitions are equivalent. The first is preferred since tactics can obscure the precise expressions used in a definition. Just so you know about it (and I'm not suggesting you use it here), you can use let expressions. Again untested, but rather than by {have r1 := wt u x, have r2 := walk_weight3 p, exact (r1 * r2)} you should be able to do let r1 := wt u x, r2 := walk_weight3 p in r1 * r2

Ah I see. I am not familiar with all syntactic possibilities, so good to know. Thanks.

[Alistair Tucker]

(deleted)

[Junyan Xu]

Notice that have should only be used for proofs because it erases data; for data use let instead.