Adposition: the function-marking relator

[hagege-2010] [dryer-2013] [Sve10]

The P-head word class — a function-marking relator — as a theory-neutral object, sibling to Syntax/Pronoun in the closed-class function-word family. The base encodes only the cross-framework criteria that define the category; every framework (Minimalist cartography, HPSG, CCG, Dependency Grammar, cognitive grammar) and every semantic theory (Pantcheva direction, Zwarts path algebra, the Svenonius AxPart decomposition in Adposition/Spatial.lean) plugs into this base rather than defining it — exactly as Caha's containment refines Case without being Case.

Defining criteria (typological tradition: [hagege-2010], [dryer-2013])

1. governs a complement (the Ground/régime) — a relator; [] is the intransitive/particle limit;
2. marks the function of that complement — a RelationType;
3. closed-class grammatical element (a category fact; may inflect/agree — Celtic, Uralic, Hebrew);
4. fixed linearization relative to the complement (a set: a lexeme may be both pre- and post-positional, e.g. Dutch op);
5. exponence on the grammaticalization cline (the case-affix boundary).

Main declarations

• Adposition — the category object (the five criteria as fields)
• Adposition.RelationType / Linearization / Complement / Exponence / Form — the criterion vocabularies
• Adposition.isIntransitive / isComplex / isAmbipositional

inductive Adposition.RelationType : Type

The relation an adposition marks (criterion 2) — coarse only. A spatial relation's internal structure (AxPart × Region × PathDir × Bound) is a theory (Adposition/Spatial.lean), never part of the category.

• spatial : RelationType

  Spatial: in/on/under/to/from. Refined by the cartographic decomposition.

• temporal : RelationType

  Temporal: before/after/during/until.

• grammatical : RelationType

  Grammatical/relational: of/by/with — function-marking (agent, instrument, comitative). The marked role is a Study-level refinement, not a base field.

• logical : RelationType

  Logical/abstract: because-of/despite/concerning.

@[implicit_reducible]

instance Adposition.instDecidableEqRelationType : DecidableEq RelationType

Equations

• Adposition.instDecidableEqRelationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Adposition.instReprRelationType : Repr RelationType

Equations

• Adposition.instReprRelationType = { reprPrec := Adposition.instReprRelationType.repr }

def Adposition.instReprRelationType.repr : RelationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Adposition.instFintypeRelationType : Fintype RelationType

Equations

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

@[implicit_reducible]

instance Adposition.instInhabitedRelationType : Inhabited RelationType

Equations

• Adposition.instInhabitedRelationType = { default := Adposition.instInhabitedRelationType.default }

inductive Adposition.Linearization : Type

A linearization of an adposition with respect to its complement (criterion 4). The per-lexeme companion to the language-level Adposition.AdpositionOrder.

• pre : Linearization

  Preposition: P precedes the complement.

• post : Linearization

  Postposition: P follows the complement.

• circum : Linearization

  Circumposition: P brackets the complement (two exponents).

• inposition : Linearization

  Inposition: P appears inside/second-position in the complement.

@[implicit_reducible]

instance Adposition.instDecidableEqLinearization : DecidableEq Linearization

Equations

• Adposition.instDecidableEqLinearization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Adposition.instReprLinearization.repr : Linearization → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Adposition.instReprLinearization : Repr Linearization

Equations

• Adposition.instReprLinearization = { reprPrec := Adposition.instReprLinearization.repr }

@[implicit_reducible]

instance Adposition.instFintypeLinearization : Fintype Linearization

Equations

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

inductive Adposition.Complement : Type

What an adposition governs (criterion 1) — P-specific complement types (NOT the verb-argument Features.Complementation.ComplementType, which carries ditransitive frames an adposition never selects).

• np : Complement
• pp : Complement
• clause : Complement
• ap : Complement

  Adjectival complement (Dutch tot voor kort 'until recently').

@[implicit_reducible]

instance Adposition.instDecidableEqComplement : DecidableEq Complement

Equations

• Adposition.instDecidableEqComplement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Adposition.instReprComplement.repr : Complement → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Adposition.instReprComplement.repr Adposition.Complement.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.Complement.np")).group prec✝
• Adposition.instReprComplement.repr Adposition.Complement.pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.Complement.pp")).group prec✝
• Adposition.instReprComplement.repr Adposition.Complement.ap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.Complement.ap")).group prec✝

@[implicit_reducible]

instance Adposition.instReprComplement : Repr Complement

Equations

• Adposition.instReprComplement = { reprPrec := Adposition.instReprComplement.repr }

@[implicit_reducible]

instance Adposition.instFintypeComplement : Fintype Complement

Equations

• Adposition.instFintypeComplement = { elems := { val := ↑Adposition.Complement.enumList, nodup := Adposition.Complement.enumList_nodup }, complete := Adposition.instFintypeComplement._proof_1 }

inductive Adposition.Exponence : Type

Exponence on the grammaticalization cline (criterion 5). affix is the boundary at which the adposition becomes a Case exponent — the point where this object and Case meet on the cline (Features/Case/Grammaticalization.lean).

• free : Exponence
• clitic : Exponence
• affix : Exponence

@[implicit_reducible]

instance Adposition.instDecidableEqExponence : DecidableEq Exponence

Equations

• Adposition.instDecidableEqExponence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Adposition.instReprExponence.repr : Exponence → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Adposition.instReprExponence.repr Adposition.Exponence.free prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Adposition.Exponence.free")).group prec✝

@[implicit_reducible]

instance Adposition.instReprExponence : Repr Exponence

Equations

• Adposition.instReprExponence = { reprPrec := Adposition.instReprExponence.repr }

@[implicit_reducible]

instance Adposition.instFintypeExponence : Fintype Exponence

Equations

• Adposition.instFintypeExponence = { elems := { val := ↑Adposition.Exponence.enumList, nodup := Adposition.Exponence.enumList_nodup }, complete := Adposition.instFintypeExponence._proof_1 }

@[implicit_reducible]

instance Adposition.instInhabitedExponence : Inhabited Exponence

Equations

• Adposition.instInhabitedExponence = { default := Adposition.instInhabitedExponence.default }

inductive Adposition.Form : Type

The form of an adposition: a single word, or a complex/multi-word adposition (in front of, on top of).

• simple (s : String) : Form
• complex (parts : List String) : Form

@[implicit_reducible]

instance Adposition.instDecidableEqForm : DecidableEq Form

Equations

• Adposition.instDecidableEqForm = Adposition.instDecidableEqForm.decEq

def Adposition.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

• Adposition.instDecidableEqForm.decEq (Adposition.Form.simple a) (Adposition.Form.simple b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Adposition.instDecidableEqForm.decEq (Adposition.Form.simple s) (Adposition.Form.complex parts) = isFalse ⋯
• Adposition.instDecidableEqForm.decEq (Adposition.Form.complex parts) (Adposition.Form.simple s) = isFalse ⋯
• Adposition.instDecidableEqForm.decEq (Adposition.Form.complex a) (Adposition.Form.complex b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Adposition.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Adposition.instReprForm : Repr Form

Equations

• Adposition.instReprForm = { reprPrec := Adposition.instReprForm.repr }

def Adposition.Form.text : Form → String

The surface string of a form (complex forms joined by spaces).

Equations

• (Adposition.Form.simple a).text = a
• (Adposition.Form.complex a).text = " ".intercalate a

structure Adposition : Type

An adposition: the five defining criteria as fields. Theory-neutral — spatial/grammatical refinements and framework analyses consume it.

• form : Form
• relation : RelationType

  Criterion 2: the relation marked.

• complement : List Complement

  Criterion 1: complement types selected. [] = intransitive (particle).

• linearization : List Linearization

  Criterion 4: allowed linearizations (set semantics; may be several).

• exponence : Exponence

  Criterion 5: exponence on the cline.

• agreesWithComplement : Bool

  Criterion 3 refinement: inflects/agrees with the complement's φ-features (Celtic agam, Hungarian, Hebrew).

@[implicit_reducible]

instance instReprAdposition : Repr Adposition

Equations

• instReprAdposition = { reprPrec := instReprAdposition.repr }

def instReprAdposition.repr : Adposition → ℕ → Std.Format

Equations

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

def instDecidableEqAdposition.decEq (x✝ x✝¹ : Adposition) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqAdposition : DecidableEq Adposition

Equations

• instDecidableEqAdposition = instDecidableEqAdposition.decEq

def Adposition.isIntransitive (a : Adposition) : Bool

Intransitive (the particle limit): governs no complement.

Equations

• a.isIntransitive = a.complement.isEmpty

def Adposition.isComplex (a : Adposition) : Bool

Complex/multi-word adposition (in front of).

Equations

• a.isComplex = match a.form with | Adposition.Form.complex parts => true | Adposition.Form.simple s => false

def Adposition.isAmbipositional (a : Adposition) : Bool

Ambipositional: allows both pre- and post-positional order (Dutch op).

Equations

• a.isAmbipositional = (a.linearization.contains Adposition.Linearization.pre && a.linearization.contains Adposition.Linearization.post)

Smoke tests — the mature fields exercised (stress-test seeds)

def Adposition.english_in : Adposition

English in: simple spatial preposition over an NP.

Equations

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

def Adposition.english_inFrontOf : Adposition

English in front of: a complex/multi-word spatial preposition.

Equations

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

def Adposition.dutch_op : Adposition

Dutch op: ambipositional (both pre- and post-positional).

Equations

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

def Adposition.irish_ag : Adposition

Irish ag 'at': a grammatical preposition that inflects for its complement (agam 'at-me', agat 'at-you').

Equations

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