Modal-Temporal Axes

[Con02]

The two temporal axes that any modal interpretation theory must distinguish (cf. [Con02], §2):

• Temporal perspective: the time at which the modal base / ordering source is evaluated. Either present (utterance time) or past (an earlier evaluation point, accessed via a past-shifting operator scoping over the modal).

• Temporal orientation: the relation between the perspective time and the time of the modal's prejacent. Past, present (coincident), or future.

These axes are framework-neutral: they are used by Condoravdi 2002 (English might/would), Hacquard 2006 (event-relative modals), Klecha 2016 (CIR-based future orientation), Matthewson 2013 (Gitksan dim-based future orientation), and any other modal-temporal theory.

This file is the canonical home; downstream modules import from here rather than redeclaring local copies. [Con02] uses only the future/past orientations — the present cell of TemporalOrientation goes unused there.

inductive Semantics.Modality.TemporalPerspective : Type

Temporal perspective: the time at which a modal base / ordering source is evaluated.

• present : TemporalPerspective

  Modal base evaluated at the utterance time.

• past : TemporalPerspective

  Modal base evaluated at a prior time (e.g., via PERF > MODAL).

@[implicit_reducible]

instance Semantics.Modality.instDecidableEqTemporalPerspective : DecidableEq TemporalPerspective

Equations

• Semantics.Modality.instDecidableEqTemporalPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Modality.instReprTemporalPerspective.repr : TemporalPerspective → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Modality.instReprTemporalPerspective : Repr TemporalPerspective

Equations

• Semantics.Modality.instReprTemporalPerspective = { reprPrec := Semantics.Modality.instReprTemporalPerspective.repr }

@[implicit_reducible]

instance Semantics.Modality.instBEqTemporalPerspective : BEq TemporalPerspective

Equations

• Semantics.Modality.instBEqTemporalPerspective = { beq := Semantics.Modality.instBEqTemporalPerspective.beq }

def Semantics.Modality.instBEqTemporalPerspective.beq : TemporalPerspective → TemporalPerspective → Bool

Equations

• Semantics.Modality.instBEqTemporalPerspective.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Semantics.Modality.instInhabitedTemporalPerspective : Inhabited TemporalPerspective

Equations

• Semantics.Modality.instInhabitedTemporalPerspective = { default := Semantics.Modality.instInhabitedTemporalPerspective.default }

inductive Semantics.Modality.TemporalOrientation : Type

Temporal orientation: the temporal relation between the perspective time and the prejacent's instantiation time.

• past : TemporalOrientation

  Prejacent instantiated before the perspective time.

• present : TemporalOrientation

  Prejacent coincides with the perspective time.

• future : TemporalOrientation

  Prejacent instantiated at or after the perspective time.

@[implicit_reducible]

instance Semantics.Modality.instDecidableEqTemporalOrientation : DecidableEq TemporalOrientation

Equations

• Semantics.Modality.instDecidableEqTemporalOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Modality.instReprTemporalOrientation : Repr TemporalOrientation

Equations

• Semantics.Modality.instReprTemporalOrientation = { reprPrec := Semantics.Modality.instReprTemporalOrientation.repr }

def Semantics.Modality.instReprTemporalOrientation.repr : TemporalOrientation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Modality.instBEqTemporalOrientation : BEq TemporalOrientation

Equations

• Semantics.Modality.instBEqTemporalOrientation = { beq := Semantics.Modality.instBEqTemporalOrientation.beq }

def Semantics.Modality.instBEqTemporalOrientation.beq : TemporalOrientation → TemporalOrientation → Bool

Equations

• Semantics.Modality.instBEqTemporalOrientation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Semantics.Modality.instInhabitedTemporalOrientation : Inhabited TemporalOrientation

Equations

• Semantics.Modality.instInhabitedTemporalOrientation = { default := Semantics.Modality.instInhabitedTemporalOrientation.default }