Focus marking

A focus indicates the presence of alternatives that are relevant to interpretation, Krifka's definition of the notion after Rooth's alternative semantics. A constituent is F-marked or unfeatured (Focus.Mark). An F-marked constituent keeps its ordinary value and evokes every value of its type, and an unfeatured one evokes what its parts compose (WithAlternatives.mark), so the two marks are ordered by the alternatives they evoke, unfeatured below F-marked. Where a language realizes a focus is a separate matter, and one cut is whether the focused constituent stays in its base position or is fronted (Focus.Strategy).

Main definitions

• Focus.Mark: F-marked or unfeatured, a two-element linear order.
• WithAlternatives.mark: the meaning of a constituent bearing a mark.
• Focus.Strategy: a focus realized in place or fronted.

Main results

• WithAlternatives.alternatives_mark_subset_alternatives_mark_iff: unless a constituent already evokes its whole type, its alternatives grow exactly along the order of the marks.
• WithAlternatives.mark_eq_bind: on a well-formed meaning a mark is a continuation.
• WithAlternatives.ordinary_eq_of_given_mark_focused_bind: an F-marked constituent under a continuation is Given only if the continuation's ordinary values ignore it.

References

• [Kri08]
• [Roo92]
• [HZ07c]

inductive Focus.Mark : Type

A constituent is F-marked or unfeatured.

• unfeatured : Mark

  The constituent bears no focus feature.

• focused : Mark

  The constituent bears the focus feature.

@[instance_reducible]

instance Focus.instDecidableEqMark : DecidableEq Mark

Equations

• Focus.instDecidableEqMark x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Focus.instReprMark : Repr Mark

Equations

• Focus.instReprMark = { reprPrec := Focus.instReprMark.repr }

def Focus.instReprMark.repr : Mark → ℕ → Std.Format

Equations

• Focus.instReprMark.repr Focus.Mark.unfeatured prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Mark.unfeatured")).group prec✝
• Focus.instReprMark.repr Focus.Mark.focused prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Mark.focused")).group prec✝

@[instance_reducible]

instance Focus.instFintypeMark : Fintype Mark

Equations

• Focus.instFintypeMark = { elems := { val := ↑Focus.Mark.enumList, nodup := Focus.Mark.enumList_nodup }, complete := Focus.instFintypeMark._proof_1 }

@[instance_reducible]

instance Focus.instLinearOrderMark : LinearOrder Mark

Equations

• Focus.instLinearOrderMark = LinearOrder.lift' Focus.Mark.ctorIdx Focus.instLinearOrderMark._proof_1

@[instance_reducible]

instance Focus.instBoundedOrderMark : BoundedOrder Mark

Equations

• Focus.instBoundedOrderMark = { top := Focus.Mark.focused, le_top := Focus.instBoundedOrderMark._proof_1, bot := Focus.Mark.unfeatured, bot_le := Focus.instBoundedOrderMark._proof_2 }

instance Focus.instIsSimpleOrderMark : IsSimpleOrder Mark

inductive Focus.Strategy : Type

A focused constituent is realized in its base position or fronted to the left periphery of its clause.

• inSitu : Strategy

  The focus stays in its base position.

• exSitu : Strategy

  The focus is fronted.

@[instance_reducible]

instance Focus.instDecidableEqStrategy : DecidableEq Strategy

Equations

• Focus.instDecidableEqStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Focus.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

• Focus.instReprStrategy.repr Focus.Strategy.inSitu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Strategy.inSitu")).group prec✝
• Focus.instReprStrategy.repr Focus.Strategy.exSitu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Strategy.exSitu")).group prec✝

@[instance_reducible]

instance Focus.instReprStrategy : Repr Strategy

Equations

• Focus.instReprStrategy = { reprPrec := Focus.instReprStrategy.repr }

@[instance_reducible]

instance Focus.instInhabitedStrategy : Inhabited Strategy

Equations

• Focus.instInhabitedStrategy = { default := Focus.instInhabitedStrategy.default }

def WithAlternatives.mark {α : Type u_1} (d : WithAlternatives α) : Focus.Mark → WithAlternatives α

The meaning of a constituent bearing a mark. F-marking keeps the ordinary value and makes the alternatives the whole type; an unfeatured constituent keeps the alternatives of its parts.

Equations

• d.mark Focus.Mark.unfeatured = d
• d.mark Focus.Mark.focused = WithAlternatives.focused d.ordinary

@[simp]

theorem WithAlternatives.mark_unfeatured {α : Type u_1} (d : WithAlternatives α) : d.mark Focus.Mark.unfeatured = d

@[simp]

theorem WithAlternatives.mark_focused {α : Type u_1} (d : WithAlternatives α) : d.mark Focus.Mark.focused = focused d.ordinary

@[simp]

theorem WithAlternatives.ordinary_mark {α : Type u_1} (d : WithAlternatives α) (m : Focus.Mark) : (d.mark m).ordinary = d.ordinary

theorem WithAlternatives.WellFormed.mark {α : Type u_1} {d : WithAlternatives α} (hd : d.WellFormed) (m : Focus.Mark) : (d.mark m).WellFormed

theorem WithAlternatives.nontrivial_alternatives_mark_focused {α : Type u_1} [Nontrivial α] (d : WithAlternatives α) : (d.mark Focus.Mark.focused).alternatives.Nontrivial

An F-marked constituent of a type with two values evokes two alternatives.

@[simp]

theorem WithAlternatives.alternatives_map₂_focused_unfeatured {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : α) (y : β) : (map₂ f ((unfeatured x).mark Focus.Mark.focused) ((unfeatured y).mark Focus.Mark.unfeatured)).alternatives = Set.range fun (x : α) => f x y

Narrow focus on the first argument of a predication f x y evokes f x' y for every x'.

@[simp]

theorem WithAlternatives.alternatives_map₂_unfeatured_focused {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : α) (y : β) : (map₂ f ((unfeatured x).mark Focus.Mark.unfeatured) ((unfeatured y).mark Focus.Mark.focused)).alternatives = Set.range (f x)

Narrow focus on the second argument of a predication f x y evokes f x y' for every y'.

theorem WithAlternatives.alternatives_mark_subset_alternatives_mark_iff {α : Type u_1} {d : WithAlternatives α} (hd : d.alternatives ≠ Set.univ) {m m' : Focus.Mark} : (d.mark m).alternatives ⊆ (d.mark m').alternatives ↔ m ≤ m'

Unless a constituent already evokes its whole type, its alternatives grow exactly along the order of the marks: the order on marks is the order of the alternatives they evoke.

theorem WithAlternatives.mark_eq_bind {σ : Type u} {d : WithAlternatives σ} (hd : d.WellFormed) (m : Focus.Mark) : d.mark m = do let a ← d (pure a).mark m

On a well-formed meaning a mark is a continuation: each alternative is bound into the meaning of a terminal bearing the mark, so F-marking replaces it by the whole type.

theorem WithAlternatives.ordinary_eq_of_given_mark_focused_bind {σ τ : Type u} {d : WithAlternatives σ} {k : σ → WithAlternatives τ} (hk : ∀ (a : σ), (k a).WellFormed) {c : τ} (h : (d.mark Focus.Mark.focused >>= k).Given c) (a : σ) : (k a).ordinary = c

An F-marked constituent under a continuation with well-formed values is Given only if the ordinary values of the continuation ignore it.