Terms of the composition modes

A tree that the composition modes interpret has a logical form: the term recording the constants its words translate to, the variables its traces bind, and the mode by which each binary node composes its daughters (HeimKratzer.Term, HeimKratzer.Tree.translate). Translation is the one type-driven step: a terminal translates to its word's constant, a binary node to the composition of its daughters' terms by the mode their types select, a trace to the variable of its index, and a binder to the abstraction over that variable.

Every interpretation of the trees is an evaluation of their terms: the denotation, under an assignment of the variables (HeimKratzer.Term.eval); the denotation under an applicative effect, where abstraction needs the effect's distributor (HeimKratzer.Term.evalM); and the partial denotation of Composition/Partial.lean. Each is defined by recursion on terms, once for all trees.

Main definitions

• HeimKratzer.Term: the terms over a signature of constants.
• HeimKratzer.Term.eval, HeimKratzer.Term.evalM: the denotation of a term, pure and under an applicative effect.
• HeimKratzer.PredAbs: the distributor an effect needs for abstraction.
• HeimKratzer.Tree.translate: the term a tree translates to.

Main results

• HeimKratzer.Term.evalM_id: at the identity effect, evaluation is the pure denotation.
• HeimKratzer.Term.evalM_congr_of_agree: a term's denotation depends on the assignment only at its free variables.
• HeimKratzer.Tree.translate_map_const: translation commutes with renaming the constants.
• HeimKratzer.Tree.freeVars_subset: the free variables of a tree's term are its free traces.

Implementation notes

Variables are named by the trace indices, so a binder with index n translates to the abstraction over the variable n, and translation needs no fresh names.

References

• [HK98]
• [Mon73]

inductive HeimKratzer.Term (K : Montague.Ty → Type u) : Montague.Ty → Type u

The terms over a signature K of constants are, by type, the constants, the variables of type e, the abstractions over a variable, and the compositions of two terms by a mode.

• const {K : Montague.Ty → Type u} {ty : Montague.Ty} (c : K ty) : Term K ty
• var {K : Montague.Ty → Type u} (n : ℕ) : Term K Montague.Ty.e
• lam {K : Montague.Ty → Type u} {τ : Montague.Ty} (n : ℕ) (body : Term K τ) : Term K (Montague.Ty.e ⇒ τ)
• comp {K : Montague.Ty → Type u} {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) (l : Term K σ₁) (r : Term K σ₂) : Term K τ

class HeimKratzer.PredAbs (M : Type → Type) (E W : Type) (D : Type := ℝ) : Type

An effect supports Predicate Abstraction when it has an entity-distributor, which commutes M over entity-indexed families. Id and the Reader-like effects have one; scope effects such as Cont R do not, since abstraction would have to run one continuation at every entity at once, and record that by dist? = none.

• dist? : Option ((ty : Montague.Ty) → (E → M (Montague.Ty.Domain E W ty D)) → M (E → Montague.Ty.Domain E W ty D))

  The entity-distributor, if the effect has one.

@[instance_reducible]

instance HeimKratzer.instPredAbsId (E W D : Type) : PredAbs Id E W D

Equations

• HeimKratzer.instPredAbsId E W D = { dist? := some fun (x : Montague.Ty) (f : E → Id (Montague.Ty.Domain E W x D)) => f }

@[simp]

theorem HeimKratzer.PredAbs.dist?_id (E W D : Type) : dist? = some fun (x : Montague.Ty) (f : E → Id (Montague.Ty.Domain E W x D)) => f

def HeimKratzer.Term.map {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} (f : {ty : Montague.Ty} → K ty → K' ty) {ty : Montague.Ty} : Term K ty → Term K' ty

Rename the constants of a term.

Equations

• HeimKratzer.Term.map f (HeimKratzer.Term.const c) = HeimKratzer.Term.const (f c)
• HeimKratzer.Term.map f (HeimKratzer.Term.var n) = HeimKratzer.Term.var n
• HeimKratzer.Term.map f (HeimKratzer.Term.lam n b) = HeimKratzer.Term.lam n (HeimKratzer.Term.map (fun {ty : Montague.Ty} => f) b)
• HeimKratzer.Term.map f (HeimKratzer.Term.comp m l r) = HeimKratzer.Term.comp m (HeimKratzer.Term.map (fun {ty : Montague.Ty} => f) l) (HeimKratzer.Term.map (fun {ty : Montague.Ty} => f) r)

def HeimKratzer.Term.freeVars {K : Montague.Ty → Type u_1} {ty : Montague.Ty} : Term K ty → Finset ℕ

The free variables of a term.

Equations

• (HeimKratzer.Term.const c).freeVars = ∅
• (HeimKratzer.Term.var n).freeVars = {n}
• (HeimKratzer.Term.lam n b).freeVars = b.freeVars.erase n
• (HeimKratzer.Term.comp m l r).freeVars = l.freeVars ∪ r.freeVars

inductive HeimKratzer.Term.Rel {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} (R : (ty : Montague.Ty) → K ty → K' ty → Prop) {ty : Montague.Ty} : Term K ty → Term K' ty → Prop

Two terms over two signatures have the same shape, with constants related by R.

• const {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} {R : (ty : Montague.Ty) → K ty → K' ty → Prop} {ty : Montague.Ty} {c : K ty} {c' : K' ty} : R ty c c' → Rel R (Term.const c) (Term.const c')
• var {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} {R : (ty : Montague.Ty) → K ty → K' ty → Prop} (n : ℕ) : Rel R (Term.var n) (Term.var n)
• lam {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} {R : (ty : Montague.Ty) → K ty → K' ty → Prop} {τ : Montague.Ty} (n : ℕ) {b : Term K τ} {b' : Term K' τ} : Rel R b b' → Rel R (Term.lam n b) (Term.lam n b')
• comp {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} {R : (ty : Montague.Ty) → K ty → K' ty → Prop} {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) {l : Term K σ₁} {l' : Term K' σ₁} {r : Term K σ₂} {r' : Term K' σ₂} : Rel R l l' → Rel R r r' → Rel R (Term.comp m l r) (Term.comp m l' r')

def HeimKratzer.Term.eval {K : Montague.Ty → Type u_1} {E W D : Type} (I : {ty : Montague.Ty} → K ty → Montague.Ty.Domain E W ty D) (g : Assignment E) {ty : Montague.Ty} : Term K ty → Montague.Ty.Domain E W ty D

The denotation of a term under an interpretation of the constants and an assignment of the variables.

Equations

• HeimKratzer.Term.eval I g (HeimKratzer.Term.const c) = I c
• HeimKratzer.Term.eval I g (HeimKratzer.Term.var n) = g n
• HeimKratzer.Term.eval I g (HeimKratzer.Term.lam n b) = fun (x : Montague.Ty.Domain E W Montague.Ty.e D) => HeimKratzer.Term.eval (fun {ty : Montague.Ty} => I) (Function.update g n x) b
• HeimKratzer.Term.eval I g (HeimKratzer.Term.comp m l r) = m.eval (HeimKratzer.Term.eval (fun {ty : Montague.Ty} => I) g l) (HeimKratzer.Term.eval (fun {ty : Montague.Ty} => I) g r)

def HeimKratzer.Term.evalM {K : Montague.Ty → Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] (I : {ty : Montague.Ty} → K ty → M (Montague.Ty.Domain E W ty D)) (g : Assignment E) {ty : Montague.Ty} : Term K ty → Option (M (Montague.Ty.Domain E W ty D))

evalM I g t is the denotation of t under an applicative effect, given an interpretation I of the constants as computations and an assignment g. A composition runs its left daughter first, and an abstraction distributes the effect over the entities, so evalM is none when the effect has no distributor.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Term.evalM I g (HeimKratzer.Term.const c) = some (I c)
• HeimKratzer.Term.evalM I g (HeimKratzer.Term.var n) = some (pure (g n))

@[simp]

theorem HeimKratzer.Term.evalM_id {K : Montague.Ty → Type u_1} {E W D : Type} (I : {ty : Montague.Ty} → K ty → Montague.Ty.Domain E W ty D) (g : Assignment E) {ty : Montague.Ty} (t : Term K ty) : evalM (fun {ty : Montague.Ty} => I) g t = some (eval (fun {ty : Montague.Ty} => I) g t)

At the identity effect, evaluation is the pure denotation.

theorem HeimKratzer.Term.eval_map {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} {E W D : Type} (I : {ty : Montague.Ty} → K' ty → Montague.Ty.Domain E W ty D) (f : {ty : Montague.Ty} → K ty → K' ty) (g : Assignment E) {ty : Montague.Ty} (t : Term K ty) : eval (fun {ty : Montague.Ty} => I) g (map (fun {ty : Montague.Ty} => f) t) = eval (fun {ty : Montague.Ty} (c : K ty) => I (f c)) g t

The denotation of a renamed term interprets the renamed constants.

theorem HeimKratzer.Term.evalM_map {K : Montague.Ty → Type u_1} {K' : Montague.Ty → Type u_2} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] (I : {ty : Montague.Ty} → K' ty → M (Montague.Ty.Domain E W ty D)) (f : {ty : Montague.Ty} → K ty → K' ty) (g : Assignment E) {ty : Montague.Ty} (t : Term K ty) : evalM (fun {ty : Montague.Ty} => I) g (map (fun {ty : Montague.Ty} => f) t) = evalM (fun {ty : Montague.Ty} (c : K ty) => I (f c)) g t

Evaluating a renamed term interprets the renamed constants.

theorem HeimKratzer.Term.isSome_evalM {K : Montague.Ty → Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] (I : {ty : Montague.Ty} → K ty → M (Montague.Ty.Domain E W ty D)) (g g' : Assignment E) {ty : Montague.Ty} (t : Term K ty) : (evalM (fun {ty : Montague.Ty} => I) g t).isSome = (evalM (fun {ty : Montague.Ty} => I) g' t).isSome

Whether a term has a denotation under an effect, and at which type, does not depend on the assignment.

theorem HeimKratzer.Term.evalM_congr_of_agree {K : Montague.Ty → Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] (I : {ty : Montague.Ty} → K ty → M (Montague.Ty.Domain E W ty D)) {ty : Montague.Ty} (t : Term K ty) {g g' : Assignment E} (h : ∀ n ∈ t.freeVars, g n = g' n) : evalM (fun {ty : Montague.Ty} => I) g t = evalM (fun {ty : Montague.Ty} => I) g' t

A term's denotation depends on the assignment only at its free variables.

Translation

def HeimKratzer.Tree.translate {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) : PhraseStructure.Tree C L → Option ((ty : Montague.Ty) × Term K ty)

translate lex t is the term the tree t translates to by the composition principles of [HK98]. A terminal translates to its word's constant, a non-branching node to its daughter's term, a binary node to the composition of its daughters' terms by the mode their types select, a trace to the variable of its index, and a binder to the abstraction over that variable.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Tree.translate lex (RoseTree.node (PhraseStructure.Tree.Label.terminal a w) []) = Option.map (fun (c : (ty : Montague.Ty) × K ty) => ⟨c.fst, HeimKratzer.Term.const c.snd⟩) (lex w)
• HeimKratzer.Tree.translate lex (RoseTree.node (PhraseStructure.Tree.Label.node a) [t]) = HeimKratzer.Tree.translate lex t
• HeimKratzer.Tree.translate lex (RoseTree.node (PhraseStructure.Tree.Label.node a) children) = none
• HeimKratzer.Tree.translate lex (RoseTree.node (PhraseStructure.Tree.Label.segment a) [t]) = HeimKratzer.Tree.translate lex t
• HeimKratzer.Tree.translate lex (RoseTree.node (PhraseStructure.Tree.Label.segment a) children) = none
• HeimKratzer.Tree.translate lex (RoseTree.node (PhraseStructure.Tree.Label.trace n a) []) = some ⟨Montague.Ty.e, HeimKratzer.Term.var n⟩
• HeimKratzer.Tree.translate lex x✝ = none

@[simp]

theorem HeimKratzer.Tree.translate_terminal {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (c : C) (w : L) : translate lex (PhraseStructure.Tree.terminal c w) = Option.map (fun (c : (ty : Montague.Ty) × K ty) => ⟨c.fst, Term.const c.snd⟩) (lex w)

@[simp]

theorem HeimKratzer.Tree.translate_node_unary {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (c : C) (t : PhraseStructure.Tree C L) : translate lex (PhraseStructure.Tree.node c [t]) = translate lex t

@[simp]

theorem HeimKratzer.Tree.translate_node_binary {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : translate lex (PhraseStructure.Tree.node c [t₁, t₂]) = (translate lex t₁).bind fun (d₁ : (ty : Montague.Ty) × Term K ty) => (translate lex t₂).bind fun (d₂ : (ty : Montague.Ty) × Term K ty) => Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) (l : Term K σ₁) (r : Term K σ₂) => Term.comp m l r) d₁ d₂

@[simp]

theorem HeimKratzer.Tree.translate_adjoin_unary {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (c : C) (t : PhraseStructure.Tree C L) : translate lex (PhraseStructure.Tree.adjoin c [t]) = translate lex t

@[simp]

theorem HeimKratzer.Tree.translate_adjoin_binary {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : translate lex (PhraseStructure.Tree.adjoin c [t₁, t₂]) = (translate lex t₁).bind fun (d₁ : (ty : Montague.Ty) × Term K ty) => (translate lex t₂).bind fun (d₂ : (ty : Montague.Ty) × Term K ty) => Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} (m : Mode σ₁ σ₂ τ) (l : Term K σ₁) (r : Term K σ₂) => Term.comp m l r) d₁ d₂

@[simp]

theorem HeimKratzer.Tree.translate_trace {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (n : ℕ) (c : C) : translate lex (PhraseStructure.Tree.trace n c) = some ⟨Montague.Ty.e, Term.var n⟩

@[simp]

theorem HeimKratzer.Tree.translate_bind {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) (n : ℕ) (c : C) (body : PhraseStructure.Tree C L) : translate lex (PhraseStructure.Tree.bind n c body) = Option.map (fun (d : (ty : Montague.Ty) × Term K ty) => ⟨Montague.Ty.e ⇒ d.fst, Term.lam n d.snd⟩) (translate lex body)

theorem HeimKratzer.Tree.translate_junk {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) {l : PhraseStructure.Tree.Label C L} {cs : List (PhraseStructure.Tree C L)} (h : ¬l.Licenses (List.map RoseTree.value cs)) : translate lex (RoseTree.node l cs) = none

A node whose daughters its label does not license translates to nothing.

theorem HeimKratzer.Tree.translate_map_const {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) {K' : Montague.Ty → Type u_3} (f : {ty : Montague.Ty} → K ty → K' ty) (t : PhraseStructure.Tree C L) : translate (fun (w : L) => Option.map (fun (c : (ty : Montague.Ty) × K ty) => ⟨c.fst, f c.snd⟩) (lex w)) t = Option.map (fun (d : (ty : Montague.Ty) × Term K ty) => ⟨d.fst, Term.map (fun {ty : Montague.Ty} => f) d.snd⟩) (translate lex t)

Translation commutes with renaming the constants.

theorem HeimKratzer.Tree.translate_map_fst {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) {K' : Montague.Ty → Type u_3} {lex' : L → Option ((ty : Montague.Ty) × K' ty)} (h : ∀ (w : L), Option.map (fun (x : (ty : Montague.Ty) × K ty) => x.fst) (lex w) = Option.map (fun (x : (ty : Montague.Ty) × K' ty) => x.fst) (lex' w)) (t : PhraseStructure.Tree C L) : Option.map (fun (x : (ty : Montague.Ty) × Term K ty) => x.fst) (translate lex t) = Option.map (fun (x : (ty : Montague.Ty) × Term K' ty) => x.fst) (translate lex' t)

The types of a tree's term depend only on the types of its words' constants.

theorem HeimKratzer.Tree.translate_rel {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} (lex : L → Option ((ty : Montague.Ty) × K ty)) {K' : Montague.Ty → Type u_3} {R : (ty : Montague.Ty) → K ty → K' ty → Prop} {lex' : L → Option ((ty : Montague.Ty) × K' ty)} (hlex : ∀ (w : L) (d' : (ty : Montague.Ty) × K' ty), lex' w = some d' → ∃ (c : K d'.fst), lex w = some ⟨d'.fst, c⟩ ∧ R d'.fst c d'.snd) (t : PhraseStructure.Tree C L) {d' : (ty : Montague.Ty) × Term K' ty} : translate lex' t = some d' → ∃ (u : Term K d'.fst), translate lex t = some ⟨d'.fst, u⟩ ∧ Term.Rel R u d'.snd

Lexicons whose constants are related translate a tree to terms of the same shape with related constants.