Relation Origins and Declerck's PUTI

@cite{declerck-1991} @cite{declerck-2006}

Step 6 of the Tense-API redesign. A relation origin tags where a temporal relation between two TOs came from — grammatical tense, lexical aspect, an overt adverbial, a pragmatic default, world knowledge, or direct stipulation. Tagged relations let downstream modules distinguish:

• Defeasible defaults (e.g., the iconic-ordering reading produced by Declerck's PUTI) from semantic entailments (relations contributed by tense morphology).
• Encoded vs. inferred content: a precedes relation contributed by the past perfect's chain link is encoded; the same precedes inferred from "first … then …" discourse markers is a different speech act.
• Conflict resolution: when a tense-encoded relation and a PUTI default disagree, the encoded relation wins. Tagging the origin makes the conflict observable.

The PUTI lemma (Declerck's Principle of Unmarked Temporal Interpretation) states that the pragmatically-default Allen atom-set between two situations is fully determined by their boundedness profile: bounded+bounded → iconic (sequential), unbounded+unbounded → simultaneous, mixed → inclusion (the bounded inside the unbounded). PUTI is a defeasible default, not a semantic entailment — origin-tagging is what lets us say so.

inductive Core.Time.RelationOrigin : Type

The provenance of a temporal relation between two TOs.

• tense: the relation is encoded by tense morphology (e.g., the before link in the past perfect's chain).
• aspect: the relation comes from aspectual / lexical-aspectual semantics (e.g., perfective E ⊆ R).
• adverbial: the relation is contributed by an overt temporal adverbial ("yesterday", "before noon").
• puti: the relation is the pragmatic default produced by Declerck's Principle of Unmarked Temporal Interpretation (boundedness-based; see putiDefault).
• context: the relation is inherited from prior discourse, world knowledge, or conversational implicature.
• stipulated: direct stipulation (e.g., as a hypothesis in a formal derivation).

The tag is content-free: an origin doesn't change which Allen atom holds, only why. Conflict-resolution policies (encoded > defeasible) live at the consumer site.

• tense : RelationOrigin
• aspect : RelationOrigin
• adverbial : RelationOrigin
• puti : RelationOrigin
• context : RelationOrigin
• stipulated : RelationOrigin

@[implicit_reducible]

instance Core.Time.instDecidableEqRelationOrigin : DecidableEq RelationOrigin

Equations

• Core.Time.instDecidableEqRelationOrigin x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Time.instReprRelationOrigin : Repr RelationOrigin

Equations

• Core.Time.instReprRelationOrigin = { reprPrec := Core.Time.instReprRelationOrigin.repr }

def Core.Time.instReprRelationOrigin.repr : RelationOrigin → ℕ → Std.Format

Equations

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

def Core.Time.instInhabitedRelationOrigin.default : RelationOrigin

Equations

• Core.Time.instInhabitedRelationOrigin.default = Core.Time.RelationOrigin.tense

@[implicit_reducible]

instance Core.Time.instInhabitedRelationOrigin : Inhabited RelationOrigin

Equations

• Core.Time.instInhabitedRelationOrigin = { default := Core.Time.instInhabitedRelationOrigin.default }

def Core.Time.RelationOrigin.isDefeasible : RelationOrigin → Prop

Defeasible origins are those a hearer can override: PUTI defaults and inherited contextual relations. Tense, aspect, adverbial, and stipulated relations are non-defeasible (their content is encoded/asserted).

Equations

• Core.Time.RelationOrigin.puti.isDefeasible = True
• Core.Time.RelationOrigin.context.isDefeasible = True
• x✝.isDefeasible = False

@[implicit_reducible]

instance Core.Time.RelationOrigin.instDecidablePredIsDefeasible : DecidablePred isDefeasible

Equations

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

structure Core.Time.OriginTaggedRelation : Type

An Allen atom-set tagged with its provenance — "this is the atom- set holding between two TOs, and here's why." Atom-sets (rather than single atoms) cover both exact-atom claims (precedesSet) and union claims (beforeSet, containmentSet).

Two tagged relations are compatible if their atom-sets intersect (Compatible); incompatibility on a non-defeasible-only pair indicates a genuine theoretical contradiction.

• atoms : List AllenRelation

  The atom-set asserted to hold.

• origin : RelationOrigin

  Where the assertion comes from.

@[implicit_reducible]

instance Core.Time.instReprOriginTaggedRelation : Repr OriginTaggedRelation

Equations

• Core.Time.instReprOriginTaggedRelation = { reprPrec := Core.Time.instReprOriginTaggedRelation.repr }

def Core.Time.instReprOriginTaggedRelation.repr : OriginTaggedRelation → ℕ → Std.Format

Equations

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

def Core.Time.OriginTaggedRelation.Compatible (r₁ r₂ : OriginTaggedRelation) : Prop

Two tagged relations are compatible when their atom-sets share at least one atom. Used for conflict detection: an encoded tense relation is compatible with a PUTI default exactly when the default is consistent with the encoded content.

Equations

• r₁.Compatible r₂ = ∃ a ∈ r₁.atoms, a ∈ r₂.atoms

def Core.Time.OriginTaggedRelation.isDefeasible (r : OriginTaggedRelation) : Prop

A relation is defeasible if its origin is.

Equations

• r.isDefeasible = r.origin.isDefeasible

@[implicit_reducible]

instance Core.Time.OriginTaggedRelation.instDecidablePredIsDefeasible : DecidablePred isDefeasible

Equations

• r.instDecidablePredIsDefeasible = id inferInstance

Declerck's Principle of Unmarked Temporal Interpretation (@cite{declerck-1991}). Given two situations described by minimally-marked clauses, the default Allen atom-set between their event times is determined by their boundedness profile:

- **bounded + bounded** → iconic / sequential: the second is after
  the first (`beforeSet = {precedes, meets}` from the perspective
  of situation 1).
- **unbounded + unbounded** → simultaneous (`equalSet = {equal}`,
  strict identity at the point-time level; on intervals the
  `containmentSet` weakens to inclusion).
- **bounded + unbounded** → the bounded situation is inside the
  unbounded one (`containmentSet = {starts, equal, finishes,
  during}`).
- **unbounded + bounded** → the unbounded situation contains the
  bounded one (`reverseContainmentSet`).

PUTI is **defeasible**: an explicit adverbial or contextual
relation can override it. The `putiDefault` function returns the
*unmarked* atom-set, tagged with origin `.puti` so the result is
visibly an inference rather than an entailment. 

def Core.Time.putiDefault (b₁ b₂ : SituationBoundedness) : List AllenRelation

Declerck's PUTI default Allen atom-set for a (s₁, s₂) boundedness pair.

Equations

• Core.Time.putiDefault Core.Time.SituationBoundedness.bounded Core.Time.SituationBoundedness.bounded = Core.Time.AllenRelation.beforeSet
• Core.Time.putiDefault Core.Time.SituationBoundedness.unbounded Core.Time.SituationBoundedness.unbounded = Core.Time.AllenRelation.equalSet
• Core.Time.putiDefault Core.Time.SituationBoundedness.bounded Core.Time.SituationBoundedness.unbounded = Core.Time.AllenRelation.containmentSet
• Core.Time.putiDefault Core.Time.SituationBoundedness.unbounded Core.Time.SituationBoundedness.bounded = Core.Time.AllenRelation.reverseContainmentSet

def Core.Time.putiTaggedRelation (b₁ b₂ : SituationBoundedness) : OriginTaggedRelation

The PUTI default packaged as an OriginTaggedRelation — explicitly tagged .puti so consumers can see it's a defeasible default.

Equations

• Core.Time.putiTaggedRelation b₁ b₂ = { atoms := Core.Time.putiDefault b₁ b₂, origin := Core.Time.RelationOrigin.puti }

theorem Core.Time.puti_default_defeasible (b₁ b₂ : SituationBoundedness) : (putiTaggedRelation b₁ b₂).isDefeasible

PUTI defaults are always defeasible.