SeptiM: Кстати, я осознал свою ошибку. Спасибо, что ещё раз напомнили мне выражение для предела. Там же надо брать , а я считал только само , да к тому же ещё и не правильно. Если считать корректно, то получается именно то, что нужно.
Хоар рассматривает только частный случай для рекурсивного определения процесса . Но есть более общая теория семантических доменов (например, math.nsc.ru/~asm256/lambda/LambdaSep2014.pdf), и я пытаюсь понять, хорошо ли оно всё согласовано. В моём примере X(i) - это функция, которая определяет процесс по индексу, а не собственно сам процесс. Хоар использовал в построениях возрастающие ω-цепи, но, вроде как, можно обойтись всего лишь определением полного чум.
Вы правы, но это, кажется, в данном вопросе не принципиально. Можно сделать ситуацию менее симметричной и более интересной, заменим left -> X(0) на left -> beep ->X(0), чтобы оно ещё и бибикало.
Написано
Войдите на сайт
Чтобы задать вопрос и получить на него квалифицированный ответ.
