Writing your first program with Budge-TP

Budge-TP (bʌdʒ, b’dzh) is a theorem prover (really, just another programming language) that allows you to express formal systems (really, just programs).

In this post, I will show you how to write a simple program in Budge-TP.

Budge-TP has very simple semantics: it only consists of rules (functions) and theorems (function calls). Applying a rule (function call) performs a direct substitution of the variables, and that’s it!

Formal definition per the original paper

The syntax is also simple, but instead of giving a formal definition for the syntax, let’s jump to code right away and learn by doing!

Budge-TP has no built-in numbers, only constant atoms (uppercase characters) and variables (single lowercase letters). In this post, we will implement number representation and the addition operation.

Representing the number 1

Consider the following Budge-TP code:

rTm- : -
tm- : rTm-

The rTm- : - part in the code defines a rule (function) named rTm- with 0 hypotheses (0 parameters) which is basically an axiom (a constant): the representation of a single dash -. The tm- part in the code defines a derived theorem (a function call result) by applying the rule (function). The symbol : is used as a separator between the rule name and the rule’s output, and similarly between the theorem name and the rules applied.

If you run the above code, it will output the derived theorem:

$ ./budge-tp.py numbers.btp 
tm- : -

Since rTm- starts with an r, Budge-TP considers it a rule. Similarly, since tm- starts with t, Budge-TP considers it a theorem.

Representing other numbers

Now we can represent the number 1, which is basically a single dash. But we cannot express any other numbers. For that, we introduce a rule with variables in which we will be able to perform substitution:

rTmMk : xy

This rule contains no hypotheses (arguments), but since it contains lowercase characters, we are now able to perform substitution like this:

tm-- : rTmMk x=tm-;y=tm-
tm--- : rTmMk x=tm--;y=tm-

The theorem (function call) tm-- calls the rule (function) rTmMk and substitutes x and y with the existing theorem (constant returned by a function call) tm-. So, once substituted, the theorem tm-- produces the symbol -- (two dashes), which is basically the number 2. Similarly, tm--- represents the number 3. Observe:

$ ./budge-tp.py numbers.btp 
tm- : -
tm-- : --
tm--- : ---

Addition

Now that we have a way to represent numbers, we can implement the addition operator!

rAddBase : xP-Qx-

The rule rAddBase contains a mixture of lowercase letters (variables) and uppercase letters and dash (constant symbols). Basically, xP-Qx- represents the formula $x+1=(x+1)$ .

To see this, try substituting x with - to get -P-Q--, which is really $1+1=2$ . We can also substitute x with -- to get --P-Q--- which is really $2+1=3$ . In code:

tmOnePlusOne : rAddBase x=tm-
tmTwoPlusOne : rAddBase x=tm--

Observe the results:

$ ./budge-tp.py numbers.btp 
tm- : -
tm-- : --
tm--- : ---
tmOnePlusOne : -P-Q--
tmTwoPlusOne : --P-Q---

rAddBase is great, but we can’t really express formulas where the second number is different than 1, e.g. $2+2=4$ . To be able to express such formulas, we will need to add another rule:

rAddSucc : xPyQz -> xPy-Qz-

Since this rule (function) contains a mixture of lowercase letters and other symbols, it will rely on substitution when applied, but also, there’s an arrow -> which is a special symbol in Budge-TP that indicates that the rule accepts one hypothesis (argument). So rAddSucc states the following: for me to derive a theorem of the form xPy-Qz- for you, you will have to give me a theorem of the form xPyQz. Basically, the rule represents $x+y = z \to x+(y+1)=(z+1)$ .

Finally, here’s how we can derive (prove) that based on these rules, $2+2=4$ :

tmTwoPlusTwo : rAddSucc x=tm--;y=tm-;z=tm--- tmTwoPlusOne

Basically, this statement defines a new theorem (function call) named tmTwoPlusTwo which uses the rule (function) rAddSucc and substitutes x with tm--, y with tm-, and z with tm---, and then supplies tmTwoPlusOne as the hypothesis (argument) to the rule (function) to fulfill the rule’s requirements. Now that the rule’s hypothesis (argument) was filled with --P-Q---, it will return --P--Q----.

Adding this theorem to the existing code will produce the following output:

$ ./budge-tp.py numbers.btp 
tm- : -
tm-- : --
tm--- : ---
tmOnePlusOne : -P-Q--
tmTwoPlusOne : --P-Q---
tmTwoPlusTwo : --P--Q----

Conclusion

The formal system used as an example in this post is known as the PQ system from the GEB book. As can be seen, theorem proving is really close to programming. We used a very simple system in this post but really, any kind of computation/proof can be derived with Budge-TP.

As an example, here are the rules for expressing Budge-PL, a language similar to FRACTRAN, together with helper theorems rAppendNil : APPEND NIL y y and rAppendRec : APPEND x y z -> APPEND (a x) y (a z) for appending lists:

# Lists and numbers  # Commands 1, -1, 2, -2
rMkList : (x y)      rNext+1 : (S0 x) (a b) -> x (Sa b)
rTmNil : NIL         rNext-1 : (P0 x) (Sa b) -> x (a b)
rTm0 : 0             rNext+2 : (SS0 x) (a b) -> x (a Sb)
rTmS : Sx            rNext-2 : (PP0 x) (a Sb) -> x (a b)
rTmP : Px
                     # Looping on 2nd register
# Initial program    rLoopB : ((SS0 x) y) (a 0) -> y (a 0)
rInit : p (a b)      rLoopS : ((SS0 x) y) (a Sb)
                     -> APPEND x ((SS0 x) y) z -> z (a Sb)

To calculate the program ((2, −2, 1)) with the first register 1 and the second 2, we use these rules: rInit, rLoop2S, rNext-2, rNext+1, rLoop2S, rNext-2, rNext+1, rLoop2B. This application takes the initial state (1 2) and evaluates it to (3 0) which represents the sum.

If this was fun, you can find more examples on the GitHub repository.