Go backward to 2.3 Predicate Logic Go up to 2 The Language of Logic |
Write a program that takes a number and returns the next prime number.
Specification The task can be formally specified as follows:
As for the input condition, we can reasonably assume from the problem statement that the input is a natural number. We denote by N the set of natural numbers and define
isNumber(n) : <=> n in Nusing the set theoretic predicate ` in ' ("is element of") to be introduced in the next chapter and the notion `: <=> ' to define a new predicate.
The output condition is a bit more complicated. Apparently, the result p shall be again an object of the same kind as input n; but it shall be also a prime and it shall be the "next" such number. Thus we define
isNextPrime(n, p) : <=> isNumber(p) /\ isPrime(p) /\ isNextP(n, p).
A natural number p greater than 1 is a prime if and only if there is no number n between 1 and p that divides p
isPrime(p) : <=> 1 < p /\ ~(exists 1 < n < p: n | p).
This can be written a bit more elegantly as
isPrime(p) : <=> 1 < p /\ forall 1 < n < p: n not | p.
The number n divides m if there exists some p such that the product of n and p is m:
n | m : <=> exists p: n*p = m.
Thus we have reduced the description of the predicate isPrime to formulas that only use the function constant * and the predicates = and < with their usual interpretation on natural numbers.
Now we proceed to the question what n's next prime p is. A little thinking reveals that the notion "next" intends to express that there is no other number between n and p that is also a prime. But what if n is itself prime? Shall we then return n itself or the smallest prime greater than n? The natural language term "next" is somewhat ambiguous in this respect, so we discuss with our client and learn that the first interpretation is the desired one. Thus we write:
isNextP(n, p) : <=> n <= p /\ ~(exists n <= q < p: isPrime(q)).
The predicate isNumber is rather trivial and the predicate isNextP in isolation does not describe a very interesting property; thus we insert the corresponding formulas to yield the final specification:
isNextPrime(n, p) : <=> n <= p /\ isPrime(p) /\ ~(exists n <= q < p: isPrime(q)) isPrime(p) : <=> 1 < p /\ forall 1 < n < p: n not | p n | m : <=> exists p: n*p = m.
These predicates can be defined in the Logic Evaluator as follows:
pred <(m, n) <=> and(<=(m, n), not(=(m, n))); pred divides(n, m) <=> exists(p in nat(1, m): =(*(n, p), m)); pred isPrime(p) <=> and(<(1, p), forall(n in nat(2, -(p, 1)): not(divides(n, p)))); pred isNextPrime(n, p) <=> and(<=(n, p), isPrime(p), not(exists(q in nat(n, -(p, 1)): isPrime(q))));
The only difference to the mathematical definitions is that we have to
explicitly restrict the range of the existentially quantified variable
p in the definition of divides
(which is easy, because any
divisor of m is in the range [1...m]).
We can use these definitions to check the validity of input/output pairs:
We will now use the "such" quantifier
which returns a value of term T such that A holds (for some value of x, provided that such an x exists). With the help of this quantifier we can define a functionsuch(x: A, T)
We restrict our search for the next prime to the range [n...2n] applying the mathematical knowledge that between every number and its double there exists at least one prime number. Thus we can simulate a program that satisfies our specification:fun program(n) = such(p in nat(n, *(2, n)): isNextPrime(n, p), p);
Operational Interpretation From the formal specification constructed above, one can already derive a straight-forward program that solves the stated problem. We recall the operational interpretations of formulas introduced in the previous sections and encode every formula (forall a <= x <= b: A) as the following piece of code
boolean forallX = true; for (int x = a; x <= b; x++) { // value of A(x) boolean isTrue = ...; ... if (!isTrueA) { forallX = false; break; } }
Then the variable forallX
is true after the termination of the
loop if and only if the universal formula is true.
Correspondingly, we can encode (exists a <= x <= b: A) as
boolean existsX = false; for (int x = a; x <= b; x++) { // value of A(x) boolean isTrue = ...; ... if (isTrueA) { existsX = true; break; } }
Here the variable existsX
is true after the termination of the loop if
and only if the existential formula is true.
Based on this idea, we implement the predicates as the following Java methods:
// ------------------------------------------------------- // divides(m, n) :<=> (exists p in 1..n: m*p = n) // ------------------------------------------------------- boolean divides(int m, int n) { // exists p in 1..n boolean existsP = false; for (int p = 1; p <= n; p++) { // m*p = n boolean equalsMPN = (m*p == n); if (equalsMPN) { existsP = true; break; } } return existsP; } // ------------------------------------------------------- // isPrime(p) :<=> // 1 < p /\ // (forall n in 2..p-1: ~divides(n, p)) // ------------------------------------------------------- boolean isPrime(int p) { // p > 1 /\ if (p > 1) { // forall n in 2..p-1 boolean forallN = true; for (int n = 2; n <= p-1; n++) { // ~divides(n, p) boolean notDividesNP = !divides(n, p); if (!notDividesNP) { forallN = false; break; } } return forallN; } else return false; } // ------------------------------------------------------- // isNextPrime(n, p) :<=> // n <= p /\ isPrime(p) /\ // ~exists(q in n..p-1: isPrime(q)))); // ------------------------------------------------------- boolean isNextPrime(int n, int p) { // n <= p /\ if (n <= p) { // isPrime(p) /\ if (isPrime(p)) { // ~exists q in nat(n, p-1): boolean existsQ = false; for (int q = n; q <= p-1; q++) { boolean isPrimeQ = isPrime(q); if (isPrimeQ) { existsQ = true; break; } } if (existsQ) return false; else return true; } else return false; } else return false; } // ------------------------------------------------------- // program(n) := such(p in n..2*n: isNextPrime(n, p)) // ------------------------------------------------------- int program(int n) { for (int p = n; p <= 2*n; p++) { if (isNextPrime(n, p)) return p; } return -1; // not reached }
While above program solves the stated problem, a little bit of thinking reveals that we can do this more efficiently. The first prime number found is exactly the wanted "next" prime such that we do not need an extra check for this property. Thus we write:
// ------------------------------------------------------ // program(n) := such(p in n..2*n: isPrime(p)) // ------------------------------------------------------ int program(int n) { for (int p = n; p <= 2*n; p++) { if (isPrime(p)) return p; } return -1; }