В
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
if