Кванторы и запись утверждений о массивах

Квантор существования. Пусть m и n – выражения с целочисленными значениями (m  n). Рассмотрим предикат P_m or P _m + 1 or ... or P_n  1, (4.1)

где каждое P_i – предикат. Предикат (4.1) истинен, если истинно хотя бы одно из P_i. Предикат (4.1) можно записать в другой форме, использующей квантор существования : ( i: m  i < n: P_i). (4.2)

Здесь i называется квантифицированной переменной, а нер-во m  i < n задает область её значений. На естественном языке (4.2) читается следующим образом: существует по крайней мере одно (целое) значение i, лежащее между m и n  1 (включительно), для которого выполнено утверждение P_i.

Используемые в математике способы записи сумм и произведений тоже могут рассматриваться как кванторы:

Их иногда записывают в форме

что совсем близко к виду (4.2). Далее там, где удобно, будем записывать их в виде

(  i: m  i < n:   a_i), (  i: m  i < n:   a_i).

Формально квантор существования  можно определить рекурсивно следующим образом.

Определение :

1) для n = m : ( i: m  i < m:  P_i) = false,

2)для n = k + 1 > m: ( i: m  i < k + 1:  P_i) = ( i: m  i < k:  P_i) or P_k. Квантор всеобщности. Содержательно определим квантор всеобщности  (читается: «для всех») как

( i: m  i < n: P_i) = P_m & P _m + 1 & ... & P_n  1.

Формально можно либо дать рекурсивное определение, аналогичное определению квантора , либо определить квантор всеобщности через квантор , подчеркивая тот факт, что с формальной точки зрения лишь один из этих кванторов является новым понятием. Действительно, используя законы отрицания и де Моргана, получаем

P_m & P _m + 1 & ... & P_n  1 = not not (P_m & P _m + 1 & ... & P_n  1 ) =

= not (not P_m or not P _m + 1 or ... or not P_n  1) = not ( i: m  i < n:  not P_i),

что дает возможность определить квантор  через квантор .

Определение : ( i: m  i < n: P_i) = not ( i: m  i < n:  not P_i).

Из этого опред следует, что( i: m  i < m:  P_i) =  =not ( i: m  i < m:  not P_i) = not false = true.

Квантор количества (счёта). Для количества различных значений i из области m  i < n, при которых истинно P_i, удобно иметь специальное обозначение ( i: m  i < n:  P_i) .

Дадим формальное определение (по существу, это определение некоторой индуктивной ф-ции).

Определение :

1) для n = m : ( i: m  i < m:  P_i) = 0,

2) для n = k +1 > m: (i: m  i < k + 1: P_i)=

= ( i: m  i < k: P_i)+(if P_k then 1 else 0).

Заметим, что кванторы существования и всеобщности можно выразить через квантор количества:

( i: m  i < n:  P_i) = ( ( i: m  i < n :  P_i)  1),

( i: m  i < n:  P_i) = ( ( i: m  i < n :  P_i) = n  m).

В качестве примера использования квантора количества приведем ситуацию, когда нужно записать утверждение о том, что k  второе по величине из чисел, для которых выполняется P_k (из ряда возможных P₀, P₁, ...). Если бы требовалось найти наименьшее k, при котором истинно P_k, то это можно было бы выразить таким образом: (k  0) & ( i: 0  i < k:  not P_i) & P_k.

Утверждение о втором по величине k выглядит уже более громоздко:

(k  0) & (0  j < k) & ( i: 0  i < j:  not P_i) & P_j &  ( i: j + 1  i < k:  not P_i) & P_k,

не говоря уже об утверждениях относительно третьего и следующих по величине k. С помощью квантора счёта все эти утверждения можно записать лаконичнее и яснее:

для первого k:  ( ( i: 0  i < k :  P_i) = 0 ) & P_k,

для второго k:  ( ( i: 0  i < k :  P_i) = 1 ) & P_k,  ...

для -го по величине k: ( ( i: 0  i < k :  P_i) =   1 ) & P_k.

Замечание 1. Можно доопредилить введенные кванторы на тот случай, когда область значений квантифицированной переменной включает правую границу n, например:

( i: m  i  n:  P_i) = ( i: m  i < n + 1:  P_i).

Замечание 2. Кванторы с прилегающими друг к другу областями можно соединять следующим образом:

( i: m  i < n:  P_i) or ( i: n  i < q:  P_i) = ( i: m  i < q:  P_i) ,

( i: m  i < n:  P_i) & ( i: n  i < q:  P_i) = ( i: m  i < q:  P_i) ,

( i: m  i < n:  P_i) + ( i: n  i < q:  P_i) = ( i: m  i < q:  P_i) .

Рассмотрим примеры записи утверждений о массивах с помощью кванторов. Пусть имеется массив a[1..n] и целые переменные j и k, такие, что 1  j  k + 1  n + 1. Запись a[j..k] обозначает отрезок (или сегмент) массива. Первый элемент этого сегмента есть a[j], а последний  a[k]. При j = k + 1 сегмент пуст. В каждом приведенном ниже примере даны содержательная и формальная формулировки утверждения:

1)все элементы a[j..k]нулевые: ( i: j  i < k + 1:  a[i] = 0)

2) все элементы a[j..k]  ненулевые: ( i: j  i < k + 1:  a[i]  0), или not ( i: j  i < k + 1:  a[i] = 0); 3) значения элементов a[j..k] расположены в возрастающем порядке: ( i: j  i < k:  a[i] < a[i + 1]);

4) любой элемент a[1..j] меньше y, а любой элемент a[j+1..n] больше y: (0  j  n) & ( i: 1  i < j + 1:  a[i] < y) & ( i: j + 1  i < n + 1:  a[i] > y);

5) значение y встречается в массивах b[1..n] и c[1..m] одинаковое число раз: ( i: 1  i  n:  b[i] = y) = ( i: 1  i  m:  c[i] = y).

Сокращения. В некоторых случаях удобно использовать сокращенную запись утверждений о массивах, например:



Предикат Сокращение



( i: 1  i < j + 1:  a[i] < y)  a[1..j] < y

( i: j  i < k + 1:  a[i] = 0) a[j..k] = 0

( i: j  i < k + 1:  a[i] = y) y  a[j..k]

Картинки массивов. Многие часто встречающиеся утверждения о массивах легче понять, если представить их в форме так называемых картинок. При этом важно, что каждую картинку можно при необходимости заменить на эквивалентный ей предикат. Например, картинка

	1	j k	n
a:	?	= 0	?	& (1  j  k + 1  n + 1)

Эквивалентна предикату (1  j  k + 1  n + 1) & ( i: j  i < k + 1:  a[i] = 0) , а картинка

	1 j	n
a:	< y	> y	& (0  j  n )

эквивалентна предикату

(0  j  n ) & ( i: 1  i < j + 1:  a[i] < y) & ( i: j + 1  i < n + 1:  a[i] > y).

Билет№28 Правила вывода для операторов цикла с парпаметром и верификаця программ с одномерными массивами №28