module plfa.part3.Compositional where

Introduction

In this chapter we prove that the denotational semantics is compositional, which means we fill in the ellipses in the following equations.

ℰ (` x) ≃ ...
ℰ (ƛ M) ≃ ... ℰ M ...
ℰ (M · N) ≃ ... ℰ M ... ℰ N ...

Such equations would imply that the denotational semantics could be instead defined as a recursive function. Indeed, we end this chapter with such a definition and prove that it is equivalent to ℰ.

Imports

open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Unit.Base using (⊤; tt)
open import plfa.part2.Untyped
  using (Context; _,_; ★; _∋_; _⊢_; `_; ƛ_; _·_)
open import plfa.part3.Denotational
  using (Value; _↦_; _`,_; _⊔_; ⊥; _⊑_; _⊢_↓_;
         ⊑-bot; ⊑-fun; ⊑-conj-L; ⊑-conj-R1; ⊑-conj-R2;
         ⊑-dist; ⊑-refl; ⊑-trans; ⊔↦⊔-dist;
         var; ↦-intro; ↦-elim; ⊔-intro; ⊥-intro; sub;
         up-env; ℰ; _≃_; ≃-sym; Denotation; Env)
open plfa.part3.Denotational.≃-Reasoning

Equation for lambda abstraction

Regarding the first equation

ℰ (ƛ M) ≃ ... ℰ M ...

we need to define a function that maps a Denotation (Γ , ★) to a Denotation Γ. This function, let us name it ℱ, should mimic the non-recursive part of the semantics when applied to a lambda term. In particular, we need to consider the rules ↦-intro, ⊥-intro, and ⊔-intro. So ℱ has three parameters, the denotation D of the subterm M, an environment γ, and a value v. If we define ℱ by recursion on the value v, then it matches up nicely with the three rules ↦-intro, ⊥-intro, and ⊔-intro.

ℱ : ∀{Γ} → Denotation (Γ , ★) → Denotation Γ
ℱ D γ (v ↦ w) = D (γ `, v) w
ℱ D γ ⊥ = ⊤
ℱ D γ (u ⊔ v) = (ℱ D γ u) × (ℱ D γ v)

If one squints hard enough, the ℱ function starts to look like the curry operation familiar to functional programmers. It turns a function that expects a tuple of length n + 1 (the environment Γ , ★) into a function that expects a tuple of length n and returns a function of one parameter.

Using this ℱ, we hope to prove that

ℰ (ƛ N) ≃ ℱ (ℰ N)

The function ℱ is preserved when going from a larger value v to a smaller value u. The proof is a straightforward induction on the derivation of u ⊑ v, using the up-env lemma in the case for the ⊑-fun rule.

sub-ℱ : ∀{Γ}{N : Γ , ★ ⊢ ★}{γ v u}
  → ℱ (ℰ N) γ v
  → u ⊑ v
    ------------
  → ℱ (ℰ N) γ u
sub-ℱ d ⊑-bot = tt
sub-ℱ d (⊑-fun lt lt′) = sub (up-env d lt) lt′
sub-ℱ d (⊑-conj-L lt lt₁) = ⟨ sub-ℱ d lt , sub-ℱ d lt₁ ⟩
sub-ℱ d (⊑-conj-R1 lt) = sub-ℱ (proj₁ d) lt
sub-ℱ d (⊑-conj-R2 lt) = sub-ℱ (proj₂ d) lt
sub-ℱ {v = v₁ ↦ v₂ ⊔ v₁ ↦ v₃} {v₁ ↦ (v₂ ⊔ v₃)} ⟨ N2 , N3 ⟩ ⊑-dist =
   ⊔-intro N2 N3
sub-ℱ d (⊑-trans x₁ x₂) = sub-ℱ (sub-ℱ d x₂) x₁

With this subsumption property in hand, we can prove the forward direction of the semantic equation for lambda. The proof is by induction on the semantics, using sub-ℱ in the case for the sub rule.

ℰƛ→ℱℰ : ∀{Γ}{γ : Env Γ}{N : Γ , ★ ⊢ ★}{v : Value}
  → ℰ (ƛ N) γ v
    ------------
  → ℱ (ℰ N) γ v
ℰƛ→ℱℰ (↦-intro d) = d
ℰƛ→ℱℰ ⊥-intro = tt
ℰƛ→ℱℰ (⊔-intro d₁ d₂) = ⟨ ℰƛ→ℱℰ d₁ , ℰƛ→ℱℰ d₂ ⟩
ℰƛ→ℱℰ (sub d lt) = sub-ℱ (ℰƛ→ℱℰ d) lt

The “inversion lemma” for lambda abstraction is a special case of the above. The inversion lemma is useful in proving that denotations are preserved by reduction.

lambda-inversion : ∀{Γ}{γ : Env Γ}{N : Γ , ★ ⊢ ★}{v₁ v₂ : Value}
  → γ ⊢ ƛ N ↓ v₁ ↦ v₂
    -----------------
  → (γ `, v₁) ⊢ N ↓ v₂
lambda-inversion{v₁ = v₁}{v₂ = v₂} d = ℰƛ→ℱℰ{v = v₁ ↦ v₂} d

The backward direction of the semantic equation for lambda is even easier to prove than the forward direction. We proceed by induction on the value v.

ℱℰ→ℰƛ : ∀{Γ}{γ : Env Γ}{N : Γ , ★ ⊢ ★}{v : Value}
  → ℱ (ℰ N) γ v
    ------------
  → ℰ (ƛ N) γ v
ℱℰ→ℰƛ {v = ⊥} d = ⊥-intro
ℱℰ→ℰƛ {v = v₁ ↦ v₂} d = ↦-intro d
ℱℰ→ℰƛ {v = v₁ ⊔ v₂} ⟨ d1 , d2 ⟩ = ⊔-intro (ℱℰ→ℰƛ d1) (ℱℰ→ℰƛ d2)

So indeed, the denotational semantics is compositional with respect to lambda abstraction, as witnessed by the function ℱ.

lam-equiv : ∀{Γ}{N : Γ , ★ ⊢ ★}
  → ℰ (ƛ N) ≃ ℱ (ℰ N)
lam-equiv γ v = ⟨ ℰƛ→ℱℰ , ℱℰ→ℰƛ ⟩

Equation for function application

Next we fill in the ellipses for the equation concerning function application.

ℰ (M · N) ≃ ... ℰ M ... ℰ N ...

For this we need to define a function that takes two denotations, both in context Γ, and produces another one in context Γ. This function, let us name it ●, needs to mimic the non-recursive aspects of the semantics of an application L · M. We cannot proceed as easily as for ℱ and define the function by recursion on value v because, for example, the rule ↦-elim applies to any value. Instead we shall define ● in a way that directly deals with the ↦-elim and ⊥-intro rules but ignores ⊔-intro. This makes the forward direction of the proof more difficult, and the case for ⊔-intro demonstrates why the ⊑-dist rule is important.

So we define the application of D₁ to D₂, written D₁ ● D₂, to include any value w equivalent to ⊥, for the ⊥-intro rule, and to include any value w that is the output of an entry v ↦ w in D₁, provided the input v is in D₂, for the ↦-elim rule.

infixl 7 _●_

_●_ : ∀{Γ} → Denotation Γ → Denotation Γ → Denotation Γ
(D₁ ● D₂) γ w = w ⊑ ⊥ ⊎ Σ[ v ∈ Value ]( D₁ γ (v ↦ w) × D₂ γ v )

If one squints hard enough, the _●_ operator starts to look like the apply operation familiar to functional programmers. It takes two parameters and applies the first to the second.

Next we consider the inversion lemma for application, which is also the forward direction of the semantic equation for application. We describe the proof below.

ℰ·→●ℰ : ∀{Γ}{γ : Env Γ}{L M : Γ ⊢ ★}{v : Value}
  → ℰ (L · M) γ v
    ----------------
  → (ℰ L ● ℰ M) γ v
ℰ·→●ℰ (↦-elim{v = v′} d₁ d₂) = inj₂ ⟨ v′ , ⟨ d₁ , d₂ ⟩ ⟩
ℰ·→●ℰ {v = ⊥} ⊥-intro = inj₁ ⊑-bot
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (⊔-intro{v = v₁}{w = v₂} d₁ d₂)
    with ℰ·→●ℰ d₁ | ℰ·→●ℰ d₂
... | inj₁ lt1 | inj₁ lt2 = inj₁ (⊑-conj-L lt1 lt2)
... | inj₁ lt1 | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ =
      inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
      where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂
            lt = (⊑-fun ⊑-refl (⊑-conj-L (⊑-trans lt1 ⊑-bot) ⊑-refl))
... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₁ lt2 =
      inj₂ ⟨ v₁′ , ⟨ sub L↓v12 lt , M↓v3 ⟩ ⟩
      where lt : v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁
            lt = (⊑-fun ⊑-refl (⊑-conj-L ⊑-refl (⊑-trans lt2 ⊑-bot)))
... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁′′ , ⟨ L↓v12′ , M↓v3′ ⟩ ⟩ =
      let L↓⊔ = ⊔-intro L↓v12 L↓v12′ in
      let M↓⊔ = ⊔-intro M↓v3 M↓v3′ in
      inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ ⊔↦⊔-dist , M↓⊔ ⟩ ⟩
ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (sub d lt)
    with ℰ·→●ℰ d
... | inj₁ lt2 = inj₁ (⊑-trans lt lt2)
... | inj₂ ⟨ v₁ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ =
      inj₂ ⟨ v₁ , ⟨ sub L↓v12 (⊑-fun ⊑-refl lt) , M↓v3 ⟩ ⟩

We proceed by induction on the semantics.

  • In case ↦-elim we have γ ⊢ L ↓ (v′ ↦ v) and γ ⊢ M ↓ v′, which is all we need to show (ℰ L ● ℰ M) γ v.

  • In case ⊥-intro we have v = ⊥. We conclude that v ⊑ ⊥.

  • In case ⊔-intro we have ℰ (L · M) γ v₁ and ℰ (L · M) γ v₂ and need to show (ℰ L ● ℰ M) γ (v₁ ⊔ v₂). By the induction hypothesis, we have (ℰ L ● ℰ M) γ v₁ and (ℰ L ● ℰ M) γ v₂. We have four subcases to consider.

    • Suppose v₁ ⊑ ⊥ and v₂ ⊑ ⊥. Then v₁ ⊔ v₂ ⊑ ⊥.

    • Suppose v₁ ⊑ ⊥, γ ⊢ L ↓ v₁′ ↦ v₂, and γ ⊢ M ↓ v₁′. We have γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂) by rule sub because v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₂.

    • Suppose γ ⊢ L ↓ v₁′ ↦ v₁, γ ⊢ M ↓ v₁′, and v₂ ⊑ ⊥. We have γ ⊢ L ↓ v₁′ ↦ (v₁ ⊔ v₂) by rule sub because v₁′ ↦ (v₁ ⊔ v₂) ⊑ v₁′ ↦ v₁.

    • Suppose γ ⊢ L ↓ v₁′′ ↦ v₁, γ ⊢ M ↓ v₁′′, γ ⊢ L ↓ v₁′ ↦ v₂, and γ ⊢ M ↓ v₁′. This case is the most interesting. By two uses of the rule ⊔-intro we have γ ⊢ L ↓ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁) and γ ⊢ M ↓ (v₁′ ⊔ v₁′′). But this does not yet match what we need for ℰ L ● ℰ M because the result of L must be an ↦ whose input entry is v₁′ ⊔ v₁′′. So we use the sub rule to obtain γ ⊢ L ↓ (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂), using the ⊔↦⊔-dist lemma (thanks to the ⊑-dist rule) to show that

        (v₁′ ⊔ v₁′′) ↦ (v₁ ⊔ v₂) ⊑ (v₁′ ↦ v₂) ⊔ (v₁′′ ↦ v₁)

      So we have proved what is needed for this case.

  • In case sub we have Γ ⊢ L · M ↓ v₁ and v ⊑ v₁. By the induction hypothesis, we have (ℰ L ● ℰ M) γ v₁. We have two subcases to consider.

    • Suppose v₁ ⊑ ⊥. We conclude that v ⊑ ⊥.
    • Suppose Γ ⊢ L ↓ v′ → v₁ and Γ ⊢ M ↓ v′. We conclude with Γ ⊢ L ↓ v′ → v by rule sub, because v′ → v ⊑ v′ → v₁.

The backward direction is proved by cases on the premise (ℰ L ● ℰ M) γ v. In case v ⊑ ⊥, we obtain Γ ⊢ L · M ↓ ⊥ by rule ⊥-intro. Otherwise, we conclude immediately by rule ↦-elim.

●ℰ→ℰ· : ∀{Γ}{γ : Env Γ}{L M : Γ ⊢ ★}{v}
  → (ℰ L ● ℰ M) γ v
    ----------------
  → ℰ (L · M) γ v
●ℰ→ℰ· {γ}{v} (inj₁ lt) = sub ⊥-intro lt
●ℰ→ℰ· {γ}{v} (inj₂ ⟨ v₁ , ⟨ d1 , d2 ⟩ ⟩) = ↦-elim d1 d2

So we have proved that the semantics is compositional with respect to function application, as witnessed by the ● function.

app-equiv : ∀{Γ}{L M : Γ ⊢ ★}
  → ℰ (L · M) ≃ (ℰ L) ● (ℰ M)
app-equiv γ v = ⟨ ℰ·→●ℰ , ●ℰ→ℰ· ⟩

We also need an inversion lemma for variables. If Γ ⊢ x ↓ v, then v ⊑ γ x. The proof is a straightforward induction on the semantics.

var-inv : ∀ {Γ v x} {γ : Env Γ}
  → ℰ (` x) γ v
    -------------------
  → v ⊑ γ x
var-inv (var) = ⊑-refl
var-inv (⊔-intro d₁ d₂) = ⊑-conj-L (var-inv d₁) (var-inv d₂)
var-inv (sub d lt) = ⊑-trans lt (var-inv d)
var-inv ⊥-intro = ⊑-bot

To round-out the semantic equations, we establish the following one for variables.

var-equiv : ∀{Γ}{x : Γ ∋ ★} → ℰ (` x) ≃ (λ γ v → v ⊑ γ x)
var-equiv γ v = ⟨ var-inv , (λ lt → sub var lt) ⟩

Congruence

The main work of this chapter is complete: we have established semantic equations that show how the denotational semantics is compositional. In this section and the next we make use of these equations to prove some corollaries: that denotational equality is a congruence and to prove the compositionality property, which states that surrounding two denotationally-equal terms in the same context produces two programs that are denotationally equal.

We begin by showing that denotational equality is a congruence with respect to lambda abstraction: that ℰ N ≃ ℰ N′ implies ℰ (ƛ N) ≃ ℰ (ƛ N′). We shall use the lam-equiv equation to reduce this question to whether ℱ is a congruence.

ℱ-cong : ∀{Γ}{D D′ : Denotation (Γ , ★)}
  → D ≃ D′
    -----------
  → ℱ D ≃ ℱ D′
ℱ-cong{Γ} D≃D′ γ v =
  ⟨ (λ x → ℱ≃{γ}{v} x D≃D′) , (λ x → ℱ≃{γ}{v} x (≃-sym D≃D′)) ⟩
  where
  ℱ≃ : ∀{γ : Env Γ}{v}{D D′ : Denotation (Γ , ★)}
    → ℱ D γ v  →  D ≃ D′ → ℱ D′ γ v
  ℱ≃ {v = ⊥} fd dd′ = tt
  ℱ≃ {γ}{v ↦ w} fd dd′ = proj₁ (dd′ (γ `, v) w) fd
  ℱ≃ {γ}{u ⊔ w} fd dd′ = ⟨ ℱ≃{γ}{u} (proj₁ fd) dd′ , ℱ≃{γ}{w} (proj₂ fd) dd′ ⟩

The proof of ℱ-cong uses the lemma ℱ≃ to handle both directions of the if-and-only-if. That lemma is proved by a straightforward induction on the value v.

We now prove that lambda abstraction is a congruence by direct equational reasoning.

lam-cong : ∀{Γ}{N N′ : Γ , ★ ⊢ ★}
  → ℰ N ≃ ℰ N′
    -----------------
  → ℰ (ƛ N) ≃ ℰ (ƛ N′)
lam-cong {Γ}{N}{N′} N≃N′ =
  start
    ℰ (ƛ N)
  ≃⟨ lam-equiv ⟩
    ℱ (ℰ N)
  ≃⟨ ℱ-cong N≃N′ ⟩
    ℱ (ℰ N′)
  ≃⟨ ≃-sym lam-equiv ⟩
    ℰ (ƛ N′)
  ☐

Next we prove that denotational equality is a congruence for application: that ℰ L ≃ ℰ L′ and ℰ M ≃ ℰ M′ imply ℰ (L · M) ≃ ℰ (L′ · M′). The app-equiv equation reduces this to the question of whether the ● operator is a congruence.

●-cong : ∀{Γ}{D₁ D₁′ D₂ D₂′ : Denotation Γ}
  → D₁ ≃ D₁′ → D₂ ≃ D₂′
  → (D₁ ● D₂) ≃ (D₁′ ● D₂′)
●-cong {Γ} d1 d2 γ v = ⟨ (λ x → ●≃ x d1 d2) ,
                         (λ x → ●≃ x (≃-sym d1) (≃-sym d2)) ⟩
  where
  ●≃ : ∀{γ : Env Γ}{v}{D₁ D₁′ D₂ D₂′ : Denotation Γ}
    → (D₁ ● D₂) γ v  →  D₁ ≃ D₁′  →  D₂ ≃ D₂′
    → (D₁′ ● D₂′) γ v
  ●≃ (inj₁ v⊑⊥) eq₁ eq₂ = inj₁ v⊑⊥
  ●≃ {γ} {w} (inj₂ ⟨ v , ⟨ Dv↦w , Dv ⟩ ⟩) eq₁ eq₂ =
    inj₂ ⟨ v , ⟨ proj₁ (eq₁ γ (v ↦ w)) Dv↦w , proj₁ (eq₂ γ v) Dv ⟩ ⟩

Again, both directions of the if-and-only-if are proved via a lemma. This time the lemma is proved by cases on (D₁ ● D₂) γ v.

With the congruence of ●, we can prove that application is a congruence by direct equational reasoning.

app-cong : ∀{Γ}{L L′ M M′ : Γ ⊢ ★}
  → ℰ L ≃ ℰ L′
  → ℰ M ≃ ℰ M′
    -------------------------
  → ℰ (L · M) ≃ ℰ (L′ · M′)
app-cong {Γ}{L}{L′}{M}{M′} L≅L′ M≅M′ =
  start
    ℰ (L · M)
  ≃⟨ app-equiv ⟩
    ℰ L ● ℰ M
  ≃⟨ ●-cong L≅L′ M≅M′ ⟩
    ℰ L′ ● ℰ M′
  ≃⟨ ≃-sym app-equiv ⟩
    ℰ (L′ · M′)
  ☐

Compositionality

The compositionality property states that surrounding two terms that are denotationally equal in the same context produces two programs that are denotationally equal. To make this precise, we define what we mean by “context” and “surround”.

A context is a program with one hole in it. The following data definition Ctx makes this idea explicit. We index the Ctx data type with two contexts for variables: one for the hole and one for terms that result from filling the hole.

data Ctx : Context → Context → Set where
  ctx-hole : ∀{Γ} → Ctx Γ Γ
  ctx-lam :  ∀{Γ Δ} → Ctx (Γ , ★) (Δ , ★) → Ctx (Γ , ★) Δ
  ctx-app-L : ∀{Γ Δ} → Ctx Γ Δ → Δ ⊢ ★ → Ctx Γ Δ
  ctx-app-R : ∀{Γ Δ} → Δ ⊢ ★ → Ctx Γ Δ → Ctx Γ Δ

  • The constructor ctx-hole represents the hole, and in this case the variable context for the hole is the same as the variable context for the term that results from filling the hole.

  • The constructor ctx-lam takes a Ctx and produces a larger one that adds a lambda abstraction at the top. The variable context of the hole stays the same, whereas we remove one variable from the context of the resulting term because it is bound by this lambda abstraction.

  • There are two constructions for application, ctx-app-L and ctx-app-R. The ctx-app-L is for when the hole is inside the left-hand term (the operator) and the later is when the hole is inside the right-hand term (the operand).

The action of surrounding a term with a context is defined by the following plug function. It is defined by recursion on the context.

plug : ∀{Γ}{Δ} → Ctx Γ Δ → Γ ⊢ ★ → Δ ⊢ ★
plug ctx-hole M = M
plug (ctx-lam C) N = ƛ plug C N
plug (ctx-app-L C N) L = (plug C L) · N
plug (ctx-app-R L C) M = L · (plug C M)

We are ready to state and prove the compositionality principle. Given two terms M and N that are denotationally equal, plugging them both into an arbitrary context C produces two programs that are denotationally equal.

compositionality : ∀{Γ Δ}{C : Ctx Γ Δ} {M N : Γ ⊢ ★}
  → ℰ M ≃ ℰ N
    ---------------------------
  → ℰ (plug C M) ≃ ℰ (plug C N)
compositionality {C = ctx-hole} M≃N =
  M≃N
compositionality {C = ctx-lam C′} M≃N =
  lam-cong (compositionality {C = C′} M≃N)
compositionality {C = ctx-app-L C′ L} M≃N =
  app-cong (compositionality {C = C′} M≃N) λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩
compositionality {C = ctx-app-R L C′} M≃N =
  app-cong (λ γ v → ⟨ (λ x → x) , (λ x → x) ⟩) (compositionality {C = C′} M≃N)

The proof is a straightforward induction on the context C, using the congruence properties lam-cong and app-cong that we established above.

The denotational semantics defined as a function

Having established the three equations var-equiv, lam-equiv, and app-equiv, one should be able to define the denotational semantics as a recursive function over the input term M. Indeed, we define the following function ⟦ M ⟧ that maps terms to denotations, using the auxiliary curry ℱ and apply ● functions in the cases for lambda and application, respectively.

⟦_⟧ : ∀{Γ} → (M : Γ ⊢ ★) → Denotation Γ
⟦ ` x ⟧ γ v = v ⊑ γ x
⟦ ƛ N ⟧ = ℱ ⟦ N ⟧
⟦ L · M ⟧ = ⟦ L ⟧ ● ⟦ M ⟧

The proof that ℰ M is denotationally equal to ⟦ M ⟧ is a straightforward induction, using the three equations var-equiv, lam-equiv, and app-equiv together with the congruence lemmas for ℱ and ●.

ℰ≃⟦⟧ : ∀ {Γ} {M : Γ ⊢ ★} → ℰ M ≃ ⟦ M ⟧
ℰ≃⟦⟧ {Γ} {` x} = var-equiv
ℰ≃⟦⟧ {Γ} {ƛ N} =
  let ih = ℰ≃⟦⟧ {M = N} in
    ℰ (ƛ N)
  ≃⟨ lam-equiv ⟩
    ℱ (ℰ N)
  ≃⟨ ℱ-cong (ℰ≃⟦⟧ {M = N}) ⟩
    ℱ ⟦ N ⟧
  ≃⟨⟩
    ⟦ ƛ N ⟧
  ☐
ℰ≃⟦⟧ {Γ} {L · M} =
   ℰ (L · M)
  ≃⟨ app-equiv ⟩
   ℰ L ● ℰ M
  ≃⟨ ●-cong (ℰ≃⟦⟧ {M = L}) (ℰ≃⟦⟧ {M = M}) ⟩
   ⟦ L ⟧ ● ⟦ M ⟧
  ≃⟨⟩
    ⟦ L · M ⟧
  ☐

Unicode

This chapter uses the following unicode:

ℱ  U+2131  SCRIPT CAPITAL F (\McF)
●  U+2131  BLACK CIRCLE (\cib)