RE: Motion 42 (not 41): Decoration system, revised text
Jurgen Wolff von Gudenberg wrote:
> Nate, John
> I wanted to come to a common agreement how to choose decorations on
> intersect and convexhull, in order to be able to propagate decoratoins
> for piecewise defined functions.
I wish for this too.
> The recommendation, however, was faulty.
> Let me try again.
> (rule 1)
> dec (a_da intersect b_db) = if (a disjoint b) then emp else min(da,db)
> (rule 2)
> dec (a_da convex_hull b_db) = if (a empty or b empty) then max(da,db)
> else min(da,db)
>
...
> intersectionDec(xdx, ydy) is as intersection(xdx, ydy), except that it
> decorates the result with min(dx, dy).
> <<<<<<<<<<<<
> this produces Empty_dac, unless one specfies that use of newDec is
> mandatory. IMO rule 1 is easier.
> <<<<<<<<<<<
We should be careful: if one uses newDec it may be possible to lose a def or
gap decoration from dx or dy... that could be rather serious. So, I would
suggest rule 1 would be required.
But then, it seems the behavior of the EIN decoration is attempted to be
specified by these rules without actually defining the EIN decoration?
For me, this is still a subtle form of contradiction: Empty_dac is a
contradiction by Motion 42, but the rules are designed to circumvent this
and make the decoration system behave as if it is not a contradiction.
We should also consider: underlying inconsistencies that remain in the
decoration system may not be circumvented when cases not anticipated by the
rules are encountered, and this may not give correct results.
For example, what if the emp decoration truly represents an empty result
obtained by evaluating a real function on a nonempty interval that is
outside the function's natural domain? Rule 2 does not anticipate this case,
and the convex hull operation may therefore return a nonempty result with a
"good" decoration (dac or def), depending on the other operand. This seems a
potentially very serious error to me.
On the other hand, if there is an EIN decoration the following things occur:
-- no rules that contradict (even subtly) the actual specification
of the underlying decoration system as a whole are needed, e. g., Empty_DAC
would no longer be a contradiction that requires rules to circumvent in
first place
-- convex hull would give correct results even in the case when
application of rule 2 to Motion 42 fails
Nate