Свободные и связанные переменные кортежей

Каждая ссылка на переменную кортежа (в некотором контексте, в частности в формуле WFF) является или свободной, или связанной. Сначала поясним это утверждение в чисто синтаксических терминах, а затем перейдем к обсуждению его смысла.

Пусть V - переменная кортежа. Тогда имеем следующее.

Ссылки на переменную V в формулах WFF типа NOT р свободны или связаны в пределах этой формулы в зависимости от того, свободны ли они в формуле р. Ссылки на переменную V в формулах WFF типа (р AND q) и (р OR q) свободны или связаны в зависимости от того, свободны ли они в формулах р и q.

Ссылки на переменную V, которые свободны в формуле WFF р, связаны в формулах WFF типа EXISTS V(p) и FORALL V(p). Другие ссылки на переменные кортежей в формуле р будут свободны или связаны в формулах WFF типа EXISTS V{p) и FORALL V(p) в соответствии с тем, свободны ли они в формуле р.

Для полноты необходимо добавить следующие замечания.

Единственная ссылка на переменную V в значении параметра <имя переменной кортежа> является свободной в пределах этого параметра <имя переменной кортежа>.

Единственная ссылка на переменную V в значении параметра <ссылка на атрибут кортежа> V.A является свободной в пределах этого параметра <ссылка на атрибут кортежа>.

Если ссылка на переменную V является свободной в некотором выражении ехр, то эта ссылка будет также свободной в любом выражении ехр непосредственно содержащем выражение ехр как подвыражение, если только в выражении ехр не вводится квантор, связывающий переменную V.

Приведем несколько примеров формул WFF, содержащих переменные кортежей.

Простые сравнения SX.S# = S# ( SI ) SX.Si = SPX.Si SPX.PI Ф PX.Pi

Здесь все ссылки на переменные SX, РХ и SPX являются свободными.

Логические выражения из простых сравнений

РХ.WEIGHT < WEIGHT ( 15.5 ) OR PX.CITY = Rome

NOT ( SX.CITY = London )

SX.SI = SPX.SI AND SPX.Pi Ф PX.Pi

PX.COLOR = COLOR ( Red ) OR PX.CITY = London

Здесь также все ссылки на переменные SX, РХ и SPX являются свободными.

Формулы WFF с кванторами

EXISTS SPX ( SPX.Si = SX.Si AND SPX.Pi = Pi ( P2 ) ) FORALL PX ( PX.COLOR = COLOR ( Red ) )

В этих примерах ссылки на переменные SPX и РХ являются связанными, а ссылка на переменную SX является свободной. Подробнее данные примеры объясняются ниже.

Кванторы

Существует два квантора: EXISTS и FORALL. Квантор EXISTS является квантором существования, а FORALL - квантором всеобщности. По сути, если выражение р - формула WFF, в которой переменная V свободна, то выражения

EXISTS V ( р )

FORALL V ( р )

также являются допустимыми формулами WFF, но переменная V в них обеих будет связанной. Первая формула означает следующее: Существует по крайней мере одно значение переменной V, такое, что вычисление формулы р дает для него значение истина . Вторая формула означает следующее: Для всех значений переменной V вычисление формулы р дает значение истина . Предположим, например, что переменная V изменяется на множестве Члены сената США в 1999 году , и предположим также, что выражение р - следующая формула WFF: V - женщина (разумеется, мы не пытаемся использовать здесь формальный синтаксис). Тогда выражение EXISTS V(p) будет допустимой формулой WFF, имеющей значение истина (true); выражение FORALL V(p) также будет допустимой формулой WFF, но вычисление его значения будет давать значение ложь (false).

Теперь рассмотрим квантор существования EXISTS более внимательно. Еще раз обратимся к примеру из предыдущего раздела.

EXISTS SPX ( SPX.Si = SX.Si AND SPX.Pi = Pi ( P2 ) )

Из приведенных ранее рассуждений следует, что эта формула WFF может быть прочитана следующим образом.

В текущем значении переменной-отношения SP существует кортеж (скажем, SPX), такой, для которого значение атрибута Si в это.м кортеже равно значению атрибута SX. Si (какое бы оно ни было), а значение атрибута Pi в кортеже SPXравно Р2.

Каждая ссылка на переменную SPX в этом примере является связанной. Единственная ссылка на переменную SX свободна.

Формально квантор существования EXISTS определяется как повторение операции OR (ИЛИ). Другими словами, если г - это отнощение с кортежами tl, t2, ... , tm, V - это переменная кортежа, изменяющаяся на данном отнощений, и p{V) - это формула WFF, в которой переменная V используется как свободная переменная, то формула WFF вида

EXISTS V ( р ( V ) )

равносильна следующей формуле WFF. false OR р ( tl ) OR ... OR р ( tm )

В частности, обратите внимание, что если отношение R пустое (т.е. т=0), то результатом вычисления данного выражения будет значение лолсь.

Рассмотрим в качестве примера отношение г, содержащее следующие кортежи.

( 1, 2, 3 ) ( 1, 2, 4 ) ( 1, 3, 4 )

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

EXISTS V ( V.C > 1 ) : true

EXISTS V ( V.B > 3 ) : false

EXISTS V ( V.A > 1 OR V.C = 4 ) : true

Теперь рассмотрим квантор общности FORALL, для чего вернемся к соответствующему примеру из предыдущего раздела.

FORALL РХ ( РХ.COLOR = COLOR ( Red ) )

Эта формула WFF может быть прочитана следующим образом.

В текущем значении переменной-отношения Р для всех кортежей (скажем, РХ) значение их атрибута COLOR равно Red.

Обе ссылки на переменную РХ в этом примере связаны.

Подобно тому, как квантор EXISTS был определен как повторение операции OR, квантор существования FORALL определяется как повторяющаяся операция AND (И). Другими словами, если обозначения г, V и p(V) имеют тот же смысл, что и в приведенном выше определении квантора EXISTS, то формула WFF вида

FORALL V { р ( V ) )

равносильна следующей формуле WFF.

true AND р ( tl ) AND ... AND р ( tm )

В частности, обратите внимание, что если отношение г пустое, то результатом вычисления данного выражения будет значение истина.

В качестве примера рассмотрим отношение R, содержащее те же кортежи, что и в предыдущем примере. Тогда приведенные ниже выражения будут иметь указанные значения.

FORALL V ( V.A > 1 ) : false

FORALL V ( V.B > 1 ) : true

FORALL V ( V.A = 1 AND V.C > 2 ) : true