Allen's interval relations

import Linglib.Semantics.Tense.Allen · namespace Allen

This file defines the relations between closed intervals of a linear order Allen 1983, extended to point intervals. How one interval stands to another is the order type of their four endpoints, recorded as the comparisons among them, and the relations are the comparisons that two intervals realize, twenty-six in all. A cell is a set of relations, and cells have converses, composites and chains.

Main definitions

Allen.Comparisons, Allen.realizable: the comparisons among the endpoints of two intervals, and those that two intervals realize.
Allen.Relation, Allen.relation: the relations, and the relation of two intervals.
Allen.toSetRel, Allen.inv, Allen.comp: a cell as a relation, its converse and composite.
Allen.precedes, Allen.isBefore, Allen.le, Allen.lt, Allen.overlaps, Allen.startsWithin, Allen.finalSubinterval, Allen.nonfinalSubinterval, Allen.eq, Allen.pure, Allen.ofPosition: named cells.
Allen.HoldsAlong, Allen.compAlong: chains of cells and their composites.

Main results

Allen.card_relation: there are twenty-six relations.
Allen.forall_toSetRel_subset_iff: one cell's relation lies in another's on every linear order exactly when the cell lies in the other.
Allen.relation_map: the relation of two intervals survives an order embedding.
Allen.toSetRel_comp: composition is exact on dense time without endpoints, and so are the operators the cells induce on sets of intervals (Allen.image_toSetRel_comp).
Allen.comp_precedes_precedes: precedence is transitive, an entry of Allen's table that the kernel decides.
Allen.comp_pure: on points, Allen composition is the composition of comparison cells.
Allen.mem_compAlong_iff: on dense time, the composite of a chain is exactly realized.

Implementation notes

A relation records whether each interval is a point; with the four cross comparisons alone composition is not exact. The composite of two cells is read off the intervals among six points, placing a second interval only beside first intervals that stand to it in the first cell, which keeps it small enough for decide +kernel. It and the named cells are irreducible, so that elaboration, which never needs their values, does not compute them.

References

Allen 1983, Maintaining Knowledge about Temporal Intervals

Declarations

The comparisons among the endpoints of two intervals: the first interval's start and end against the second's start and end, and each interval's start against its own end, lt for a proper interval and eq for a point.

structure Comparisons L68–84

Type

fstFst : Ordering
The first interval's start against the second's start.
fstSnd : Ordering
The first interval's start against the second's end.
sndFst : Ordering
The first interval's end against the second's start.
sndSnd : Ordering
The first interval's end against the second's end.
firstShape : Ordering
The first interval's start against its end.
secondShape : Ordering
The second interval's start against its end.

Derives DecidableEq, Repr.

Used by ofEndpoints, Comparisons.swap, Comparisons.swap_swap, realizable, Comparisons.swap_mem_realizable, Relation

The comparisons that two intervals realize, those of two intervals among four points.

def realizable L110–113

Finset Comparisons

realizable = Finset.image (fun (p : NonemptyInterval (Fin 4) × NonemptyInterval (Fin 4)) => ofEndpoints p.1.toProd.1 p.1.toProd.2 p.2.toProd.1 p.2.toProd.2) Finset.univ

Built from ,

Used by ofEndpoints_mem_realizable, Comparisons.swap_mem_realizable, Relation, Relation.equivRealizable, Relation.instFintype

L115–121

L123–127

A relation is how one interval of a linear order stands to another: comparisons among the endpoints of two intervals that some two intervals realize.

structure Relation L129–133

extends Comparisons :

Type

fstFst : Ordering
fstSnd : Ordering
sndFst : Ordering
sndSnd : Ordering
firstShape : Ordering
secondShape : Ordering
mem_realizable : self.toComparisons ∈ realizable
Two intervals realize the comparisons.

Built from ,

Used by Relation.ext, Relation.ext_iff, Relation.instDecidableEq, Relation.equivRealizable, Relation.instFintype, Relation.inv, Relation.inv_inv, card_relation, relation, toSetRel, mem_toSetRel, instDecidableMemProdNonemptyIntervalSetRelToSetRelMk, toSetRel_mono, exists_relation_eq, forall_toSetRel_subset_iff, inv, mem_inv, inv_inv, toSetRel_inv, comp, mem_comp, toSetRel_comp_subset, toSetRel_comp, image_toSetRel_subset_comp, image_toSetRel_comp, precedes, isBefore, le, lt, overlaps, startsWithin, finalSubinterval, nonfinalSubinterval, Relation.position, ofPosition, relation_mem_filter, eq, pure, HoldsAlong, instDecidableHoldsAlong, compAlong, HoldsAlong.mem_compAlong, mem_compAlong_iff

Used in Fragments/Manambu/Clause, Semantics/Aspect/Viewpoint, Semantics/Tense/Perspective, Syntax/Clause/Chaining, AnandToosarvandani2019 and 5 more

There are twenty-six relations: Allen's thirteen between proper intervals, five between a point and a proper interval, five between a proper interval and a point, and three between points.

theorem card_relation L157–160

Fintype.card Relation = 26

Built from

The relation of two intervals

The relation of the interval i to the interval j.

def relation L168–170

{T : Type u_1} [LinearOrder T] (i j : NonemptyInterval T) :

Relation

relation i j = { toComparisons := ofEndpoints i.toProd.1 i.toProd.2 j.toProd.1 j.toProd.2, mem_realizable := ⋯ }

Built from ,

Used by toComparisons_relation, relation_map, toSetRel, mem_toSetRel, exists_relation_eq, inv_relation, relation_eq_of_mem_partialIso, exists_partialIso_of_relation_eq, mem_comp, position_relation, relation_mem_filter, relation_mem_precedes, relation_mem_isBefore, relation_mem_le, relation_mem_lt, relation_mem_overlaps, relation_mem_startsWithin, relation_mem_finalSubinterval, relation_mem_nonfinalSubinterval, relation_mem_ofPosition, relation_mem_eq, relation_mem_pure

Used in Fragments/Manambu/Clause, Aikhenvald2008

L172–173

The relation of two intervals survives an order embedding.

theorem relation_map L175–183

{T : Type u_1} [LinearOrder T] {β : Type u_2} [LinearOrder β] (f : T ↪o β) (i j : NonemptyInterval T) :

relation (NonemptyInterval.map f.toOrderHom i) (NonemptyInterval.map f.toOrderHom j) = relation i j

Built from

The relation of a cell relates an interval to the intervals that stand to it in one of the cell's relations, as the relation of a comparison cell relates a perspective time to the reference times its tense allows.

def toSetRel L185–189

{T : Type u_1} [LinearOrder T] (C : Finset Relation) :

SetRel (NonemptyInterval T) (NonemptyInterval T)

toSetRel C = {p : NonemptyInterval T × NonemptyInterval T | relation p.2 p.1 ∈ C}

Built from ,

Used by mem_toSetRel, instDecidableMemProdNonemptyIntervalSetRelToSetRelMk, toSetRel_mono, forall_toSetRel_subset_iff, toSetRel_inv, toSetRel_comp_subset, toSetRel_comp, image_toSetRel_subset_comp, image_toSetRel_comp, instIsTransNonemptyIntervalToSetRelPrecedes, toSetRel_precedes_subset_comp_self_iff, toSetRel_precedes_comp_self, HoldsAlong, instDecidableHoldsAlong, HoldsAlong.mem_compAlong, mem_compAlong_iff

Used in Semantics/Aspect/Viewpoint, Semantics/Tense/Perspective, Semantics/Tense/Quantificational, ArreguiKusumoto1998, BonehDoron2013 and 6 more

theorem forall_toSetRel_subset_iff L208–213

{C D : Finset Relation} :

(∀ (T : Type) [inst : LinearOrder T], toSetRel C ⊆ toSetRel D) ↔ C ⊆ D

Built from ,

Converse

The converse of a cell.

def inv L217–218

(C : Finset Relation) :

Finset Relation

inv C = Finset.image Relation.inv C

Built from ,

Used by mem_inv, inv_inv, toSetRel_inv

Used in Semantics/Aspect/Viewpoint, Semantics/Tense/Perspective, BonehDoron2013, Declerck1991, Kratzer1998 and 1 more

Partial isomorphisms

Mathlib's Order.PartialIso pairs finitely many points of two linear orders that compare alike, so intervals whose endpoints it pairs stand in the same relation.

L252–261

L263–279

The composite of two cells: the relations of an interval to a third compatible with its standing in C to a second that stands in D to the third, read off the intervals among six points. The second interval is placed only beside a first that stands in C to it, so the kernel decides composites of the named cells.

@[irreducible] def comp L283–291

(C D : Finset Relation) :

Finset Relation

The definition is too large to print here; read it in the source.

Built from

Used by mem_comp, toSetRel_comp_subset, toSetRel_comp, image_toSetRel_subset_comp, image_toSetRel_comp, comp_precedes_precedes, comp_pure, compAlong

Used in Semantics/Tense/Perspective, Syntax/Clause/Chaining, BonehDoron2013

L293–299

L305–320

On dense time without endpoints, the composite of two cells' relations is the relation of the composite cell: the middle interval of a configuration of endpoints can be placed between any two intervals that stand as its outer ones do.

theorem toSetRel_comp L322–339

{T : Type u_1} [LinearOrder T] {C D : Finset Relation} [DenselyOrdered T] [NoMinOrder T] [NoMaxOrder T] :

(toSetRel C).comp (toSetRel D) = toSetRel (comp D C)

Built from , ,

L341–346

theorem image_toSetRel_comp L348–351

{T : Type u_1} [LinearOrder T] {C D : Finset Relation} [DenselyOrdered T] [NoMinOrder T] [NoMaxOrder T] (s : Set (NonemptyInterval T)) :

(toSetRel C).image ((toSetRel D).image s) = (toSetRel (comp C D)).image s

Built from , ,

Named cells

The first interval ends before the second starts.

@[irreducible] def precedes L357–359

Finset Relation

precedes = {x : Relation | x.sndFst = Ordering.lt}

Built from

Used by comp_precedes_precedes, ofPosition_lt, relation_mem_precedes, instIsTransNonemptyIntervalToSetRelPrecedes, toSetRel_precedes_subset_comp_self_iff, toSetRel_precedes_comp_self

Used in Fragments/Manambu/Clause, Semantics/Tense/Perspective, Semantics/Tense/Quantificational, Aikhenvald2008, AnandToosarvandani2019 and 8 more

The first interval ends no later than the second starts.

@[irreducible] def isBefore L361–363

Finset Relation

isBefore = {x : Relation | x.sndFst ≠ Ordering.gt}

Built from

Used by relation_mem_isBefore

Used in Semantics/Aspect/Viewpoint, Declerck1991

The first interval lies within the second.

@[irreducible] def le L365–367

Finset Relation

le = {r : Relation | r.fstFst ≠ Ordering.lt ∧ r.sndSnd ≠ Ordering.gt}

Built from

Used by lt, relation_mem_le

Used in Semantics/Aspect/Viewpoint, Semantics/Tense/Perspective, AnandToosarvandani2019, BonehDoron2013, Declerck1991 and 3 more

The first interval lies within the second and is not the whole of it.

@[irreducible] def lt L369–371

Finset Relation

lt = {r ∈ le | r.fstFst = Ordering.gt ∨ r.sndSnd = Ordering.lt}

Built from ,

Used by relation_mem_lt

Used in Semantics/Aspect/Viewpoint

The two intervals overlap.

@[irreducible] def overlaps L373–375

Finset Relation

overlaps = {r : Relation | r.fstSnd ≠ Ordering.gt ∧ r.sndFst ≠ Ordering.lt}

Built from

Used by ofPosition_eq, relation_mem_overlaps

Used in Semantics/Tense/Perspective

The first interval starts within the second.

@[irreducible] def startsWithin L377–379

Finset Relation

startsWithin = {r : Relation | r.fstFst ≠ Ordering.lt ∧ r.fstSnd ≠ Ordering.gt}

Built from

Used by relation_mem_startsWithin

Used in Semantics/Aspect/Viewpoint

The first interval lies within the second and ends with it.

@[irreducible] def finalSubinterval L381–383

Finset Relation

finalSubinterval = {r : Relation | r.fstFst ≠ Ordering.lt ∧ r.sndSnd = Ordering.eq}

Built from

Used by relation_mem_finalSubinterval

Used in Semantics/Aspect/Viewpoint

The first interval lies within the second and ends before it.

@[irreducible] def nonfinalSubinterval L385–388

Finset Relation

nonfinalSubinterval = {r : Relation | r.fstFst ≠ Ordering.lt ∧ r.sndSnd = Ordering.lt}

Built from

Used by relation_mem_nonfinalSubinterval

Used in Toosarvandani2016

theorem comp_precedes_precedes L390

comp precedes precedes = precedes

Built from ,

L392–395

L401–405

The cell of the relations whose position is one of C.

@[irreducible] def ofPosition L409–411

(C : Finset Ordering) :

Finset Relation

ofPosition C = {x : Relation | x.position ∈ C}

Built from ,

Used by ofPosition_eq, ofPosition_lt, relation_mem_ofPosition

Used in Fragments/Manambu/Clause, Semantics/Tense/Perspective, AnandToosarvandani2019, ArreguiKusumoto1998, Heim1994a and 3 more

Points

The comparison cells of the tenses are the cells of point intervals.

The two intervals are the same.

@[irreducible] def eq L489–491

Finset Relation

eq = {r : Relation | r.fstFst = Ordering.eq ∧ r.sndSnd = Ordering.eq}

Built from

Used by relation_mem_eq, compAlong

Used in Syntax/Clause/Chaining

The cell of point intervals whose points compare as C allows.

@[irreducible] def pure L493–496

(C : Finset Ordering) :

Finset Relation

pure C = {r : Relation | r.firstShape = Ordering.eq ∧ r.secondShape = Ordering.eq ∧ r.fstFst ∈ C}

Built from

Used by relation_mem_pure, comp_pure

Used in Kratzer1998

L502–504

L506–509

On points, Allen composition is the composition of comparison cells.

theorem comp_pure L523–537

(R S : Finset Ordering) :

comp (pure R) (pure S) = pure (Tense.comp R S)

Built from ,

Chains

A clause's times form a chain, each related to the one before it by a head's cell.

The intervals tos stand along the cells cs from b: the first stands to b as the first cell says, and each later one to the one before it as the next cell says.

def HoldsAlong L547–552

{T : Type u_1} [LinearOrder T] :

List (Finset Relation) → NonemptyInterval T → List (NonemptyInterval T) → Prop

HoldsAlong [] x✝ [] = True
HoldsAlong (C :: cs) x✝ (x_3 :: xs) = ((x✝, x_3) ∈ toSetRel C ∧ HoldsAlong cs x_3 xs)
HoldsAlong x✝² x✝¹ x✝ = False

Built from ,

Used by instDecidableHoldsAlong, HoldsAlong.mem_compAlong, mem_compAlong_iff

Used in Declerck1991, Kratzer1998

L554–562

The composite of a chain of cells, how its last time stands to its first.

def compAlong L566–569

List (Finset Relation) → Finset Relation

compAlong [] = eq
compAlong (C :: cs) = comp (compAlong cs) C

Built from , ,

Used by HoldsAlong.mem_compAlong, mem_compAlong_iff

Used in Syntax/Clause/Chaining

L575–582

On dense time without endpoints, two times stand in a chain's composite exactly when the chain can be realized from the first to the second.

theorem mem_compAlong_iff L584–601

{T : Type u_1} [LinearOrder T] [DenselyOrdered T] [NoMinOrder T] [NoMaxOrder T] {cs : List (Finset Relation)} {b x : NonemptyInterval T} :

(b, x) ∈ toSetRel (compAlong cs) ↔ ∃ (tos : List (NonemptyInterval T)), HoldsAlong cs b tos ∧ (b :: tos).getLast ⋯ = x

Built from , , ,