Constraint modules and objectives
Lax434175.Modules · concepts/Lax434175/Modules.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A scheduling problem over a kernel is described by choosing one value in each of several independent fields. A field is a constraint module or an objective.
A constraint module offers, for each of its values, additional instance data, a condition that this data must satisfy, and a constraint on schedules stated in terms of the data. Release dates are a constraint module with two values: the value "none" carries no data, the value "release dates" carries one number per job, and no job may start before its release date. A module may also carry no data at all and only restrict the instances of the kernel: identical machines is such a restriction of unrelated machines.
An objective offers, for each value, additional instance data, a condition that this data must satisfy, and a cost.
Every field comes with a decidable relation "is a special case of" on its values and a map that turns the data of a value into data of a more general value. The field is sound if this map does not change the meaning: admissible data stays admissible, for admissible data the constraint is equivalent, and the cost is equal.
Concept map
Lean source view on GitHub
| 1 | import Lax434175.Kernels |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Constraint modules and objectives |
| 6 | type: definition |
| 7 | --- |
| 8 | A scheduling problem over a kernel is described by choosing one value in each |
| 9 | of several independent fields. A field is a constraint module or an |
| 10 | objective. |
| 11 | |
| 12 | A constraint module offers, for each of its values, additional instance data, |
| 13 | a condition that this data must satisfy, and a constraint on schedules stated |
| 14 | in terms of the data. Release dates are a constraint module with two values: |
| 15 | the value "none" carries no data, the value "release dates" carries one |
| 16 | number per job, and no job may start before its release date. A module may |
| 17 | also carry no data at all and only restrict the instances of the kernel: |
| 18 | identical machines is such a restriction of unrelated machines. |
| 19 | |
| 20 | An objective offers, for each value, additional instance data, a condition |
| 21 | that this data must satisfy, and a cost. |
| 22 | |
| 23 | Every field comes with a decidable relation "is a special case of" on its |
| 24 | values and a map that turns the data of a value into data of a more general |
| 25 | value. The field is sound if this map does not change the meaning: admissible |
| 26 | data stays admissible, for admissible data the constraint is equivalent, and |
| 27 | the cost is equal. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax434175.Modules |
| 31 | open Lax434175.Kernels |
| 32 | |
| 33 | /-- A field whose values add data to an instance and a constraint on its |
| 34 | schedules. -/ |
| 35 | structure Module (K : Kernel) where |
| 36 | Value : Type |
| 37 | /-- The data a value adds to an instance. -/ |
| 38 | Data : Value → K.Inst → Type |
| 39 | /-- The condition a value imposes on an instance and its data. -/ |
| 40 | admits : (v : Value) → (x : K.Inst) → Data v x → Prop |
| 41 | /-- The constraint a value imposes on the schedules. -/ |
| 42 | constraint : (v : Value) → (x : K.Inst) → Data v x → K.Sched x → Prop |
| 43 | /-- `le v w`: the value `v` is a special case of `w`. -/ |
| 44 | le : Value → Value → Bool |
| 45 | /-- Data of a value read as data of a more general value. -/ |
| 46 | embed : {v w : Value} → le v w = true → (x : K.Inst) → Data v x → Data w x |
| 47 | |
| 48 | /-- Reading data with a more general value keeps it admissible and does not |
| 49 | change the constraint. -/ |
| 50 | structure Module.Sound {K : Kernel} (M : Module K) : Prop where |
| 51 | admits : ∀ (v w : M.Value) (h : M.le v w = true) (x : K.Inst) (d : M.Data v x), |
| 52 | M.admits v x d → M.admits w x (M.embed h x d) |
| 53 | constraint : ∀ (v w : M.Value) (h : M.le v w = true) (x : K.Inst) (d : M.Data v x) |
| 54 | (σ : K.Sched x), M.admits v x d → |
| 55 | (M.constraint w x (M.embed h x d) σ ↔ M.constraint v x d σ) |
| 56 | |
| 57 | /-- A module without data and without a constraint on schedules: each value |
| 58 | only restricts the instances of the kernel. -/ |
| 59 | def Module.ofRestriction {K : Kernel} (Value : Type) (holds : Value → K.Inst → Prop) |
| 60 | (le : Value → Value → Bool) : Module K where |
| 61 | Value := Value |
| 62 | Data _ _ := Unit |
| 63 | admits v x _ := holds v x |
| 64 | constraint _ _ _ _ := True |
| 65 | le := le |
| 66 | embed _ _ _ := () |
| 67 | |
| 68 | /-- A field whose values add data to an instance and determine the cost of a |
| 69 | schedule. -/ |
| 70 | structure Objective (K : Kernel) where |
| 71 | Value : Type |
| 72 | /-- The data a value adds to an instance. -/ |
| 73 | Data : Value → K.Inst → Type |
| 74 | /-- The condition a value imposes on an instance and its data. -/ |
| 75 | admits : (v : Value) → (x : K.Inst) → Data v x → Prop |
| 76 | /-- The cost of a schedule. -/ |
| 77 | cost : (v : Value) → (x : K.Inst) → Data v x → K.Sched x → ℚ |
| 78 | /-- `le v w`: the value `v` is a special case of `w`. -/ |
| 79 | le : Value → Value → Bool |
| 80 | /-- Data of a value read as data of a more general value. -/ |
| 81 | embed : {v w : Value} → le v w = true → (x : K.Inst) → Data v x → Data w x |
| 82 | |
| 83 | /-- Reading data with a more general value keeps it admissible and does not |
| 84 | change the cost. -/ |
| 85 | structure Objective.Sound {K : Kernel} (O : Objective K) : Prop where |
| 86 | admits : ∀ (v w : O.Value) (h : O.le v w = true) (x : K.Inst) (d : O.Data v x), |
| 87 | O.admits v x d → O.admits w x (O.embed h x d) |
| 88 | cost : ∀ (v w : O.Value) (h : O.le v w = true) (x : K.Inst) (d : O.Data v x) |
| 89 | (σ : K.Sched x), O.cost w x (O.embed h x d) σ = O.cost v x d σ |
| 90 | |
| 91 | end Lax434175.Modules |
| 92 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments