According to Wikipedia, the bisection method in mathematics is a root-finding method that repeatedly bisects an interval and then selects a subinterval in which a root must lie for further processing. We can use this method to find zeroes of some continuous function.

Finding zeroes of a function is a very useful concept in practice. Since the function can be almost anything, this means that we can solve about any equality.

For a given continuous function , and an interval , where and (that is, the function changes sign for some value in that interval), the algorithm thus tries to minimize such that , where .

The algorithm is as follows:

1. Set interval
2. Calculate
   • If is sufficiently small, stop
   • Else if , then set
   • Else, set
3. Goto 1

As always, definitions are best understood with examples, so we’ll give a few examples.

Example 1: Approximating square root

We will start by approximating the value of . The function we want to find zero for is then , since . We have that , thus our interval is .

Let's apply the algorithm a few times now:

a	b
2	4
2	3
2	2.5
2	2.25
2.125	2.25
2.1875	2.25

So, 2.21875 is a close approximation of . We can make it even closer by applying the algorithm a couple of more times.

Example 2: Finding a bad commit in a sequence of commits

As a second example, let’s imagine a function that will represent a bunch of Git commits, where one of the commits are bad. Let’s pick such a function at random, maybe . We will also agree that the function returns a value greater than 0 if the software is functioning at that point of commit, and a value less than or equal to 0 otherwise.

How will you find the bad commit? Brute-force or linear search is one way, but it may not be as efficient as bisecting. You can graph the function and look at its zeroes, but that’s a bit cheating, and usually impossible to do in practice with git-bisect since we cannot cover all predicates (in which case here is “software is functioning”), and thus cannot construct a graph of all such functions w.r.t commits. Since we’re cool, we’ll use the bisection method.

Let’s start at random, knowing at least one good and one bad commit. Maybe picking the interval is a good start. We have that .

Our task is to find which commit caused the software to break. Let's apply the same algorithm.

a	b
50	10
50	30
40	30

So, in just 3 steps we found that the bad commit was 35.

Git-bisect

git-bisect is a very useful command. Given a sequence of commits, it allows you to find a commit that satisfies some property.

The way bisect works is that it will find zeroes of the function . So, given an interval of commits , the function will return such that holds for it.

The fastest way to do that is to use bisection, which we explained earlier. Git uses good and bad for bisecting left and right.

For example, let’s assume we have the following setup:

bor0@boro:~$ git init
Initialized empty Git repository in /Users/bor0/.git/
bor0@boro:~$ echo "Hello World!" > test.txt
bor0@boro:~$ git add test.txt && git commit -m "First commit"
[master (root-commit) faf3b15] First commit
 1 file changed, 1 insertion(+)
 create mode 100644 test.txt
bor0@boro:~$ echo "Hello Worldd!" >> test.txt
bor0@boro:~$ git add test.txt && git commit -m "Second commit"
[master c9b527b] Second commit
 1 file changed, 1 insertion(+)
bor0@boro:~$ echo "Hello World!" >> test.txt
bor0@boro:~$ git add test.txt && git commit -m "Third commit"
[master 8d28e4a] Third commit
 1 file changed, 1 insertion(+)

Now, if we check the contents of the file:

bor0@boro:~$ cat test.txt
Hello World!
Hello Worldd!
Hello World!

For the sake of this demo, let’s assume the the only acceptable string in a list of strings is “Hello World!”. So the latest commit is now broken. In order to find which commit broke this, we can use bisect as follows:

bor0@boro:~$ git bisect start
bor0@boro:~$ git bisect bad 8d28e4a
bor0@boro:~$ git bisect good faf3b15
Bisecting: 0 revisions left to test after this (roughly 0 steps)
[c9b527bbd44542fb7d69df15ce82919055b36578] Second commit
bor0@boro:~$ cat test.txt 
Hello World!
Hello Worldd!
bor0@boro:~$ git bisect bad
c9b527bbd44542fb7d69df15ce82919055b36578 is the first bad commit
commit c9b527bbd44542fb7d69df15ce82919055b36578
Author: Boro Sitnikovski <buritomath@gmail.com>
Date:   Sun Oct 21 20:10:44 2018 +0200

    Second commit

:100644 100644 980a0d5f19a64b4b30a87d4206aade58726b60e3 0c5b693e0f16f325e967f6482d4f9fe02159472b M	test.txt
bor0@boro:~$ 

It was easy in this case, since we had 3 commits. But if you had 1000 commits, it would only take about 10 good or bad choices, which is cool.

So our property was , and so our function (the result of git bisect) returned c9b527bbd44542fb7d69df15ce82919055b36578, the first commit where the property was satisfied.

As a conclusion, it’s interesting to think that we’re actually finding a zero of a function when we use git-bisect 🙂

Bonus: Example implementation in Scheme:

(define (bisect f iterations low high)
  (letrec ([approx (/ (+ low high) 2)]
           [computed (f approx)])
    (cond ((zero? iterations) approx)
          ((> computed 0) (bisect f (- iterations 1) low approx))
          (else (bisect f (- iterations 1) approx high)))))

Interacting with it:

> (bisect (lambda (x) (- (* x x) 5)) 50 2.0 4)
2.236067977499789

Lambda calculus is a formal system for representing computation. As with most formal systems and mathematics, it relies heavily on substitution.

We will start by implementing a subst procedure that accepts an expression e, a source src and a destination dst which will replace all occurences of src with dst in e.

(define (subst e src dst)
  (cond ((equal? e src) dst)
        ((pair? e) (cons (subst (car e) src dst)
                         (subst (cdr e) src dst)))
        (else e)))

Trying it a couple of times:

> (subst '(lambda (x) x) 'x 'y)
'(lambda (y) y)
> (subst '(lambda (x) x) '(lambda (x) x) 'id)
'id

Next, based on this substitution we need to implement a beta-reduce procedure that, for a lambda expression will reduce to , that is, with all within replaced to .

Our procedure will consider 3 cases:

1. Lambda expression that accepts zero args – in which case we just return the body without any substitutions
2. Lambda expression that accepts a single argument – in which case we substitute every occurrence of that argument in the body with what’s passed to the expression and return the body
3. Lambda expression that accepts multiple arguments – in which case we substitute every occurrence of the first argument in the body with what’s passed to the expression and return a new lambda expression

Before implementing the beta reducer, we will implement a predicate lambda-expr? that returns true if the expression is a lambda expression, and false otherwise:

(define (lambda-expr? e)
  (and (pair? e)
       (equal? (car e) 'lambda)
       (list? (cadr e))))

Here’s the helper procedure which accepts a lambda expression e and a single argument x to pass to the expression:

(define (beta-reduce-helper e x)
  (cond ((and (lambda-expr? e)
              (pair? (cadr e))
              (pair? (cdadr e)))
         ; lambda expr that accepts multiple args
         (list 'lambda
               (cdadr e)
               (subst (caddr e) (caadr e) x)))
        ((and (lambda-expr? e)
              (pair? (cadr e)))
         ; lambda expr that accepts a single arg
         (subst (caddr e) (caadr e) x))
        ((and (lambda-expr? e)
              (equal? (cadr e) '()))
         ; lambda expr with zero args
         (caddr e))
        (else e)))

Then, our procedure beta-reduce will accept variable number of arguments, and apply each one of them to beta-reduce-helper:

(define (beta-reduce l . xs)
  (if (pair? xs)
      (apply beta-reduce
             (beta-reduce-helper l (car xs))
             (cdr xs))
      l))

Testing these with a few cases:

> (beta-reduce '(lambda (x y) x) 123)
'(lambda (y) 123)
> (beta-reduce '(lambda (x y) y) 123)
'(lambda (y) y)
> (beta-reduce '(lambda (x) (lambda (y) x)) 123)
'(lambda (y) 123)
> (beta-reduce '(lambda (x) (lambda (y) y)) 123)
'(lambda (y) y)

However, note this case:

> (beta-reduce '(lambda (n f x) (f (n f x))) '(lambda (f x) x))
'(lambda (f x) (f ((lambda (f x) x) f x)))

It seems that we can further apply beta reductions to simplify that expression. For that, we will implement lambda-eval that will recursively evaluate lambda expressions to simplify them:

(define (lambda-eval e)
  (cond ((can-beta-reduce? e) (lambda-eval (apply beta-reduce e)))
        ((pair? e) (cons (lambda-eval (car e))
                         (lambda-eval (cdr e))))
        (else e)))

But, what does it mean for an expression e to be beta reducible? The predicate is simply:

(define (can-beta-reduce? e)
  (and (pair? e) (lambda-expr? (car e)) (pair? (cdr e))))

Great. Let’s try a few examples now:

> ; Church encoding: 1 = succ 0
> (lambda-eval '((lambda (n f x) (f (n f x))) (lambda (f x) x)))
'(lambda (f x) (f x))
> ; Church encoding: 2 = succ 1
> (lambda-eval '((lambda (n f x) (f (n f x))) (lambda (f x) (f x))))
'(lambda (f x) (f (f x)))
> ; Church encoding: 3 = succ 2
> (lambda-eval '((lambda (n f x) (f (n f x))) (lambda (f x) (f (f x)))))
'(lambda (f x) (f (f (f x))))

There’s our untyped lambda calculus 🙂

There are a couple of improvements that we can do, for example implement define within the system to define variables with values. Another neat addition would be to extend the system with a type checker.

EDIT: As noted by a reddit user, the substitution procedure is not considering free/bound variables. Here’s a gist that implements that as well.

One well known fact is the sum . Let’s try to prove this fact in Idris.

We start intuitively by defining our recursive sum function:

total sum : Nat -> Nat
sum Z     = Z
sum (S n) = (S n) + sum n

Testing it a few times:

Idris> sum 3
6 : Nat
Idris> sum 4
10 : Nat

Looks good.

Next, we will come up with out dependently typed function to prove the fact.

theorem_1_firsttry : (n : Nat) -> sum n = divNat (n * (n + 1)) 2
theorem_1_firsttry Z     = ?a
theorem_1_firsttry (S n) = ?b

The base case that we need to prove is of type 0 = divNat 0 2. Looks a bit tricky. Let’s try to use divNatNZ along with a proof that 2 is not zero:

theorem_1_secondtry : (n : Nat) -> sum n = divNatNZ (n * (n + 1)) 2 (SIsNotZ {x = 1})
theorem_1_secondtry Z     = ?a
theorem_1_secondtry (S n) = ?b

Now the base case is just Refl. Let’s put an inductive hypothesis as well:

theorem_1_secondtry : (n : Nat) -> sum n = divNatNZ (n * (n + 1)) 2 (SIsNotZ {x = 1})
theorem_1_secondtry Z     = Refl
theorem_1_secondtry (S n) = let IH = theorem_1_secondtry n in ?b

Idris tells us that we now need to prove:

b : S (plus n (sum n)) =
    ifThenElse (lte (plus (plus n 1) (mult n (S (plus n 1)))) 0)
               (Delay 0)
               (Delay (S (Prelude.Nat.divNatNZ, div' (S (plus (plus n 1) (mult n (S (plus n 1)))))
                                                     1
                                                     SIsNotZ
                                                     (plus (plus n 1) (mult n (S (plus n 1))))
                                                     (minus (plus (plus n 1) (mult n (S (plus n 1)))) 1)
                                                     1)))

Woot.

Let’s take a slightly different route by doing a few algebraic tricks to get rid off division. Instead of proving that , we will prove .

total theorem_1 : (n : Nat) -> 2 * sum n = n * (n + 1) -- sum n = n * (n + 1) / 2
theorem_1 Z     = Refl
theorem_1 (S n) = ?b

Now we need to show that b : S (plus (plus n (sum n)) (S (plus (plus n (sum n)) 0))) = S (plus (plus n 1) (mult n (S (plus n 1)))).

total theorem_1 : (n : Nat) -> 2 * sum n = n * (n + 1) -- sum n = n * (n + 1) / 2
theorem_1 Z     = Refl
theorem_1 (S n) = let IH = theorem_1 n in
                  rewrite (multRightSuccPlus n (plus n 1)) in
                  rewrite sym IH in
                  rewrite (plusZeroRightNeutral (sum n)) in
                  rewrite (plusZeroRightNeutral (plus n (sum n))) in
                  rewrite (plusAssociative n (sum n) (sum n)) in
                  rewrite (sym (plusSuccRightSucc (plus n (sum n)) (plus n (sum n)))) in
                  rewrite plusCommutative (plus n 1) (plus (plus n (sum n)) (sum n)) in
                  rewrite sym (plusSuccRightSucc n Z) in
                  rewrite plusZeroRightNeutral n in
                  rewrite (sym (plusSuccRightSucc (plus (plus n (sum n)) (sum n)) n)) in
                  rewrite (sym (plusAssociative (n + sum n) (sum n) n)) in
                  rewrite plusCommutative (sum n) n in Refl

Looks a bit big, but it works! With line 4 and 5 we get rid off multiplication and then all we need to do is some algebraic re-ordering of plus to show that both sides are equivalent.

Now that we proved it, you can use this fact in your favorite programming language 🙂

First, let’s start by implementing map' and filter' for lists:

total map' : (a -> b) -> List a -> List b
map' _ [] = []
map' f (x :: xs) = f x :: map' f xs

total filter' : (a -> Bool) -> List a -> List a
filter' p []      = []
filter' p (x::xs) with (p x)
  filter' p (x::xs) | True  = x :: filter' p xs
  filter' p (x::xs) | False = filter' p xs

Trying a few cases:

Idris> map' (\x => x + 1) [1, 2]
[2, 3] : List Integer
Idris> filter' (\x => x /= 2) [1, 2]
[1] : List Integer

Looks neat.

A valid question would be: What do we know about the length of a mapped and length of a filtered list?

Intuition says that the length of a mapped list will be the same as the length of that list, since the values of the elements might change but not the actual length (size) of the original list. Let’s prove this fact:

-- For any given list xs, and any function f, the length of xs is same as the length of xs mapped with f
total theorem_1 : (xs : List a) -> (f : a -> b) -> length xs = length (map' f xs)
theorem_1 [] _        = Refl
theorem_1 (x :: xs) f = let I_H = theorem_1 xs f in rewrite I_H in Refl

Easy peasy, just use induction.

Filtering is a bit trickier. The length of a filtered list can be less than or equal to the original list. The intuitive reasoning for this is as follows:

1. Maybe the filter will apply to some elements, in which case the length of the filtered list will be less than the length of the original list
2. Or, maybe the filter will not apply at all, in which case the length of the filtered list is the same as the length of the original list

Let’s prove it!

-- For any given list xs, and any filtering function f, the length of xs >= the length of xs filtered with f
total theorem_2 : (xs : List a) -> (f : a -> Bool) -> LTE (length (filter' f xs)) (length xs)
theorem_2 [] _        = LTEZero {right = 0}
theorem_2 (x :: xs) f with (f x)
  theorem_2 (x :: xs) f | False = let I_H = theorem_2 xs f in let LTESuccR_I_H = lteSuccRight I_H in LTESuccR_I_H
  theorem_2 (x :: xs) f | True  = let I_H = theorem_2 xs f in let LTESucc_I_H  = LTESucc I_H in LTESucc_I_H

I constructed this proof using holes. The base case was very simple, however, for the inductive step we needed to do something else. With the inductive step we consider two cases:

1. In the case the filter was applied (False), the I_H needs to match the target type LTE _ (S _)
2. In the case the filter was not applied (True), the I_H needs to match the target type LTE (S _) (S _)

Idris has built-in proofs for these, with the following types:

Idris> :t lteSuccRight
lteSuccRight : LTE n m -> LTE n (S m)
Idris> :t LTESucc
LTESucc : LTE left right -> LTE (S left) (S right)

So we just needed to use them to conclude the proof.

Bonus: The only reason I rewrote filter' was to use with which seems easier to rewrite to when proving stuff about it. The built-in filter uses ifThenElse and I haven’t found a way to rewrite goals that are using it. I rewrote map' just for consistency.

Bonus 2: Thanks to gallais@reddit for this hint. It seems that the same with (f x) used in the proof also makes the ifThenElse reduce.

In an earlier post, we’ve defined what formal systems are.

In this example, we’ll put formal systems into action by building a proof tree generator in the Racket programming language.

We should be able to specify axioms and inference rules, and then query the program so that it will produce all valid combinations of inference in attempt to reach the target result.

First, we’ll start by defining our data structures:

; A rule is a way to change a theorem
(struct rule (name function) #:transparent)

; A theorem is consisted of an initial axiom and rules (ordered set) applied
(struct theorem (axiom rules result) #:transparent)

; A prover system is consisted of a bunch of axioms and rules to apply between them
(struct theorem-prover (axioms rules) #:transparent)

; An axiom is just a theorem already proven
(define (axiom a) (theorem (list a) '() a))

Now, to apply a rule to a theorem, we create a new theorem whose result is all the rules applied to the target theorem:

; Apply a single rule to a theorem
(define (theorem-apply-rule p t r)
  (theorem (theorem-axiom t)
           (append (theorem-rules t) (list r))
           ((rule-function r) (theorem-result t) p)))

We will need a procedure that will apply all the rules to all theorems consisted in a given object theorem-prover:

; Apply all prover's rules to a list of theorems
(define (theorems-apply-rules-iter prover theorems result)
  (cond
    ((eq? theorems '()) result)
    (else
     (theorems-apply-rules-iter
      prover
      (cdr theorems)
      (append (map (lambda (r) (theorem-apply-rule prover (car theorems) r)) (theorem-prover-rules prover))
              result)))))

; Helper procedure
(define (theorems-apply-rules prover theorems) (theorems-apply-rules-iter prover theorems '()))

Now, in order to find a proof for a given theorem-prover, we search through the theorem results and see if the target is there. If it is, we just return. Otherwise, we recursively go through the theorems and apply rules in order to attempt to find the target theorem. Here’s the procedure that searches for a proof:

; Find a proof by constructing a proof tree by iteratively applying theorem rules
(define (find-proof-iter prover target max-depth found-proofs depth)
  (cond
    ; The case where the proof was found
    ((member target (map theorem-result found-proofs)) (findf (lambda (t) (equal? (theorem-result t) target)) found-proofs))
    ; The case where max depth of search was reached
    ((> depth max-depth) #f)
    ; Otherwise just try to apply the known rules to the found proofs
    (else (letrec ([theorems (theorems-apply-rules prover found-proofs)]
                   [proofs-set (list->set (map theorem-result found-proofs))]
                   [theorems-set (list->set (map theorem-result theorems))])
            (if (equal? (set-union proofs-set theorems-set) proofs-set)
                ; The case where no new theorems were produced, that is, A union B = A
                #f
                ; Otherwise keep producing new proofs
                (find-proof-iter prover target max-depth (merge-proofs found-proofs theorems) (+ 1 depth)))))))

; Helper procedure
(define (find-proof prover target max-depth)
  (find-proof-iter prover target max-depth (theorem-prover-axioms prover) 0))

But what is merge-proofs? It’s simply a procedure that given 2 lists of proofs, it will return them merged. However, we want to avoid duplicates to skip duplicate processing. So the proof tree should not contain duplicate nodes.

; Merge two list of proofs but skip duplicate proofs, giving the first argument priority
; This is used to avoid circular results in the search tree
; E.g. application of rules resulting in an earlier theorem/axiom
(define (merge-proofs p1 p2)
  (remove-duplicates (append p1 p2) (lambda (t1 t2) (equal? (theorem-result t1) (theorem-result t2)))))

So, as an example usage:

; Example rules
(define mu-rules
  (list
   (rule "One" (lambda (t p) (if (string-suffix? t "I") (string-append t "U") t)))
   (rule "Two" (lambda (t p)
                 (let ([matches (regexp-match #rx"M(.*)" t)])
                   (if (and (list? matches) (>= 2 (length matches)))
                       (string-append t (cadr matches))
                       t))))
   (rule "Three" (lambda (t p) (string-replace t "III" "U" #:all? #f)))
   (rule "Four" (lambda (t p) (string-replace t "UU" "" #:all? #f)))))

; Example prover
(define test-prover (theorem-prover (list (axiom "MI")) mu-rules))

; Find the proof of "MIUIU" with max-depth of 5
(find-proof test-prover "MIUIU" 5)

As a result, we get: (theorem '("MI") (list (rule "One" #) (rule "Two" #)) "MIUIU"), which says that for a starting theorem MI, we apply rule “One” and rule “Two” (in that order) to get to MIUIU (our target proof that we’ve specified) which is pretty awesome 🙂