Условные выражения - часть 2

В соответствии с этим для вычисления значения условных выражении применяются следующие правила текстовых замен:

В

 В' => if В then Е else Е' fi  if В' then Е else Е' fi

if true then Е else Е' fi

 Е

if false then Е else Е' fi

 Е'

Эти правила вычисления делают особенно ясным, что условие всегда вычисляется до вычисления ветвей. Это очень существенно, так как возможно, что вычисление одной из ветвей условного выражения не завершится. Так что если бы вычисление этой ветви начиналось сразу, то вычисление условного выражения не завершилось бы. хотя условие направило бы вычисления как раз но другой ветви, которая может привести и к завершающемуся вычислению. Отсюда становится ясным, почему необходимо введение условных ПТЗ.

Заметим, что условное выражение в определенной степени соответствует нестрогому

отображению: даже в том случае, когда выражение в одной из ветвей интерпретируется к

, значение условного выражения может быть отлично от.

Семантика условных выражений описывается также достаточно точно с помощью следующих равенств:

if true then E else E' fi = E

if false then E else E' fi = E'

if В then E else E' fi = if

B then E' else E fi

if

 then E else E' fi =

Содержание  Назад  Вперед

---

---

---