Третий манифест Кристофера Дейта и Хью Дарвена

       

Формальные определения


Формальные определения

Поскольку этот раздел носит очень формальный характер, Д&Д начинают его с повтора некоторых необходимых определений. Пусть r - отношение, A - имя атрибута r, T - тип атрибута A, v - значение типа T. Тогда:

  • Заголовок Hr отношения r - это множество упорядоченных пар вида <A, T>, по одной такой паре для каждого атрибута A r. По определению никакие две пары в этом множестве не могут содержать одно и то же имя атрибута A.
  • Пусть tr - это кортеж, соответствующий Hr; т.е. tr - это множество упорядоченных кортежей вида <A, T, v> по одному такому кортежу для каждого атрибута A Hr.
  • Тело Br отношения r - это множество таких кортежей tr. Заметим, что в общем случае могут существовать такие кортежи tr, соответствующие Hr, но не появляющиеся в Br.

    Заметим, что заголовок - это множество, тело - это множество, и кортеж - это множество. Элемент заголовка - это упорядоченная пара вида <A, T>; элемент тела - это кортеж; элемент кортежа - это упорядоченный триплет вида <A, T, v>. Любое подмножество заголовка - это заголовок, любое подмножество тела - это тело, и любое подмножество кортежа - это кортеж.

    Теперь можно определить операции. Каждое из определений состоит из (a) формальной спецификации ограничений (если они имеются), применимых к операндам соответствующей операции; (b) формальная спецификация заголовка результата операции; (c) формальную спецификацию тела результата и (d) неформальное обсуждение формальных спецификаций.

  • Пусть s есть >NOT< r.

    Hs = Hr

    Bs = { ts : exists tr ( tr П Br and ts = tr ) }

    Операция >NOT< производит дополнение s заданного отношения r. Заголовком s является заголовок r. Тело s включает все кортежи с этим заголовком, не входящие в тело r.

  • Пусть s есть r >REMOVE< A. Требуется, чтобы существовал некоторый тип T такой, что <A,T> Hr.

    Hs = Hr minus { <A,T> }

    Ds = { ts : exists tr exists v

                ( tr Br and v T and <A,T,V> tr and ts = tr minus { <A,T,v> } ) }




    Операция >REMOVE< производит отношение s, формируемое путем удаления указанного атрибута A из данного отношения r. Операция эквивалентна взятию проекции r на все атрибуты, кроме A. Заголовок s получается вычитанием из заголовка r пары <A,T>. Тело s состоит из таких кортежей, которые соответствуют заголовку и каждый из которых является подмножеством некоторого кортежа r.

  • Пусть s есть r >RENAME< (A, B). Требуется, чтобы существовал некоторый тип T такой, что <A,T> Hr и чтобы не существовал какой-либо тип T такой, что

    <B,T> Hr. Hs = ( Hr minus { <A,T> } ) union { <B,T> } Bs = { ts : exists tr exists v ( tr Br and v T and <A,T,v> tr and ts = ( tr minus { <A,T,v> } ) union { <B,T,v> } )

    Операция >RENAME< производит отношение s, которое отличается отзаданного отношения r только именем одного атрибута, которое изменяется с A на B. Заголовок s такой же, как заголовок r за исключением того, что пара <A,T> заменяется на пару <B,T>. Тело s включает все кортежи тела r, но в каждом из этих кортежей триплет <A,T,v> заменяется на триплет <B,T,v>.

  • Пусть s есть r1 >AND< r2. Требуется, что если <A,T1> Hr1 и <A,T2> Hr2, то должно быть T1 = T2.

    Hs = Hr1 union Hr2 Bs = { ts : exists tr1 exists tr2 ( ( tr1 Br1 and tr2 Br2 ) and ts = tr1 union tr2 ) }

    Операция >AND< является реляционной конъюнкцией, производящей результат, называвшийся ранее в литературе естественным соединением заданных отношений r1 и r2. Заголовок s является объединением заголовков r1 и r2. Тело s состоит из всех кортежей, соответствующих заголовку s и являющихся надмножеством некоторого кортежа из тела r1 и некоторого кортежа из тела r2. Операцию >AND< можно было бы логически назвать conjoin (конъюнктивным соединением).

  • Пусть s есть r1 >OR< r2. Требуется, что если <A,T1> Hr1 и <A,T2> Hr2, то должно быть T1 = T2.

    Hs = Hr1 union Hr2 Bs = { ts : exists tr1 exists tr2 ( ( tr1 Br1 or tr2 Br2 ) and ts = tr1 union tr2 ) }



    Операция >OR< является реляционной дизъюнкцией, являясь обобщением того, что ранее в литературе называлось объединением (в этом частном случае заданные отношения r1 и r2 имеют одинаковые заголовки, и результат s является объединением этих двух отношений в традиционном смысле). Заголовок s есть объединение заголовков r1 и r2. Тело s состоит из всех кортежей, соответствующих заголовку s и являющихся надмножеством либо некоторого кортежа из тела r1, либо некоторого кортежа из тела r2. Операцию >OR< можно было бы логически назвать disjoin (дизъюнктивным соединением).

    Наконец, определим "макро"-операцию >COMPOSE<. Пусть s есть r1 >COMPOSE< r2 (r1 и r2 должны удовлетворять тем же требованиям, что и для >AND<). Пусть общими атрибутами для r1 и r2 являются A1, A2, …, An (n і 0). Тогда s определяется как результат выражения

    ( r1 >AND< r2 ) >REMOVE< An … >REMOVE< A2 >REMOVE< A1

    При n = 0 r1 >COMPOSE< r2 - это то же самое, что r1 >AND< r2, что, в свою очередь, то же самое, что r1 TIMES r2 в алгебре Кодда.



    Содержание раздела