Using your Head is Permitted

January 2008 solution

If xy equals z then it should be possible to prove this equality. Such a proof may be provided by a sequence of tuples such as the following:

etc., until

This constitutes a proof if the first tuple is (1,0), the last tuple is (z,y), and each tuple is related to the next tuple by a multiplication of the first part by x and incrementing the second part by 1.

Unfortunately, QCPL doesn't support sequences or tuples. Therefore, we will need to represent a tuple of naturals as a natural and a series of naturals as a natural.

Representing a tuple of naturals as a natural can be done as follows: the tuple (a,b) can be represented as a*m+b. This works if we can guarantee that m is greater than any b we may wish to encode. Because we won't need to put anything larger than y on the right hand side of our tuples, any m larger than y will do.

A useful QCPL function for packing and unpacking tuples is DIVMOD.

DIVMOD(n,m,a,b): LT(b,m)&(n=m*a+b)

The function LT is true if and only if b<m. It, and the other useful comparators, can be defined as follows:

LE(a,b): Ex, a+x=b
GE(a,b): LE(b,a)
LT(a,b): !GE(a,b)
GT(a,b): !LE(a,b)
NE(a,b): !(a=b)

Representing a sequence, a0 through ay, can be done by selecting a base, n, and taking the sum of niai for all i between 0 and y. This works for any n larger than the maximum expected ai value, which, in our case, can be anything at least as large as (z+1)*(y+1). (NB - This packing method is a bit simplistic, as it doesn't work well if we have trailing zero values in the sequence. It's always possible to just add one to every element to solve this problem, but for our current purposes this was deemed unnecessary.)

To unpack a single element of a sequence, we can use the following function.

ELEMENT(a,n,v,x): Er,Ey,Eq,DIVMOD(a,v,r,y)&DIVMOD(r,n,q,x)

Using this function with ni as the value of v will give the element ai of the sequence packed into the natural a.

This, however, seems to return us back to where we started: now we need to be able to verify that a number is a power of n. In fact, this is a much simpler problem than the original one, and that for two reasons:

  1. We don't need to specify the exponent.
  2. We can choose an n convenient for us.
In particular, it turns out to be very easy to verify this when n is a prime, p. In QCPL, this is done as follows:

PRIMEPOWER(p,x): (x=1)|Aa,Ab,(!(a*b=x))|(!PRIME(a))|(p=a)

This definition uses the definition for PRIME given in the question. In words, it says (with a few simplifications) that if x is a prime power of p then p is its only prime divisor.

So, armed with all this, we can verify the three conditions required of a natural (representing a sequence of tuples) to be our proof. First, it must begin with (1,0). Letting a be the "proof" sequence, p be the prime used for decoding it and m be the modulo for decoding tuples inside it, this condition can be stated as

CONDITION_ONE(a,p,m): Er,DIVMOD(a,p,r,m)

Second, the sequence must end with (z,y).

CONDITION_TWO(a,p,m,z,y): Ev,Er,En,PRIMEPOWER(p,v) & DIVMOD(a,v,n,r) & DIVMOD(n,m,z,y)

(We don't use the function ELEMENT here, because this allows us to easily verify, as part of the extraction, that this is, indeed, the last element in the sequence. For all elements other than the last, the z value that satisfies the condition is greater than p.)

Third, each element in the sequence (except the last) must be related to the next element by multiplication of the left part of the tuple by x and incrementing the right part by one.

GT(v*p,a) | /* ignoring the last element of a */
(Ed,Ee,Eq,Er,Es,Et, ELEMENT(a,p,v,d) & ELEMENT(a,p,v*p,e) & DIVMOD(d,m,q,r) & DIVMOD(e,m,s,t) & (q*x=s) & (r+1=t))

With these three conditions, we can now formulate our main function.

(!((x=0)&(y=0))) & /* avoiding 0^0 */
Ea, /* a is our "proof" sequence */
Ep, /* p is the prime used in decoding a */
Em, /* m is used in decoding tuples within a */
GT(m,y) & PRIME(p) & GT(p,m*(z+1)) & CONDITION_ONE(a,p,m) & CONDITION_TWO(a,p,m,z,y) & CONDITION_THREE(a,p,m,x)

Here are some asides you may find interesting regarding this month's riddle:

Back to riddle

Back to main page