Кванторы, свободные и связанные переменные
Допускается построение WFF с помощью кванторов существования (EXISTS) и всеобщности (FORALL). Если form – это WFF, в которой участвует переменная var, то конструкции EXISTS var (form) и FORALL var (form) представляют собой WFF. По определению, формула EXISTS var (form) принимает значение true в том и только в том случае, если в области определения переменной var найдется хотя бы одно значение (кортеж), для которого WFF form принимает значение true. Формула FORALL var (form) принимает значение true, если для всех значений переменной var из ее области определения WFF form принимает значение true.
Переменные, входящие в WFF, могут быть свободными или связанными. По определению, все переменные, входящие в WFF, при построении которой не использовались кванторы, являются свободными. Фактически, это означает, что если для какого-то набора значений свободных кортежных переменных при вычислении WFF получено значение true, то эти значения кортежных переменных могут входить в результирующее отношение. Если же имя переменной использовано сразу после квантора при построении WFF вида EXISTS var (form) или FORALL var (form), то в этой WFF и во всех WFF, построенных с ее участием, var является связанной переменной. Это означает, что такая переменная не видна за пределами минимальной WFF, связавшей эту переменную. При вычислении значения такой WFF используется не одно значение связанной переменной, а вся область ее определения.
Пусть здесь и далее в этом разделе СЛУ1 и СЛУ2 представляют собой две кортежные переменные, определенные на отношении СЛУЖАЩИЕ. Тогда WFF
EXISTS СЛУ2 (СЛУ1.СЛУ_ЗАРП > СЛУ2.СЛУ_ЗАРП)
для текущего кортежа переменной СЛУ1 принимает значение true в том и только в том случае, если во всем отношении СЛУЖАЩИЕ найдется такой кортеж (ассоциированный с переменной СЛУ2), чтобы значение его атрибута СЛУ_ЗАРП удовлетворяло внутреннему условию сравнения. Легко видеть, что эта формула принимает значение true только для тех значений кортежной переменной СЛУ1, которые соответствуют служащим, не получающим минимальную зарплату.
Соответствующее множество кортежей показано на рис. 5.2a (для тела отношения СЛУЖАЩИЕ из рис. 5.1).
Рис. 5.2. Примеры правильно построенных формул с кванторами
Правильно построенная формула
FORALL СЛУ2 (СЛУ1.СЛУ_ЗАРП
СЛУ2.СЛУ_ЗАРП)
для текущего кортежа переменной СЛУ1 принимает значение true в том и только в том случае, если для всех кортежей отношения СЛУЖАЩИЕ (связанных с переменной СЛУ2) значения атрибута СЛУ_ЗАРП удовлетворяют условию сравнения. Снова легко видеть, что формула принимает значение true только для тех значений кортежной переменной СЛУ1, которые соответствуют служащим, получающим максимальную зарплату1). Соответствующее множество кортежей показано на рис. 5.2b.
Очевидно, что показанные на рис. 5.2 отношения соответствуют условиям обеих формул. Но как в данном случае можно реализовать систему, которая по заданной формуле производит правильный результат? Наиболее очевидный способ интерпретации обеих обсуждавшихся выше формул следующий. В некотором порядке просматривать область определения свободной кортежной переменной СЛУ1. Для каждого очередного кортежа из области определения СЛУ1 просматривать область определения связанной переменной СЛУ2 до тех пор, пока не будет установлено истинностное значение формулы для данного кортежа СЛУ1 (в случае наличия квантора существования процесс просмотра для СЛУ2 можно остановить после нахождения первого кортежа, для которого значением подформулы, находящейся под знаком квантора, станет true; при наличии квантора всеобщности необходимо просмотреть всю область определения СЛУ2). Заметим, что здесь мы снова получаем два цикла, как и при интерпретации WFF с двумя свободными переменными. Но в данном случае во внешнем цикле обязательно просматривается область определения свободной переменной.
На самом деле, правильнее говорить не о свободных и связанных переменных, а о свободных и связанных вхождениях переменных. Если переменная var является связанной в WFF form, то во всех WFF, включающих form, вне form может использоваться вхождение того же имени переменной var, которое может быть свободным или связанным, но в любом случае не имеет никакого отношения к вхождению переменной var в WFF form.
Вот пример:
EXISTS СЛУ2 (СЛУ1.ПРО_НОМ = СЛУ2.ПРО_НОМ AND СЛУ1.СЛУ_НОМЕР
СЛУ2.СЛУ_НОМЕР) AND FORALL СЛУ2 (IF СЛУ1.ПРО_НОМ = СЛУ2.ПРО_НОМ THEN СЛУ1.СЛУ_ЗАРП = СЛУ2.СЛУ_ЗАРП)
Эта формула принимает значение true только для тех значений переменной СЛУ1, которые соответствуют служащим, участвующим в проектах с более чем одним участником, причем все участники проекта получают одну и ту же зарплату. Здесь мы имеем два связанных вхождения переменной СЛУ2 с совершенно разным смыслом. Грубо говоря, для текущего значения переменной СЛУ1 переменная СЛУ2 два раза "пробежит" свою область определения – первый раз при вычислении части формулы с квантором существования, а второй при вычислении части с квантором всеобщности. Кстати, к тому же результату приведет формула с одним квантором всеобщности вида:
FORALL СЛУ2 (IF (СЛУ1.ПРО_НОМ = СЛУ2.ПРО_НОМ AND СЛУ1.СЛУ_НОМЕР
СЛУ2.СЛУ_НОМЕР) THEN СЛУ1.СЛУ_ЗАРП = СЛУ2.СЛУ_ЗАРП)
Легко заметить, что кванторы можно трактовать как булевские функции (функции, принимающие значения true или false) над множеством значений связанной кортежной переменной. С тем же успехом можно ввести в реляционное исчисление числовые функции над множествами, такие, как MIN (минимальное значение), MAX (максимальное значение), AVG (среднее значение) и т. д.
В этом случае можно было бы написать, например, WFF
СЛУ1.СЛУ_ЗАРП > MIN СЛУ2.СЛУ_ЗАРП (СЛУ1.ПРО_НОМ = СЛУ2.ПРО_НОМ)
в области истинности которой содержатся все кортежи отношения СЛУЖАЩИЕ, соответствующие тем служащим, которые получают заработную плату, превышающую минимальную зарплату служащих, участвующих в том же проекте. Понятно, что для получения результирующего отношения можно интерпретировать формулу таким же образом, как в обсуждавшемся выше случае наличия кванторов.
Содержание Назад Вперед