Simple theorem prover in Racket

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 🙂

Advertisements

Effects of Side effects

Recently I was working on a project that involved the usage of PayPal REST API SDK.

To give a little bit of background, starting in PHP 7.x (I believe 7.2), the language will throw a warning if you use sizeof on a variable that does not implement Countable. Arrays implement Countable, but obviously not primitive types, such as integer for example:

php > var_dump( sizeof( [] ) );
int(0)
php > var_dump( sizeof( 1 ) );
PHP Warning:  sizeof(): Parameter must be an array or an object that implements Countable in php shell code on line 1
int(1)

So, now depending on how we use sizeof, it can trigger the warning which is a kind of a side-effect. In PayPal, before they provided a fix for it, what they did was:

if (sizeof($v) <= 0 && is_array($v))

After:

if (is_array($v) && sizeof($v) <= 0)

The only difference in the code above is the order of operations. The second code snippet won’t trigger the warning. However, for the first one, obviously if the variable $v does not implement Countable, you will get the warning.

Mathematically, the logical AND operation is commutative, i.e. a AND b = b AND a. In some cases, it can also be commutative in programming, up until the point side effects are involved.

So a AND b may not necessarily be b AND a if there are side effects involved. There’s a good reason for this “trade-off”, since side effects can be expensive so if evaluating only the first one returns false there’s no need to evaluate the rest of them to waste resources (since we know that false AND a AND ... is false). The side effect here is PHP throwing warnings to stdout on sizeof.

Refactoring using mathematical properties of min

Today I refactored a small piece of code.

Before:

$coupon_amount = self::get_coupon_prop( $coupon, 'amount' ) - $already_applied_coupons;

if ( isset( WC()->cart ) ) {
	$coupon_amount = min( WC()->cart->subtotal - $already_applied_coupons, $coupon_amount );
}

if ( $coupon_amount < 0 ) {
	return $discount;
}

After:

$coupon_amount = self::get_coupon_prop( $coupon, 'amount' );

if ( isset( WC()->cart ) ) {
	$coupon_amount = min( WC()->cart->subtotal, $coupon_amount );
}

$coupon_amount -= $already_applied_coupons;

if ( $coupon_amount < 0 ) {
	return $discount;
}

This was intuitive to me, but I wanted to prove that it really does the same thing. For that, we need to use the property min(a - c, b - c) = min(a, b) - c.

The usual definition for min is:
min(a, b) =  \left\{  	\begin{array}{ll}  		a,  & \mbox{if } a < b \\  		b,  & \mbox otherwise  	\end{array}  \right.

Now we can use proof by cases to prove our property which will allow us to confidently refactor our code. There are two cases we can assume:

1. Case a - c > b - c:
In this case, min(a - c, b - c) = b - c, and since from a - c > b - c we can conclude that a > b, then min(a, b) = b.
So, we have that b - c = b - c, which proves this case.

2. Case a - c \le b - c:
In this case, min(a - c, b - c) = a - c, and since from a - c < b - c we can conclude that a < b, then min(a, b) = a.
So, we have that a - c = a - c, which proves this case.

Thus, the property min(a - c, b - c) = min(a, b) - c is proven. 🙂

There are also some other properties like min(a, a) = a and min(a, b) = min(b, a) but you can try doing these yourself. Stuff with max is proven analogously.