Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Word Encoding of an Instance

Lax117284.InstanceEncoding · concepts/Lax117284/InstanceEncoding.lean · lax-117284

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    An instance is handed to a word random access machine as a word of numbers: the number nn of clients, the number mm of days, then the nmnm processing times day by day, then the nmnm due dates day by day. A decision instance of 1∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j} appends the fairness parameter as a final entry, and a decision instance of the per-client problem appends one parameter per client.

    A word determines the instance it encodes, so notions defined for instances — the number of days, the treewidth of the overall conflict graph — are notions of the word as well.

    Concept map
    4 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 decode_eq proven

    2 encodesInstance_unique proven

    Lean source view on GitHub

    1import Lax117284.ConflictGraph
    2
    3/-!
    4---
    5title: Word Encoding of an Instance
    6type: definition
    7---
    8An instance is handed to a word random access machine as a word of numbers: the number nn
    9of clients, the number mm of days, then the nmnm processing times day by day, then the nmnm
    10due dates day by day. A decision instance of
    111∣rep∣min⁡j∑iZi,j1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j} appends the fairness parameter as a final
    12entry, and a decision instance of the per-client problem appends one parameter per client.
    13
    14A word determines the instance it encodes, so notions defined for instances — the number of
    15days, the treewidth of the overall conflict graph — are notions of the word as well.
    16
    17# Formalization Notes
    18
    19This is the point at which magnitudes stop being free. The processing times and due dates
    20are entries of the word, so a claim about a program reading it has to say that they are
    21words, which the fitting condition of the parameterized notions does. A size measure
    22counting only the number of clients and days would make the due dates of an instance
    23invisible and a running time stated against it would not be a claim about anything a
    24machine does.
    25
    26Cells are read with `List.getD`, which returns `0` outside the word; the length condition
    27pins the word down completely, so the default is never reached at a position the other
    28conditions constrain.
    29
    30The parameter is appended last, so that the instance block sits at the same positions
    31whether or not a parameter follows it, and the split of the word into its two parts is
    32determined by the word rather than chosen.
    33
    34Decoding is stated as a function into instances, undefined — an instance with no client and
    35no day — on the words that encode none. That a word encodes at most one instance is a
    36statement rather than a convention, and it is what makes the decoded instance a function of
    37the word.
    38-/
    39
    40namespace Lax117284.InstanceEncoding
    41
    42open Lax117284.Scheduling
    43
    44/-- The number of clients declared by a word: its first entry. -/
    45def clientCount (x : List ℕ) : ℕ := x.getD 0 0
    46
    47/-- The number of days declared by a word: its second entry. -/
    48def dayCount (x : List ℕ) : ℕ := x.getD 1 0
    49
    50/-- The processing time of client `j`'s job on day `i`: the processing times follow the two
    51header entries, day by day. -/
    52def proc (x : List ℕ) (i j : ℕ) : ℕ := x.getD (2 + i * clientCount x + j) 0
    53
    54/-- The due date of client `j`'s job on day `i`: the due dates follow the processing
    55times. -/
    56def due (x : List ℕ) (i j : ℕ) : ℕ :=
    57 x.getD (2 + dayCount x * clientCount x + i * clientCount x + j) 0
    58
    59/-- The word `x` encodes the instance `I`. -/
    60structure EncodesInstance (x : List ℕ) (I : Instance) : Prop where
    61 /-- The word declares `I`'s clients. -/
    62 clientCount_eq : clientCount x = I.clients
    63 /-- The word declares `I`'s days. -/
    64 dayCount_eq : dayCount x = I.days
    65 /-- The word consists of the two header entries and the two arrays of one number per
    66 job. -/
    67 length_eq : x.length = 2 + 2 * I.days * I.clients
    68 /-- The processing times are `I`'s. -/
    69 proc_eq : ∀ (i : Fin I.days) (j : Fin I.clients), proc x i j = I.p i j
    70 /-- The due dates are `I`'s. -/
    71 due_eq : ∀ (i : Fin I.days) (j : Fin I.clients), due x i j = I.d i j
    72
    73/-- The word `x` presents the instance `I` together with the fairness parameter `k`: an
    74instance block followed by the single entry `k`. -/
    75def EncodesUniform (x : List ℕ) (I : Instance) (k : ℕ) : Prop :=
    76 ∃ y, x = y ++ [k] ∧ EncodesInstance y I
    77
    78/-- The word `x` presents the instance `I` together with one fairness parameter per
    79client. -/
    80def EncodesPerClient (x : List ℕ) (I : Instance) (k : Fin I.clients → ℕ) : Prop :=
    81 ∃ y, x = y ++ (List.ofFn k) ∧ EncodesInstance y I
    82
    83/-- The words that encode an instance and a fairness parameter. -/
    84def UniformInstances : Set (List ℕ) := {x | ∃ I k, EncodesUniform x I k}
    85
    86/-- The instance with no client and no day, the value of the decoding on a word that
    87encodes no instance. -/
    88def empty : Instance where
    89 clients := 0
    90 days := 0
    91 p := fun i => i.elim0
    92 d := fun i => i.elim0
    93 p_pos := fun i => i.elim0
    94 p_le_d := fun i => i.elim0
    95
    96open Classical in
    97/-- The instance a word encodes, and `empty` on a word that encodes none. -/
    98noncomputable def decode (x : List ℕ) : Instance :=
    99 if h : ∃ I, EncodesInstance x I then h.choose else empty
    100
    101/-- The fairness parameter a word declares: its last entry. -/
    102def parameter (x : List ℕ) : ℕ := (x.getLast? ).getD 0
    103
    104/-- **A word encodes at most one instance.** -/
    105axiom encodesInstance_unique {x : List ℕ} {I J : Instance} (hI : EncodesInstance x I)
    106 (hJ : EncodesInstance x J) : I = J
    107
    108/-- **The decoding of a word that encodes an instance is that instance.** -/
    109axiom decode_eq {x : List ℕ} {I : Instance} (h : EncodesInstance x I) : decode x = I
    110
    111end Lax117284.InstanceEncoding
    112
    Show ProofShow Proof
    Formalization Notes

    This is the point at which magnitudes stop being free. The processing times and due dates are entries of the word, so a claim about a program reading it has to say that they are words, which the fitting condition of the parameterized notions does. A size measure counting only the number of clients and days would make the due dates of an instance invisible and a running time stated against it would not be a claim about anything a machine does.

    Cells are read with List.getDList.getD, which returns 00 outside the word; the length condition pins the word down completely, so the default is never reached at a position the other conditions constrain.

    The parameter is appended last, so that the instance block sits at the same positions whether or not a parameter follows it, and the split of the word into its two parts is determined by the word rather than chosen.

    Decoding is stated as a function into instances, undefined — an instance with no client and no day — on the words that encode none. That a word encodes at most one instance is a statement rather than a convention, and it is what makes the decoded instance a function of the word.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…