this paragraph
safety properties become compositional only when the functions involved are themselves safety‑preserving.
We're talking about the safety of operations, i.e. “the functions involved.” The composition property described in the text posits safety-preserving operations.
In other words, from the fact that a safety property p holds for f(x) and for g(x), nothing follows about p(f(g(x))) unless f and g each preserve p.
Surely these two statements are equivalent for a safety property p:
- for any x, p holds for f(x)
- f preserves p
I added “for any x” but that is implicit in all of the text in the definitions, if you read them. If your quibble depends on the distinction between “for any x” and some specific x, then I think you're confused either about what's written in the document, or some of the fancy language in those papers you cite.
If you drop “for any x,” we must interpret your premise “a safety property p holds for f(x) and for g(x)” as applying to some specific x. In that case, f(g(x)) may not even make any sense (because of type—or if you are positing some kind of untyped calculus, precondition—violations). But if it did make sense, its upholding of p would obviously not follow because it's likely that g(x) ≠ x and we only have an assertion about the safety of f(x). But then the functional composition operation g•f is not what we're talking about here! The operations are composed by sequencing, and I claim the composition f(x); g(x) does uphold p. If I am wrong, a single counterexample would suffice to show it.
this paragraph
We're talking about the safety of operations, i.e. “the functions involved.” The composition property described in the text posits safety-preserving operations.
Surely these two statements are equivalent for a safety property p:
I added “for any x” but that is implicit in all of the text in the definitions, if you read them. If your quibble depends on the distinction between “for any x” and some specific x, then I think you're confused either about what's written in the document, or some of the fancy language in those papers you cite.
If you drop “for any x,” we must interpret your premise “a safety property p holds for f(x) and for g(x)” as applying to some specific x. In that case, f(g(x)) may not even make any sense (because of type—or if you are positing some kind of untyped calculus, precondition—violations). But if it did make sense, its upholding of p would obviously not follow because it's likely that g(x) ≠ x and we only have an assertion about the safety of f(x). But then the functional composition operation g•f is not what we're talking about here! The operations are composed by sequencing, and I claim the composition f(x); g(x) does uphold p. If I am wrong, a single counterexample would suffice to show it.