Communication delays

Lax434175.CommunicationDelays · concepts/Lax434175/CommunicationDelays.lean · lax-434175

proven

Loading review…

Natural Language Statement

Theorem

The communication-delay field of a machine model on parallel machines has the values

none: no delays;
unit: a set of ordered pairs of jobs is given; if $(i, j)$ is such a pair and the two jobs are processed on different sets of machines, then job $j$ may not start before one time unit after the completion of job $i$ ;
general: for some ordered pairs of jobs a delay $c_{ij}$ is given, and the same holds with $c_{ij}$ in place of one time unit.

The pairs with a delay are those related by the precedence constraints of the problem; the delay adds to the precedence constraint only when the two jobs are not processed in the same place.

No delays is the special case without pairs; unit delays are the special case $c_{ij} = 1$ .

Theorem. Over every machine model, the communication-delay field is sound.

Concept map

4 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax434175.CommunicationDelays

⊢Lax434175Proofs.CommunicationDelays.sound

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.Order.Field.Rat
2	import Lax434175.ParallelMachines
3
4	/-!
5	---
6	title: Communication delays
7	type: theorem
8	---
9	The communication-delay field of a machine model on parallel machines has
10	the values
11
12	- none: no delays;
13	- unit: a set of ordered pairs of jobs is given; if $(i, j)$ is such a pair
14	and the two jobs are processed on different sets of machines, then job $j$
15	may not start before one time unit after the completion of job $i$ ;
16	- general: for some ordered pairs of jobs a delay $c_{ij}$ is given, and the
17	same holds with $c_{ij}$ in place of one time unit.
18
19	The pairs with a delay are those related by the precedence constraints of
20	the problem; the delay adds to the precedence constraint only when the two
21	jobs are not processed in the same place.
22
23	No delays is the special case without pairs; unit delays are the special
24	case $c_{ij} = 1$ .
25
26	Theorem. Over every machine model, the communication-delay field is
27	sound.
28	-/
29
30	namespace Lax434175.CommunicationDelays
31	open Lax434175.Kernels Lax434175.Modules Lax434175.ParallelMachines
32
33	inductive Value
34	\| none
35	\| unit
36	\| general
37
38	/-- The data of a value. -/
39	def Data : Value → Inst → Type
40	\| .none, _ => Unit
41	\| .unit, x => Fin x.jobs → Fin x.jobs → Prop
42	\| .general, x => Fin x.jobs → Fin x.jobs → ℕ → Prop
43
44	/-- `view v d i j c`: the pair `(i, j)` has the delay `c`. -/
45	def view {x : Inst} : (v : Value) → Data v x → Fin x.jobs → Fin x.jobs → ℕ → Prop
46	\| .none, _ => fun _ _ _ => False
47	\| .unit, r => fun i j c => r i j ∧ c = 1
48	\| .general, d => d
49
50	def le : Value → Value → Bool
51	\| .none, _ => true
52	\| .unit, .none => false
53	\| .unit, _ => true
54	\| .general, .general => true
55	\| .general, _ => false
56
57	def embed : {v w : Value} → le v w = true → (x : Inst) → Data v x → Data w x
58	\| _, .none, _, _, _ => ()
59	\| .none, .unit, _, _, _ => fun _ _ => False
60	\| .unit, .unit, _, _, d => d
61	\| v, .general, _, _, d => view v d
62	\| .general, .unit, h, _, _ => absurd h Bool.false_ne_true
63
64	/-- The communication-delay field of a machine model. -/
65	def module (M : Model) : Module M.kernel where
66	Value := Value
67	Data v x := Data v (M.inst x)
68	admits _ _ _ := True
69	constraint v x d σ := ∀ i j c, view v d i j c → ∀ S S', M.uses x σ i S → M.uses x σ j S' →
70	S ≠ S' →
71	(M.kernel.completion x σ (Fin.cast (M.jobs_eq x).symm i) : ℚ) + (c : ℚ) ≤
72	(M.kernel.start x σ (Fin.cast (M.jobs_eq x).symm j) : ℚ)
73	le := le
74	embed h x d := embed h (M.inst x) d
75
76	axiom sound (M : Model) : (module M).Sound
77
78	end Lax434175.CommunicationDelays
79