Docs / Syntax / Agreement / Target

Agreement targets

import Linglib.Syntax.Agreement.Target · namespace Agreement

Source

An agreement target is an element whose form agreement determines. This file records a target by the positions of the Agreement Hierarchy at which it occurs, its form in each cell of a paradigm, and the dimensions it inflects for.

A cell gives each dimension a value a language distinguishes, so a target's form is a function on a product, and the target inflects for a dimension when that function does not ignore it: changing that value alone changes the form somewhere. These dimensions are the least set the form depends on, so what a target agrees in is read off its forms, and the targets of one language may differ in it, as Corbett shows of the Upper Sorbian finite verb and participle.

Main definitions

Main results

Implementation notes

The inflection is a finset, certified against the form by mem_inflection, so that it can be computed with, as Fintype.elems is certified by Fintype.complete.

References

Declarations

An agreement target over the values V d of each dimension d records the positions of the Agreement Hierarchy at which it occurs, its form in each cell, and the dimensions it inflects for, those its form does not ignore.

structure TargetL49–60
(V : Dimension → Type u_1) (F : Type u_2) :
Type (max u_1 u_2)
  • positions : Finset Position

    The positions of the Agreement Hierarchy at which the target occurs.

  • form : ((d : Dimension) → V d) → F

    The form of the target in each cell.

  • inflection : Finset Dimension

    The dimensions the target inflects for.

  • mem_inflection (d : Dimension) : d ∈ self.inflection ↔ ¬DependsOn self.form {d}ᶜ

    The target inflects for a dimension exactly when its form does not ignore it.

Used by Target.ofDependsOn, Target.coe_inflection, Target.isLeast_inflection, Target.dependsOn_inflection, Target.dependsOn_form_iff, Target.mem_inflection_iff

Used in Fragments/English/Auxiliaries, Fragments/Slavic/Russian/Agreement, AlexeyenkoZeijlstra2025

The target with the given positions and form that inflects for s, given that the form depends on s and that each dimension of s changes it somewhere.

def Target.ofDependsOnL66–79
{V : Dimension → Type u_1} {F : Type u_2} (positions : Finset Position) (form : ((d : Dimension) → V d) → F) (s : Finset Dimension) (h : DependsOn form ↑s) (hs : ∀ d ∈ s, ∃ (x : (a : Dimension) → V a) (a : V d), form (Function.update x d a) ≠ form x) :
Target V F
  • Target.ofDependsOn positions form s h hs = { positions := positions, form := form, inflection := s, mem_inflection := ⋯ }

Built from