Writing your second program with Budge-TP (complexity and abstraction)

In a previous blog post, we showed and implemented a formal system that was able to represent numbers and the addition operator.

In this blog post, we will show an implementation of a subset formal system of Peano’s axioms that will also be able to represent numbers and the addition operator.

Finally, we will compare both systems.

---

The PQ system

Let’s start by recalling the rules from the previous formal system:

# Terms (numbers)
rTm- : -
tm- : rTm-
rTmMk : xy
# Addition rules
rAddBase : xP-Qx-
rAddSucc : xPyQz -> xPy-Qz-

With this system, we were able to deduce facts such as --P--Q---- (). However, this system is very limited in what it can do – merely deduce formulas that represent addition and that’s it.

Numbers in Peano’s axioms

We start with the rules that allow us to represent numbers:

# Zero is a natural number
rTmZ : 0
tmZ : rTmZ
# Successor
rTmS : S(x)

Here is how we can represent the numbers one and two:

tm1 : rTmS x=tmZ
tm2 : rTmS x=tm1

Executing this code with Budge-TP gives:

$ ./budge-tp.py peano.btp
tmZ : 0
tm1 : S(0)
tm2 : S(S(0))

Addition in Peano’s axioms

While the PQ system abstracts equality away (it’s built in the formula), Peano’s axioms introduce it explicitly, so that we can express or even . Multiplication, or even nested addition cannot be represented as easily in the PQ system.

We now provide the rules that allow addition to be expressed in this system:

rAZ : ⊢EQ(ADD(x,0),x)
rAS : ⊢EQ(ADD(x,S(y)),S(ADD(x,y)))

Basically, these rules are a direct representation of the following two formulas, which represent standard addition:

• rAZ:
• rAS:

So, suppose we want to show that . How can we approach this proof given these rules? Here’s how we can start:

th1step1 : rAS x=tm1;y=tmZ
th1step2 : rAZ x=tm1

These two theorems produce the following:

th1step1 : ⊢EQ(ADD(S(0),S(0)),S(ADD(S(0),0)))
th1step2 : ⊢EQ(ADD(S(0),0),S(0))

That is, and . How can we relate these two theorems together, i.e., how can we proceed forward with the proof?

Since we decided to introduce equality (whereas in the PQ system it was “bound” to the formulas), we are stuck. We need to introduce other rules that will allow us to “link” these two theorems together.

To get from ADD(S(0),0)) to S(ADD(S(0),0),S(0))), we need to somehow “inject” S into the first formula. Those formulas are called injections, and are defined as follows:

rIL : ⊢EQ(m,n) -> ⊢EQ(S(m),S(n))
rIR : ⊢EQ(S(m),S(n)) -> ⊢EQ(m,n)

Since injections are defined for m and n (which can be any other expressions), we also need to lift addition to the term level to make it possible to construct terms for it:

rTmAD : ADD(x,y)

These now allow us to deduce the following theorem:

tmADD10 : rTmAD x=tm1;y=tmZ # Term needed for the theorem
th1step3 : rIL m=tmADD10;n=tm1 th1step2

Budge will now output:

$ ./budge-tp.py peano.btp
tmZ : 0
tm1 : S(0)
tm2 : S(S(0))
th1step1 : ⊢EQ(ADD(S(0),S(0)),S(ADD(S(0),0)))
th1step2 : ⊢EQ(ADD(S(0),0),S(0))
tmADD10 : ADD(S(0),0)
th1step3 : ⊢EQ(S(ADD(S(0),0)),S(S(0)))

Now we have shown that , and to proceed with the proof, we need another set of rules, namely, equality rules. What we want to do here is “link” th1step1 with th1step3, i.e., from and , deduce that .

How can we make this link? Enter the equality rules:

# Equality refl, symm, tr
rEqR : ⊢EQ(x,x)
rEqS : ⊢EQ(x,y) -> ⊢EQ(y,x)
rEqT : ⊢EQ(x,y) -> ⊢EQ(y,z) -> ⊢EQ(x,z)

The rule rEqT can now link the two theorems together as follows:

tmADD11 : rTmAD x=tm1;y=tm1
tm1ADD11 : rTmS x=tmADD10
th1 : rEqT x=tmADD11;y=tm1ADD11;z=tm2 th1step1 th1step3

Budge will now be able to deduce th1 : ⊢EQ(ADD(S(0),S(0)),S(S(0))) which really represents .

Conclusion

While the subset of Peano’s axioms we just introduced expresses the same system as PQ, it has more power than PQ – we introduced equality rather than abstracting it away, and we can easily introduce other rules such as multiplication that depend on equality as well.

Both systems are complex in their own ways. In the PQ system, as the system holds a whole formula of the form , we need to “match” the z argument in xPyQz with whatever makes sense for x and y. In Peano’s axioms, it feels more like searching for valid puzzle pieces and linking them together, i.e., instead of providing z, we provide xQy and yQz to get to xQz. The difference in the inference rules is what affects the thought process of a programmer, and thus the programmer’s experience.

Peano’s axioms are more powerful in terms of what they can express compared to the PQ system, however, they are also more inconvenient to use. Recall how easy it was to show that in PQ: we only needed a single theorem tm1PlusOne : rAddBase x=tm-. With Peano’s axioms, we also needed to implement rules to take care of the terms and “link” equalities. That is, complexity shifts between thinking at the “addition” level (PQ) and thinking at the “equational” (Peano) level.

In any case, this can be summarized into a single quote:

The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.

Edsger Dijkstra

That is, each abstraction has its own semantic level and thus its own complexity. Abstractions are only helpful for humans; machines don’t understand them, as to them, everything is a Turing machine (according to the Church-Turing thesis), and thus the complexity is one.

The new semantic level that we introduce comes with its own trade-offs and complexity specific to the domain, and it’s up to us to choose which ones are acceptable.