Shop problems in three-field notation
Lax434175.ShopProblems · concepts/Lax434175/ShopProblems.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
The family of shop problems has the constraint fields shop type, machines of the operations, number of machines, number of jobs, processing times, no-wait, no-idle, transportation delays, a server, batch setups, release dates, deadlines and precedence constraints between jobs, and the completion-time objectives.
A problem with one of , , , possibly followed by a number of machines, is one specification of this family. Without an entry on machine sets, the operations of an open shop or flow shop occupy the machines by position and those of a job shop occupy dedicated machines. For example and are the specifications below. The concept on one family for shops joins these problems and the preemptive shop problems into a single family with an interruption field.
Theorem. 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 describes a problem whose decision version reduces to that of the other. In particular is a special case of .
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.Assembly |
| 2 | import Lax434175.Counts |
| 3 | import Lax434175.ReleaseDates |
| 4 | import Lax434175.Deadlines |
| 5 | import Lax434175.Precedence |
| 6 | import Lax434175.Thresholds |
| 7 | import Lax434175.Shops |
| 8 | import Lax434175.Transportation |
| 9 | import Lax434175.Servers |
| 10 | import Lax434175.ShopExtras |
| 11 | |
| 12 | /-! |
| 13 | --- |
| 14 | title: Shop problems in three-field notation |
| 15 | type: theorem |
| 16 | --- |
| 17 | The family of shop problems has the constraint fields shop type, machines of |
| 18 | the operations, number of machines, number of jobs, processing times, no-wait, no-idle, transportation |
| 19 | delays, a server, batch setups, release dates, deadlines and precedence constraints between jobs, and the completion-time objectives. |
| 20 | |
| 21 | A problem with one of , , , |
| 22 | possibly followed by a number of machines, is one specification of this |
| 23 | family. Without an entry on machine sets, the operations of an open shop or |
| 24 | flow shop occupy the machines by position and those of a job shop occupy |
| 25 | dedicated machines. For example and |
| 26 | are the specifications below. |
| 27 | The concept on one family for shops joins these problems and the preemptive |
| 28 | shop problems into a single family with an interruption field. |
| 29 | |
| 30 | **Theorem.** A specification that is field by field a special case of |
| 31 | another describes a special case of the other's problem, and a specification |
| 32 | that reduces to another describes a problem whose decision version reduces |
| 33 | to that of the other. In particular |
| 34 | is a special case of . |
| 35 | -/ |
| 36 | |
| 37 | namespace Lax434175.ShopProblems |
| 38 | open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly |
| 39 | open Lax434175 |
| 40 | |
| 41 | /-- The constraint fields of the family. -/ |
| 42 | inductive FieldName |
| 43 | | shopType |
| 44 | | machineSets |
| 45 | | machineCount |
| 46 | | jobCount |
| 47 | | processingTimes |
| 48 | | noWait |
| 49 | | transportation |
| 50 | | server |
| 51 | | noIdle |
| 52 | | batchSetups |
| 53 | | releaseDates |
| 54 | | deadlines |
| 55 | | precedence |
| 56 | deriving DecidableEq |
| 57 | |
| 58 | instance : Fintype FieldName where |
| 59 | elems := {.shopType, .machineSets, .machineCount, .jobCount, .processingTimes, .noWait, .transportation, .server, .noIdle, .batchSetups, .releaseDates, |
| 60 | .deadlines, .precedence} |
| 61 | complete x := by cases x <;> decide |
| 62 | |
| 63 | /-- The shop problems. -/ |
| 64 | abbrev family : Family Shops.kernel := |
| 65 | Thresholds.family FieldName fun |
| 66 | | .shopType => Shops.shopType |
| 67 | | .machineSets => Shops.machineSets |
| 68 | | .machineCount => Counts.module _ Shops.machines 1 |
| 69 | | .jobCount => Counts.module _ Shops.kernel.jobs |
| 70 | | .processingTimes => Shops.processingTimes |
| 71 | | .noWait => Shops.noWait |
| 72 | | .transportation => Transportation.module |
| 73 | | .server => Servers.shop |
| 74 | | .noIdle => ShopExtras.noIdle |
| 75 | | .batchSetups => ShopExtras.batchSetups |
| 76 | | .releaseDates => ReleaseDates.module _ |
| 77 | | .deadlines => Deadlines.module _ |
| 78 | | .precedence => Precedence.module _ Shops.machines |
| 79 | |
| 80 | instance : Fintype family.ModuleName := inferInstanceAs (Fintype FieldName) |
| 81 | |
| 82 | /-- The specification `α | β | γ` of a shop problem. -/ |
| 83 | def spec (shopType : Shops.ShopType) |
| 84 | (machineSets : Shops.Machines) |
| 85 | (machineCount : Counts.Bound := .any) |
| 86 | (jobCount : Counts.Bound := .any) |
| 87 | (processingTimes : Shops.ProcessingTimes := .arbitrary) |
| 88 | (waiting : Shops.NoWait := .none) |
| 89 | (transportation : Transportation.Value := .none) |
| 90 | (server : Servers.Value := .none) |
| 91 | (idling : ShopExtras.NoIdle := .none) |
| 92 | (setups : ShopExtras.BatchSetups := .none) |
| 93 | (release : ReleaseDates.Value := .none) |
| 94 | (deadline : Deadlines.Value := .none) |
| 95 | (precedence : Precedence.Value := .none) |
| 96 | (objective : Objectives.Value) : Spec family where |
| 97 | module |
| 98 | | .shopType => shopType |
| 99 | | .machineSets => machineSets |
| 100 | | .machineCount => machineCount |
| 101 | | .jobCount => jobCount |
| 102 | | .processingTimes => processingTimes |
| 103 | | .noWait => waiting |
| 104 | | .transportation => transportation |
| 105 | | .server => server |
| 106 | | .noIdle => idling |
| 107 | | .batchSetups => setups |
| 108 | | .releaseDates => release |
| 109 | | .deadlines => deadline |
| 110 | | .precedence => precedence |
| 111 | objective := objective |
| 112 | |
| 113 | /-- `F2 || C_max` -/ |
| 114 | def flow2_makespan : Spec family := |
| 115 | spec (shopType := .flow) (machineSets := .byPosition) (machineCount := .atMost 2) (objective := .makespan) |
| 116 | |
| 117 | /-- `J | r_j | L_max` -/ |
| 118 | def job_release_lmax : Spec family := |
| 119 | spec (shopType := .job) (machineSets := .dedicated) (release := .releaseDates) (objective := .lmax) |
| 120 | |
| 121 | axiom family_sound : family.Sound |
| 122 | |
| 123 | axiom specialCase_of_le {s t : Spec family} : |
| 124 | s.le t → SpecialCase (problem family s) (problem family t) |
| 125 | |
| 126 | axiom reducible_of_reduces {s t : Spec family} : |
| 127 | Thresholds.Reduces s t → Reducible (problem family s) (problem family t) |
| 128 | |
| 129 | axiom flow2_makespan_specialCase : |
| 130 | SpecialCase (problem family flow2_makespan) (problem family job_release_lmax) |
| 131 | |
| 132 | end Lax434175.ShopProblems |
| 133 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments