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

One family for parallel machines with and without preemption

Lax434175.ParallelFamily · concepts/Lax434175/ParallelFamily.lean · lax-434175

proven

Loading review…

Sign in with ORCID

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

    Theorem

    The problems on parallel machines form one family over the machine model with pieces: its fields are the interruption field and the fields of parallel machines (machine environment, number of machines, number of jobs, processing times, machine sets, release dates, deadlines, precedence constraints with time lags, communication delays, a server, forbidden times and the input encoding), and its objectives are the completion-time objectives. The entry pmtn\mathrm{pmtn} of the three-field notation is the value preemption of the interruption field, the entry restarts the value restarts, and no entry the value none. The value preemption without migration has no machine model of its own.

    A problem of the non-preemptive, the preemptive, or the restarts machine model determines the problem of this family with the same values in the common fields and the corresponding value of the interruption field.

    Theorem. The two problems are special cases of each other, so that the family describes the problems of the three machine models faithfully. In the family, 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, directly or through flow time, describes a problem whose decision version reduces to that of the other.

    Concept map
    23 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    5 reducible_of_reducesThroughFlow proven

    Lean source view on GitHub

    1import Lax434175.ParallelProblems
    2import Lax434175.Interruption
    3
    4/-!
    5---
    6title: One family for parallel machines with and without preemption
    7type: theorem
    8---
    9The problems on parallel machines form one family over the machine model with
    10pieces: its fields are the interruption field and the fields of parallel
    11machines (machine environment, number of machines, number of jobs,
    12processing times, machine sets, release dates, deadlines, precedence
    13constraints with time lags, communication delays, a server, forbidden times
    14and the input encoding), and its objectives are the completion-time
    15objectives. The entry pmtn\mathrm{pmtn} of the three-field notation is the value
    16preemption of the interruption field, the entry restarts the value restarts,
    17and no entry the value none. The value preemption without migration has no
    18machine model of its own.
    19
    20A problem of the non-preemptive, the preemptive, or the restarts machine model
    21determines the problem of this family with the same values in the common
    22fields and the corresponding value of the interruption field.
    23
    24**Theorem.** The two problems are special cases of each other, so that the
    25family describes the problems of the three machine models faithfully. In
    26the family, a specification that is field by field a special case of another
    27describes a special case of the other's problem, and a specification that
    28reduces to another, directly or through flow time, describes a problem whose
    29decision version reduces to that of the other.
    30-/
    31
    32namespace Lax434175.ParallelFamily
    33open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
    34open Lax434175
    35
    36/-- The fields of the family: interruption and the fields of parallel
    37machines. -/
    38inductive FieldName
    39 | interruption
    40 | field (i : ParallelProblems.FieldName)
    41 deriving DecidableEq
    42
    43instance : Fintype FieldName where
    44 elems := {.interruption, .field .environment, .field .machineCount, .field .jobCount,
    45 .field .processingTimes, .field .machineSets, .field .releaseDates, .field .deadlines,
    46 .field .precedence, .field .communicationDelays, .field .server, .field .forbiddenTimes,
    47 .field .encoding}
    48 complete x := by
    49 cases x with
    50 | interruption => decide
    51 | field i => cases i <;> decide
    52
    53/-- The problems on parallel machines. -/
    54abbrev family : Family Interruption.kernel :=
    55 Thresholds.family FieldName fun
    56 | .interruption => Interruption.module
    57 | .field i => (ParallelProblems.family Interruption.model).module i
    58
    59instance : Fintype family.ModuleName :=
    60 inferInstanceAs (Fintype FieldName)
    61
    62/-- The specification `α | β | γ`. -/
    63def spec (interruption : Interruption.Mode := .none)
    64 (environment : ParallelMachines.Environment)
    65 (machineCount : Counts.Bound := .any)
    66 (jobCount : Counts.Bound := .any)
    67 (machineSets : MachineSets.Value := .none)
    68 (processingTimes : ParallelMachines.ProcessingTimes := .arbitrary)
    69 (release : ReleaseDates.Value := .none)
    70 (deadline : Deadlines.Value := .none)
    71 (precedence : Precedence.Value := .none)
    72 (communicationDelays : CommunicationDelays.Value := .none)
    73 (server : Servers.Value := .none)
    74 (forbiddenTimes : ForbiddenTimes.Value := .none)
    75 (encoding : ForbiddenTimes.Encoding := .standard)
    76 (objective : Objectives.Value) : Spec family where
    77 module
    78 | .interruption => interruption
    79 | .field .environment => environment
    80 | .field .machineCount => machineCount
    81 | .field .jobCount => jobCount
    82 | .field .processingTimes => processingTimes
    83 | .field .machineSets => machineSets
    84 | .field .releaseDates => release
    85 | .field .deadlines => deadline
    86 | .field .precedence => precedence
    87 | .field .communicationDelays => communicationDelays
    88 | .field .server => server
    89 | .field .forbiddenTimes => forbiddenTimes
    90 | .field .encoding => encoding
    91 objective := objective
    92
    93/-- A specification of one machine model on parallel machines read in another:
    94the values of the fields are the same. -/
    95def transSpec {M M' : ParallelMachines.Model} (s : Spec (ParallelProblems.family M)) :
    96 Spec (ParallelProblems.family M') where
    97 module
    98 | .environment => s.module .environment
    99 | .machineCount => s.module .machineCount
    100 | .jobCount => s.module .jobCount
    101 | .processingTimes => s.module .processingTimes
    102 | .machineSets => s.module .machineSets
    103 | .releaseDates => s.module .releaseDates
    104 | .deadlines => s.module .deadlines
    105 | .precedence => s.module .precedence
    106 | .communicationDelays => s.module .communicationDelays
    107 | .server => s.module .server
    108 | .forbiddenTimes => s.module .forbiddenTimes
    109 | .encoding => s.module .encoding
    110 objective := s.objective
    111
    112/-- The specification of the family with the values of a specification of a
    113machine model on parallel machines and a way of interruption. -/
    114def ofSpec {M : ParallelMachines.Model} (interruption : Interruption.Mode)
    115 (s : Spec (ParallelProblems.family M)) : Spec family where
    116 module
    117 | .interruption => interruption
    118 | .field i => (transSpec (M' := Interruption.model) s).module i
    119 objective := s.objective
    120
    121axiom nonpreemptive_faithful (s : Spec ParallelProblems.nonpreemptive) :
    122 SpecialCase (problem _ s) (problem family (ofSpec .none s)) ∧
    123 SpecialCase (problem family (ofSpec .none s)) (problem _ s)
    124
    125axiom preemptive_faithful (s : Spec ParallelProblems.preemptive) :
    126 SpecialCase (problem _ s) (problem family (ofSpec .pmtn s)) ∧
    127 SpecialCase (problem family (ofSpec .pmtn s)) (problem _ s)
    128
    129axiom restarts_faithful (s : Spec ParallelProblems.restarts) :
    130 SpecialCase (problem _ s) (problem family (ofSpec .restarts s)) ∧
    131 SpecialCase (problem family (ofSpec .restarts s)) (problem _ s)
    132
    133axiom family_sound : family.Sound
    134
    135axiom specialCase_of_le {s t : Spec family} :
    136 s.le t → SpecialCase (problem family s) (problem family t)
    137
    138axiom reducible_of_reduces {s t : Spec family} :
    139 Thresholds.Reduces s t → Reducible (problem family s) (problem family t)
    140
    141axiom reducible_of_reducesThroughFlow {s t : Spec family} :
    142 Thresholds.ReducesThroughFlow s t → Reducible (problem family s) (problem family t)
    143
    144end Lax434175.ParallelFamily
    145
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…