Однозначность предикатов. Предикат H(x, y) является однозначным в области X для набора переменных x, если он определяет функцию

Предикат H(x, y) является однозначным в области X для набора переменных x, если он определяет функцию, отображающую значения набора x в значения набора y. Должно быть истинным следующее условие:

"xÎX "y₁,y₂. H(x, y₁) & H(x, y₂) Þ y₁ = y₂.

Отметим, что однозначный предикат в некоторой области X не обязательно является реализуемым в этой области.

Оператор S является однозначным в области X, если формула LS(S)(x, y) однозначна в области X. Нетрудно убедиться, что оператор суперпозиции A; B, параллельный оператор A || B и условный оператор if ( C) A else B являются однозначными, если однозначными являются операторы A и B.

Спецификация оператора S, представленная предусловием P(x) и постусловием Q(x, y), является однозначной, если постусловие является однозначным в области предусловия, т. е.

"x. P(x) Þ "y₁,y₂. (Q(x, y₁) & Q(x, y₂) Þ y₁ = y₂).

Отметим, что однозначная спецификация не обязательно является реализуемой.

Лемма 2.7. Допустим, предикат D(x, y) является однозначным в области X, а предикат Z(x, y) реализуем в области X. Пусть истинна формула Z(x, y) Þ D(x, y). Тогда истинна следующая формула: "xÎX. D(x, y) Þ Z(x, y). Как следствие, предикаты D и Z оказываются тождественными в области X.

Доказательство. Пусть истинно D(x, y) для некоторого xÎX. Докажем истинность Z(x, y). Поскольку предикат Z реализуем, то существует некоторый y’, для которого истинно Z(x, y’). Из Z(x, y) Þ D(x, y) получаем истинность D(x, y’). Поскольку истинны D(x, y) и D(x, y’), то из однозначности D следует y = y’. Тогда истинно Z(x, y). □