Proofs and computation with trees

In this post, I will make the analogy between trees and proofs and computation.

Lately (after a long pause ), I started reading Logical Foundations again and started re-doing the exercises for the latest version (6.5). While doing the proofs this time, I kept thinking about tree traversals, so that inspired me to write this post.

Trees

A tree is a structure that represents hierarchical data. Here is one possible tree:

2
 / \
1   3

The meaning of the hierarchy, or the connection between the nodes, is defined by us. In the tree above, the meaning is “the left branch is less than the root, and the right branch is greater than the root”. The tree traversal operation can also be defined by us (such as print the current node, or execute it, etc).

Proof trees

Allowing us to define these meanings is what makes trees interesting. One application is the so-called proof trees , which allow us to validate logical arguments for mathematical proofs. Some examples that allow us to specify and traverse this type of tree are theorem provers such as Coq .

Computation trees

Another application is the Computation tree , which allows us to mimic any computation. In this case, the traversal is the “execution” of the code. Some examples that allow us to specify and traverse this type of tree are Lisp-like programming languages, such as Racket .

Proofs

In the Tactics chapter of Logical Foundations, there’s a section “Varying the Induction Hypothesis” that’s discussed. For example, if we want to prove , we introduce and and use induction on . But, the proof will be impossible because we cannot use the inductive hypothesis on the goal. So we “backtrack” (traverse up) in the tree of *all possible proofs* and take a different branch to attempt the proof. If we avoid introducing the variable , and use as the inductive hypothesis, we will be able to complete the proof.

Computation

Did the previous paragraph sound confusing? I will make the analogy with my favorite time killer game – Spider Solitaire .

Observe how I start by moving the 4♠ from the 1st column to the 8th column. This move will reach the end of the tree without any substantial progress. But, when I undo the move (traverse up in the tree) and take a different direction by moving the 4♠ from the 2nd column to the 8th column, then things bloom and this branch of the tree is far more successful.

Conclusion

How does one find the most successful branches in advance? I think that comes with experience, but also luck, because sometimes you just don’t know what’s behind the cards unless you open them. This is why mathematical proofs, programming, and (some) games are not that easy of a challenge.

In any case, it was interesting to make this connection