CCG combinatory rules as combinatory-logic combinators

CCG's combinatory rules correspond to the basis combinators of combinatory logic ([CF58], [Smu85]): forward and backward composition to B, type-raising to T, the substitution rule to S. The combinator algebra itself lives in Semantics/Composition/Combinator.lean; this file establishes the correspondence between those combinators and the types CCG assigns (catToTy), so that each rule's semantic action is literally a combinator acting on Denot meanings ([Ste00a], Chapters 3 and 8).

theorem CCG.Combinators.fcomp_is_B {E W : Type} {x y z : Cat} (f_sem : Intensional.Denot E W (catToTy (x.rslash y))) (g_sem : Intensional.Denot E W (catToTy (y.rslash z))) : (fun (arg : Intensional.Denot E W (catToTy z)) => f_sem (g_sem arg)) = Combinator.B f_sem g_sem

Forward composition is B: its semantics is B f g.

theorem CCG.Combinators.fcomp_type_is_B (x _y z : Cat) : catToTy (x.rslash z) = (catToTy z ⇒ catToTy x)

The type of a forward-composition result.

theorem CCG.Combinators.bcomp_is_B {E W : Type} {x y z : Cat} (g_sem : Intensional.Denot E W (catToTy (y.lslash z))) (f_sem : Intensional.Denot E W (catToTy (x.lslash y))) : (fun (arg : Intensional.Denot E W (catToTy z)) => f_sem (g_sem arg)) = Combinator.B f_sem g_sem

Backward composition is also B, with reversed linear order.

theorem CCG.Combinators.type_raise_is_T {E W : Type} {x t : Cat} (a_sem : Intensional.Denot E W (catToTy x)) : (fun (f : Intensional.Denot E W (catToTy (t.lslash x))) => f a_sem) = Combinator.T a_sem

Forward type-raising is T: its semantics is T a.

theorem CCG.Combinators.ftr_type_is_T (x t : Cat) : catToTy (forwardTypeRaise x t) = ((catToTy x ⇒ catToTy t) ⇒ catToTy t)

The type of a forward-type-raised category T/(T\X).

theorem CCG.Combinators.btr_type_is_T (x t : Cat) : catToTy (backwardTypeRaise x t) = ((catToTy x ⇒ catToTy t) ⇒ catToTy t)

Backward type-raising has the same type as forward type-raising.

theorem CCG.Combinators.crossed_comp_is_S {E W : Type} {x y z : Cat} (f_sem : Intensional.Denot E W (catToTy ((x.rslash y).rslash z))) (g_sem : Intensional.Denot E W (catToTy (y.rslash z))) : (fun (arg : Intensional.Denot E W (catToTy z)) => f_sem arg (g_sem arg)) = Combinator.S f_sem g_sem

Crossed composition is S: (X/Y)/Z + Y/Z ⇒ X/Z with S f g x = f x (g x).

theorem CCG.Combinators.fapp_via_T {E W : Type} {x y : Cat} (f_sem : Intensional.Denot E W (catToTy (x.rslash y))) (a_sem : Intensional.Denot E W (catToTy y)) : f_sem a_sem = Combinator.T a_sem f_sem

Forward application is T applied the other way: f a = T a f.

theorem CCG.Combinators.subject_verb_composition {E W : Type} (subj_sem : Intensional.Denot E W (catToTy NP)) (verb_sem : Intensional.Denot E W (catToTy TV)) (obj : Intensional.Denot E W (catToTy NP)) : Combinator.B (Combinator.T subj_sem) verb_sem obj = verb_sem obj subj_sem

Non-constituent coordination: a type-raised subject composed (B) with a transitive verb is a function from objects to truth values — B (T subj) verb obj = verb obj subj. This is the combinator account of "John likes and Mary hates beans".