Docs / Semantics / Dynamic / DRT / Accessibility

Subordination and accessibility

import Linglib.Semantics.Dynamic.DRT.Accessibility · namespace DRT

Source

A DRS is subordinate to another when it occurs inside one of its complex conditions. A discourse referent is accessible from a condition when it is declared in a box that is accessible where the condition occurs: the box containing the condition, the boxes it is nested in, and the antecedent of a conditional for its consequent. Accessibility is a property of occurrences: one box can occur twice in a DRS, at places with different accessible boxes. An occurrence is reached from the host by a walk that steps into the sub-boxes of complex conditions, collecting the boxes accessible at each step, and the walk is computed by a structural recursion that decides accessibility.

Main definitions

Main statements

Implementation notes

Kamp and Reyle state accessibility for DRS values. Read on values, it lets a chain pass through a second occurrence of an equal box and make a referent accessible where no occurrence of the condition sees it, so the definitions here quantify over occurrences. AccessibleFrom, like their definition, asks only that some occurrence of the condition see the referent, which properness does not imply: in [ | ¬[y | P y], ¬[ | P y]] the condition P y sees y at its first occurrence and leaves it free at its second. Properness is therefore characterized at occurrences.

References

Subordination

DirectlySubordinate K' K says K' is a sub-box of one of K's conditions, by the neg case of Def. 1.4.10(i), the ⇒ cases of Def. 2.1.2 (which subordinates both components of a conditional to the containing DRS), and the ∨ cases of Def. 2.4.3(i)(c), where no disjunct is subordinate to another. It is a relation on DRS values, where the textbook's is on box occurrences. Every clause pins the containing box in its conclusion, since an unpinned clause (such as consequent-below-antecedent) would hold of every pair of DRSs via a manufactured container. The ⇒ visibility asymmetry is not subordination but accessibility.

inductive DirectlySubordinateL64–81
{L : FirstOrder.Language} {V : Type w} :
DRS L V → DRS L V → Prop

Used by Subordinate, WeakSubordinate, DirectlySubordinate.sizeOf_lt

Used in KampReyle1993

L93–100
L102–106
L111–118

Occurrences

One step of the walk, from an occurrence of a box D whose accessible boxes are bs (innermost first, D included) into a sub-box of one of its complex conditions; the consequent of a conditional also sees the antecedent.

inductive ScopeStepL122–135
{L : FirstOrder.Language} {V : Type w} :
List (DRS L V) × DRS L V → List (DRS L V) × DRS L V → Prop

Used by Occurrence, Condition.occurrence_of_mem, DRS.mem_occurrences_iff

L161–162

The referent x is accessible from the condition γ in host when γ occurs in a box at an occurrence whose accessible boxes declare x (Def. 1.4.11, Def. 2.1.3).

def AccessibleFromL167–170
{L : FirstOrder.Language} {V : Type w} [DecidableEq V] (host : DRS L V) (x : V) (γ : Condition L V) :
Prop

Built from ,

Used by DRS.IsProper.accessibleFrom

Computing the occurrences

The occurrences below a box are listed by structural recursion through the nested conditions, matching each box as ⟨U, cs⟩, so that the kernel evaluates the list and decide closes concrete accessibility claims.

L207–209
L225–230

Properness and accessibility

L392–397