Studies in Qi

How to Build a Quantifier Machine

Issue #4 in Advanced Programming in Qi

This short study is about how to use functional programming to test first-order logic conjectures about finite domains. A program that does this I call a quantifier machine. Some of the material here is drawn from my forthcoming book Logic, Proof and Computation. You can find the link to the text file for the code for this study at the very bottom of this page.

Bon voyage!

Quantifiers

Two common operations used in functional programming are testing a list to see if some element of the list has a property P and testing a list to see if all elements of the list have the property P. These can be encoded in Qi as two higher order functions.

(define some
[ ] P -> false
[X | Y] P -> (or (P X) (some Y P)))

(define all
[ ] P -> true
[X | Y] P -> (and (P X) (all Y P)))

Thus (some [8 9 10 11 12 13] prime?) returns true (meaning that some element of the domain {8 9 10 11 12 13} is prime) whereas (all [11 12] prime?) returns false.

What if we want to test if two distinct elements of a domain are prime? The problem with our treatment of quantification is that it lacks the concept of a bound variable. We want to be able to say something like

(exists x [8 9 10 11 12 13] (exists y [8 9 10 11 12 13] (and (and (prime? x) (prime? y)) (not (= x y)))))

Here the predicate exists has three inputs not two, the extra input being a bound variable. The problem with this expression is that Qi will try to evaluate (and (and (prime? x) (prime? y)) (not (= x y))))) and this will return an error because the symbol x is not a number.

An Eager Quantifier Machine

Figure 1 The Quantifier Machine as a Black Box

An alternative is to build a special quantifier machine (QM) which will receive quantified first-order sentences and evaluate them using the semantics of first-order logic. The machine will output either true or false (figure 1). If the quantifiers will range over finite domains and the predicates used in the sentence are computable, then the evaluation of the sentence will halt.

There are several ways we can tackle this. The easiest is to represent the inputs to the quantifier machine as list structures. A nice bonus of writing first-order sentences as lists, is that we can use the syntax of first-order logic. So our representation can look like this.

[exists x [8 9 10 11 12 13]
[exists y [8 9 10 11 12 13]
[[[prime? x] & [prime? y]] & [~ [x = y]]]]]

where prime? is defined as

(define prime?
{number --> boolean}
X -> (prime-help X (sqrt X) 2))

(define prime-help
{number --> number --> number --> boolean}
X Max Div -> false where (integer? (/ X Div))
X Max Div -> true where (> Div Max)
X Max Div -> (prime-help X Max (+ 1 Div)))

The simplest machine which will handle this sort of input I call the Eager Quantifier Machine. Here is the code.

(define quantifier-machine
[exists X [ ] P] -> false
[exists X [Y | Z] P] -> (or (quantifier-machine (subst Y X P)) (quantifier-machine [exists X Z P]))
[forall X [ ] P] -> true
[forall X [Y | Z] P] -> (and (quantifier-machine (subst Y X P)) (quantifier-machine [forall X Z P]))
[~ P] -> (not (quantifier-machine P))
[P & Q] -> (and (quantifier-machine P) (quantifier-machine Q))
[P v Q] -> (or (quantifier-machine P) (quantifier-machine Q))
[P => Q] -> (or (not (quantifier-machine P)) (quantifier-machine Q))
[P <=> Q] -> (and (quantifier-machine [P => Q]) (quantifier-machine [Q => P]))
[X = Y] -> (= (quantifier-machine X) (quantifier-machine Y))
[F X] -> ((quantifer-machine F) (quantifer-machine X))
[F X | Y] -> (quantifier-machine [(F X) | Y])
X -> X)

The penultimate line of the eager quantifier machine (below) uses on-the-fly currying to handle n-place (n > 1) predicates by successively generating closures which are in turn recycled back into the quantifer machine. The expression (subst Y X P) substitutes Y for X throughout P.

Here is a script.

(3-) (quantifier-machine [exists x [8 9 10 11 12 13] [exists y [8 9 10 11 12 13] [[[prime? x] & [prime? y]] & [~ [x = y]]]]]).
true

(4-) (quantifier-machine [exists x [8 9 10 11 12 13] [exists y [8 9 10 11 12 13] [x = [+ y 4]]]])
true

Conjectures Involving Large Domains

The EQM is nice because it is simple. But it falls down when we want to compute solutions for large domains. Here is an example involving twin primes.

Twin primes are primes whose difference is 2. 3 and 5 are twin primes and so is 11 and 13. How could we test the following conjecture?

There are twin primes between 1000 and 2000.

Using our eager quantifier machine, we need to first write down 1001 numbers in a list and then set a symbol to denote the list. This is not practical. The problem is that we have learnt no way of representing very large lists.

But there is a way of doing this which uses streams or lazy lists. A stream is a three element list composed of the following items.

1. The first element is the head of the list.
2. The second element is a successor function that, when applied to the first element, will generate the next element of the stream.
3. The final element is a function which tests when the stream has ended.

For example, we can represent the stream of natural numbers from 1000 to 2000 by the following stream.

[1000 (+ 1) (= 2001)]

= is an alternative to the equality relation = which is one of a few special forms in Qi (i.e. like the others if, @p, output, input+, error, cons and let, its not intended to be curried or partially applied and has its own type rule). If streams can be manipulated like lists then we need analogs to the bread-and-butter list functions used in Qi like head, tail and cons. Here are the analogs.

List Function	Stream Function	Qi Definition
head	force	(define force [X S E] -> X)
tail	delay	(define delay [X S E] -> [(S X) S E])
empty? (= NULL in Lisp)	end?	(define end? [X S E] -> (E X))
cons	push	(define push X [Y S E] -> [X (/. Z (if (= Z X) Y (S Z))) E])

force, delay and end? are not hard to define. How about push, the analog to cons? If I push an element x on a stream I should make a larger stream. But I cannot simply place x at the front of the stream without making an list of four objects, which is not a stream. On the other hand, if I simply throw away the first element y of the stream and replace it with x, then I have not made a larger stream but simply replaced y.

The solution is to see that when an object x is pushed on a stream, it does indeed replace the first element y of the stream, but that y is not lost. Instead the successor function S is modified to a new function S’ which is just like S except that if it receives the input x it returns y. In order to code this in Qi, we use abstractions. The function that doubles a number can be represented in Qi as (/. X (* X 2)). The /. is the Qi ASCII substitute for the Greek lambda, and (/. X (* X 2)) is referred to as an abstraction. We can most easily read the notation of abstractions by taking /. to mean “the function that receives an input…”. Thus (/. X (* X 2)) is read as “the function that receives an input X and returns the result of multiplying X by 2”.

The good aspect of abstractions is that they can be used to describe functions that are generated dynamically during the execution of a program. This is precisely what happens to the successor function in the execution of push.

Another useful operation is unpack; which unpacks a stream by turning it into the corresponding list. For instance (unpack [1000 (+ 1) (= 2001)]) will generate [1000 1001 ….. 1999 2000].

(define unpack
Stream -> (if (end? Stream) [ ] [(force Stream) | (unpack (delay Stream))]))

Armed with streams, we can now approach the twin prime conjecture. All that is needed is to evaluate each of the following. set allocates a value to a symbol and value recovers it.

(set 1000to2000 (unpack [1000 (+ 1) (= 2001)]))
(quantifier-machine [exists x (value 1000to2000) [exists y (value 1000to2000) [[[prime? x] & [prime? y]] & [[- x y] = 2]]]])

A Lazy Quantifier Machine

This works fine, but an alternative would be to design a lazy quantifier machine (LQM) that operates directly with streams, rather than requiring them to be unpacked into lists. Here it is.

(define lazy-quantifier-machine
[exists X D P] -> false where (end? D)
[exists X D P]
-> (or (lazy-quantifier-machine (subst (force D) X P)) (lazy-quantifier-machine [exists X (delay D) P])) [forall X D P] -> true where (end? D)
[forall X D P]
-> (and (lazy-quantifier-machine (subst (force D) X P)) (lazy-quantifier-machine [forall X (delay D) P]))
[~ P] -> (not (lazy-quantifier-machine P))
[P & Q] -> (and (lazy-quantifier-machine P) (lazy-quantifier-machine Q))
[P v Q] -> (or (lazy-quantifier-machine P) (lazy-quantifier-machine Q))
[P => Q] -> (or (not (lazy-quantifier-machine P)) (lazy-quantifier-machine Q))
[P <=> Q] -> (and (lazy-quantifier-machine [P => Q]) (lazy-quantifier-machine [Q => P]))
[X = Y] -> (= (lazy-quantifier-machine X) (lazy-quantifier-machine Y))
[F X] -> ((lazy-quantifier-machine F) (lazy-quantifier-machine X))
[F X Y | Z] -> (lazy-quantifier-machine [(F X) Y | Z])
X -> X)

The LQM is more memory efficient than the eager version, but not only this, but the LQM is actually expressively more powerful, since it allows us to test conjectures that range over infinite domains. For example, domain of natural numbers is just the stream.

[0 (+ 1) (/. X false)]

Here the terminating function always returns false, so this is an example of an infinite stream. So we can write (lazy-quantifier-machine [exists x [10000000 (+ 1) (/. X false)] [prime? x]]) to test the conjecture that there exists a prime greater than 10⁷ (assuming that we define prime? to be a recognisor for prime numbers). Hence the LQM allows us to test semi-decidable conjectures. If there is a prime, the LQM will halt with true; otherwise it will run forever. Of course we know that for this particular conjecture, the LQM will return true. For universal quantifiers ranging over infinite domains, the LQM will return false if there is a counterinstance and run forever if the conjecture is true.

There is a class of undecidable problems which even the LQM cannot help us with; these are characterised by mixed existential and universal quantifiers which both range over infinite domains. Here is an example.

There is no greatest prime number.

Though the truth of this sentence has been known over 2,000 years, the LQM will not return any verdict on it. Written in first-order notation the sentence appears as

"x (prime x) ® $y ((prime y) & (y > x))

Suppose the statement is true. Since it uses a universal quantifier over an infinite domain, the quantifier machine will never return a result. Suppose it is false, then the quantifier machine will eventually find the greatest prime and spend forever looking for a bigger one. In either case, the program is silent.

So the LQM is not an omniscient oracle; but still we can make it better. We don't get the full power of quantification until we can manipulate dependent streams.

Dependent Streams and Goldbach's Conjecture

Goldbachs's Conjecture (first formulated in 1746 by the Prussian mathematician Goldbach) states that every even number > 2 is the sum of two primes. How can we test Goldbach's Conjecture using our technology?

One way to do it is this: we start with a stream for the even numbers > 2, for each element X drawn from this stream, we take samples Y and Z from two streams of prime numbers whose minimum is 2 and whose maximum is X. If we find that there is no Y and Z such that X = Y+Z then the Conjecture is false. If there is such a Y and Z, then we take N+2 and repeat. This gives us a semi-decision procedure. If the Conjecture is false, the program will halt. If it is true, it will run forever.

Now there is something important here. The ranges of the streams that generate Y and Z are dependent on the value generated from X - this is what I call a dependent stream. However here we hit a snag - our LQM program does not handle dependent streams.

The Limitations of the LQM

There are two limitations of the LQM.

The LQM as constructed does not handle dependent streams; basically because the functions buried in the streams are represented as abstractions which are resistant to manipulation. What we want to do is to reach into these abstractions at run time and tweak them by the value generated for X. But subst will not do this, since abstractions are not lists.
The EQM and the LQM are slow because they are functioning as interpreters. We need a version of these programs in which it is not necessary to traverse a list structure and call up functions, but one where the functions are called directly. Also subst is a slow and inefficient method for assigning a value to a variable.

Bound Variables Revisited

We have been searching for an implementation of a bound variable; but functional programming already has bound variables. Lambda abstractions bind variables - can we use this mechanism to implement quantification? The answer is "yes" - if we are prepared to accept a hard syntax.

For instance here is a definition of the universal quantifier forall using streams.

(define forall
{(stream A) --> (A --> boolean) --> boolean}
[X S E] P -> (if (E X) true (and (P X) (forall [(S X) S E] P))))

An example (forall [3 (+ 2) (= 9)] prime?) means every second number from 3 to 7 is prime.

Quantifiers work with streams. So lets define a stream as a type in Qi.

(datatype stream

X : A; S : (A --> A); E : (A --> boolean);
===============================
[X S E] : (stream A);)

Here is the definition of exists using streams.

(define exists
{(stream A) --> (A --> boolean) --> boolean}
[X S E] P -> (if (E X) false (or (P X) (exists [(S X) S E] P))))

An example; (exists [33 (+ 2) (= 39)] prime?) means at least one of 33, 35, 37 is prime.

There are no bound variables in the inputs of these functions, but no matter because lambda-bound variables will do the trick. Here is Goldbach's Conjecture.

(forall [4 (+ 2) (/. N false)] (/. X (exists [2 next-prime (< X)] (/. Y (exists [2 next-prime (< X)]
(/. Z (= X (+ Y Z))))))))

Its looks pretty horrible; lets go through it. The first bit (forall [4 (+ 2) (/. N false)] ... just tells us we are quantifying over the domain of even numbers > 2. The bound variable X that follows does the job of the bound variable in quantification. This makes it hard to read because here the bound variable follows the domain of its quantification. Never mind for the moment. The next bit .... (exists [2 next-prime (< X)] .... says there exists a number in the range of primes between 2 and a value less than X. This number is Y and the last bit ... (exists [2 next-prime (< X)] (/. Z (= X (+ Y Z)))))))) says there exists a number Z in the range of primes between 2 and a value less than X such that X = Y + Z.

Phew!

So it captures Goldbach's Conjecture and it uses dependent domains and it is amazingly compact. If you look the Qi book, Goldbach's Conjecture occupies 20 lines in chapter 4 at least - excluding the prime program. This chappie does it in one line with a 3 line help function. But its hard to read - some syntactic sugar would be nice. I'll come back to this.

The next-prime stuff? Here it is.

(define next-prime
{number --> number}
N -> (if (prime? (+ N 1)) (+ N 1) (next-prime (+ N 1))))

Super Quantification

I'm now going to talk about super quantification which is at a level more abstract than ordinary quantifiers. Super quantifiers allow us to tie together a lot of diverse processes from universal and existential quantification to FOR loops and filters.

Super quantifiers begin from an observation. The code for forall and exists is very similar; one uses true and the other false, one uses or and the other and. Suppose we parameterise these definitions to extract the common content - we get the code for super quantification. Here is the code for super quantification.

(define super
{(stream A) --> (A --> B) --> (B --> C --> C) --> C --> C}
[X S E] P F Y -> (if (E X) Y (F (P X) (super [(S X) S E] P F Y))))

Haskell programmers will recognise the code for super quantification as a close relative of their foldr function. The main difference is that there are 4 and not 3 arguments to the function and the function operates on streams and not lists.

What does this function do and why is it so super? Well first we can define forall and exists in it.

(define forall
{(stream A) --> (A --> boolean) --> boolean}
Stream P -> (super Stream P and true))

(define exists
{(stream A) --> (A --> boolean) --> boolean}
Stream P -> (super Stream P or false))

Thats not all - we can also define the FOR loop beloved of procedural programmers since FORTRAN was a lad. Here is the code.

(define for
{(stream A) --> (A --> B) --> number}
Stream P -> (super Stream P progn 0))

(define progn
{A --> B --> B}
X Y -> Y)

Lets try it out. Print the numbers 0 to 99.

(101+) (for [0 (+ 1) (= 100)] print)
0123456789101112131415161718192021222324252627282930313233343536373839404142434
4546474849505152535455565758596061626364656667686970717273747576777879808182838
8586878889909192939495969798990 : number

Filtering a stream gathers all elements of a certain kind. But with super quantification, filtering over streams is easy. Here is the definition.

(define filter
{(stream A) --> (A --> boolean) --> [A]}
Stream P -> (super Stream (/. X (if (P X) [X] [])) append []))

Here is an example; find all the perfect squares between 1 and 99.

(104+) (filter [1 (+ 1) (= 100)] (/. X (integer? (sqrt X))))
[1 4 9 16 25 36 49 64 81] : (list number)

You can also devise mapping functions over streams and other such stuff with super quantification; I leave you to explore this.

One source of annoyance. Our encoding of super quantifiers uses strict evaluation because Qi uses strict evaluation in all functions except or and and if. A higher-order function will be strict in its evaluation and this is also the case with super. Unfortunately, when we pass lazy functions to super like and and or we want the evaluation in super to be lazy too. The only practical solution is to make these special cases in a case statement. The result works, but cannot be type checked as before (the explicit use of booleans in the function puts constraints on the type checker).

(define super

[X S E] P F Y -> (if (E X) Y

(if (= F or)

(or (P X) (super [(S X) S E] P F Y))

(if (= F and)

(and (P X) (super [(S X) S E] P F Y))

(F (P X) (super [(S X) S E] P F Y))))))

Sugaring the Syntax

Our new treatment of quantification is very powerful, but the syntax leaves something to be desired. Really this is unavoidable, since the position of the lambda bound variables determines the proper evaluation of the whole expression. However it would be nice to have something more readable.

Qi contains a facility for changing its own syntax. In fact you can make Qi look like almost anything using this facility. The facility is called macroexpand. macroexpand is a function that is applied to every input, whether typed or read from a file. By default, macroexpand is the identity function i.e. it does nothing. However you, the user, can change the definition of this function to suit your convenience. For example, suppose we want an infix +; the following macroexpansion does it.

(0-)(define macroexpand
[X + Y] -> (macroexpand [+ X Y])
[X | Y] -> [(macroexpand X) | (macroexpand Y)]
X -> X)

WARNING:
DEFUN/DEFMACRO: redefining function macroexpand in C:\Documents and Settings\Mar
k Tarver\My Documents\Lambda Associates\Qi 6.2\startup_qi.txt, was defined in C:
\Documents and Settings\Mark Tarver\My Documents\Lambda Associates\Qi 6.2\Instal
l Qi\Qi 6.3.txt
macroexpand

(1-)(tc +)
true

(2+) (1 + 7)
8 : number

(3+) (define total
{[number] --> number}
[] -> 0
[X | Y] -> (X + (total Y)))
total : ((list number) --> number)

Macroexpansion reads in infix additions and outputs the prefix form. Hence the external syntax of Qi now permits infix addition, whereas the internal syntax stays the same. The macroexpand function maps external to internal syntax.

Ergo, if you don't like Qi syntax - invent your own!

OK, lets invent our own syntax for quantification to make our lambda stuff more readable. Here is my shot at it.

(define macroexpand
[exists X S P] -> (macroexpand [exists S [/. X P]])
[forall X S P] -> (macroexpand [forall S [/. X P]])
[X | Y] -> [(macroexpand X) | (macroexpand Y)]
X -> X)

Now I can enter Goldbach's conjecture in a friendlier form and reduce the bracketing.

(forall X [4 (+ 2) (/. N false)] (exists Y [2 next-prime (< X)] (exists Z [2 next-prime (< X)] (= X (+ Y Z)))))

Now this can be read quite easily left to right.

For all X from the stream [4 (+ 2) (/. X false)], there is a Y from the stream [2 next-prime (< X)] such that there is a Z from the stream [2 next-prime (< X)] such that (= X (+ Y Z)).

Olé!

Mark

The code for this study is in this file. 120 lines in total.