Help on writing symbols
symbol write
/\
\/
¬ !
F FF
T TT
==>
<==
<=>
-->
<->
AA
EE
<=
>=
!=
+ +
-
xy x y
x+1
y
(x+1)/y

Array and Quantifiers

The most important data structure in programming is an array. It is like a row of boxes numbered consecutively. The ordering numbers of the boxes are called indices. Here is an array of characters with indices in the range [0, 5]:

We will, however, work on arrays of numbers. Here is an example:

It is often necessary to express complicated things about arrays. It is possible with quantifiers:

symbol read write as
for all AA
there exists EE

Here are some examples on an array A whose indices are in the range [0, n − 1]:

Every element is 1:
i; 0 ≤ i < n: A[i] = 1
It is sorted in increasing order:
i; 0 ≤ i < n − 1: A[i] ≤ A[i + 1]
Some element occurs at least twice:
i: ∃ j; 0 ≤ i < j < n: A[i] = A[ j]
The smallest element is unique:
i; 0 ≤ i < n: ∀ j; 0 ≤ j < nij: A[i] < A[ j]

Express the following claims on an array A whose indices are in the range [0, n − 1].

Every element is less than 2.

The array contains at least one element with value zero.

The first element is bigger than the others.

The last element is not the smallest element of the array A.

The array is sorted in decreasing order.

The array is a palindrome (reads the same forwards and backwards).
Because of a technical limitation of the current version of the tool, it is not allowed to use other operations than + and − in value ranges of quantified variables.

The claims in the following section need at least two quantors.

The array contains at least two distinct elements.

The array contains exactly one element with value zero.

A smallest element in the array is 2.

Every element of the array occurs at least twice.

Some element in the array occurs only once.

Every element in the array occurs at most twice.

For a given k the array is in increasing order up to index k (which must exist), and from then on in decreasing order.

Express the following claims as briefly as you can. It may require a lot of thinking! You may proceed in steps.

Try the following filled-in example as such. It first says that some element is bigger than all elements:
i; 0 ≤ i < n: ∀ j; 0 ≤ j < n: A[i] > A[ j]
However, we can reason that if that “some element” is bigger than all elements, then it is bigger than itself, which is impossible. Therefore, this claim is actually logically equivalent to false. The part
F
says that what was claimed before it, is equivalent to false.

Now remove <=> FF from the above and try again, to see a message telling that your answer is mathematically correct but not as brief as wanted.

Now you try!

Some element in the array is at least as big as all elements. help1 The biggest element is at least as big as all elements, including itself. help 2 You can use the variable n also in other ways than used this far.

All elements in the array are equal.

Every element in the array is bigger than some other element.

The array is sorted in strictly decreasing order.

A prefix of at least size 2 is sorted in increasing order.

A prefix of at least size ⌊n/2⌋ is sorted in strictly increasing order.
Because of a technical limitation of the current version of the tool, it is not allowed to use other operations than + and − in value ranges of quantified variables. help For integer division you have to use div instead of /.


back