Voice derivations

A derivation applies voices one after another to a clause's participants. A Stage records where each participant sits in the current frame, the referential dependencies established and the agreements registered so far; applying a voice moves each participant to the slot its own corresponds to (Voice.image), suppresses those without one, lets a fresh participant into the slot the voice adds (Voice.newSlots) and links a subject the voice cumulates (Voice.fate) to each participant cumulated with it. Agreement registers the participants in the subject slot, the pivot of the frame.

The single-process architecture of [Bak85] §6 reads a word's morphology and its grammatical functions off one such sequence, and [Hym03] separates the two again for Bantu, where the syntactic derivation is read off scope while the affix order is templatic.

Main definitions

• Voice.Stage — participants at the slots of a frame, with links and registrations.
• Voice.Stage.subjects, Stage.apply, Stage.agree — the subject participants, the stage a voice derives, and agreement registration.

Main results

• Voice.Stage.registered_agree_apply, registered_apply_agree — agreement before a voice registers the subject before it applied, agreement after it the subject after.

References

• [Bak85]
• [Hym03]

structure Voice.Stage (α : Type u_1) : Type u_1

A derivational stage over participants α records the current frame, the slot each participant occupies, the referential dependencies established and the agreements registered so far.

• frame : ArgumentFrame

  The current frame.

• slots : List (α × ArgumentFrame.Slot)

  The slot each participant occupies.

• links : List (α × α)

  The referential dependencies established, a subject with each participant bound to it.

• registered : List α

  The participants agreement has registered, in order.

def Voice.instDecidableEqStage.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Stage α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Voice.instDecidableEqStage {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Stage α✝)

Equations

• Voice.instDecidableEqStage = Voice.instDecidableEqStage.decEq

@[instance_reducible]

instance Voice.instReprStage {α✝ : Type u_1} [Repr α✝] : Repr (Stage α✝)

Equations

• Voice.instReprStage = { reprPrec := Voice.instReprStage.repr }

def Voice.instReprStage.repr {α✝ : Type u_1} [Repr α✝] : Stage α✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Voice.Stage.subjects {α : Type u_1} (s : Stage α) : List α

The participants in the subject slot, the pivot of the frame.

Equations

• s.subjects = List.map (fun (x : α × ArgumentFrame.Slot) => x.1) (List.filter (fun (p : α × ArgumentFrame.Slot) => decide (some p.2 = s.frame.coreSlots.head?)) s.slots)

def Voice.Stage.apply {α : Type u_1} (s : Stage α) (v : Voice) (fresh : Option α) : Stage α

In the stage a voice derives, each participant moves to the slot its own corresponds to or is suppressed if none, a fresh participant enters the first slot the voice adds, and a subject the voice cumulates is linked to each participant cumulated with it.

Equations

• One or more equations did not get rendered due to their size.

def Voice.Stage.agree {α : Type u_1} (s : Stage α) : Stage α

Agreement registers the subject.

Equations

• s.agree = { frame := s.frame, slots := s.slots, links := s.links, registered := s.registered ++ s.subjects }

@[simp]

theorem Voice.Stage.frame_apply {α : Type u_1} (s : Stage α) (v : Voice) (a : Option α) : (s.apply v a).frame = v.derived.toArgumentFrame

@[simp]

theorem Voice.Stage.registered_apply {α : Type u_1} (s : Stage α) (v : Voice) (a : Option α) : (s.apply v a).registered = s.registered

@[simp]

theorem Voice.Stage.frame_agree {α : Type u_1} (s : Stage α) : s.agree.frame = s.frame

@[simp]

theorem Voice.Stage.slots_agree {α : Type u_1} (s : Stage α) : s.agree.slots = s.slots

@[simp]

theorem Voice.Stage.registered_agree {α : Type u_1} (s : Stage α) : s.agree.registered = s.registered ++ s.subjects

@[simp]

theorem Voice.Stage.subjects_agree {α : Type u_1} (s : Stage α) : s.agree.subjects = s.subjects

theorem Voice.Stage.registered_agree_apply {α : Type u_1} (s : Stage α) (v : Voice) (a : Option α) : (s.agree.apply v a).registered = s.registered ++ s.subjects

Agreement before a voice registers the subject before the voice applied.

theorem Voice.Stage.registered_apply_agree {α : Type u_1} (s : Stage α) (v : Voice) (a : Option α) : (s.apply v a).agree.registered = s.registered ++ (s.apply v a).subjects

Agreement after a voice registers the subject after it applied.