Compositional Correctness

Introduction

Writing and proving programs correct is generally considered to be much harder than writing them alone. There is quite a bit of evidence to support this position but I will not cover it in this post. Conal Elliott has a hunch about why proving programs correct is so much more difficult. He thinks the main reason is that – most of the time – people attempt to prove properties about existing systems; systems designed in the absence of mathematical constraints.

If “proving at the end” is the main reason for the difficulty of proof, then it may be the case that an approach where we simultaneously write and prove is the solution.

It is a well-recognised principle that composing programs from simpler building blocks is a good way to construct larger programs. Another well-recognised “good thing” is the principle of compositionality which states that when trying to reason about the composition of A and B, it is desirable that the meaning of the composition is determined by the meanings of A, B and the rules used to combine them. It is undesirable (and non-compositional) in the case where reasoning about A and B together either

• can’t be done by reasoning about A and B independently, or
• is significantly more complicated than reasoning about A and B in isolation

What if we were to adopt a discipline where programs and their proofs were composed simultaneously? This style of programming is well-supported in dependently typed languages such as Agda, Coq, and Idris. Conal has even coined a name for this technique: compositional correctness.

In this post we will look at an example of compositional correctness in action.

Proving at the end

But first, we’ll take a look at constructing a program and then only “proving at the end”.

In my last post we define a function called splitPermute as follows:

  splitPermute : (m : ℕ) {n : ℕ} → (𝔽 (m + n) → 𝔽 (n + m))
  splitPermute m {n} = join n m ∘ swap ∘ splitAt m

We were able to prove that splitPermute n was the inverse of splitPermute m, for a given m + n : ℕ as follows:

  inverse : {m n : ℕ} → splitPermute n ∘ splitPermute m ≗ id
  inverse {m} {n} =
    begin
      (splitPermute n ∘ splitPermute m)
    ≡⟨⟩
      (join m n ∘ swap ∘ splitAt n) ∘ (join n m ∘ swap ∘ splitAt m)
    ≡⟨⟩
      (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m)
    ≈⟨ cong-[ join m n ∘ swap ]∘⟨ splitAt-join n m ⟩∘[ swap ∘ splitAt m ] ⟩
      (join m n ∘ swap ∘ swap ∘ splitAt m)
    ≈⟨ cong-[ join m n ]∘⟨ swap-involutive ⟩∘[ splitAt m ] ⟩
      (join m n ∘ splitAt m)
    ≈⟨ join-splitAt m n ⟩
      id
    ∎
    where
      open import Relation.Binary.PropositionalEquality
      open import Relation.Binary.Reasoning.Setoid (𝔽 (m + n) →-setoid 𝔽 (m + n))

We then constructed a bijection – called an Inverse in Agda – as follows. This packages up a program with proofs of invertibility.

  splitPermute↔ : (m : ℕ) {n : ℕ} → (𝔽 (m + n) ↔ 𝔽 (n + m))
  splitPermute↔ m {n} = mk↔′ (splitPermute m) (splitPermute n) (inverse {n} {m}) (inverse {m} {n})

Construction via compositional correctness

But there is a better way! The beautiful thing about bijections is that their proofs are bundled together with the program. This is just what we need for compositional correctness.

Let’s see how this is done for splitPermute.

  splitPermute↔ : (m : ℕ) {n : ℕ} → 𝔽 (m + n) ↔ 𝔽 (n + m)
  splitPermute↔ m {n} = (+↔⊎ {m} {n} ∘-↔ swap↔) ∘-↔ sym-↔ +↔⊎

That’s it! The function, its inverse and accompanying proofs of invertibility have all been defined in a single line.

In order to understand this code you will need to study the definitions of +↔︎⊎ and swap↔︎. +↔︎⊎ is defined in module Data.Fin.Properties and has the following definition:

+↔⊎ : ∀ {m n} → Fin (m ℕ.+ n) ↔ (Fin m ⊎ Fin n)
+↔⊎ {m} {n} = mk↔′ (splitAt m {n}) (join m n) (splitAt-join m n) (join-splitAt m n)

Function swap↔︎ is something that I had to write myself even though all the building blocks were already present in Data.Sum and Data.Sum.Properties.

  swap↔ : ∀ {a b} {A : Set a} {B : Set b} →  (A ⊎ B) ↔ (B ⊎ A)
  swap↔ {a} {b} {A} {B} = mk↔′ swap swap swap-involutive swap-involutive

I submitted a PR to the GitHub agda-stdlib repository which added this function. It has now been incorporated and will appear in a future release of the Agda Standard Library.

Compositional correctness via the bijection composition operator ∘-↔︎

The magic of this approach is in the ∘-↔︎ operator which is defined in module Function.Construct.Composition. It is a synonym for function inverse which is defined as:

  inverse : Inverse R S → Inverse S T → Inverse R T
  inverse inv₁ inv₂ = record
    { f       = G.f ∘ F.f
    ; f⁻¹     = F.f⁻¹ ∘ G.f⁻¹
    ; cong₁   = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
    ; cong₂   = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
    ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ (trans R) (trans T) G.cong₁ F.cong₂ F.inverse G.inverse
    } where module F = Inverse inv₁; module G = Inverse inv₂

One can further understand this code by looking at:

  inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
             Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
             Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x)

  inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ →
             Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
             Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x)

  inverseᵇ : Transitive ≈₁ → Transitive ≈₃ →
             Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ →
             Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
             Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) =
    inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ

As you can see a single, general, proof serves whenever one wants to compose two bijections together.

If we compare the “prove at the end” with the compositional correctness approach, we see that in the “prove at the end” approach we had to carefully apply three different invertibility proofs (in order):

1. splitAt-join
2. swap-involutive
3. join-splitAt

However, by using the approach of compositional correctness, we actually applied inverseᵇ (under the hood) three times, and the application was implicitly done with each application of the ∘-↔︎ operator.

Conclusion

A style of programming coined by Conal Elliott and called compositional correctness can be used to reduce the cost of proving one’s programs correct. In the example we considered, “proving at the end” involved carefully selecting specific theorems while compositional correctness used a general theorem (at three specific types) to achieve its goals.

It will remain to be seen whether compositional correctness radically reduces the difficulty of proving program correctness, but it is a very promising candidate.