Linglib.Phenomena.WordOrder.CrossSerial

source

structure Phenomena.WordOrder.CrossSerial.Dependency :

Type

A dependency pairing: which NP goes with which verb.

Position 1 is leftmost in the string.

npPosition : Nat
Position of the NP (1-indexed from left)
verbPosition : Nat
Position of the verb (1-indexed from left among verbs)

Instances For

source

def Phenomena.WordOrder.CrossSerial.instDecidableEqDependency.decEq (x✝ x✝¹ : Dependency) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Phenomena.WordOrder.CrossSerial.instDecidableEqDependency :

DecidableEq Dependency

Equations

Phenomena.WordOrder.CrossSerial.instDecidableEqDependency = Phenomena.WordOrder.CrossSerial.instDecidableEqDependency.decEq

source

def Phenomena.WordOrder.CrossSerial.instBEqDependency.beq :

Dependency → Dependency → Bool

Equations

Phenomena.WordOrder.CrossSerial.instBEqDependency.beq { npPosition := a, verbPosition := a_1 } { npPosition := b, verbPosition := b_1 } = (a == b && a_1 == b_1)
Phenomena.WordOrder.CrossSerial.instBEqDependency.beq x✝¹ x✝ = false

Instances For

source

instance Phenomena.WordOrder.CrossSerial.instBEqDependency :

BEq Dependency

Equations

Phenomena.WordOrder.CrossSerial.instBEqDependency = { beq := Phenomena.WordOrder.CrossSerial.instBEqDependency.beq }

source

instance Phenomena.WordOrder.CrossSerial.instReprDependency :

Repr Dependency

Equations

Phenomena.WordOrder.CrossSerial.instReprDependency = { reprPrec := Phenomena.WordOrder.CrossSerial.instReprDependency.repr }

source

def Phenomena.WordOrder.CrossSerial.instReprDependency.repr :

Dependency → Nat → Std.Format

Equations

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

Instances For

source

inductive Phenomena.WordOrder.CrossSerial.DependencyPattern :

Type

Dependency pattern: how NPs and verbs are paired.

crossSerial : DependencyPattern
nested : DependencyPattern

Instances For

source

instance Phenomena.WordOrder.CrossSerial.instDecidableEqDependencyPattern :

DecidableEq DependencyPattern

Equations

Phenomena.WordOrder.CrossSerial.instDecidableEqDependencyPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.WordOrder.CrossSerial.instBEqDependencyPattern.beq :

DependencyPattern → DependencyPattern → Bool

Equations

Phenomena.WordOrder.CrossSerial.instBEqDependencyPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.WordOrder.CrossSerial.instBEqDependencyPattern :

BEq DependencyPattern

Equations

Phenomena.WordOrder.CrossSerial.instBEqDependencyPattern = { beq := Phenomena.WordOrder.CrossSerial.instBEqDependencyPattern.beq }

source

instance Phenomena.WordOrder.CrossSerial.instReprDependencyPattern :

Repr DependencyPattern

Equations

Phenomena.WordOrder.CrossSerial.instReprDependencyPattern = { reprPrec := Phenomena.WordOrder.CrossSerial.instReprDependencyPattern.repr }

source

def Phenomena.WordOrder.CrossSerial.instReprDependencyPattern.repr :

DependencyPattern → Nat → Std.Format

Equations

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

Instances For

source

def Phenomena.WordOrder.CrossSerial.crossSerialDeps (n : Nat) :

List Dependency

Generate cross-serial dependencies for n NP-V pairs

Equations

Phenomena.WordOrder.CrossSerial.crossSerialDeps n = List.map (fun (i : Nat) => { npPosition := i + 1, verbPosition := i + 1 }) (List.range n)

Instances For

source

def Phenomena.WordOrder.CrossSerial.nestedDeps (n : Nat) :

List Dependency

Generate nested dependencies for n NP-V pairs

Equations

Phenomena.WordOrder.CrossSerial.nestedDeps n = List.map (fun (i : Nat) => { npPosition := i + 1, verbPosition := n - i }) (List.range n)

Instances For

source

structure Phenomena.WordOrder.CrossSerial.DutchExample :

Type

Dutch cross-serial dependency example.

Surface:... dat Jan Piet Marie zag helpen zwemmen Gloss:... that Jan Piet Marie saw help swim Meaning:... that Jan saw Piet help Marie swim

Dependencies:

Jan (NP₁) → zag (V₁) "saw"
Piet (NP₂) → helpen (V₂) "help"
Marie (NP₃) → zwemmen (V₃) "swim"

surface : String
Surface string (Dutch)
gloss : String
English gloss
translation : String
English translation
nps : List String
NPs in order
verbs : List String
Verbs in order
pattern : DependencyPattern
The observed dependency pattern
dependencies : List Dependency
The actual pairings

Instances For

source

def Phenomena.WordOrder.CrossSerial.instReprDutchExample.repr :

DutchExample → Nat → Std.Format

Equations

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

Instances For

source

instance Phenomena.WordOrder.CrossSerial.instReprDutchExample :

Repr DutchExample

Equations

Phenomena.WordOrder.CrossSerial.instReprDutchExample = { reprPrec := Phenomena.WordOrder.CrossSerial.instReprDutchExample.repr }

source

def Phenomena.WordOrder.CrossSerial.dutch_3np_3v :

DutchExample

Equations

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

Instances For

source

def Phenomena.WordOrder.CrossSerial.dutch_2np_2v :

DutchExample

Equations

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

Instances For

source

def Phenomena.WordOrder.CrossSerial.dutch_4np_4v :

DutchExample

Equations

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

Instances For

source

structure Phenomena.WordOrder.CrossSerial.GermanExample :

Type

German nested dependency example.

German has the opposite verb order from Dutch, giving nested dependencies that are context-free.

surface : String
gloss : String
translation : String
nps : List String
verbs : List String
pattern : DependencyPattern
dependencies : List Dependency

Instances For

source

def Phenomena.WordOrder.CrossSerial.instReprGermanExample.repr :

GermanExample → Nat → Std.Format

Equations

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

Instances For

source

instance Phenomena.WordOrder.CrossSerial.instReprGermanExample :

Repr GermanExample

Equations

Phenomena.WordOrder.CrossSerial.instReprGermanExample = { reprPrec := Phenomena.WordOrder.CrossSerial.instReprGermanExample.repr }

source

def Phenomena.WordOrder.CrossSerial.german_3np_3v :

GermanExample

Equations

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

Instances For

source

def Phenomena.WordOrder.CrossSerial.crossSerialRequires :

Core.FormalLanguageType

Cross-serial dependencies require mild context-sensitivity.

Proven formally for Swiss German in Phenomena.WordOrder.Studies.Shieber1985 via the pumping lemma.

Equations

Phenomena.WordOrder.CrossSerial.crossSerialRequires = Core.FormalLanguageType.mildlyContextSensitive

Instances For

source

def Phenomena.WordOrder.CrossSerial.nestedRequires :

Core.FormalLanguageType

Nested dependencies are context-free.

Equations

Phenomena.WordOrder.CrossSerial.nestedRequires = Core.FormalLanguageType.contextFree

Instances For

source

def Phenomena.WordOrder.CrossSerial.allDutchExamples :

List DutchExample

Equations

Phenomena.WordOrder.CrossSerial.allDutchExamples = [Phenomena.WordOrder.CrossSerial.dutch_2np_2v , Phenomena.WordOrder.CrossSerial.dutch_3np_3v , Phenomena.WordOrder.CrossSerial.dutch_4np_4v ]

Instances For

source

def Phenomena.WordOrder.CrossSerial.allGermanExamples :

List GermanExample

Equations

Phenomena.WordOrder.CrossSerial.allGermanExamples = [Phenomena.WordOrder.CrossSerial.german_3np_3v ]

Instances For

source

theorem Phenomena.WordOrder.CrossSerial.crossSerial_length (n : Nat) :

(crossSerialDeps n).length = n

Cross-serial has same number of dependencies as NPs

source

theorem Phenomena.WordOrder.CrossSerial.nested_length (n : Nat) :

(nestedDeps n).length = n

Nested has same number of dependencies as NPs

source

theorem Phenomena.WordOrder.CrossSerial.dutch_3_is_crossSerial :

dutch_3np_3v.pattern = DependencyPattern.crossSerial

Dutch 3-NP example has cross-serial pattern

source

theorem Phenomena.WordOrder.CrossSerial.german_3_is_nested :

german_3np_3v.pattern = DependencyPattern.nested

German 3-NP example has nested pattern