Temporal Connective Typology — substrate

@cite{giannakidou-2002} @cite{karttunen-1974}

Type-level enums + per-language data record for the cross-linguistic typology of the durative/eventive until distinction following @cite{giannakidou-2002}.

The four strategies

1. Three-way lexicalization (e.g., Greek): separate lexemes for before, durative until, and eventive NPI-until.
2. Two-way lexicalization (e.g., Icelandic, Finnish): separate lexemes for durative until and eventive NPI-until; before may or may not be one of them.
3. Ambiguity (e.g., English): a single until lexeme is ambiguous between durative (positive contexts) and eventive/NPI (negative contexts).
4. PPI replacement (e.g., Dutch, German): durative until cannot co-occur with negation; a separate PPI supplies the 'not before' meaning without negation.

What lives here vs. Phenomena/TemporalConnectives/Studies/Giannakidou2002.lean

This file holds the substrate types (the strategy enum + the per-language record schema). Per-language entries + sample-restricted typological theorems + Fragment grounding live in the Giannakidou 2002 study file.

inductive Typology.TemporalConnectives.UntilStrategy : Type

How a language handles the durative/eventive until distinction (@cite{giannakidou-2002}).

• threeWay : UntilStrategy

  Three distinct lexemes: before, durative until, eventive NPI-until. Greek: prin, mexri, para monon.

• twoWay : UntilStrategy

  Two distinct lexemes: durative until and eventive NPI-until. Icelandic: flanga til, fyrr en. Finnish: kunnes, ennenkuin.

• ambiguous : UntilStrategy

  Single ambiguous lexeme, disambiguated by negation context. English: until.

• ppiReplacement : UntilStrategy

  Durative until blocked under negation; PPI replaces NPI-until. Dutch: tot, pas. German: bis, erst.

@[implicit_reducible]

instance Typology.TemporalConnectives.instDecidableEqUntilStrategy : DecidableEq UntilStrategy

Equations

• Typology.TemporalConnectives.instDecidableEqUntilStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.TemporalConnectives.instReprUntilStrategy.repr : UntilStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.TemporalConnectives.instReprUntilStrategy : Repr UntilStrategy

Equations

• Typology.TemporalConnectives.instReprUntilStrategy = { reprPrec := Typology.TemporalConnectives.instReprUntilStrategy.repr }

structure Typology.TemporalConnectives.UntilTypologyEntry : Type

A language's strategy for the two-until distinction.

• language : String
• strategy : UntilStrategy
• durativeForm : String

  Surface form for durative until.

• eventiveForm : String

  Surface form for eventive until (NPI or PPI).

• eventiveMorphBeforeBased : Bool

  Is the eventive form morphologically built on before? (@cite{karttunen-1974}'s identity NPI-until = ¬before.)

• hasOvertAspect : Bool

  Does the language have overt perfective/imperfective marking? Orthogonal to the lexicalization choice.

@[implicit_reducible]

instance Typology.TemporalConnectives.instReprUntilTypologyEntry : Repr UntilTypologyEntry

Equations

• Typology.TemporalConnectives.instReprUntilTypologyEntry = { reprPrec := Typology.TemporalConnectives.instReprUntilTypologyEntry.repr }

def Typology.TemporalConnectives.instReprUntilTypologyEntry.repr : UntilTypologyEntry → Nat → Std.Format

Equations

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