The heads of category c the probe at a c-commands.
The definition is too large to print here; read it in the source.
Used by horizon, horizon_eq_sealed
Docs / Syntax / Minimalist / Locality / Horizon
Horizons
import Linglib.Syntax.Minimalist.Locality.Horizon · namespace Minimalist
A probe's search stops at a head of its horizon category: what that head c-commands, its complement, is beyond the probe's reach. A horizon is thus the cut Transfer makes, the complements of a set of heads, indexed by the probe and its category rather than by the stage of the derivation.
Main definitions
Minimalist.horizon: the positions behind the horizon of a category for the probe at a position.
Main results
Minimalist.horizon_eq_sealed: a horizon is the cut of the complements of the horizon heads the probe c-commands, transferred at every stage.
References
- Keine 2019, Selective Opacity formalized
- Keine 2020, Probes and Their Horizons formalized
Declarations
The positions behind the horizon c of the probe at a, in the complement of a head of
category c the probe c-commands (Keine 2019).
- horizon t a c = {q : Core.Order.TreePath | ∃ h ∈ horizonHeads t a c, complement h ≤ q}
Built from
Used by instDecidablePredTreePathMemSetHorizon, isUpperSet_horizon, horizon_eq_sealed
Used in AissenPolian2025
(t : LinearizedSyntacticObject) (a : Core.Order.TreePath) (c : Cat) :
DecidablePred fun (x : Core.Order.TreePath) => x ∈ horizon t a c
The definition is too large to print here; read it in the source.
Built from
Built from
A horizon is the cut of the complements of the horizon heads the probe c-commands, under a schedule that transfers them at every stage.
{t : LinearizedSyntacticObject} (hd : HeadFunction) (a s : Core.Order.TreePath) (c : Cat) :
horizon t a c = sealed (horizonHeads t a c) (complementDomain hd t ∅) (fun (x : Finset Core.Order.TreePath) (x_1 x_2 : Core.Order.TreePath) => True) s
Built from ,