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 using (_Γ—_; Ξ£; Ξ£-syntax; βˆƒ; βˆƒ-syntax; proj₁; projβ‚‚)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; injβ‚‚)
open import Data.Unit 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 familar 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
      let x = injβ‚‚ ⟨ v₁′ βŠ” v₁′′ , ⟨ sub Lβ†“βŠ” βŠ”β†¦βŠ”-dist , Mβ†“βŠ” ⟩ ⟩ in
      x
ℰ·→●ℰ {Ξ“}{Ξ³}{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 forward 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 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)