sublanguage. It is shown in that paper that, when restricting to L
x
, P
x
and P
2
are equivalent for success and finite failure. For the transformation to be cor-
rect it cannot also preserve equivalence for ground failure. Consideration of the
program
A — Β
Β — Β
and its result under the transformation shows that none of the other equiv-
alences we have considered apply to P
x
and P
2
. •
EXAMPLE 6
Finally, consider a transformation system like that of Tamaki and Sato [1986]
(and also related to the transformation system in Tamaki and Sato [1984]) but
somewhat weaker ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month, and much more.