Word Encoding of an Instance
Lax496464.WordEncoding · concepts/Lax496464/WordEncoding.lean · lax-496464
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is handed to a word random access machine as a word of numbers: the number of jobs, the number of machines, then the preprocessing times, the processing times, the due dates and the weights, in that order. A decision instance appends the threshold as a final entry.
Concept map
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Lax496464.FlowShop |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Word Encoding of an Instance |
| 6 | type: definition |
| 7 | --- |
| 8 | An instance is handed to a word random access machine as a word of numbers: the number |
| 9 | of jobs, the number of machines, then the preprocessing times, the |
| 10 | processing times, the due dates and the weights, in that order. A decision |
| 11 | instance appends the threshold as a final entry. |
| 12 | |
| 13 | # Formalization Notes |
| 14 | |
| 15 | This is the point at which magnitudes stop being free. The preprocessing times, |
| 16 | processing times, due dates and weights are entries of the word, so a claim about a |
| 17 | program reading it has to say that they are words — which the fitting conditions state, |
| 18 | once, as an explicit inequality against . A size measure counting only the number of |
| 19 | jobs would make the due dates of a reduction's output invisible, and a running time |
| 20 | stated against it would not be a claim about anything a machine does. |
| 21 | |
| 22 | Cells are read with `List.getD`, which returns outside the word. The length condition |
| 23 | pins the word down completely, so the default is never reached at a position the other |
| 24 | conditions constrain, and a word of the right length determines its instance. |
| 25 | |
| 26 | The threshold is appended last, so that the instance block sits at the same offsets |
| 27 | whether or not a threshold follows it, and the split of the word into its two parts is |
| 28 | determined by the word rather than chosen. |
| 29 | |
| 30 | Unlike the instance itself, the word carries no start times: is |
| 31 | computed from the word, one subtraction per job, and appears in the predicates below |
| 32 | rather than in the format. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax496464.WordEncoding |
| 36 | |
| 37 | open Lax496464.FlowShop Lax496464.FlowShop.Instance |
| 38 | |
| 39 | /-- The number of jobs declared by a word: its first entry. -/ |
| 40 | def jobCount (x : List ℕ) : ℕ := x.getD 0 0 |
| 41 | |
| 42 | /-- The number of machines declared by a word: its second entry. -/ |
| 43 | def machineCount (x : List ℕ) : ℕ := x.getD 1 0 |
| 44 | |
| 45 | /-- The preprocessing time of job `j`, from the block following the two header |
| 46 | entries. -/ |
| 47 | def preTime (x : List ℕ) (j : ℕ) : ℕ := x.getD (2 + j) 0 |
| 48 | |
| 49 | /-- The processing time of job `j`, from the block following the preprocessing times. -/ |
| 50 | def procTime (x : List ℕ) (j : ℕ) : ℕ := x.getD (2 + jobCount x + j) 0 |
| 51 | |
| 52 | /-- The due date of job `j`, from the block following the processing times. -/ |
| 53 | def due (x : List ℕ) (j : ℕ) : ℕ := x.getD (2 + 2 * jobCount x + j) 0 |
| 54 | |
| 55 | /-- The weight of job `j`, from the block following the due dates. -/ |
| 56 | def wt (x : List ℕ) (j : ℕ) : ℕ := x.getD (2 + 3 * jobCount x + j) 0 |
| 57 | |
| 58 | /-- The threshold of a decision instance: the entry following the four blocks. -/ |
| 59 | def threshold (x : List ℕ) : ℕ := x.getD (2 + 4 * jobCount x) 0 |
| 60 | |
| 61 | /-- The start time `s j = d j - q j` of job `j`, as read off the word. -/ |
| 62 | def start (x : List ℕ) (j : ℕ) : ℤ := (due x j : ℤ) - procTime x j |
| 63 | |
| 64 | /-- The word `x` encodes the instance `I`. -/ |
| 65 | structure EncodesInstance (x : List ℕ) (I : Instance) : Prop where |
| 66 | /-- The word declares `I`'s jobs. -/ |
| 67 | jobCount_eq : jobCount x = I.jobs |
| 68 | /-- The word declares `I`'s machines. -/ |
| 69 | machineCount_eq : machineCount x = I.machines |
| 70 | /-- The word is the two header entries followed by four blocks of one number per job. -/ |
| 71 | length_eq : x.length = 2 + 4 * I.jobs |
| 72 | /-- The preprocessing times are `I`'s. -/ |
| 73 | preTime_eq : ∀ j : I.Job, preTime x j = I.p j |
| 74 | /-- The processing times are `I`'s. -/ |
| 75 | procTime_eq : ∀ j : I.Job, procTime x j = I.q j |
| 76 | /-- The due dates are `I`'s. -/ |
| 77 | due_eq : ∀ j : I.Job, due x j = I.d j |
| 78 | /-- The weights are `I`'s. -/ |
| 79 | wt_eq : ∀ j : I.Job, wt x j = I.w j |
| 80 | |
| 81 | /-- The word `x` presents the instance `I` together with the threshold `W`: an instance |
| 82 | block followed by the single entry `W`. -/ |
| 83 | def EncodesDecisionInstance (x : List ℕ) (I : Instance) (W : ℕ) : Prop := |
| 84 | ∃ y, x = y ++ [W] ∧ EncodesInstance y I |
| 85 | |
| 86 | /-- The words that encode an instance, with no threshold. -/ |
| 87 | def Instances : Set (List ℕ) := {x | ∃ I, EncodesInstance x I} |
| 88 | |
| 89 | /-- The words that encode a decision instance. -/ |
| 90 | def DecisionInstances : Set (List ℕ) := {x | ∃ I W, EncodesDecisionInstance x I W} |
| 91 | |
| 92 | end Lax496464.WordEncoding |
| 93 |
Formalization Notes
This is the point at which magnitudes stop being free. The preprocessing times, processing times, due dates and weights are entries of the word, so a claim about a program reading it has to say that they are words — which the fitting conditions state, once, as an explicit inequality against . A size measure counting only the number of jobs would make the due dates of a reduction's output invisible, and a running time stated against it would not be a claim about anything a machine does.
Cells are read with , which returns outside the word. The length condition pins the word down completely, so the default is never reached at a position the other conditions constrain, and a word of the right length determines its instance.
The threshold is appended last, so that the instance block sits at the same offsets whether or not a threshold follows it, and the split of the word into its two parts is determined by the word rather than chosen.
Unlike the instance itself, the word carries no start times: is computed from the word, one subtraction per job, and appears in the predicates below rather than in the format.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments