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)
    ((eq? theorems '()) result)
      (cdr theorems)
      (append (map (lambda (r) (theorem-apply-rule prover (car theorems) r)) (theorem-prover-rules prover))

; 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)
    ; 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
                ; 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
   (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))
   (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 🙂


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( [] ) );
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

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))


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.

Creating our own ‘struct’ macro in Racket

One thing that was always interesting to me about Lisps in general is their minimality, which means that with a couple of starting points you can implement almost anything in the language, even parts of the language itself.

SICP in chapter 2 asks us to re-implement car, cons, and cdr (related post).

That’s a neat way to represent structured data.

Now, for something more interesting, how about we re-implement the struct syntax, by providing our own create-struct macro that will generate a data type with fields, and procedures for retrieving them?

For example, if we did the following:

(create-struct person (firstname lastname))

This macro should generate these procedures for us:

  1. person – to construct an object of such type, which accepts 2 parameters in this case
  2. person? – to check if a variable is really of that struct type, which accepts 1 parameter
  3. person-firstname – to retrieve the first field of a person object, which accepts 1 parameter
  4. person-lastname – to retrieve the second field of a person object, which accepts 1 parameter

That is, the code above should generate something similar to this:

(define (person firstname lastname) (list 'person firstname lastname))
(define (person? p) (and (list? p) (>= (length p) 1) (equal? (car p) 'person)))
(define (person-firstname p) (list-ref p 1))
(define (person-lastname p) (list-ref p 2))

So that when we evaluate it, we get:

> (person-firstname (person "Hello" "World"))
> (person-lastname (person "Hello" "World"))
> (person? (person "Hello" "World"))

Sounds fun?

We will use non-hygienic macros just for fun, since I find them easier to write code with and understand them.

So, our code starts with:

#lang racket

; Non-hygienic macros support.
(require mzlib/defmacro)

Let’s start by just implementing our constructor person initially:

(define-macro (create-struct struct-name struct-fields)
  (list 'begin
        (list 'define struct-name
              (list 'lambda struct-fields (cons 'list (cons (list 'quote struct-name) struct-fields))))))

Testing it:

> (person "Hello" "World")
'(person "Hello" "World")

Seems to be working fine.

To get a better grasp for the code above, what I usually do is change it to a function, and call it to see what it returns. But testing it this way can be tricky as it won’t have the variables in context, so you will have to quote allthethings:

#lang racket
(require mzlib/defmacro)

(define (create-struct struct-name struct-fields)
  (list 'begin
        (list 'define struct-name
              (list 'lambda struct-fields (cons 'list (cons (list 'quote struct-name) struct-fields))))))

(create-struct 'person '(firstname lastname))
; returns '(begin (define person (lambda (firstname lastname) (list 'person firstname lastname))))

Looking good.

Now, let’s proceed by implementing person?:

(define-macro (create-struct struct-name struct-fields)
   (list 'begin
         (list 'define struct-name
               (list 'lambda struct-fields (cons 'list (cons (list 'quote struct-name) struct-fields))))
         (list 'define (string->symbol (string-append (symbol->string struct-name) "?"))
               (list 'lambda '(x) (list 'and (list 'list? 'x) (list '>= (list 'length 'x) 1) (list 'equal? (list 'car 'x) (list 'quote struct-name))))))))

Testing it:

> (person? (person "Hello" "World"))
> (person? '(1 2 3))
> (person? '(person 2 3))

We will have to re-use the string->symbol magic we did, so it’s good to even have that as a macro:

(define-macro (symbol-append . x)
  (list 'string->symbol (list 'apply 'string-append (list 'map 'symbol->string (cons 'list x)))))

(symbol-append 'a 'b 'c) ; returns 'abc

Looks good. Now, let’s try to use it in our macro by changing that line to:

(list 'define (symbol-append struct-name '?)

We get the following:

. symbol-append: unbound identifier in module (in the transformer environment, which does not include the macro definition that is visible to run-time expressions) in: symbol-append

After some searching through the docs, I found out that it’s related to compilation phases. Note that in REPL mode it would not make any difference.

In order to define a function that we can use in our macro, we can use define-for-syntax. It acts just like define, except that the binding is at phase level 1 instead of phase level 0.

(define-for-syntax (symbol-append . x)
  (string->symbol (apply string-append (map symbol->string x))))

Now our code works. Phew!

To finalize our macro, we also have to implement the getters. We could try with the following code:

(define struct-name 'test)
(define struct-fields '(a b c))

(map (lambda (field index)
       (list 'define
             (symbol-append struct-name '- field)
             (list 'lambda (list 'ctx) (list 'list-ref 'ctx index))))
     (range 1 (+ 1 (length struct-fields))))

What this code does is it will map through all the struct-fields, create a definition for them named by using our symbol-append helper concatenated with their field name, and then the body of that function should just use list-ref. Note how we added another field to our map (index) so that we know what to list-ref to.

Running the code above produces:

'((define test-a (lambda (ctx) (list-ref ctx 1))) (define test-b (lambda (ctx) (list-ref ctx 2))) (define test-c (lambda (ctx) (list-ref ctx 3))))

Looks good. Now, let’s try to merge the code above in our macro, so that the final definition is:

(define-macro (create-struct struct-name struct-fields)
   (list 'begin
         (list 'define struct-name
               (list 'lambda struct-fields (cons 'list (cons (list 'quote struct-name) struct-fields))))
         (list 'define (symbol-append struct-name '?)
               (list 'lambda '(x) (list 'and (list 'list? 'x) (list '>= (list 'length 'x) 1) (list 'equal? (list 'car 'x) (list 'quote struct-name))))))
   (map (lambda (field index)
          (list 'define
                (symbol-append struct-name '- field)
                (list 'lambda (list 'ctx) (list 'list-ref 'ctx index))))
        (range 1 (+ 1 (length struct-fields))))))

Whoops, again a compilation phases error:

range: unbound identifier in module (in phase 1, transformer environment) in: range

By visiting the same docs as above, we just need to do the following:

; We need to do this so that the bindings for `range` are provided in context for the macro.
(require (for-syntax racket))

And that concludes our macro. Let’s give it a few tries now:

(create-struct person (firstname lastname))
(define test-p1 (person "Test" "Person"))
(person-firstname test-p1)
(person-lastname test-p1)
(person? test-p1)

(struct person-2 (firstname lastname))
(define test-p2 (person-2 "Test" "Person"))
(person-2-firstname test-p2)
(person-2-lastname test-p2)
(person-2? test-p2)

This post re-implements the struct keyword just for fun. It also demonstrates how tricky compilation and runtime phases can be.

Bonus: Serialization works pretty well with a structure like this. If you try to serialize a struct you will see it binds the data to the current executing module:

#lang racket
(require racket/serialize)

(serializable-struct person (firstname lastname) #:transparent)
(serialize (person "Hello" "World"))
; Produces the following:
; '((3) 1 (('anonymous-module . deserialize-info:person-v0)) 0 () () (0 "Hello" "World"))

There is a good reason for the behaviour above, since a fish structure used by one programmer in one module is likely to be different from a fish structure used by another programmer.

However, you can pass #:prefab with a struct to achieve similar functionality with our struct macro above, that is, generate a “global” serialized value:

#lang racket
(require racket/serialize)

(struct person (firstname lastname) #:prefab)
(serialize (person "Hello" "World"))
; Produces the following:
; '((3) 0 () 0 () () (f person "Hello" "World"))