ГОСТ Р ИСО/МЭК 10746-3-2001
Правила подтипов дают в виде правил вывода суждений, похожих на программу в Прологе. Суждения имеют вид Г |— а < в, где Г — множество предложений об образовании подтипа для переменных типа в виде {tj < Sj, ... , tn < sn}. Типичное правило может иметь следующий вид:
Г |— aj < Pj, Г |— а2 < Р2 = > Г |— а < р.
Неформально это означает, что для того, чтобы определить, имеет ли место Г |— a < р, следует определить, имеют ли место Г |— aj < Pj и Г |— a 2 < P2. Если эти цели достигнуты, то можно сделать вывод, что а является подтипом р.
|
(Е. 1) |
|
а = а |
|
|
(Е. 2) |
|
а = р = > р = а |
|
|
(Е. З) |
|
a = р , р = у = > a = > у |
|
|
(Е. 4) |
|
aj = a2 , р = р2 = > aj ^ р1 = а2 ^ р1 |
|
|
(Е. 5) |
|
а = р = > р t . а = р t . р |
|
|
(Е. 6) |
|
Vje{1, ... , n}, aj = р = > aj х . . . х an = Pj х . . . х рп |
|
|
(Е. 7) |
Vje{1, .. |
, n}, aj = р] = > < aj : aj , . . . , ап : an > = < aj : Pj , . . . |
, an : рп > |
|
(Е. 8) |
Vje{1, . |
. , n}, Oj = р] = > [ aj : aj , . . . , Kn : an ] = [aj : Pj , . . . |
, a n : рп ] |
|
(Е. 9) |
|
р t . t = ± |
|
|
(Е. 10) |
|
a [pt . a/t ] = pt . a |
|
|
(Е. 11) |
|
a[ р1 /t] = PJ , a [ р2/t ] = р2 a i t = > Pj = р2 |
|
Рисунок А.2 — Правила равенства типов
Правила подтипов приведены на рисунке А.З. Можно сказать, что а является подтипом р, если 0 |— a < р может быть выведено с помощью правил подтипов и правил равенства.
А.2.2 Определения типов
Элементы множества Type определяются множеством уравнений взаимозависимости, смоделированным как строго построенная среда. Среда является конечным отображением между переменными типов и типами, относящимися к Т, где Т — нерекурсивное подмножество Type. Строго построенная среда у является такой средой, что свободные переменные типа а, связанные с переменной t в области у, все относятся к области у. Интуитивно ясно,
|
(S.1) |
|
a = р = > Г |— a < р |
|
(S.2) |
|
Г |— a < р , Г |— р < у = > Г |— a < у , |
|
(S.3) |
|
t < s e Г = > Г |— t < s |
|
(S.4) |
|
Г |— 1 < a |
|
(S.5) |
|
Г |— < a T |
|
(S.6) |
|
Г |— a2 < a2 , Г |— PJ < р2 = > Г |— aj ^ р1 < a2 ^ р2 < |
|
(S.7) |
Vje{1, ... |
, n}, Г |— aj < р = > Г — <aj : aj , . . . , am : am > < < a j : Pj , . . . , ап : рп >
для n < m |
|
(S.8) |
Vje{1, . |
. , n}, Г |— aj < р] = > Г — [a j : aj , . . . , an : an ] < [ a j : |3j , . . . , an : рп ]
для n < m |
|
(S.9) |
|
Vje{1, ... , n}, Г — aj < Pj = > Г — ai х . . . х an < Pj х . . . х рп |
|
(S.10) |
|
Г v {t < s } |— a < р = > Г |— pt . a < ps . р для t только в a ; s только в р ; t, s не в Г |
|
|
Рисунок А.З — Правила подтипов |
48