[IAI01]: Observations about the form and meaning of the Perfect

[IAI01]

Iatridou, Anagnostopoulou & Izvorski (Kenstowicz ed., Ken Hale: A Life in Language, MIT Press 2001) introduce the Perfect Time Span (PTS) framework for analyzing English perfect-aspect morphology and its interaction with temporal adverbials.

Verified content (vs PDF; § refs from the paper, not page numbers)

• PTS framework with LB and RB terminology (§3.1, "Inclusion of the utterance time by assertion"): "There is an interval that we will call the perfect time span. The left boundary (LB) of the perfect time span is specified by the argument of the adverbial. The right boundary (RB) is set by tense."
• U-perfect vs E-perfect distinction (§3): the paper's central focus, arguing for a semantic (not pragmatic) treatment of the ambiguity.
• Four uses of the present perfect (§2.2): universal, experiential, perfect of result, perfect of recent past — descriptive taxonomy borrowed from McCawley 1971, Comrie 1976, Binnick 1991.
• Unmodified perfects are never U-perfects (§3.2.1): diagnostic for U-reading availability — requires adverbial modification.
• Bounded vs unbounded distinction (§3): related to but distinct from stativity; perfect of state requires unboundedness.
• Perfect-level vs eventuality-level adverbials (§3.2.2): two levels at which adverbials can attach, corresponding to scope.

Companion files (paper-anchored extensions)

• Studies/Kiparsky2002.lean — [Kip02]'s event-structure account of perfect polysemy (four readings from subevent-structure mappings; three puzzles).
• Studies/IatridouZeijlstra2021.lean — [IZ21]'s unification of in years and until via the Until Time Span (UTS), NPI-strength classification, Actuality Inference and Beyond Expectation Inference. Imports the BoundaryKind from this file.

inductive IatridouEtAl2001.BoundaryKind : Type

Which boundary of a time span an adverbial sets.

• left: LB adverbials (in years, since, in (the last) 5 years)
• right: RB adverbials (until) [IAI01] §3.1.

• left : BoundaryKind
• right : BoundaryKind

@[implicit_reducible]

instance IatridouEtAl2001.instDecidableEqBoundaryKind : DecidableEq BoundaryKind

Equations

• IatridouEtAl2001.instDecidableEqBoundaryKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance IatridouEtAl2001.instReprBoundaryKind : Repr BoundaryKind

Equations

• IatridouEtAl2001.instReprBoundaryKind = { reprPrec := IatridouEtAl2001.instReprBoundaryKind.repr }

def IatridouEtAl2001.instReprBoundaryKind.repr : BoundaryKind → Nat → Std.Format

Equations

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

inductive IatridouEtAl2001.PerfectVariant : Type

The two perfect readings IAI 2001 argue for as semantically (not pragmatically) distinct: universal (U-perfect) and existential (E-perfect). The paper's central §3 focus.

The four-use descriptive taxonomy (universal / experiential / result / recent past) borrowed from McCawley 1971 lives in the Kiparsky2002 file's richer PerfectReading enum, which folds recent past into resultative per Kiparsky's own §1.

• universal : PerfectVariant
• existential : PerfectVariant

@[implicit_reducible]

instance IatridouEtAl2001.instDecidableEqPerfectVariant : DecidableEq PerfectVariant

Equations

• IatridouEtAl2001.instDecidableEqPerfectVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance IatridouEtAl2001.instReprPerfectVariant : Repr PerfectVariant

Equations

• IatridouEtAl2001.instReprPerfectVariant = { reprPrec := IatridouEtAl2001.instReprPerfectVariant.repr }

def IatridouEtAl2001.instReprPerfectVariant.repr : PerfectVariant → Nat → Std.Format

Equations

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

inductive IatridouEtAl2001.PerfectAvailability : Type

IAI §3.2.1: "Unmodified perfects are never U-perfects". A perfect sentence has a U-reading available only if it carries an adverbial modifier. We encode this as a property of perfect sentences: the U constructor takes evidence of adverbial modification.

• unmodified : PerfectAvailability

  Unmodified perfect: only the E-reading is available.

• adverbiallyModified : PerfectAvailability

  Adverbially modified perfect: both U- and E- readings available.

@[implicit_reducible]

instance IatridouEtAl2001.instDecidableEqPerfectAvailability : DecidableEq PerfectAvailability

Equations

• IatridouEtAl2001.instDecidableEqPerfectAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance IatridouEtAl2001.instReprPerfectAvailability : Repr PerfectAvailability

Equations

• IatridouEtAl2001.instReprPerfectAvailability = { reprPrec := IatridouEtAl2001.instReprPerfectAvailability.repr }

def IatridouEtAl2001.instReprPerfectAvailability.repr : PerfectAvailability → Nat → Std.Format

Equations

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

def IatridouEtAl2001.availableVariants : PerfectAvailability → List PerfectVariant

The U-perfect-requires-adverbial diagnostic.

Equations

• IatridouEtAl2001.availableVariants IatridouEtAl2001.PerfectAvailability.unmodified = [IatridouEtAl2001.PerfectVariant.existential]
• IatridouEtAl2001.availableVariants IatridouEtAl2001.PerfectAvailability.adverbiallyModified = [IatridouEtAl2001.PerfectVariant.universal, IatridouEtAl2001.PerfectVariant.existential]

theorem IatridouEtAl2001.unmodifiedNotU : ¬PerfectVariant.universal ∈ availableVariants PerfectAvailability.unmodified

Unmodified perfects do not license the U-reading (§3.2.1).

theorem IatridouEtAl2001.adverbiallyModifiedBothVariants : PerfectVariant.universal ∈ availableVariants PerfectAvailability.adverbiallyModified ∧ PerfectVariant.existential ∈ availableVariants PerfectAvailability.adverbiallyModified

Adverbially modified perfects license both readings.