Idiom classification

An idiomatic expression is something a language user could fail to know while knowing everything else in the language ([FKOC88] §1). This file defines the paper's classificatory dimensions — decoding vs. encoding-only, grammatical vs. extragrammatical, substantive vs. formal — and its §1.2 typology by familiarity of pieces and of arrangement, with formality derived from the typed form rather than stipulated.

Main definitions

• IdiomInterpretability: decoding vs. encoding-only idioms
• IdiomGrammaticality: grammatical vs. extragrammatical idioms
• IdiomFormality.ofForm: substantive vs. formal, read off the slot structure
• Construction.IsFormalIdiom: constructions whose form is lexically open
• FamiliarityPattern: the pieces × arrangement typology, its fourth cell excluded by piecesFamiliar_of_arrangementFamiliar

Implementation notes

The paper's fourth contrast — idioms with vs. without pragmatic point (§1.1.4) — is the Construction.pragmaticPoint field.

inductive ConstructionGrammar.IdiomInterpretability : Type

A decoding idiom cannot be interpreted with confidence without prior learning; an encoding idiom is one whose conventionality must be learned. Every decoding idiom is an encoding idiom, so the cases are decoding ("kick the bucket", "pull a fast one") and encoding-only ("answer the door", "wide awake", "bright red") ([FKOC88] §1.1.1, following [Mak72]).

• decoding : IdiomInterpretability
• encodingOnly : IdiomInterpretability

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqIdiomInterpretability : DecidableEq IdiomInterpretability

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprIdiomInterpretability : Repr IdiomInterpretability

Equations

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

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

Equations

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

inductive ConstructionGrammar.IdiomGrammaticality : Type

A grammatical idiom has words filling proper and familiar grammatical structures ("kick the bucket", "spill the beans", "blow one's nose"); an extragrammatical idiom has structure the rest of the grammar cannot account for ("first off", "sight unseen", "all of a sudden", "by and large") ([FKOC88] §1.1.2).

• grammatical : IdiomGrammaticality
• extragrammatical : IdiomGrammaticality

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqIdiomGrammaticality : DecidableEq IdiomGrammaticality

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprIdiomGrammaticality : Repr IdiomGrammaticality

Equations

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

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

Equations

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

inductive ConstructionGrammar.IdiomFormality : Type

A substantive (lexically filled) idiom has fixed lexical content ("kick the bucket"); a formal (lexically open) idiom is a syntactic pattern dedicated to semantic and pragmatic purposes not knowable from its form alone ("the X-er the Y-er") ([FKOC88] §1.1.3).

• substantive : IdiomFormality
• formal : IdiomFormality

@[instance_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 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprIdiomFormality : Repr IdiomFormality

Equations

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

def ConstructionGrammar.IdiomFormality.ofForm {Lex : Type u_1} (form : TypedForm Lex) : IdiomFormality

The formality of a typed form: substantive iff lexically specified. The distinction is a cline ([FKOC88] fn. 3); derivedSpecificity discretizes it.

Equations

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

theorem ConstructionGrammar.IdiomFormality.ofForm_eq_substantive_iff {Lex : Type u_1} (form : TypedForm Lex) : ofForm form = substantive ↔ form ≠ [] ∧ ∀ s ∈ form, s.filler.isOpen = false

A form is substantive exactly when it is nonempty and no slot is open.

def ConstructionGrammar.Construction.IsFormalIdiom {Sem : Type u_2} (c : Construction Sem) : Prop

A formal idiom in the sense of [FKOC88] §1.1.3: a construction whose form is lexically open.

Equations

• c.IsFormalIdiom = (ConstructionGrammar.IdiomFormality.ofForm c.form = ConstructionGrammar.IdiomFormality.formal)

@[instance_reducible]

instance ConstructionGrammar.instDecidableIsFormalIdiom {Sem : Type u_2} (c : Construction Sem) : Decidable c.IsFormalIdiom

Equations

• ConstructionGrammar.instDecidableIsFormalIdiom c = ConstructionGrammar.instDecidableIsFormalIdiom._aux_1 c

inductive ConstructionGrammar.FamiliarityPattern : Type

How familiar are an idiom's pieces, and how familiar is their arrangement ([FKOC88] §1.2)? 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). The fourth cell is excluded by piecesFamiliar_of_arrangementFamiliar.

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

@[instance_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 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprFamiliarityPattern : Repr FamiliarityPattern

Equations

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

def ConstructionGrammar.FamiliarityPattern.PiecesFamiliar : FamiliarityPattern → Prop

The pieces coordinate: the idiom's pieces occur independently in the language. Fails only for idioms built on cranberry words ("kith", "main").

Equations

• x✝.PiecesFamiliar = (x✝ ≠ ConstructionGrammar.FamiliarityPattern.unfamiliarPiecesUnfamiliarlyArranged)

def ConstructionGrammar.FamiliarityPattern.ArrangementFamiliar : FamiliarityPattern → Prop

The arrangement coordinate: the pieces are combined according to familiar combinatorial principles.

Equations

• x✝.ArrangementFamiliar = (x✝ = ConstructionGrammar.FamiliarityPattern.familiarPiecesFamiliarlyArranged)

@[instance_reducible]

instance ConstructionGrammar.FamiliarityPattern.instDecidablePiecesFamiliar (p : FamiliarityPattern) : Decidable p.PiecesFamiliar

Equations

• p.instDecidablePiecesFamiliar = ConstructionGrammar.FamiliarityPattern.instDecidablePiecesFamiliar._aux_1 p

@[instance_reducible]

instance ConstructionGrammar.FamiliarityPattern.instDecidableArrangementFamiliar (p : FamiliarityPattern) : Decidable p.ArrangementFamiliar

Equations

• p.instDecidableArrangementFamiliar = ConstructionGrammar.FamiliarityPattern.instDecidableArrangementFamiliar._aux_1 p

theorem ConstructionGrammar.FamiliarityPattern.piecesFamiliar_of_arrangementFamiliar {p : FamiliarityPattern} (h : p.ArrangementFamiliar) : p.PiecesFamiliar

A familiar arrangement forces familiar pieces: unique pieces admit no standard principles of arrangement ([FKOC88] §1.2.1), so the fourth familiarity cell is uninhabited.

def ConstructionGrammar.FamiliarityPattern.grammaticality : FamiliarityPattern → IdiomGrammaticality

An idiom's §1.1.2 classification, determined by its familiarity pattern: an arrangement is familiar exactly when the general grammar accounts for it ([FKOC88] §1.2.2–1.2.3).

Equations

• ConstructionGrammar.FamiliarityPattern.familiarPiecesFamiliarlyArranged.grammaticality = ConstructionGrammar.IdiomGrammaticality.grammatical
• x✝.grammaticality = ConstructionGrammar.IdiomGrammaticality.extragrammatical

theorem ConstructionGrammar.FamiliarityPattern.grammaticality_eq_grammatical_iff (p : FamiliarityPattern) : p.grammaticality = IdiomGrammaticality.grammatical ↔ p.ArrangementFamiliar

A pattern is grammatical exactly when its arrangement is familiar.