Maximum lateness against deadlines
Lax434175.DeadlineSteps · concepts/Lax434175/DeadlineSteps.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The maximum lateness is at most exactly if some schedule meets the deadlines ; a schedule that meets them has makespan at most the largest of them. So the decision version of a problem minimizing the maximum lateness without deadlines reduces to that of the problem with the deadlines that minimizes the makespan, with the largest deadline as threshold. If some is negative, or there are no jobs and is negative, the threshold is .
A specification of the family with operations, or of the batching family, reduces to through deadlines if minimizes the maximum lateness without deadlines and the specification obtained by giving it deadlines and the makespan as objective is field by field a special case of . The relation is decidable.
Theorem. In both families, a specification that reduces to another through deadlines describes a problem whose decision version reduces to that of the other.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.OperationsFamily |
| 2 | import Lax434175.BatchFamily |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Maximum lateness against deadlines |
| 7 | type: theorem |
| 8 | --- |
| 9 | The maximum lateness is at most exactly if some schedule meets the |
| 10 | deadlines ; a schedule that meets them has makespan at |
| 11 | most the largest of them. So the decision version of a problem minimizing the |
| 12 | maximum lateness without deadlines reduces to that of the problem with the |
| 13 | deadlines that minimizes the makespan, with the largest deadline as |
| 14 | threshold. If some is negative, or there are no jobs and is |
| 15 | negative, the threshold is . |
| 16 | |
| 17 | A specification of the family with operations, or of the batching family, |
| 18 | reduces to through deadlines if minimizes the maximum lateness without |
| 19 | deadlines and the specification obtained by giving it deadlines and the |
| 20 | makespan as objective is field by field a special case of . The relation is |
| 21 | decidable. |
| 22 | |
| 23 | **Theorem.** In both families, a specification that reduces to another through |
| 24 | deadlines describes a problem whose decision version reduces to that of the |
| 25 | other. |
| 26 | -/ |
| 27 | |
| 28 | namespace Lax434175.DeadlineSteps |
| 29 | open Lax434175.Problems Lax434175.Assembly |
| 30 | open Lax434175 |
| 31 | |
| 32 | /-- The value without deadlines. -/ |
| 33 | def noDeadlines : Deadlines.Value → Bool |
| 34 | | .none => true |
| 35 | | _ => false |
| 36 | |
| 37 | /-- The specification with deadlines and the makespan as objective. -/ |
| 38 | def opsWithDeadlines (s : Spec OperationsFamily.family) : Spec OperationsFamily.family where |
| 39 | module |
| 40 | | .deadlines => Deadlines.Value.deadlines |
| 41 | | i => s.module i |
| 42 | objective := .makespan |
| 43 | |
| 44 | /-- `s` minimizes the maximum lateness without deadlines, and with deadlines and |
| 45 | the makespan it is field by field a special case of `t`. -/ |
| 46 | def OpsReducesThroughDeadlines (s t : Spec OperationsFamily.family) : Prop := |
| 47 | Thresholds.objectiveOf s = .lmax ∧ noDeadlines (s.module .deadlines) = true ∧ (opsWithDeadlines s).le t |
| 48 | |
| 49 | instance (s t : Spec OperationsFamily.family) : Decidable (OpsReducesThroughDeadlines s t) := by |
| 50 | unfold OpsReducesThroughDeadlines |
| 51 | infer_instance |
| 52 | |
| 53 | /-- The batching specification with deadlines and the makespan as objective. -/ |
| 54 | def batchWithDeadlines (s : Spec BatchFamily.family) : Spec BatchFamily.family where |
| 55 | module |
| 56 | | .field .deadlines => Deadlines.Value.deadlines |
| 57 | | i => s.module i |
| 58 | objective := .makespan |
| 59 | |
| 60 | def BatchReducesThroughDeadlines (s t : Spec BatchFamily.family) : Prop := |
| 61 | Thresholds.objectiveOf s = .lmax ∧ noDeadlines (s.module (.field .deadlines)) = true ∧ |
| 62 | (batchWithDeadlines s).le t |
| 63 | |
| 64 | instance (s t : Spec BatchFamily.family) : Decidable (BatchReducesThroughDeadlines s t) := by |
| 65 | unfold BatchReducesThroughDeadlines |
| 66 | infer_instance |
| 67 | |
| 68 | axiom ops_reducible {s t : Spec OperationsFamily.family} : |
| 69 | OpsReducesThroughDeadlines s t → |
| 70 | Reducible (problem OperationsFamily.family s) (problem OperationsFamily.family t) |
| 71 | |
| 72 | axiom batch_reducible {s t : Spec BatchFamily.family} : |
| 73 | BatchReducesThroughDeadlines s t → |
| 74 | Reducible (problem BatchFamily.family s) (problem BatchFamily.family t) |
| 75 | |
| 76 | end Lax434175.DeadlineSteps |
| 77 |
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