Combination Schema

Theory-neutral interface for @cite{mueller-2013}'s three universal combination schemata.

All syntactic theories (Minimalism, HPSG, CCG, CxG, DG) converge on three fundamental modes of combination:

Schema	Minimalism	HPSG	CCG	DG
Head-Complement	Ext Merge (1st)	Head-Comp	fapp/bapp	obj/det/... dep
Head-Specifier	Ext Merge (later)	Head-Subj	T+bapp	subj dep
Head-Filler	Int Merge	Head-Filler	fcomp/bcomp	non-proj dep

inductive Core.Interfaces.CombinationKind : Type

Müller's three universal combination schemata (§2).

Every syntactic theory implements these three modes of combination, though they use different terminology and formalisms.

• headComplement : CombinationKind

  Head combines with its complement (first-merged argument). Minimalism: External Merge (first); HPSG: Head-Complement Schema; CCG: forward/backward application; DG: core dependency (obj, det,...).

• headSpecifier : CombinationKind

  Head combines with its specifier (later-merged argument). Minimalism: External Merge (later); HPSG: Head-Subject Schema; CCG: type-raise + backward app; DG: subject dependency.

• headFiller : CombinationKind

  Filler combines with a gapped structure (long-distance dependency). Minimalism: Internal Merge; HPSG: Head-Filler Schema; CCG: forward/backward composition; DG: non-projective dependency.

instance Core.Interfaces.instReprCombinationKind : Repr CombinationKind

Equations

• Core.Interfaces.instReprCombinationKind = { reprPrec := Core.Interfaces.instReprCombinationKind.repr }

def Core.Interfaces.instReprCombinationKind.repr : CombinationKind → Nat → Std.Format

Equations

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

instance Core.Interfaces.instDecidableEqCombinationKind : DecidableEq CombinationKind

Equations

• Core.Interfaces.instDecidableEqCombinationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Interfaces.instBEqCombinationKind.beq : CombinationKind → CombinationKind → Bool

Equations

• Core.Interfaces.instBEqCombinationKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Interfaces.instBEqCombinationKind : BEq CombinationKind

Equations

• Core.Interfaces.instBEqCombinationKind = { beq := Core.Interfaces.instBEqCombinationKind.beq }

class Core.Interfaces.HasCombinationSchemata (T : Type) : Type 1

Core convergence: a theory provides three combination schemata.

This is the minimal interface for Müller's convergence claim. T is a theory tag type (e.g., Minimalism, HPSG). Expr is the theory's expression type (e.g., SyntacticObject, Sign).

• Expr : Type

  The expression type for this theory

• classify : Expr T → Expr T → Expr T → Option CombinationKind

  Classify a combination of head + nonHead → result as one of the three schemata

• catOf : Expr T → Option UD.UPOS

  Get the category of an expression (if available)

class Core.Interfaces.HasHeadFeaturePrinciple (T : Type) extends Core.Interfaces.HasCombinationSchemata T : Type 1

Müller's labeling claim (§2.1): the head determines the category of the result.

This is the Head Feature Principle: in any combination, the category of the resulting phrase equals the category of the head daughter.

• Expr : Type
• classify : Expr T → Expr T → Expr T → Option CombinationKind
• catOf : Expr T → Option UD.UPOS
• headDeterminesLabel (head nonHead result : HasCombinationSchemata.Expr T) : HasCombinationSchemata.classify head nonHead result ≠ none → HasCombinationSchemata.catOf result = HasCombinationSchemata.catOf head

  The head's category determines the result's category

class Core.Interfaces.HasCoordination (T : Type) extends Core.Interfaces.HasCombinationSchemata T : Type 1

Coordination diagnostic (§2.2): same category required.

Coordination is a diagnostic for constituency: only expressions of the same category can coordinate. This holds across all theories.

• Expr : Type
• classify : Expr T → Expr T → Expr T → Option CombinationKind
• catOf : Expr T → Option UD.UPOS
• canCoordinate : HasCombinationSchemata.Expr T → HasCombinationSchemata.Expr T → Bool

  Whether two expressions can coordinate