Pantcheva (2011): Decomposing Path

This file formalizes the syncretism typology of the ninth chapter of Pantcheva's thesis. The directional heads Place, Goal, Source, and Route form the containment sequence of Spatial.Path.Direction, and a syncretism pattern over the four is a paradigm over that sequence (Pattern). Two constraints restrict the patterns: the *ABA generalization of Bobaljik (then circulating in manuscript), on which a syncretism targets only adjacent heads of the sequence, the same contiguity that governs nominal case in Caha's analysis (Morphology.IsContiguous); and *A&¬A, on which Goal and Source never share a marker, because the Source head is the locus of a reversal of the Goal path (§5.4), so one marker for both would be contradictory (GoalSourceMerged, goalSource_disjoint). Together they say exactly that no syncretism crosses the seam between Goal and Source (possible_iff_respectsSeam), which cuts the fifteen set-partitions of the four roles to the four attested patterns, Types 1 to 4 of Table 9.2: Place and Goal may merge, Source and Route may merge, and nothing else (possible_syncretisms). Seven of the eleven excluded patterns fall to *ABA and the other four to *A&¬A, Table 9.3 (aba_excluded, ana_excluded). The containment itself is visible where the Source marker contains the Goal marker, as in Imbabura Quechua -man against -man-da (Table 4.2, source_contains_goal), and Georgian instantiates Type 3, with Location and Goal syncretic (Table 9.1, georgian_loc_goal_possible).

Implementation notes

The patterns are restricted-growth strings over the four positions, one representative per set-partition; the seam characterization is proved for every pattern, and the enumerations are its corollaries. The attested lexicalization patterns of §9.3.1 are described in prose.

References

• [Pan11]
• [Bob12]
• [Cah09]

@[reducible, inline]

abbrev Pantcheva2011.Pattern : Type

A syncretism pattern assigns form-class indices to the four path roles, in containment order Place, Goal, Source, Route, as the four-cell instance of Morphology.Paradigm.

Equations

• Pantcheva2011.Pattern = Morphology.Paradigm 4 ℕ

def Pantcheva2011.allPatterns : List Pattern

The fifteen syncretism patterns up to relabeling are the restricted-growth strings over four positions, one per set-partition of the four roles.

Equations

• One or more equations did not get rendered due to their size.

def Pantcheva2011.GoalSourceMerged (p : Pattern) : Prop

Goal and Source share a form class, which *A&¬A forbids.

Equations

• Pantcheva2011.GoalSourceMerged p = (p 1 = p 2)

@[instance_reducible]

instance Pantcheva2011.instDecidableGoalSourceMerged (p : Pattern) : Decidable (GoalSourceMerged p)

Equations

• Pantcheva2011.instDecidableGoalSourceMerged p = { decide := (p 1).beq (p 2), reflects_decide := ⋯ }

def Pantcheva2011.Possible (p : Pattern) : Prop

A pattern is possible iff it is contiguous, *ABA, and keeps Goal distinct from Source, *A&¬A.

Equations

• Pantcheva2011.Possible p = (Morphology.IsContiguous p ∧ ¬Pantcheva2011.GoalSourceMerged p)

@[instance_reducible]

instance Pantcheva2011.instDecidablePossible (p : Pattern) : Decidable (Possible p)

Equations

• Pantcheva2011.instDecidablePossible p = { decide := decide (Morphology.IsContiguous p) && decide ¬Pantcheva2011.GoalSourceMerged p, reflects_decide := ⋯ }

def Pantcheva2011.RespectsSeam (p : Pattern) : Prop

A pattern respects the seam when no form class straddles Goal and Source: cells that share a form lie on the same side of the seam.

Equations

• Pantcheva2011.RespectsSeam p = ∀ (i j : Fin 4), p i = p j → (i ≤ 1 ↔ j ≤ 1)

theorem Pantcheva2011.possible_iff_respectsSeam (p : Pattern) : Possible p ↔ RespectsSeam p

The two constraints together say exactly that no syncretism crosses the Goal–Source seam.

theorem Pantcheva2011.possible_syncretisms : List.filter (fun (p : Pattern) => decide (Possible p)) allPatterns = [![0, 0, 1, 1], ![0, 0, 1, 2], ![0, 1, 2, 2], ![0, 1, 2, 3]]

Of the fifteen patterns, exactly four respect the seam, Types 1 to 4 of Table 9.2, with all roles distinct (English), Place=Goal (Georgian), Source=Route, and both.

theorem Pantcheva2011.aba_excluded : List.filter (fun (p : Fin 4 → ℕ) => decide ¬Morphology.IsContiguous p) allPatterns = [![0, 0, 1, 0], ![0, 1, 0, 0], ![0, 1, 0, 1], ![0, 1, 0, 2], ![0, 1, 1, 0], ![0, 1, 2, 0], ![0, 1, 2, 1]]

*ABA excludes seven patterns, Types 5 to 11 of Table 9.3, each a syncretism spanning non-adjacent roles.

theorem Pantcheva2011.ana_excluded : List.filter (fun (p : Fin 4 → ℕ) => decide (Morphology.IsContiguous p ∧ GoalSourceMerged p)) allPatterns = [![0, 0, 0, 0], ![0, 0, 0, 1], ![0, 1, 1, 1], ![0, 1, 1, 2]]

*A&¬A alone, the constraint peculiar to the directional domain, excludes four contiguous patterns, Types 12 to 15 of Table 9.3.

Morphological containment (Table 4.2)

The Source structure contains the Goal structure, visible where the Source marker contains the Goal marker, as in Quechua -man against -man-da, the shell containment of Spatial.Path.Direction.

theorem Pantcheva2011.source_contains_goal : Spatial.Path.Direction.place.shells ⊂ Spatial.Path.Direction.goal.shells ∧ Spatial.Path.Direction.goal.shells ⊂ Spatial.Path.Direction.source.shells ∧ Spatial.Path.Direction.source.shells ⊂ Spatial.Path.Direction.route.shells

Source contains Goal contains Place, as shell-stack inclusion.

theorem Pantcheva2011.georgian_loc_goal_possible : Possible ![0, 0, 1, 2]

Georgian's Location=Goal syncretism (Table 9.1) is Type 3.

The semantic ground of *A&¬A (§5.4)

theorem Pantcheva2011.goalSource_disjoint {ι : Type u_1} {α : Type u_2} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) : Spatial.Path.IsCofinal R γ → ¬Spatial.Path.IsCoinitial R γ

A Source path is a Goal path traversed the other way, so no path is both, and a single marker for Goal and Source would denote a path and its reverse at once, the ground of the *A&¬A constraint.