Chapter Info

In this chapter $ 2 ∈ 3$ we will confine ourselves to just two examples. The first is a simple scheduling problem, while the second involves breaking paragraphs into lines.

@[reducible, inline]

abbrev Chapter12.Segment (a : Type) : Type

A partition of a list of type [A] has type [[A]], so a list of partitions has type [[[A]]].

Equations

• Chapter12.Segment a = List a

@[reducible, inline]

abbrev Chapter12.Partition (a : Type) : Type

Equations

• Chapter12.Partition a = List (Chapter12.Segment a)

def Chapter12.splits {a : Type} : List a → List (List a × List a)

Equations

• Chapter12.splits [] = []
• Chapter12.splits (x_1 :: xs) = ([x_1], xs) :: List.map (fun (x : List a × List a) => match x with | (ys, zs) => (x_1 :: ys, zs)) (Chapter12.splits xs)

theorem Chapter12.length_lt_of_cons_split {α : Type} (xs ys zs : List α) (h : (ys, zs) ∈ splits xs) : zs.length < xs.length

@[irreducible]

def Chapter12.parts {a : Type} : List a → List (Partition a)

Equations

• One or more equations did not get rendered due to their size.
• Chapter12.parts [] = [[]]

def Chapter12.cons {a : Type} (x : a) (p : Partition a) : Partition a

Equations

• Chapter12.cons x p = [x] :: p

def Chapter12.glue {a : Type} (x : a) : Partition a → Partition a

Equations

• Chapter12.glue x (s :: p) = (x :: s) :: p
• Chapter12.glue x [] = panicWithPosWithDecl "Fad.Chapter12" "Chapter12.glue" 64 13 "glue: empty partition"

def Chapter12.extendl {a : Type} (x : a) : Partition a → List (Partition a)

Equations

• Chapter12.extendl x [] = [Chapter12.cons x []]
• Chapter12.extendl x x✝ = [Chapter12.cons x x✝, Chapter12.glue x x✝]

def Chapter12.parts₁ : List ℕ → List (Partition ℕ)

Equations

• Chapter12.parts₁ = List.foldr (Chapter1.concatMap ∘ Chapter12.extendl) [[]]

def Chapter12.last {a : Type u_1} [Inhabited a] : List a → a

Equations

• Chapter12.last [x_1] = x_1
• Chapter12.last [] = panicWithPosWithDecl "Fad.Chapter12" "Chapter12.last" 76 12 "last: empty list"
• Chapter12.last (head :: xs) = Chapter12.last xs

def Chapter12.init {a : Type u_1} [Inhabited a] : List a → List a

Equations

• Chapter12.init [x_1] = []
• Chapter12.init [] = panicWithPosWithDecl "Fad.Chapter12" "Chapter12.init" 81 14 "init: empty list"
• Chapter12.init (head :: xs) = head :: Chapter12.init xs

def Chapter12.snoc {a : Type} (x : a) (p : Partition a) : Partition a

Equations

• Chapter12.snoc x p = p ++ [[x]]

def Chapter12.bind {a : Type} (x : a) (p : Partition a) : Partition a

Equations

• Chapter12.bind x p = Chapter12.init p ++ [Chapter12.last p ++ [x]]

def Chapter12.extendr {a : Type} (x : a) : Partition a → List (Partition a)

Equations

• Chapter12.extendr x [] = [Chapter12.snoc x []]
• Chapter12.extendr x x✝ = [Chapter12.snoc x x✝, Chapter12.bind x x✝]

def Chapter12.parts₂ : List ℕ → List (Partition ℕ)

Equations

• Chapter12.parts₂ = List.foldl (flip (Chapter1.concatMap ∘ Chapter12.extendr)) [[]]

def Chapter12.maxWidth : ℕ

The major constraint on paragraphs is that all lines have to fit into a specified width. For simplicity, we assume a single globally defined value maxWidth that gives the maximum width a line can possess.

Equations

• Chapter12.maxWidth = 80

def Chapter12.optWidth : ℕ

The definition depends on another globally defined constant optWidth, whose value is at most maxWidth and which specifies the optimum width of each line of a paragraph.

Equations

• Chapter12.optWidth = 60

@[reducible, inline]

abbrev Chapter12.Word : Type

It is assumed that a text consists of a nonempty sequence of words, each word being a nonempty sequence of non-space characters. A paragraph therefore consists of at least one line.

Equations

• Chapter12.Word = List Char

@[reducible, inline]

abbrev Chapter12.Text : Type

Equations

• Chapter12.Text = List Chapter12.Word

@[reducible, inline]

abbrev Chapter12.Line : Type

Equations

• Chapter12.Line = List Chapter12.Word

@[reducible, inline]

abbrev Chapter12.Para : Type

Equations

• Chapter12.Para = List Chapter12.Line

def Chapter12.width (line : Line) : ℕ

Equations

• Chapter12.width line = Chapter8.S1.foldrn (fun (w : Chapter12.Word) (n : ℕ) => List.length w + 1 + n) (fun (w : Chapter12.Word) => List.length w) line

def Chapter12.aux_add (w : Word) (n : ℕ) : ℕ

Equations

• Chapter12.aux_add w n = List.length w + 1 + n

def Chapter12.width₁ : Line → ℕ

Equations

• Chapter12.width₁ = Chapter8.S1.foldrn Chapter12.aux_add List.length

def Chapter12.fits (line : Line) : Bool

Equations

• Chapter12.fits line = decide (Chapter12.width line ≤ Chapter12.maxWidth)

def Chapter12.foo : Word

Equations

• Chapter12.foo = ['f', 'o', 'o']

def Chapter12.bar : Word

Equations

• Chapter12.bar = ['b', 'a', 'r']

def Chapter12.line : Line

Equations

• Chapter12.line = [Chapter12.foo, Chapter12.bar]

def Chapter12.cost₁ (p : Para) : ℕ

Cost functions

Equations

• Chapter12.cost₁ p = List.length p

def Chapter12.waste₂ (line : Line) : ℕ

Equations

• Chapter12.waste₂ line = Chapter12.maxWidth - Chapter12.width line

def Chapter12.cost₂ (p : Para) : ℕ

Equations

• Chapter12.cost₂ p = (List.map Chapter12.waste₂ (Chapter12.init p)).sum

def Chapter12.waste₃ (line : Line) : ℕ

Equations

• Chapter12.waste₃ line = (Chapter12.optWidth - Chapter12.width line) * (Chapter12.optWidth - Chapter12.width line)

def Chapter12.cost₃ (p : Para) : ℕ

Equations

• Chapter12.cost₃ p = (List.map Chapter12.waste₃ (Chapter12.init p)).sum

def Chapter12.cost₄ (p : Para) : ℕ

Equations

• Chapter12.cost₄ p = List.foldr max 0 (List.map Chapter12.waste₂ (Chapter12.init p))

def Chapter12.cost₅ (p : Para) : ℕ

Equations

• Chapter12.cost₅ p = List.foldr max 0 (List.map Chapter12.waste₃ (Chapter12.init p))

def Chapter12.add (p : Para) (w : Word) : Para

There is an obvious greedy algorithm for the paragraph problem:

Equations

• Chapter12.add [] w = Chapter12.snoc w []
• Chapter12.add p w = (List.filter (fun (para : List Chapter12.Line) => Chapter12.fits (Chapter12.last para)) [Chapter12.bind w p, Chapter12.snoc w p]).headD []

def Chapter12.basic_greedy (ws : Text) : Para

Equations

• Chapter12.basic_greedy ws = List.foldl Chapter12.add [] ws

def Chapter12.tstep (ps : List Para) (w : Word) (cost : Para → ℕ) : List Para

Adding cost to the algorithm

Equations

• Chapter12.tstep [[]] w cost = [[[w]]]
• Chapter12.tstep ps w cost = Chapter7.minWith cost (List.map (Chapter12.snoc w) ps) :: List.filter (Chapter12.fits ∘ Chapter12.last) (List.map (Chapter12.bind w) ps)

def Chapter12.para (ws : Text) (cost : Para → ℕ) : Para

Equations

• Chapter12.para ws cost = Chapter7.minWith cost (List.foldl (fun (ps : List Chapter12.Para) (w : Chapter12.Word) => Chapter12.tstep ps w cost) [[]] ws)