Structural alternatives

This file defines Katzir's structural alternatives of a parse tree: the trees obtainable from it by deletion, contraction, and substitution of a constituent by a same-category item of the substitution source, the lexicon together with the tree's own subtrees. StructuralOp is one such operation, atMostAsComplex its reflexive-transitive closure, the complexity preorder of the paper's definition (19), equalComplexity the antisymmetrization of that preorder, and structuralAlternatives the set of trees at most as complex as the given one, definition (20). Structural alternatives form an alternative source for the competition relations of Competition.

No operation introduces a category absent from the tree and the source (category_preservation), nor a phrase of a category of which neither has a phrase (phrase_preservation), which is what excludes the symmetric alternatives, nor a subtree property the operations cannot create (subtree_preservation); and substituting one lexical item for another of the same category throughout a tree, a Horn-scale alternative, is a chain of substitutions (horn_alternatives_are_structural), so scalar alternatives are a special case. More generally the Hamblin composition engine of WithAlternatives, applied to a tree whose terminals evoke their same-category lexical items, generates exactly the substitution fragment: its alternatives are structural (alternatives_withAlternatives_subset), while deletion and contraction, which act on the whole tree, lie outside any pointwise composition.

Main definitions

• substitutionSource — the lexicon together with the subtrees of the host.
• StructuralOp, atMostAsComplex, equalComplexity — one operation, its reflexive-transitive closure as a preorder, and the equal-complexity equivalence.
• structuralAlternatives — the trees at most as complex as the host over its source.
• withAlternatives — the Hamblin composition of a tree over a lexicon, a WithAlternatives value.

Main results

• category_preservation, phrase_preservation, subtree_preservation — the operations create no category, no phrase of a category and no subtree property absent from the host and the source.
• horn_alternatives_are_structural — leaf substitution of a same-category lexical item is a structural alternative.
• alternatives_withAlternatives_subset — the alternatives composed by the Hamblin engine over the lexicon are structural alternatives.

Implementation notes

atMostAsComplex is reachability, not an operation count, so equalComplexity, mutual reachability, is coarser than the paper's equal complexity. The inBind constructor extends the operations into the body of a binder, which the paper's trees lack.

References

• [Kat07]
• [FK11]

def PhraseStructure.Tree.substitutionSource {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) (φ : Tree C W) : Set (Tree C W)

The substitution source of φ (the paper's definition (41)) is the lexicon together with the subtrees of φ, so that a complex constituent of φ can replace a simpler one elsewhere in it.

Equations

• PhraseStructure.Tree.substitutionSource lex φ = ↑lex ∪ {t : PhraseStructure.Tree C W | t ∈ RoseTree.subtrees φ}

theorem PhraseStructure.Tree.forall_mem_substitutionSource {C : Type u_1} {W : Type u_2} {lex : Finset (Tree C W)} {φ : Tree C W} {P : Tree C W → Prop} : (∀ t ∈ substitutionSource lex φ, P t) ↔ (∀ t ∈ lex, P t) ∧ ∀ t ∈ RoseTree.subtrees φ, P t

inductive PhraseStructure.Tree.StructuralOp {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) : Tree C W → Tree C W → Prop

A structural operation on parse trees substitutes a constituent by a same-category item of the source, deletes a child of a phrase, contracts a phrase to one of its same-category children, or applies one of these inside a child of a phrase or a binder body. A phrase is a node or an adjunction structure.

• subst {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} {φ ψ : Tree C W} (h_cat : ψ.cat = φ.cat) (h_src : ψ ∈ source) : StructuralOp source φ ψ

  Substitute a tree by a same-category item of the source.

• delete {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} {l : Label C W} {cs : List (Tree C W)} (i : Fin cs.length) (hl : l.IsPhrase := by trivial) : StructuralOp source (RoseTree.node l cs) (RoseTree.node l (cs.eraseIdx ↑i))

  Delete the i-th child of a phrase.

• contract {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} {l : Label C W} {cs : List (Tree C W)} {child : Tree C W} (h_mem : child ∈ cs) (h_cat : child.cat = l.cat) (hl : l.IsPhrase := by trivial) : StructuralOp source (RoseTree.node l cs) child

  Contract a phrase to one of its same-category children.

• inChild {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} {l : Label C W} {cs : List (Tree C W)} (i : Fin cs.length) {ψ_child : Tree C W} (h_step : StructuralOp source (cs.get i) ψ_child) (hl : l.IsPhrase := by trivial) : StructuralOp source (RoseTree.node l cs) (RoseTree.node l (cs.set (↑i) ψ_child))

  Apply an operation inside one child of a phrase.

• inBind {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} {n : ℕ} {cat : C} {body body' : Tree C W} (h_step : StructuralOp source body body') : StructuralOp source (bind n cat body) (bind n cat body')

  Apply an operation inside a binder body.

def PhraseStructure.Tree.atMostAsComplex {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) (ψ φ : Tree C W) : Prop

ψ is at most as complex as φ when a chain of structural operations over the source leads from φ to ψ, the paper's definition (19) as a reachability preorder.

Equations

• PhraseStructure.Tree.atMostAsComplex source ψ φ = Relation.ReflTransGen (PhraseStructure.Tree.StructuralOp source) φ ψ

instance PhraseStructure.Tree.instIsPreorderAtMostAsComplex {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) : IsPreorder (Tree C W) (atMostAsComplex source)

def PhraseStructure.Tree.equalComplexity {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) : Tree C W → Tree C W → Prop

Two trees are of equal complexity when each is at most as complex as the other.

Equations

• PhraseStructure.Tree.equalComplexity source = AntisymmRel (PhraseStructure.Tree.atMostAsComplex source)

theorem PhraseStructure.Tree.equalComplexity.equivalence {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) : Equivalence (equalComplexity source)

theorem PhraseStructure.Tree.equalComplexity_terminal_subst {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} {cat : C} {oldW newW : W} (h_old : terminal cat oldW ∈ source) (h_new : terminal cat newW ∈ source) : equalComplexity source (terminal cat oldW) (terminal cat newW)

A same-category terminal substitution with both terminals in the source is reversible, so the two terminals are of equal complexity.

def PhraseStructure.Tree.structuralAlternatives {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) (φ : Tree C W) : Set (Tree C W)

The structural alternatives of φ, the paper's definition (20), are the trees at most as complex as φ over its substitution source.

Equations

• PhraseStructure.Tree.structuralAlternatives lex φ = {ψ : PhraseStructure.Tree C W | PhraseStructure.Tree.atMostAsComplex (PhraseStructure.Tree.substitutionSource lex φ) ψ φ}

theorem PhraseStructure.Tree.self_mem_structuralAlternatives {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) (φ : Tree C W) : φ ∈ structuralAlternatives lex φ

Category and subtree preservation

theorem PhraseStructure.Tree.category_preservation {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) (c : C) (φ ψ : Tree C W) (h_source : ∀ s ∈ source, c ∉ s.cats) (h_φ : c ∉ φ.cats) (h_reach : atMostAsComplex source ψ φ) : c ∉ ψ.cats

No tree reachable by structural operations contains a category absent from the source and the host, since substitution introduces only source material, deletion removes material, and contraction promotes a subtree.

theorem PhraseStructure.Tree.subtree_preservation {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) (Bad : Tree C W → Prop) (h_source : ∀ s ∈ source, ∀ t ∈ RoseTree.subtrees s, ¬Bad t) (h_delete : ∀ (l : Label C W) (cs : List (Tree C W)) (i : Fin cs.length), l.IsPhrase → ¬Bad (RoseTree.node l cs) → ¬Bad (RoseTree.node l (cs.eraseIdx ↑i))) (h_set : ∀ (l : Label C W) (cs : List (Tree C W)) (i : Fin cs.length) (ψ : Tree C W), l.IsPhrase → ¬Bad (RoseTree.node l cs) → ¬Bad (RoseTree.node l (cs.set (↑i) ψ))) (h_bind : ∀ (n : ℕ) (cat : C) (body body' : Tree C W), ¬Bad (bind n cat body) → ¬Bad (bind n cat body')) {φ ψ : Tree C W} (h_φ : ∀ t ∈ RoseTree.subtrees φ, ¬Bad t) (h_reach : atMostAsComplex source ψ φ) (t : RoseTree (Label C W)) : t ∈ RoseTree.subtrees ψ → ¬Bad t

A subtree property that no source item has, that the host lacks, and that a node cannot acquire by losing a child, by having a child replaced, or by a change of a binder's body, is absent from every structural alternative of the host.

theorem PhraseStructure.Tree.phrase_preservation {C : Type u_1} {W : Type u_2} (source : Set (Tree C W)) (c : C) (h_source : ∀ s ∈ source, ∀ t ∈ RoseTree.subtrees s, ¬(t.value.IsPhrase ∧ cat t = c)) {φ ψ : Tree C W} (h_φ : ∀ t ∈ RoseTree.subtrees φ, ¬(t.value.IsPhrase ∧ cat t = c)) (h_reach : atMostAsComplex source ψ φ) (t : RoseTree (Label C W)) : t ∈ RoseTree.subtrees ψ → ¬(t.value.IsPhrase ∧ cat t = c)

No structural alternative has a phrase of a category, a node or adjunction structure of category c, that neither the host nor any source item has.

Horn scales are structural alternatives

theorem PhraseStructure.Tree.horn_alternatives_are_structural {C : Type u_1} {W : Type u_2} [DecidableEq C] [DecidableEq W] (lex : Finset (Tree C W)) (φ : Tree C W) (α β : W) (c : C) (h_β : terminal c β ∈ lex) (hφ : φ.IsWellFormed) : leafSubst α β c φ ∈ structuralAlternatives lex φ

Leaf substitution of a same-category lexical item throughout a well-formed tree is a structural alternative, so Horn-scale alternatives are a special case of structural ones.

Hamblin composition generates the substitution fragment

The composition engine of WithAlternatives computes alternatives pointwise from the parts: withAlternatives lex φ gives each terminal the same-category items of the lexicon as alternatives and composes the constructors through the applicative. Every alternative it evokes is a chain of substitutions at the leaves, hence a structural alternative (alternatives_withAlternatives_subset); deletion and contraction lie outside the compositional fragment, so the converse fails.

def PhraseStructure.Tree.withAlternatives {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) : Tree C W → WithAlternatives (Tree C W)

In the Hamblin composition of a tree over a lexicon a terminal evokes itself and the same-category items of the lexicon, and the constructors compose pointwise.

Equations

• One or more equations did not get rendered due to their size.
• PhraseStructure.Tree.withAlternatives lex (RoseTree.node (PhraseStructure.Tree.Label.node c) cs) = PhraseStructure.Tree.node c <$> PhraseStructure.Tree.withAlternatives.list lex cs
• PhraseStructure.Tree.withAlternatives lex (RoseTree.node (PhraseStructure.Tree.Label.segment c) cs) = PhraseStructure.Tree.adjoin c <$> PhraseStructure.Tree.withAlternatives.list lex cs
• PhraseStructure.Tree.withAlternatives lex (RoseTree.node (PhraseStructure.Tree.Label.trace a a_1) []) = pure (RoseTree.node (PhraseStructure.Tree.Label.trace a a_1) [])
• PhraseStructure.Tree.withAlternatives lex (RoseTree.node (PhraseStructure.Tree.Label.bind n c) [body]) = PhraseStructure.Tree.bind n c <$> PhraseStructure.Tree.withAlternatives lex body
• PhraseStructure.Tree.withAlternatives lex x✝ = pure x✝

def PhraseStructure.Tree.withAlternatives.list {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) : List (Tree C W) → WithAlternatives (List (Tree C W))

The pointwise composition of a list of children.

Equations

• One or more equations did not get rendered due to their size.
• PhraseStructure.Tree.withAlternatives.list lex [] = pure []

theorem PhraseStructure.Tree.withAlternatives_node_of_not_licenses {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) {l : Label C W} {cs : List (Tree C W)} (h : ¬l.Licenses (List.map RoseTree.value cs)) : withAlternatives lex (RoseTree.node l cs) = pure (RoseTree.node l cs)

A node whose daughters its label does not license evokes only itself.

theorem PhraseStructure.Tree.ordinary_withAlternatives {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) (φ : Tree C W) : (withAlternatives lex φ).ordinary = φ

The ordinary value of the composition is the tree itself.

theorem PhraseStructure.Tree.wellFormed_withAlternatives {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) (φ : Tree C W) : (withAlternatives lex φ).WellFormed

The composition is well formed, since the tree is among its own alternatives.

theorem PhraseStructure.Tree.reachable_of_mem_withAlternatives {C : Type u_1} {W : Type u_2} {source : Set (Tree C W)} (lex : Finset (Tree C W)) (hlex : ↑lex ⊆ source) (φ ψ : Tree C W) : ψ ∈ (withAlternatives lex φ).alternatives → Relation.ReflTransGen (StructuralOp source) φ ψ

Over any source containing the lexicon, every alternative the composition evokes is reachable from the tree by structural operations.

theorem PhraseStructure.Tree.alternatives_withAlternatives_subset {C : Type u_1} {W : Type u_2} (lex : Finset (Tree C W)) (φ : Tree C W) : (withAlternatives lex φ).alternatives ⊆ structuralAlternatives lex φ

In the compositional fragment, the alternatives the Hamblin engine evokes from the lexicon are structural alternatives.