Construction Grammar: Idiom Typology

[FKOC88] §1's classification of idiomatic expressions, the founding taxonomy of Construction Grammar: decoding vs. encoding idioms (following [Mak72], §1.1.1), grammatical vs. extragrammatical (§1.1.2), substantive vs. formal (§1.1.3), and the familiar-pieces typology of §1.2. Originates with that paper; consumed by later construction-grammar studies (Kay & Fillmore 1999's WXDY, Osborne & Groß 2012's catena analysis).

Main declarations

• IdiomInterpretability, IdiomGrammaticality, IdiomFormality: the three classificatory dimensions
• IdiomType: their product
• FamiliarityPattern: §1.2's pieces × arrangement typology

inductive ConstructionGrammar.IdiomInterpretability : Type

Decoding vs. encoding idioms ([FKOC88] §1.1.1, following [Mak72]). A decoding idiom cannot be interpreted without prior learning ("kick the bucket"). An encoding idiom can be understood on first hearing, but its conventionality must be learned ("answer the door"). Decoding idioms are generally also encoding idioms.

• decoding : IdiomInterpretability
• encoding : IdiomInterpretability

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqIdiomInterpretability : DecidableEq IdiomInterpretability

Equations

• ConstructionGrammar.instDecidableEqIdiomInterpretability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ConstructionGrammar.instReprIdiomInterpretability : Repr IdiomInterpretability

Equations

• ConstructionGrammar.instReprIdiomInterpretability = { reprPrec := ConstructionGrammar.instReprIdiomInterpretability.repr }

def ConstructionGrammar.instReprIdiomInterpretability.repr : IdiomInterpretability → Nat → Std.Format

Equations

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

inductive ConstructionGrammar.IdiomGrammaticality : Type

Grammatical vs. extragrammatical idioms ([FKOC88] §1.1.2). Grammatical idioms have words filling proper grammatical slots ("kick the bucket", "spill the beans"); extragrammatical idioms have anomalous structure ("first off", "by and large", "so far so good").

• grammatical : IdiomGrammaticality
• extragrammatical : IdiomGrammaticality

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqIdiomGrammaticality : DecidableEq IdiomGrammaticality

Equations

• ConstructionGrammar.instDecidableEqIdiomGrammaticality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprIdiomGrammaticality.repr : IdiomGrammaticality → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprIdiomGrammaticality : Repr IdiomGrammaticality

Equations

• ConstructionGrammar.instReprIdiomGrammaticality = { reprPrec := ConstructionGrammar.instReprIdiomGrammaticality.repr }

inductive ConstructionGrammar.IdiomFormality : Type

Substantive vs. formal idioms ([FKOC88] §1.1.3). Substantive (lexically filled) idioms have fixed lexical content ("kick the bucket"); formal idioms are productive syntactic patterns "dedicated to semantic and pragmatic purposes not knowable from their form alone" ("the X-er the Y-er").

• substantive : IdiomFormality
• formal : IdiomFormality

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqIdiomFormality : DecidableEq IdiomFormality

Equations

• ConstructionGrammar.instDecidableEqIdiomFormality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprIdiomFormality.repr : IdiomFormality → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprIdiomFormality : Repr IdiomFormality

Equations

• ConstructionGrammar.instReprIdiomFormality = { reprPrec := ConstructionGrammar.instReprIdiomFormality.repr }

structure ConstructionGrammar.IdiomType : Type

Combined idiom classification: the product of [FKOC88] §1.1's three dimensions.

• interpretability : IdiomInterpretability
• grammaticality : IdiomGrammaticality
• formality : IdiomFormality

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqIdiomType : DecidableEq IdiomType

Equations

• ConstructionGrammar.instDecidableEqIdiomType = ConstructionGrammar.instDecidableEqIdiomType.decEq

def ConstructionGrammar.instDecidableEqIdiomType.decEq (x✝ x✝¹ : IdiomType) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprIdiomType : Repr IdiomType

Equations

• ConstructionGrammar.instReprIdiomType = { reprPrec := ConstructionGrammar.instReprIdiomType.repr }

def ConstructionGrammar.instReprIdiomType.repr : IdiomType → Nat → Std.Format

Equations

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

inductive ConstructionGrammar.FamiliarityPattern : Type

Familiar-pieces typology ([FKOC88] §1.2): how familiar are an idiom's pieces, and how familiar is their arrangement? Unfamiliar pieces unfamiliarly arranged: "kith and kin" (§1.2.1); familiar pieces unfamiliarly arranged: "all of a sudden", bare "home" (§1.2.2); familiar pieces familiarly arranged: "hang one on", rhetorical questions (§1.2.3).

• unfamiliarPiecesUnfamiliarlyArranged : FamiliarityPattern
• familiarPiecesUnfamiliarlyArranged : FamiliarityPattern
• familiarPiecesFamiliarlyArranged : FamiliarityPattern

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqFamiliarityPattern : DecidableEq FamiliarityPattern

Equations

• ConstructionGrammar.instDecidableEqFamiliarityPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprFamiliarityPattern.repr : FamiliarityPattern → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprFamiliarityPattern : Repr FamiliarityPattern

Equations

• ConstructionGrammar.instReprFamiliarityPattern = { reprPrec := ConstructionGrammar.instReprFamiliarityPattern.repr }