Lax Lean Archive

The Just-in-Time Flow Shop as a Problem on Words

Lax496464.Problems · concepts/Lax496464/Problems.lean · lax-496464

definition

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

    The decision problem: given an encoded instance and a threshold WW, is there a feasible set of jobs of total weight at least WW? As a parameterized problem it is taken with the number mm of machines as its parameter, which is the parameterization of the paper's fourth corollary.

    Four further quantities of an instance appear in the running times of the paper's algorithms and are defined here as functions of the word: the threshold WW itself, the largest processing time qmax⁡q_{\max}, the total preprocessing time PP, and the width ω\omega — the largest number of jobs whose second operations are alive at one instant.

    Concept map
    6 concepts; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax496464.ParameterizedComplexity
    2import Mathlib.Data.Nat.Log
    3import Lax496464.WordEncoding
    4
    5/-!
    6---
    7title: The Just-in-Time Flow Shop as a Problem on Words
    8type: definition
    9---
    10The decision problem: given an encoded instance and a threshold WW, is there a feasible
    11set of jobs of total weight at least WW? As a parameterized problem it is taken with the
    12number mm of machines as its parameter, which is the parameterization of the paper's
    13fourth corollary.
    14
    15Four further quantities of an instance appear in the running times of the paper's
    16algorithms and are defined here as functions of the word: the threshold WW itself, the
    17largest processing time qmax⁡q_{\max}, the total preprocessing time PP, and the width
    18ω\omega — the largest number of jobs whose second operations are alive at one instant.
    19
    20# Formalization Notes
    21
    22The parameter is the word's second entry, so a program obtains it at no cost, and it is
    23manifestly a function of the input rather than something supplied beside it.
    24
    25ω\omega is defined as a maximum over the start times of the jobs rather than over all of
    26Z\mathbb{Z}. The two agree: the number of jobs alive is a step function that can only
    27increase at a start time, so its maximum is attained at one. Taking the maximum over a
    28finite set is what makes the definition a computation rather than a supremum, and it is
    29also how one would compute it.
    30
    31Both ω\omega and qmax⁡q_{\max} are read off the word rather than off the decoded instance,
    32for the same reason as the parameter: a running time stated in terms of a quantity that
    33is not a function of the input would not be a statement about a program. They occur in
    34bounds only; no claim of this submission asks a program to compute them.
    35
    36The running times below are stated as the paper states them, plus a term `sortCost` for
    37putting the jobs into earliest-start-time order. The paper's algorithmic sections open by
    38indexing the jobs that way and count nothing for it; a statement about a program reading
    39an arbitrary word has to, and one pass of a comparison sort is what it costs. Where the
    40paper's own bound already dominates nlog⁡nn \log n the term is omitted.
    41
    42A word outside the domain has no meaningful threshold, width or largest processing time.
    43These functions are total regardless, and nothing is claimed about their values there,
    44since every statement quantifies over admissible words only.
    45-/
    46
    47namespace Lax496464.Problems
    48
    49open Lax496464.FlowShop Lax496464.FlowShop.Instance
    50open Lax496464.WordEncoding Lax496464.ParameterizedComplexity
    51
    52/-- The number of jobs of `x` alive at time `t`, as read off the word. -/
    53def aliveAt (x : List ℕ) (t : ℤ) : ℕ :=
    54 ((List.range (jobCount x)).filter
    55 fun i => decide (start x i ≤ t ∧ t < (due x i : ℤ))).length
    56
    57/-- The **width** `ω` of `x`: the largest number of jobs alive at one instant. -/
    58def widthOf (x : List ℕ) : ℕ :=
    59 ((List.range (jobCount x)).map fun j => aliveAt x (start x j)).foldr max 0
    60
    61/-- The largest processing time `q_max` declared by `x`. -/
    62def qmaxOf (x : List ℕ) : ℕ :=
    63 ((List.range (jobCount x)).map (procTime x)).foldr max 0
    64
    65/-- `n log n` on a word of length `n`: the cost of putting the jobs of `x` into
    66earliest-start-time order, which the algorithmic sections of the paper assume has been
    67done. -/
    68def sortCost (x : List ℕ) : ℕ := (x.length + 1) * (Nat.log 2 (x.length + 2) + 1)
    69
    70/-- The total preprocessing time declared by `x`. -/
    71def preSum (x : List ℕ) : ℕ := ((List.range (jobCount x)).map (preTime x)).sum
    72
    73/-- A word is a yes-instance when its instance has a feasible set of weight at least its
    74threshold. -/
    75def Yes (x : List ℕ) : Prop :=
    76 ∃ (I : Instance) (W : ℕ), EncodesDecisionInstance x I W ∧ HasWeight I W
    77
    78/-- **Just-in-time scheduling in a two-stage flexible flow shop**, as a parameterized
    79problem with the number of machines as its parameter. -/
    80def byMachines : Problem where
    81 Domain := DecisionInstances
    82 Yes := Yes
    83 param x := machineCount x
    84
    85end Lax496464.Problems
    86
    Formalization Notes

    The parameter is the word's second entry, so a program obtains it at no cost, and it is manifestly a function of the input rather than something supplied beside it.

    ω\omega is defined as a maximum over the start times of the jobs rather than over all of Z\mathbb{Z}. The two agree: the number of jobs alive is a step function that can only increase at a start time, so its maximum is attained at one. Taking the maximum over a finite set is what makes the definition a computation rather than a supremum, and it is also how one would compute it.

    Both ω\omega and qmax⁡q_{\max} are read off the word rather than off the decoded instance, for the same reason as the parameter: a running time stated in terms of a quantity that is not a function of the input would not be a statement about a program. They occur in bounds only; no claim of this submission asks a program to compute them.

    The running times below are stated as the paper states them, plus a term sortCostsortCost for putting the jobs into earliest-start-time order. The paper's algorithmic sections open by indexing the jobs that way and count nothing for it; a statement about a program reading an arbitrary word has to, and one pass of a comparison sort is what it costs. Where the paper's own bound already dominates nlog⁡nn \log n the term is omitted.

    A word outside the domain has no meaningful threshold, width or largest processing time. These functions are total regardless, and nothing is claimed about their values there, since every statement quantifies over admissible words only.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…