Ascetic Slug
An Agda eDSL for well-typed Hilbert style proofs.
Posted on :: Tags: Agda , logic , formal verification

I present an Agda eDSL for writing Hilbert style proofs for logic 𝑲𝑲.

This blog consists of two main parts. The first part presents the language and some examples. The second offers some insight into the key parts of the implementation. The latter targets Agda beginner/intermediate users or any programmer interested in dependent types.

The code is available here. It has been implemented using Agda 2.6.0 with the standard library (at this specific commit).

Some introductory concepts

What is an eDSL? The acronym eDSL stands for Embedded Domain Specific Language. It refers to a small language (a set of functions and data types) embedded in another language (in this case Agda) that has been designed to solve a problem in a very specific domain, in this case, Hilbert style proofs.

What is a Hilbert style proof? First we need to know what a Hilbert calculus is. A Hilbert calculus is a set of axioms plus a set of rules. The axioms are formulas that we accept as primitive theorems and the rules allow us to syntactically combine existing theorems to create new ones. Then, a Hilbert style proof is a sequence of formulas where each formula is either an axiom of the calculus or the result of applying a rule to previous formulas in the sequence. The last formula in the sequence is the theorem of the proof. It is best understood by seeing a concrete example, if you scroll down you will find one.

The eDSL and logic KK

As a preface, let me remark that that the chosen logic, 𝑲𝑲, is not of special importance here, it just lays the ground for some concrete examples. In fact, it would be interesting to implement a logic agnostic eDSL in the future.

Let’s begin by defining the syntax of modal formulas:

ModalFm≔Var βˆ£ ModalFmβ†’ModalFm βˆ£ β–‘ModalFm βˆ£ βŠ₯ \begin{align*} ModalFm ≔ Var\ |\ ModalFm β†’ ModalFm\ |\ β–‘ ModalFm \ |\ βŠ₯ \\ \end{align*}

Of course, we are missing important logical connectives like ¬,∧,∨¬,∧,∨, but it is better to have a small core language and define the other connectives in terms of the primitive ones, for instance:

¬ϕ≔ϕ→βŠ₯Ο•βˆ§Οˆβ‰”Β¬(Ο•β†’Β¬Οˆ)Ο•βˆ¨Οˆβ‰”Β¬Ο•β†’Οˆ \begin{align*} ¬ϕ & ≔ Ο•β†’βŠ₯ \\ Ο•βˆ§Οˆ & ≔ Β¬(Ο•β†’Β¬Οˆ) \\ Ο•βˆ¨Οˆ & ≔ Β¬Ο•β†’Οˆ \\ \end{align*}

The axioms of 𝑲𝑲 are the following:

(K1) Ο•β†’(Οˆβ†’Ο•)(K2) (Ο•β†’(Οˆβ†’ΞΎ))β†’((Ο•β†’Οˆ)β†’(Ο•β†’ΞΎ))(K3) (Β¬Ο•β†’Β¬Οˆ)β†’(Οˆβ†’Ο•)(Distribution) β–‘(Ο•β†’Οˆ)β†’(β–‘Ο•β†’β–‘Οˆ) \begin{align*} \text{(K1) } & Ο• β†’ (ψ β†’ Ο•) \\ \text{(K2) } & (Ο• β†’ (ψ β†’ ΞΎ)) β†’ ((Ο• β†’ ψ) β†’ (Ο• β†’ ΞΎ)) \\ \text{(K3) } & (Β¬ Ο• β†’ Β¬ ψ) β†’ (ψ β†’ Ο•) \\ \text{(Distribution) } & β–‘ (Ο• β†’ ψ) β†’ (β–‘ Ο• β†’ β–‘ ψ) \end{align*}

The above are axiom schemes (or templates), so Ο•,ψ,ΞΆΟ•,ψ,ΞΆ are formula metavariables which can be substituted for any modal formula.

And the rules are the following:

  • Modus Ponens: If ϕϕ is a theorem and Ο•β†’ΟˆΟ•β†’Οˆ is a theorem, then ψψ is a theorem.

Ο•β†’ΟˆΟ•Οˆ \begin{array}{c} Ο•β†’Οˆ \\ Ο• \\ \hline ψ \end{array}

  • Necessitation: If ϕϕ is a theorem then β–‘Ο•β–‘Ο• is a theorem.

Ο•β–‘Ο• \begin{array}{c} Ο• \\ \hline β–‘Ο• \end{array}

  • Identity: If Ο•βˆˆΞ£Ο•βˆˆΞ£ then Ξ£βŠ’Ο•Ξ£βŠ’Ο•. Note that ϕϕ may not be a theorem. See clarification at the end of this section.

Finally! we can construct our first Hilbert style proof. Let’s prove β–‘(Ο•β†’Ο•)β–‘(Ο•β†’Ο•).

[ 0 ] (Ο•β†’((Ο•β†’Ο•)β†’Ο•))β†’((Ο•β†’(Ο•β†’Ο•))β†’(Ο•β†’Ο•))By K2[ 1 ] Ο•β†’((Ο•β†’Ο•)β†’Ο•)By K1[ 2 ] Ο•β†’(Ο•β†’Ο•)By K1[ 3 ] (Ο•β†’(Ο•β†’Ο•))β†’(Ο•β†’Ο•)By MP 0, 1[ 4 ] Ο•β†’Ο•By MP 3, 2[ 5 ] β–‘(Ο•β†’Ο•)By Nec 4 \begin{array}{lr} \text{[ 0 ] } (Ο• β†’ ((Ο• β†’ Ο•) β†’ Ο•)) β†’ ((Ο• β†’ (Ο• β†’ Ο•)) β†’ (Ο• β†’ Ο•)) & \text{By K2} \\ \text{[ 1 ] } Ο• β†’ ((Ο• β†’ Ο•) β†’ Ο•) & \text{By K1} \\ \text{[ 2 ] } Ο• β†’ (Ο• β†’ Ο•) & \text{By K1} \\ \text{[ 3 ] } (Ο• β†’ (Ο• β†’ Ο•)) β†’ (Ο• β†’ Ο•) & \text{By MP 0, 1} \\ \text{[ 4 ] } Ο• β†’ Ο• & \text{By MP 3, 2} \\ \text{[ 5 ] } β–‘ (Ο• β†’ Ο•) & \text{By Nec 4}\\ \end{array}

And now… how does the same proof look in our eDSL as Agda code? Here it is:

β–‘βŸ¨Ο•β†Ο•βŸ© : βˆ€ {Ξ£ Ο•} β†’ Ξ£ ⊒ β–‘ (Ο• ↝ Ο•)
β–‘βŸ¨Ο•β†Ο•βŸ© {Ξ£} {Ο•} =
  begin[ 0 ] (Ο• ↝ ((Ο• ↝ Ο•) ↝ Ο•)) ↝ ((Ο• ↝ (Ο• ↝ Ο•)) ↝ (Ο• ↝ Ο•)) By K2
       [ 1 ] Ο• ↝ ((Ο• ↝ Ο•) ↝ Ο•)                               By K1
       [ 2 ] Ο• ↝ (Ο• ↝ Ο•)                                      By K1
       [ 3 ] (Ο• ↝ (Ο• ↝ Ο•)) ↝ (Ο• ↝ Ο•)                        ByMP 0 , 1
       [ 4 ] Ο• ↝ Ο•                                             ByMP 3 , 2
       [ 5 ] β–‘ (Ο• ↝ Ο•)                                         ByNec 4
       β– 
DEFAULT

Wow, they look really similar indeed! So what? Well, we can write Hilbert styles proofs in a paper-like syntax with the key advantage that Agda’s type checker will make sure that the proof is constructed according to the rules, that is, that there are no mistakes in it. For instance, proofs where an axiom is instantiated incorrectly, or an application of modus ponens is incorrect will fail to type check and we will get an error from the compiler telling us where the misstep is. An additional free perk that we get is that we can easily export the proofs to rich html or latex.

Let me underline that the code above is actual Agda code. This might be surprising for readers not accustomed to Agda’s mixfix operators, which give great syntactical versatility.

It is worth noting that the By step does not only accept axioms, but any theorem previously proved. So, if we were to prove another theorem and we wanted to use β–‘(Ο•β†’Ο•)β–‘ (Ο• β†’ Ο•) as an intermediate step we could do so. Also, since we proved β–‘(Ο•β†’Ο•)β–‘(Ο•β†’Ο•) for any ϕϕ, we are free to substitute it for any formula. Example:

...
[ 1 ] β–‘ (Ο• ↝ Ο•)             By β–‘βŸ¨Ο•β†Ο•βŸ©
[ 2 ] β–‘ ((ψ ∧ Ο•) ↝ (ψ ∧ Ο•)) By β–‘βŸ¨Ο•β†Ο•βŸ©
...
DEFAULT

What about premises? Well, as you may have already noticed in the previous proof, we wrote Ξ£βŠ’β–‘(Ο•β†’Ο•)Ξ£ ⊒ β–‘ (Ο• β†’ Ο•), where ΣΣ is our set of premises, and we are free to use any formula in ΣΣ as if it was a theorem within the proof. As an example, let’s prove Ο•β†’Οˆ,Ο•,Ξ£βŠ’ΟˆΟ•β†’Οˆ,Ο•,Σ⊒ψ.

Ο•β†Οˆβˆ·Ο•βˆ·Ξ£βŠ’Οˆ : βˆ€ {Ο• ψ Ξ£} β†’ Ο• ↝ ψ ∷ Ο• ∷ Ξ£ ⊒ ψ
Ο•β†Οˆβˆ·Ο•βˆ·Ξ£βŠ’Οˆ {Ο•} {ψ} =
  begin[ 0 ] Ο•       By premise 1
       [ 1 ] Ο• ↝ ψ   By premise 0
       [ 2 ] ψ       ByMP 0 , 1
       β– 
DEFAULT

Clarification: Notice that a formula ϕϕ is a theorem of the logic KK if and only if βˆ…βŠ’Ο•βˆ…βŠ’Ο•. So in case we have Ξ£βŠ’Ο•Ξ£βŠ’Ο• with ΣΣ nonempty it may be that ϕϕ is not a theorem of KK. It is worth noting that when we define ϕ↝ϕ : βˆ€ {Ξ£ Ο•} : Ξ£ ⊒ Ο• ↝ Ο•, then the term ϕ↝ϕ is really a proof that ϕ→ϕϕ β†’ Ο• is a theorem of KK since ΣΣ is a parameter of the proof and in particular it can be empty.

This concludes the overview of the language features.

Implementation tour

We start by defining the syntax of formulas. We define variables to be natural numbers but this is not really relevant.

Var : Set
Var = Nat

infixr 20 _↝_
data Fm : Set where
  _! : Var β†’ Fm
  _↝_ : Fm β†’ Fm β†’ Fm
  β–‘ : Fm β†’ Fm
  βŠ₯ : Fm
DEFAULT

Now, if we wanted, we could expand our language by defining more function symbols. For instance, we could define negation thus:

Β¬ : Fm β†’ Fm
Β¬ Ο• = Ο• ↝ βŠ₯
DEFAULT

We could do the same for ∧,∨,β™’,⊀∧,∨,β™’,⊀ and any other operator.

Let’s define a data type that represents a proof in Hilbert calculus. As expected, it will have a constructor for each axiom scheme and rule.

infix 0 _⊒_
data _⊒_ (Ξ£ : List Fm) : Fm β†’ Set where
  K1 : βˆ€ {Ο• ψ : Fm} β†’ Ξ£ ⊒ Ο• ↝ (ψ ↝ Ο•)
  K2 : βˆ€ {Ο• ψ ΞΎ : Fm} β†’ Ξ£ ⊒ (Ο• ↝ (ψ ↝ ΞΎ)) ↝ ((Ο• ↝ ψ) ↝ (Ο• ↝ ΞΎ))
  K3 : βˆ€ {Ο• ψ : Fm} β†’ Ξ£ ⊒ (Β¬ Ο• ↝ Β¬ ψ) ↝ (ψ ↝ Ο•)
  distribution : {Ο• ψ : Fm} β†’ Ξ£ ⊒ β–‘ (Ο• ↝ ψ) ↝ (β–‘ Ο• ↝ β–‘ ψ)
  necessitation : βˆ€ {Ο• : Fm} β†’ Ξ£ ⊒ Ο• β†’ Ξ£ ⊒ β–‘ Ο•
  mp : βˆ€ {Ο• ψ : Fm} β†’ Ξ£ ⊒ (Ο• ↝ ψ) β†’ Ξ£ ⊒ Ο• β†’ Ξ£ ⊒ ψ
  premise : βˆ€ {Ο• : Fm} β†’ Member Ο• Ξ£ β†’ Ξ£ ⊒ Ο•
DEFAULT

We can now write our first proof. The following proof corresponds to the proof that ϕ→ϕϕ→ϕ is a theorem of KK shown above.

ϕ↝ϕ : βˆ€ {Ξ£ Ο•} β†’ Ξ£ ⊒ (Ο• ↝ Ο•)
ϕ↝ϕ {Ξ£} {Ο•} = mp (mp (K2 {Ξ£} {Ο•} {Ο• ↝ Ο•} {Ο•}) (K1 {Ξ£} {Ο•} {Ο• ↝ Ο•})) (K1 {Ξ£} {Ο•} {Ο•})
DEFAULT

It is horrible to read and too verbose. We can make it a little more succinct by taking advantage of Agda’s implicit argument inference:

ϕ↝ϕ : βˆ€ {Ξ£ Ο•} β†’ Ξ£ ⊒ Ο• ↝ Ο•
ϕ↝ϕ {Ξ£} {Ο•} = mp (mp K2 K1) (K1 {ψ = Ο•})
DEFAULT

Much better but still hard for a human to visualize what are the intermediate steps. Computer programmers could think of this as machine code; something very useful for its simplicity but hard for humans to use. So, as we do in programming, we will design a human-friendly language and a compiler that translates nice looking proofs into (let’s call them) primitive Hilbert style proofs. Of course, everything will be guaranteed to work from the types, so no need to execute any code, just type check it (as is always the case when using Agda as a proof checker).

A sketch of the eDSL

We want a language as close to the paper-like syntax showed above as possible. We will refer to proofs in this language as nice proofs and proofs of the type _⊒_ as primitive proofs. We will refer to the process of translating nice proofs to primitive proofs as compilation.

First we need to think about the type of a nice proof. Well, it needs to keep track of the set of premises, the formula that entails and the length of it, so the following type is what we want.

data HilbertProof : List Fm β†’ Fm β†’ Nat β†’ Set
DEFAULT

Then the compile function will be of the following type.

compile : βˆ€ {n Ξ£ Ο•} β†’ HilbertProof Ξ£ Ο• n β†’ Ξ£ ⊒ Ο•
DEFAULT

We can now think about which constructors we need for a nice proof.

  1. By. To reference an axiom or another theorem.
  2. MP. To apply modus ponens to previous formulas in the proof.
  3. Nec. To apply necessitation to a previous formula in the proof.

We will refer to these constructors as instructions.

Instructions are numbered with consecutive naturals starting at 0. This number is used to reference its corresponding formula in subsequent steps. There must be a special instruction that does not expect instructions before it. We call this instruction Begin and it works the same as By with the exception that it can only be used as the first instruction.

Highlights

We face the following challenges.

  1. Numbering. We need to make sure that the user labels the instructions properly.
  2. Proper references. We need to make sure that the numbers referencing other instructions are in range of the size of the proof and that they reference the appropriate formulas.
  3. Compilation. We need to translate nice proofs into primitive proofs.

Numbering

The numbering certainly looks easier to tackle, so let’s start by this one. Instead of trying to solve our problem directly, I propose an alternative problem that captures the same challenge but with no unnecessary noise around it.

Exercise: Boring list

Define a list type such that the first number must be a zero and each subsequent number must be equal to the head plus one.

Solution

We do so with the help of singleton types.

data SingleNat : Nat β†’ Set where
  single : (n : Nat) β†’ SingleNat n

data BoringList : Nat β†’ Set where
  [_] : SingleNat 0 β†’ BoringList 0
  _∷_ : βˆ€ {n} β†’ SingleNat (suc n) β†’ BoringList n β†’ BoringList (suc n)

example : BoringList 2
example = single 2 ∷ (single 1 ∷ [ single 0 ])
DEFAULT

Well, yeah, this kind of works, but we still have to write single before each natural number, can’t we do better? Yes, indeed! using literal overloading. If we define a Number instance for SingleNat then we will be able to write singleton naturals with plain natural numbers.

instance
  NumNatSing : βˆ€ {n} β†’ Number (SingleNat n)
  NumNatSing {n} .Number.Constraint m = n ≑ m
  NumNatSing .Number.fromNat m ⦃ refl ⦄ = single m
DEFAULT

Then the example becomes:

example : BoringList 2
example = 2 ∷ (1 ∷ [ 0 ])
DEFAULT

Perfect! that’s what we needed.

With the previous solution in hand, it is easy to imagine how we can incorporate the same idea into our language.

Proper references

Let’s focus on the case of modus ponens (necessitation works analogously). Assuming the modus ponens instruction entails ψψ, it should receive one reference to Ο•β†’ΟˆΟ•β†’Οˆ and another reference to ϕϕ. As we mentioned, these reference will be written as natural numbers by the user, but as we need to make sure that they are in range and reference the correct formulas, we need an extra proof object ensuring that. More precisely, assuming we defined the function lookup-maybe : βˆ€ {Ξ£ ΞΆ Ο•} β†’ HilbertProof Ξ£ ΞΆ Ο• β†’ Nat β†’ Maybe Fm with the expected implementation we would require both proof objects lookup-maybe HP i ≑ just (Ο• ↝ ψ) and lookup-maybe HP j ≑ just Ο•.

But in the case that the references are correct, these proof objects will always be trivially solved by normalization and reflexivity, hence the code would look like this:

[ 3 ] (Ο• ↝ (Ο• ↝ Ο•)) ↝ Ο• ↝ Ο•           ByMP 0 ⟨ refl ⟩ , 1 ⟨ refl ⟩
DEFAULT

And we really want to avoid to have the explicit proof object as it makes the syntax unpleasant. Could we use literal overloading for references to previous formulas as well? Yes!

data HilbertRef {Ξ£ Ο• n} (H : HilbertProof Ξ£ Ο• n) (ψ : Fm) : Set where
  ref : (i : Nat) β†’ lookup-may H i ≑ just ψ β†’ HilbertRef H ψ

instance
  NumRef : βˆ€ {Ο• Ξ£ n} {H : HilbertProof Ξ£ Ο• n} {ψ} β†’ Number (HilbertRef H ψ)
  NumRef {Ο•} {Ξ£} {n} {H} {ψ} .Number.Constraint i = lookup-may H i ≑ just ψ
  NumRef {Ο•} {Ξ£} {n} {H} .Number.fromNat i ⦃ x ⦄ = ref i x
DEFAULT

Now we can write:

[ 3 ] (Ο• ↝ (Ο• ↝ Ο•)) ↝ Ο• ↝ Ο•                 ByMP 0 , 1
DEFAULT

And then each proof object is implicitly embedded in the natural literal 0, 1.

Compilation

It is hard to highlight a specific part over the others for the compilation process. Compilation is mostly about fiddling with types and proof objects to get the desired translation. If you are interested in this part I suggest you look at the code directly.

Conclusion

I hope that you enjoyed the reading. Any comments and suggestions are welcome.

I am not an expert Agda programmer, so in case you look at the full code, take it with a pinch of salt :)