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β)
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
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 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)
β± (β° N)
β± (β° Nβ²)
β° (Ζ 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)
β° L β β° M
ββ¨ β-cong LβLβ² MβMβ² β©
β° Lβ² β β° Mβ²
β° (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)
β± (β° N)
ββ¨ β±-cong (β°ββ¦β§ {M = N}) β©
β± β¦ N β§
β¦ Ζ N β§
β
β°ββ¦β§ {Ξ} {L Β· M} =
β° (L Β· M)
β° L β β° M
ββ¨ β-cong (β°ββ¦β§ {M = L}) (β°ββ¦β§ {M = M}) β©
β¦ L β§ β β¦ M β§

β±  U+2131  SCRIPT CAPITAL F (\McF)