One family for parallel machines with and without preemption
Lax434175.ParallelFamily · concepts/Lax434175/ParallelFamily.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The problems on parallel machines form one family over the machine model with pieces: its fields are the interruption field and the fields of parallel machines (machine environment, number of machines, number of jobs, processing times, machine sets, release dates, deadlines, precedence constraints with time lags, communication delays, a server, forbidden times and the input encoding), and its objectives are the completion-time objectives. The entry of the three-field notation is the value preemption of the interruption field, the entry restarts the value restarts, and no entry the value none. The value preemption without migration has no machine model of its own.
A problem of the non-preemptive, the preemptive, or the restarts machine model determines the problem of this family with the same values in the common fields and the corresponding value of the interruption field.
Theorem. The two problems are special cases of each other, so that the family describes the problems of the three machine models faithfully. In the family, a specification that is field by field a special case of another describes a special case of the other's problem, and a specification that reduces to another, directly or through flow time, describes a problem whose decision version reduces to that of the other.
Concept map
Evidence
This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.
1 family_sound proven
2 nonpreemptive_faithful proven
3 preemptive_faithful proven
4 reducible_of_reduces proven
5 reducible_of_reducesThroughFlow proven
6 restarts_faithful proven
7 specialCase_of_le proven
Lean source view on GitHub
| 1 | import Lax434175.ParallelProblems |
| 2 | import Lax434175.Interruption |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: One family for parallel machines with and without preemption |
| 7 | type: theorem |
| 8 | --- |
| 9 | The problems on parallel machines form one family over the machine model with |
| 10 | pieces: its fields are the interruption field and the fields of parallel |
| 11 | machines (machine environment, number of machines, number of jobs, |
| 12 | processing times, machine sets, release dates, deadlines, precedence |
| 13 | constraints with time lags, communication delays, a server, forbidden times |
| 14 | and the input encoding), and its objectives are the completion-time |
| 15 | objectives. The entry of the three-field notation is the value |
| 16 | preemption of the interruption field, the entry restarts the value restarts, |
| 17 | and no entry the value none. The value preemption without migration has no |
| 18 | machine model of its own. |
| 19 | |
| 20 | A problem of the non-preemptive, the preemptive, or the restarts machine model |
| 21 | determines the problem of this family with the same values in the common |
| 22 | fields and the corresponding value of the interruption field. |
| 23 | |
| 24 | **Theorem.** The two problems are special cases of each other, so that the |
| 25 | family describes the problems of the three machine models faithfully. In |
| 26 | the family, a specification that is field by field a special case of another |
| 27 | describes a special case of the other's problem, and a specification that |
| 28 | reduces to another, directly or through flow time, describes a problem whose |
| 29 | decision version reduces to that of the other. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax434175.ParallelFamily |
| 33 | open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly |
| 34 | open Lax434175 |
| 35 | |
| 36 | /-- The fields of the family: interruption and the fields of parallel |
| 37 | machines. -/ |
| 38 | inductive FieldName |
| 39 | | interruption |
| 40 | | field (i : ParallelProblems.FieldName) |
| 41 | deriving DecidableEq |
| 42 | |
| 43 | instance : Fintype FieldName where |
| 44 | elems := {.interruption, .field .environment, .field .machineCount, .field .jobCount, |
| 45 | .field .processingTimes, .field .machineSets, .field .releaseDates, .field .deadlines, |
| 46 | .field .precedence, .field .communicationDelays, .field .server, .field .forbiddenTimes, |
| 47 | .field .encoding} |
| 48 | complete x := by |
| 49 | cases x with |
| 50 | | interruption => decide |
| 51 | | field i => cases i <;> decide |
| 52 | |
| 53 | /-- The problems on parallel machines. -/ |
| 54 | abbrev family : Family Interruption.kernel := |
| 55 | Thresholds.family FieldName fun |
| 56 | | .interruption => Interruption.module |
| 57 | | .field i => (ParallelProblems.family Interruption.model).module i |
| 58 | |
| 59 | instance : Fintype family.ModuleName := |
| 60 | inferInstanceAs (Fintype FieldName) |
| 61 | |
| 62 | /-- The specification `α | β | γ`. -/ |
| 63 | def spec (interruption : Interruption.Mode := .none) |
| 64 | (environment : ParallelMachines.Environment) |
| 65 | (machineCount : Counts.Bound := .any) |
| 66 | (jobCount : Counts.Bound := .any) |
| 67 | (machineSets : MachineSets.Value := .none) |
| 68 | (processingTimes : ParallelMachines.ProcessingTimes := .arbitrary) |
| 69 | (release : ReleaseDates.Value := .none) |
| 70 | (deadline : Deadlines.Value := .none) |
| 71 | (precedence : Precedence.Value := .none) |
| 72 | (communicationDelays : CommunicationDelays.Value := .none) |
| 73 | (server : Servers.Value := .none) |
| 74 | (forbiddenTimes : ForbiddenTimes.Value := .none) |
| 75 | (encoding : ForbiddenTimes.Encoding := .standard) |
| 76 | (objective : Objectives.Value) : Spec family where |
| 77 | module |
| 78 | | .interruption => interruption |
| 79 | | .field .environment => environment |
| 80 | | .field .machineCount => machineCount |
| 81 | | .field .jobCount => jobCount |
| 82 | | .field .processingTimes => processingTimes |
| 83 | | .field .machineSets => machineSets |
| 84 | | .field .releaseDates => release |
| 85 | | .field .deadlines => deadline |
| 86 | | .field .precedence => precedence |
| 87 | | .field .communicationDelays => communicationDelays |
| 88 | | .field .server => server |
| 89 | | .field .forbiddenTimes => forbiddenTimes |
| 90 | | .field .encoding => encoding |
| 91 | objective := objective |
| 92 | |
| 93 | /-- A specification of one machine model on parallel machines read in another: |
| 94 | the values of the fields are the same. -/ |
| 95 | def transSpec {M M' : ParallelMachines.Model} (s : Spec (ParallelProblems.family M)) : |
| 96 | Spec (ParallelProblems.family M') where |
| 97 | module |
| 98 | | .environment => s.module .environment |
| 99 | | .machineCount => s.module .machineCount |
| 100 | | .jobCount => s.module .jobCount |
| 101 | | .processingTimes => s.module .processingTimes |
| 102 | | .machineSets => s.module .machineSets |
| 103 | | .releaseDates => s.module .releaseDates |
| 104 | | .deadlines => s.module .deadlines |
| 105 | | .precedence => s.module .precedence |
| 106 | | .communicationDelays => s.module .communicationDelays |
| 107 | | .server => s.module .server |
| 108 | | .forbiddenTimes => s.module .forbiddenTimes |
| 109 | | .encoding => s.module .encoding |
| 110 | objective := s.objective |
| 111 | |
| 112 | /-- The specification of the family with the values of a specification of a |
| 113 | machine model on parallel machines and a way of interruption. -/ |
| 114 | def ofSpec {M : ParallelMachines.Model} (interruption : Interruption.Mode) |
| 115 | (s : Spec (ParallelProblems.family M)) : Spec family where |
| 116 | module |
| 117 | | .interruption => interruption |
| 118 | | .field i => (transSpec (M' := Interruption.model) s).module i |
| 119 | objective := s.objective |
| 120 | |
| 121 | axiom nonpreemptive_faithful (s : Spec ParallelProblems.nonpreemptive) : |
| 122 | SpecialCase (problem _ s) (problem family (ofSpec .none s)) ∧ |
| 123 | SpecialCase (problem family (ofSpec .none s)) (problem _ s) |
| 124 | |
| 125 | axiom preemptive_faithful (s : Spec ParallelProblems.preemptive) : |
| 126 | SpecialCase (problem _ s) (problem family (ofSpec .pmtn s)) ∧ |
| 127 | SpecialCase (problem family (ofSpec .pmtn s)) (problem _ s) |
| 128 | |
| 129 | axiom restarts_faithful (s : Spec ParallelProblems.restarts) : |
| 130 | SpecialCase (problem _ s) (problem family (ofSpec .restarts s)) ∧ |
| 131 | SpecialCase (problem family (ofSpec .restarts s)) (problem _ s) |
| 132 | |
| 133 | axiom family_sound : family.Sound |
| 134 | |
| 135 | axiom specialCase_of_le {s t : Spec family} : |
| 136 | s.le t → SpecialCase (problem family s) (problem family t) |
| 137 | |
| 138 | axiom reducible_of_reduces {s t : Spec family} : |
| 139 | Thresholds.Reduces s t → Reducible (problem family s) (problem family t) |
| 140 | |
| 141 | axiom reducible_of_reducesThroughFlow {s t : Spec family} : |
| 142 | Thresholds.ReducesThroughFlow s t → Reducible (problem family s) (problem family t) |
| 143 | |
| 144 | end Lax434175.ParallelFamily |
| 145 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments