Lax489179.WeightedAPSP

Weighted all-pairs shortest paths

concepts/Lax489179/WeightedAPSP.lean · lax-489179

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

An input is a directed graph on vertices $0,\ldots,n-1$ with optional integer edge weights. A walk may repeat vertices and its weight is the sum of its edge weights. We promise that every closed walk has nonnegative weight, and that each edge weight has absolute value at most $n^c$ , for a fixed positive integer $c$ .

For each ordered vertex pair the output is its minimum walk weight, or infinity exactly when there is no walk. An empty walk has weight zero, so every diagonal distance is zero under the promise. The specification uses all finite walks, not a bounded or approximate surrogate for shortest paths. Negative weights and disconnected graphs are both included.

The input array is the vertex count followed by the $n^2$ adjacency entries in row-major order. The output consists of all $n^2$ distances in the same order, without a header. Optional-integer encoding separates missing edges and infinite distances from finite zero. Producing the entire matrix is charged by the word-RAM execution semantics.

Lean source view on GitHub

1	import Lax489179.WordTime
2	import Lax489179.IntegerEncoding
3	import Mathlib.Data.List.FinRange
4
5	/-!
6	---
7	title: Weighted all-pairs shortest paths
8	type: definition
9	---
10	An input is a directed graph on vertices $0,\ldots,n-1$ with optional
11	integer edge weights. A walk may repeat vertices and its weight is the
12	sum of its edge weights. We promise that every closed walk has
13	nonnegative weight, and that each edge weight has absolute value at
14	most $n^c$ , for a fixed positive integer $c$ .
15
16	For each ordered vertex pair the output is its minimum walk weight,
17	or infinity exactly when there is no walk. An empty walk has weight
18	zero, so every diagonal distance is zero under the promise. The
19	specification uses all finite walks, not a bounded or approximate
20	surrogate for shortest paths. Negative weights and disconnected graphs
21	are both included.
22
23	The input array is the vertex count followed by the $n^2$ adjacency
24	entries in row-major order. The output consists of all $n^2$ distances
25	in the same order, without a header. Optional-integer encoding separates
26	missing edges and infinite distances from finite zero. Producing the
27	entire matrix is charged by the word-RAM execution semantics.
28	-/
29
30	namespace Lax489179.WeightedAPSP
31
32	structure Graph where
33	vertices : ℕ
34	edge : Fin vertices → Fin vertices → Option ℤ
35
36	inductive Walk (G : Graph) : Fin G.vertices → Fin G.vertices → ℤ → Prop
37	\| nil (v : Fin G.vertices) : Walk G v v 0
38	\| cons {u v z : Fin G.vertices} {a b : ℤ}
39	(edge : G.edge u v = some a) (tail : Walk G v z b) : Walk G u z (a + b)
40
41	def NoNegativeCycle (G : Graph) : Prop :=
42	∀ v d, Walk G v v d → 0 ≤ d
43
44	def BoundedWeights (c : ℕ) (G : Graph) : Prop :=
45	∀ u v z, G.edge u v = some z → z.natAbs ≤ G.vertices ^ c
46
47	def Distance (G : Graph) (u v : Fin G.vertices) : Option ℤ → Prop
48	\| none => ¬ ∃ d, Walk G u v d
49	\| some d => Walk G u v d ∧ ∀ d', Walk G u v d' → d ≤ d'
50
51	def encodeMatrix (n : ℕ) (matrix : Fin n → Fin n → Option ℤ) : List ℕ :=
52	(List.finRange n).flatMap fun i =>
53	(List.finRange n).map fun j => IntegerEncoding.encodeOption (matrix i j)
54
55	def encode (G : Graph) : List ℕ := G.vertices :: encodeMatrix G.vertices G.edge
56
57	def Correct (G : Graph) (output : List ℕ) : Prop :=
58	∃ matrix : Fin G.vertices → Fin G.vertices → Option ℤ,
59	output = encodeMatrix G.vertices matrix ∧ ∀ u v, Distance G u v (matrix u v)
60
61	def problem (c : ℕ) : WordTime.Problem where
62	Input := Graph
63	size := Graph.vertices
64	encode := encode
65	valid := fun G => BoundedWeights c G ∧ NoNegativeCycle G
66	correct := Correct
67
68	end Lax489179.WeightedAPSP
69

Builds on

Used by

From Mathlib

Mathlib.Data.List.FinRange

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Weighted all-pairs shortest paths

Flags

Flag this concept