inductive CCG.Atom : Type

Atomic categories.

• S : Atom
• NP : Atom
• N : Atom
• PP : Atom

instance CCG.instReprAtom : Repr Atom

Equations

• CCG.instReprAtom = { reprPrec := CCG.instReprAtom.repr }

def CCG.instReprAtom.repr : Atom → Nat → Std.Format

Equations

• CCG.instReprAtom.repr CCG.Atom.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.S")).group prec✝
• CCG.instReprAtom.repr CCG.Atom.NP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.NP")).group prec✝
• CCG.instReprAtom.repr CCG.Atom.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.N")).group prec✝
• CCG.instReprAtom.repr CCG.Atom.PP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CCG.Atom.PP")).group prec✝

instance CCG.instDecidableEqAtom : DecidableEq Atom

Equations

• CCG.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CCG.Cat : Type

CCG categories.

• atom : Atom → Cat
• rslash : Cat → Cat → Cat
• lslash : Cat → Cat → Cat

def CCG.instReprCat.repr : Cat → Nat → Std.Format

Equations

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

instance CCG.instReprCat : Repr Cat

Equations

• CCG.instReprCat = { reprPrec := CCG.instReprCat.repr }

instance CCG.instDecidableEqCat : DecidableEq Cat

Equations

• CCG.instDecidableEqCat = CCG.instDecidableEqCat.decEq

def CCG.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (CCG.Cat.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (a_1.rslash a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (CCG.Cat.atom a) (a_1.lslash a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.rslash a_1) (CCG.Cat.atom a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.rslash a_1) (a_2.lslash a_3) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.lslash a_1) (CCG.Cat.atom a_2) = isFalse ⋯
• CCG.instDecidableEqCat.decEq (a.lslash a_1) (a_2.rslash a_3) = isFalse ⋯

def CCG.«term_/_» : Lean.TrailingParserDescr

Equations

• CCG.«term_/_» = Lean.ParserDescr.trailingNode `CCG.«term_/_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "/") (Lean.ParserDescr.cat `term 0))

def CCG.«term_\_» : Lean.TrailingParserDescr

Equations

• CCG.«term_\_» = Lean.ParserDescr.trailingNode `CCG.«term_\_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "\\") (Lean.ParserDescr.cat `term 0))

def CCG.S : Cat

Equations

• CCG.S = CCG.Cat.atom CCG.Atom.S

def CCG.NP : Cat

Equations

• CCG.NP = CCG.Cat.atom CCG.Atom.NP

def CCG.N : Cat

Equations

• CCG.N = CCG.Cat.atom CCG.Atom.N

def CCG.PP : Cat

Equations

• CCG.PP = CCG.Cat.atom CCG.Atom.PP

def CCG.IV : Cat

Equations

• CCG.IV = CCG.S.lslash CCG.NP

def CCG.TV : Cat

Equations

• CCG.TV = (CCG.S.lslash CCG.NP).rslash CCG.NP

def CCG.DTV : Cat

Equations

• CCG.DTV = ((CCG.S.lslash CCG.NP).rslash CCG.NP).rslash CCG.NP

def CCG.Det : Cat

Equations

• CCG.Det = CCG.NP.rslash CCG.N

def CCG.Prep : Cat

Equations

• CCG.Prep = CCG.PP.rslash CCG.NP

def CCG.AdjAttr : Cat

Equations

• CCG.AdjAttr = CCG.N.rslash CCG.N

def CCG.AdjPred : Cat

Equations

• CCG.AdjPred = CCG.S.lslash CCG.NP

def CCG.forwardApp : Cat → Cat → Option Cat

Forward application: X/Y Y => X.

Equations

• CCG.forwardApp (x_2.rslash y) x✝ = if (y == x✝) = true then some x_2 else none
• CCG.forwardApp x✝¹ x✝ = none

def CCG.backwardApp : Cat → Cat → Option Cat

Backward application: Y X\Y => X.

Equations

• CCG.backwardApp x✝ (x_2.lslash y) = if (y == x✝) = true then some x_2 else none
• CCG.backwardApp x✝¹ x✝ = none

def CCG.forwardComp : Cat → Cat → Option Cat

Forward composition: X/Y Y/Z => X/Z.

Equations

• CCG.forwardComp (x_2.rslash y) (y'.rslash z) = if (y == y') = true then some (x_2.rslash z) else none
• CCG.forwardComp x✝¹ x✝ = none

def CCG.backwardComp : Cat → Cat → Option Cat

Backward composition: Y\Z X\Y => X\Z.

Equations

• CCG.backwardComp (y.lslash z) (x_2.lslash y') = if (y == y') = true then some (x_2.lslash z) else none
• CCG.backwardComp x✝¹ x✝ = none

def CCG.combine : Cat → Cat → Option Cat

Try to combine two categories using all available rules.

Equations

• CCG.combine x✝¹ x✝ = (CCG.forwardApp x✝¹ x✝ <|> CCG.backwardApp x✝¹ x✝ <|> CCG.forwardComp x✝¹ x✝ <|> CCG.backwardComp x✝¹ x✝)

def CCG.forwardTypeRaise (x t : Cat) : Cat

Forward type-raising: X => T/(T\X).

Equations

• CCG.forwardTypeRaise x t = t.rslash (t.lslash x)

def CCG.backwardTypeRaise (x t : Cat) : Cat

Backward type-raising: X => T(T/X).

Equations

• CCG.backwardTypeRaise x t = t.lslash (t.rslash x)

def CCG.NPsubj : Cat

Equations

• CCG.NPsubj = CCG.forwardTypeRaise CCG.NP CCG.S

def CCG.NPobj : Cat

Equations

• CCG.NPobj = CCG.backwardTypeRaise CCG.NP CCG.S

def CCG.coordinate : Cat → Cat → Option Cat

Coordination: X conj X => X.

Equations

• CCG.coordinate x✝¹ x✝ = if (x✝¹ == x✝) = true then some x✝¹ else none

structure CCG.LexEntry : Type

A CCG lexical entry.

• form : String
• cat : Cat

instance CCG.instReprLexEntry : Repr LexEntry

Equations

• CCG.instReprLexEntry = { reprPrec := CCG.instReprLexEntry.repr }

def CCG.instReprLexEntry.repr : LexEntry → Nat → Std.Format

Equations

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

def CCG.Lexicon : Type

A CCG lexicon.

Equations

• CCG.Lexicon = List CCG.LexEntry

def CCG.exampleLexicon : Lexicon

Equations

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

inductive CCG.DerivStep : Type

A derivation step.

• lex : LexEntry → DerivStep
• fapp : DerivStep → DerivStep → DerivStep
• bapp : DerivStep → DerivStep → DerivStep
• fcomp : DerivStep → DerivStep → DerivStep
• bcomp : DerivStep → DerivStep → DerivStep
• ftr : DerivStep → Cat → DerivStep
• btr : DerivStep → Cat → DerivStep
• coord : DerivStep → DerivStep → DerivStep

def CCG.instReprDerivStep.repr : DerivStep → Nat → Std.Format

Equations

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

instance CCG.instReprDerivStep : Repr DerivStep

Equations

• CCG.instReprDerivStep = { reprPrec := CCG.instReprDerivStep.repr }

def CCG.DerivStep.cat : DerivStep → Option Cat

Get the category of a derivation.

Equations

• (CCG.DerivStep.lex a).cat = some a.cat
• (a.fapp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardApp c1 c2
• (a.bapp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.backwardApp c1 c2
• (a.fcomp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.forwardComp c1 c2
• (a.bcomp a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.backwardComp c1 c2
• (a.ftr a_1).cat = do let x ← a.cat some (CCG.forwardTypeRaise x a_1)
• (a.btr a_1).cat = do let x ← a.cat some (CCG.backwardTypeRaise x a_1)
• (a.coord a_1).cat = do let c1 ← a.cat let c2 ← a_1.cat CCG.coordinate c1 c2

def CCG.john_sleeps : DerivStep

Equations

• CCG.john_sleeps = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.sees_mary : DerivStep

Equations

• CCG.sees_mary = (CCG.DerivStep.lex { form := "sees", cat := CCG.TV }).fapp (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP })

def CCG.john_sees_mary : DerivStep

Equations

• CCG.john_sees_mary = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp CCG.sees_mary

def CCG.the_cat : DerivStep

Equations

• CCG.the_cat = (CCG.DerivStep.lex { form := "the", cat := CCG.Det }).fapp (CCG.DerivStep.lex { form := "cat", cat := CCG.N })

def CCG.the_cat_sleeps : DerivStep

Equations

• CCG.the_cat_sleeps = CCG.the_cat.bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.big_cat : DerivStep

Equations

• CCG.big_cat = (CCG.DerivStep.lex { form := "big", cat := CCG.AdjAttr }).fapp (CCG.DerivStep.lex { form := "cat", cat := CCG.N })

def CCG.the_big_cat : DerivStep

Equations

• CCG.the_big_cat = (CCG.DerivStep.lex { form := "the", cat := CCG.Det }).fapp CCG.big_cat

def CCG.the_big_cat_sleeps : DerivStep

Equations

• CCG.the_big_cat_sleeps = CCG.the_big_cat.bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.derivesS (d : DerivStep) : Bool

Check if a derivation yields category S.

Equations

• CCG.derivesS d = (d.cat == some CCG.S)

def CCG.DerivStep.opCount : DerivStep → Nat

Count combinatory operations in a derivation.

Equations

• (CCG.DerivStep.lex a).opCount = 0
• (a.fapp a_1).opCount = 1 + a.opCount + a_1.opCount
• (a.bapp a_1).opCount = 1 + a.opCount + a_1.opCount
• (a.fcomp a_1).opCount = 2 + a.opCount + a_1.opCount
• (a.bcomp a_1).opCount = 2 + a.opCount + a_1.opCount
• (a.ftr a_1).opCount = 1 + a.opCount
• (a.btr a_1).opCount = 1 + a.opCount
• (a.coord a_1).opCount = 1 + a.opCount + a_1.opCount

def CCG.DerivStep.depth : DerivStep → Nat

Depth of derivation tree.

Equations

• (CCG.DerivStep.lex a).depth = 1
• (a.fapp a_1).depth = 1 + max a.depth a_1.depth
• (a.bapp a_1).depth = 1 + max a.depth a_1.depth
• (a.fcomp a_1).depth = 1 + max a.depth a_1.depth
• (a.bcomp a_1).depth = 1 + max a.depth a_1.depth
• (a.ftr a_1).depth = 1 + a.depth
• (a.btr a_1).depth = 1 + a.depth
• (a.coord a_1).depth = 1 + max a.depth a_1.depth

def CCG.john_tr : DerivStep

Equations

• CCG.john_tr = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).ftr CCG.S

def CCG.john_likes : DerivStep

Equations

• CCG.john_likes = CCG.john_tr.fcomp (CCG.DerivStep.lex { form := "likes", cat := CCG.TV })

def CCG.mary_tr : DerivStep

Equations

• CCG.mary_tr = (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }).ftr CCG.S

def CCG.mary_hates : DerivStep

Equations

• CCG.mary_hates = CCG.mary_tr.fcomp (CCG.DerivStep.lex { form := "hates", cat := CCG.TV })

def CCG.john_likes_and_mary_hates : DerivStep

Equations

• CCG.john_likes_and_mary_hates = CCG.john_likes.coord CCG.mary_hates

def CCG.john_likes_and_mary_hates_beans : DerivStep

Equations

• CCG.john_likes_and_mary_hates_beans = CCG.john_likes_and_mary_hates.fapp (CCG.DerivStep.lex { form := "beans", cat := CCG.NP })