Completion-time objectives
Lax434175.Objectives · concepts/Lax434175/Objectives.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let denote the completion time of job . The objective field has the values
- makespan, ,
- maximum lateness, ,
- total completion time, ,
- total weighted completion time, ,
- total tardiness, with ,
- total weighted tardiness, ,
- number of late jobs, with if and otherwise,
- weighted number of late jobs, ,
- number of jobs that are not just in time, with if and otherwise, and its weighted version ,
- total flow time, with for the release date , and its weighted version ,
- maximum flow time, , and its weighted version .
Maximizing the number of jobs that are on time, or just in time, is minimizing the number of jobs that are not.
Two values restrict the due dates: total weighted tardiness with a common due date, , and the weighted number of late jobs with due dates at most after the release dates, . Each is a special case of the unrestricted value, and a smaller of a larger one.
A value carries weights exactly if it is weighted and due dates exactly if it measures lateness, tardiness or being just in time. The makespan is the maximum lateness with ; the maximum over an empty set of jobs is taken to be . The four values measuring completion time or tardiness are the single expression , with where weights are absent and where due dates are absent; the two values counting late jobs are with the same convention for the weights.
A value is a special case of another value of the same kind that carries at least the same data.
Theorem. Over every kernel, the objective field is sound.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Group.Finset.Basic |
| 2 | import Mathlib.Data.Fintype.BigOperators |
| 3 | import Mathlib.Data.Finset.Lattice.Fold |
| 4 | import Mathlib.Data.NNRat.BigOperators |
| 5 | import Mathlib.Algebra.Order.Field.Rat |
| 6 | import Lax434175.Modules |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Completion-time objectives |
| 11 | type: theorem |
| 12 | --- |
| 13 | Let denote the completion time of job . The objective field has the |
| 14 | values |
| 15 | |
| 16 | - makespan, , |
| 17 | - maximum lateness, , |
| 18 | - total completion time, , |
| 19 | - total weighted completion time, , |
| 20 | - total tardiness, with , |
| 21 | - total weighted tardiness, , |
| 22 | - number of late jobs, with if and |
| 23 | otherwise, |
| 24 | - weighted number of late jobs, , |
| 25 | - number of jobs that are not just in time, with |
| 26 | if and otherwise, and its weighted version |
| 27 | , |
| 28 | - total flow time, with for the release date |
| 29 | , and its weighted version , |
| 30 | - maximum flow time, , and its weighted version |
| 31 | . |
| 32 | |
| 33 | Maximizing the number of jobs that are on time, or just in time, is |
| 34 | minimizing the number of jobs that are not. |
| 35 | |
| 36 | Two values restrict the due dates: total weighted tardiness with a common |
| 37 | due date, , and the weighted number of late jobs with due dates at |
| 38 | most after the release dates, . Each is a special case |
| 39 | of the unrestricted value, and a smaller of a larger one. |
| 40 | |
| 41 | A value carries weights exactly if it is weighted and due dates |
| 42 | exactly if it measures lateness, tardiness or being just in time. The makespan is the maximum |
| 43 | lateness with ; the maximum over an empty set of jobs is taken to |
| 44 | be . The four values measuring |
| 45 | completion time or tardiness are the single expression |
| 46 | , with where weights are absent and |
| 47 | where due dates are absent; the two values counting late jobs are |
| 48 | with the same convention for the weights. |
| 49 | |
| 50 | A value is a special case of another value of the same kind that carries at |
| 51 | least the same data. |
| 52 | |
| 53 | **Theorem.** Over every kernel, the objective field is sound. |
| 54 | -/ |
| 55 | |
| 56 | namespace Lax434175.Objectives |
| 57 | open Lax434175.Kernels Lax434175.Modules |
| 58 | |
| 59 | inductive Value |
| 60 | | makespan |
| 61 | | lmax |
| 62 | | sumC |
| 63 | | sumWC |
| 64 | | sumT |
| 65 | | sumWT |
| 66 | | sumU |
| 67 | | sumWU |
| 68 | | sumZ |
| 69 | | sumWZ |
| 70 | | sumF |
| 71 | | sumWF |
| 72 | | fmax |
| 73 | | maxWF |
| 74 | | sumWTCommon |
| 75 | | sumWUWindow (k : ℕ) |
| 76 | deriving DecidableEq |
| 77 | |
| 78 | /-- How the cost is formed from the completion times. -/ |
| 79 | inductive Kind |
| 80 | | maximum |
| 81 | | tardiness |
| 82 | | late |
| 83 | | notJustInTime |
| 84 | | flow |
| 85 | | maximumFlow |
| 86 | deriving DecidableEq |
| 87 | |
| 88 | def kind : Value → Kind |
| 89 | | .makespan | .lmax => .maximum |
| 90 | | .sumC | .sumWC | .sumT | .sumWT | .sumWTCommon => .tardiness |
| 91 | | .sumU | .sumWU | .sumWUWindow _ => .late |
| 92 | | .sumZ | .sumWZ => .notJustInTime |
| 93 | | .sumF | .sumWF => .flow |
| 94 | | .fmax | .maxWF => .maximumFlow |
| 95 | |
| 96 | /-- Whether the value carries weights. -/ |
| 97 | def weighted : Value → Bool |
| 98 | | .sumWC | .sumWT | .sumWU | .sumWZ | .sumWF | .maxWF | .sumWTCommon | .sumWUWindow _ => true |
| 99 | | _ => false |
| 100 | |
| 101 | /-- Whether the value carries due dates. -/ |
| 102 | def hasDueDates : Value → Bool |
| 103 | | .lmax | .sumT | .sumWT | .sumU | .sumWU | .sumZ | .sumWZ | .sumWTCommon | .sumWUWindow _ => true |
| 104 | | _ => false |
| 105 | |
| 106 | /-- Weights where the value is weighted, due dates where it has them. -/ |
| 107 | def Data (K : Kernel) : Value → K.Inst → Type |
| 108 | | .makespan, _ | .sumC, _ | .sumF, _ | .fmax, _ => Unit |
| 109 | | .lmax, x | .sumWC, x | .sumT, x | .sumU, x | .sumZ, x | .sumWF, x | .maxWF, x => |
| 110 | Fin (K.jobs x) → ℕ |
| 111 | | .sumWT, x | .sumWU, x | .sumWZ, x | .sumWTCommon, x | .sumWUWindow _, x => |
| 112 | (Fin (K.jobs x) → ℕ) × (Fin (K.jobs x) → ℕ) |
| 113 | |
| 114 | /-- The weight of a job; `1` when the value is unweighted. -/ |
| 115 | def weight {K : Kernel} {x : K.Inst} : (v : Value) → Data K v x → Fin (K.jobs x) → ℕ |
| 116 | | .sumWC, w | .sumWF, w | .maxWF, w => w |
| 117 | | .sumWT, d | .sumWU, d | .sumWZ, d | .sumWTCommon, d | .sumWUWindow _, d => d.1 |
| 118 | | .makespan, _ | .lmax, _ | .sumC, _ | .sumT, _ | .sumU, _ | .sumZ, _ | .sumF, _ |
| 119 | | .fmax, _ => fun _ => 1 |
| 120 | |
| 121 | /-- The due date of a job; `0` when the value has no due dates. -/ |
| 122 | def dueDate {K : Kernel} {x : K.Inst} : (v : Value) → Data K v x → Fin (K.jobs x) → ℕ |
| 123 | | .lmax, d | .sumT, d | .sumU, d | .sumZ, d => d |
| 124 | | .sumWT, d | .sumWU, d | .sumWZ, d | .sumWTCommon, d | .sumWUWindow _, d => d.2 |
| 125 | | .makespan, _ | .sumC, _ | .sumWC, _ | .sumF, _ | .sumWF, _ | .fmax, _ | .maxWF, _ => |
| 126 | fun _ => 0 |
| 127 | |
| 128 | /-- The cost of a schedule. Subtraction of nonnegative rationals is |
| 129 | truncated, so `C - d` is the tardiness `max(0, C - d)`. -/ |
| 130 | def cost {K : Kernel} (v : Value) (x : K.Inst) (d : Data K v x) (σ : K.Sched x) : ℚ := |
| 131 | match kind v with |
| 132 | | .maximum => |
| 133 | if h : 0 < K.jobs x then |
| 134 | Finset.univ.sup' ⟨⟨0, h⟩, Finset.mem_univ _⟩ |
| 135 | (fun j => (K.completion x σ j : ℚ) - (dueDate v d j : ℚ)) |
| 136 | else 0 |
| 137 | | .tardiness => |
| 138 | ((∑ j, (weight v d j : NNRat) * (K.completion x σ j - (dueDate v d j : NNRat)) : NNRat) : ℚ) |
| 139 | | .late => |
| 140 | ((∑ j, (weight v d j : NNRat) * |
| 141 | (if (dueDate v d j : NNRat) < K.completion x σ j then 1 else 0) : NNRat) : ℚ) |
| 142 | | .notJustInTime => |
| 143 | ((∑ j, (weight v d j : NNRat) * |
| 144 | (if K.completion x σ j = (dueDate v d j : NNRat) then 0 else 1) : NNRat) : ℚ) |
| 145 | | .flow => |
| 146 | ((∑ j, (weight v d j : NNRat) * (K.completion x σ j - (K.release x j : NNRat)) : NNRat) : ℚ) |
| 147 | | .maximumFlow => |
| 148 | ((Finset.univ.sup fun j => |
| 149 | (weight v d j : NNRat) * (K.completion x σ j - (K.release x j : NNRat)) : NNRat) : ℚ) |
| 150 | |
| 151 | /-- The condition on the due dates of the two restricted values. -/ |
| 152 | def admits {K : Kernel} : (v : Value) → (x : K.Inst) → Data K v x → Prop |
| 153 | | .sumWTCommon, _, d => ∃ c, ∀ j, d.2 j = c |
| 154 | | .sumWUWindow k, x, d => ∀ j, d.2 j ≤ K.release x j + k |
| 155 | | _, _, _ => True |
| 156 | |
| 157 | /-- Comparison of the restrictions on the due dates. -/ |
| 158 | def restrictionLe : Value → Value → Bool |
| 159 | | .sumWTCommon, .sumWTCommon => true |
| 160 | | .sumWUWindow k, .sumWUWindow l => decide (k ≤ l) |
| 161 | | _, .sumWTCommon => false |
| 162 | | _, .sumWUWindow _ => false |
| 163 | | _, _ => true |
| 164 | |
| 165 | def le (v w : Value) : Bool := |
| 166 | decide (kind v = kind w) && (!weighted v || weighted w) && (!hasDueDates v || hasDueDates w) && |
| 167 | restrictionLe v w |
| 168 | |
| 169 | def embed {K : Kernel} : {v w : Value} → le v w = true → (x : K.Inst) → Data K v x → Data K w x |
| 170 | | _, .makespan, _, _, _ | _, .sumC, _, _, _ | _, .sumF, _, _, _ | _, .fmax, _, _, _ => () |
| 171 | | v, .sumWC, _, _, d | v, .sumWF, _, _, d | v, .maxWF, _, _, d => weight v d |
| 172 | | v, .lmax, _, _, d | v, .sumT, _, _, d | v, .sumU, _, _, d | v, .sumZ, _, _, d => dueDate v d |
| 173 | | v, .sumWT, _, _, d | v, .sumWU, _, _, d | v, .sumWZ, _, _, d | v, .sumWTCommon, _, _, d |
| 174 | | v, .sumWUWindow _, _, _, d => (weight v d, dueDate v d) |
| 175 | |
| 176 | /-- The objective field over a kernel. -/ |
| 177 | def objective (K : Kernel) : Objective K where |
| 178 | Value := Value |
| 179 | Data := Data K |
| 180 | admits := admits |
| 181 | cost := cost |
| 182 | le := le |
| 183 | embed := embed |
| 184 | |
| 185 | axiom sound (K : Kernel) : (objective K).Sound |
| 186 | |
| 187 | end Lax434175.Objectives |
| 188 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments