
sT s2 тогда и только тогда, когда из того что fs1(x) = true, вытекает, что fs2(x) = true, а и из того, что fs1(x) = false, вытекает, что fs2(x) = false.
Определение. Пусть T1, …, Tn - уточняемые типы. Определим на декартовом произведении T1× … ×Tn отношение уточнения: (x1, …, xn)

T1× ... ×Tn (y1, …, yn) тогда и только тогда, когда x1

T1 y1, …, xn

Tn yn. От функций, определенных на уточняемых типах будет требовать регулярности и полноты: чем определеннее значение аргумента, тем определеннее значение функции, причем полностью определенному значению аргумента соответствует полностью определенное значение функции.
Определение. Функция f: T1 → T2 называется регулярной, если из того, что x

T1 y следует, что f(x)

T2 f(y).
Определение. Функция f: T1 → T2 называется полной, если f(T1с)

T2с, то есть из того, что x

T1c следует, что f(x)

T2c. Обычно в языках программирования и спецификаций есть базовые типы и есть составные типы, значения которых строятся на основе значений других типов.
Определение. Составной тип называется регулярным, если все его конструкторы являются регулярными функциями.
Определение. Составной тип называется полным, если все его конструкторы являются полными функциями.
Содержание Назад Вперед