Licensing a derivation

A licensing of Merge, a morphism of magmas from the syntactic objects into a magma with zero, judges an object, 0 being the failure of Merge. A derivation is licensed when every stage is in the licensing's domain, the object under construction and every copy extracted from it. A licensing that judges only the derived object misses what its stages held: a moved item leaves a trace, so whether it was merged before it was saturated shows only at the stages before it moved. Stages are read off the replay, as Derivation.CCommandsAt reads c-command, so licensing decides, and LicensedAt.map_stageAt_ne_zero returns the derivation's own stage. A licensing reads the derivation with its own heads: a moved phrase leaves the trace of the item the licensing takes to head it.

Main definitions

• Minimalist.Derivation.LicensedAt: a stage of a derivation is in a licensing's domain.
• Minimalist.Derivation.LicensedBy: every stage is.

Main statements

• Minimalist.Derivation.LicensedAt.map_stageAt_ne_zero: licensing at a stage is licensing of the derivation's own stage.

def Minimalist.Derivation.LicensedAt {β : Type u_1} [Mul β] [Zero β] [Head β] (φ : SyntacticObject →ₙ* β) (d : Derivation) (n : ℕ) : Prop

φ licenses stage n of d: the ordered configuration the replay reaches after n steps, its movers leaving the traces of their heads under φ, is in its domain, the object and every copy on the stack.

Equations

• Minimalist.Derivation.LicensedAt φ d n = ∃ c ∈ (d.take n).replay? (Minimalist.head ∘ ⇑φ), ∀ x ∈ c.current :: c.stack, φ ↑x ≠ 0

@[instance_reducible]

instance Minimalist.Derivation.instDecidableLicensedAtOfDecidableEq {β : Type u_1} [Mul β] [Zero β] [Head β] (φ : SyntacticObject →ₙ* β) [DecidableEq β] (d : Derivation) (n : ℕ) : Decidable (LicensedAt φ d n)

Equations

• Minimalist.Derivation.instDecidableLicensedAtOfDecidableEq φ d n = id inferInstance

theorem Minimalist.Derivation.LicensedAt.map_stageAt_ne_zero {β : Type u_1} [Mul β] [Zero β] [Head β] (φ : SyntacticObject →ₙ* β) {d : Derivation} {n : ℕ} (h : LicensedAt φ d n) : φ (d.stageAt n (head ∘ ⇑φ)) ≠ 0

The stage licensing looks at is the derivation's own.

def Minimalist.Derivation.LicensedBy {β : Type u_1} [Mul β] [Zero β] [Head β] (φ : SyntacticObject →ₙ* β) (d : Derivation) : Prop

φ licenses d when it licenses every stage.

Equations

• Minimalist.Derivation.LicensedBy φ d = ∀ n ≤ d.length, Minimalist.Derivation.LicensedAt φ d n

@[instance_reducible]

instance Minimalist.Derivation.instDecidableLicensedByOfDecidableEq {β : Type u_1} [Mul β] [Zero β] [Head β] (φ : SyntacticObject →ₙ* β) [DecidableEq β] (d : Derivation) : Decidable (LicensedBy φ d)

Equations

• Minimalist.Derivation.instDecidableLicensedByOfDecidableEq φ d = id inferInstance