Guillaume's alternative definition(s) of "com"
Guillaume
On 13 Feb 2013, at 07:33, Guillaume Melquiond wrote:
> Le mardi 12 février 2013 à 19:32 +0000, John Pryce a écrit :
>> On 12 Feb 2013, at 17:43, Guillaume Melquiond wrote:
>>> Is the result of f(x)=1/(2*x) applied to [1,M] bounded or not (from the
>>> point of view of decorations)? I cannot think of a good reason for
>>> forbidding it.
>>
>> Your f as given, and assuming your M is REALMAX, gives
>> 1/(2*[1,M]) = 1/[2,oo] = [0,0.5]
>> which is not a tricky case and can't be what you intended.
>
> The example is as I intended. The issue lies with the intermediate
> interval. The input and output intervals are bounded, and the
> intermediate one too, from a mathematical point of view (but not from an
> implementation point of view, due to limited range).
>
> The decoration mechanism is a combination of the following schemes for
> inputs and output:
> - i1: inputs have to be bounded for com to be generated
> - i2: inputs do not
> - o1: actual output has to be bounded for com to be generated
> - o2: mathematical output has to be bounded for com to be generated
>
> If i1 is in place, the division discards com. If o1 is in place, the
> multiplication discards com. If either is in place, the propagation rule
> prevents the final result from being com. The motion mandates i1+o1,
> which means that the output cannot be com. If the constraints were
> relaxed (i2+o2), then the output would be com. Am I making sense?
Very much making sense, but there's another point, which must have influenced me to put i1+o1 into the current definition. Namely assuming (as you do) the input XX=xx_dx has the standard initial decoration, scheme i1+o1 gives
YY = f(XX) = 1/(2*[1,M]_com) = 1/[2,oo]_dac = [0,0.5]_dac
The dac, together with the bounded input(s), suffices to prove that all the intermediate values, as well as the output, are mathematically bounded, by compactness. (A continuous function on a compact set is bounded.)
I think this was my reason for saying that com should describe what actually happens at Level 2, rather than what ideally happens at Level 1. Namely, I claim that your i2+o2 can never produce more informative results than what such a compactness argument can produce using i1+o1. And that there is no other good reason to move to i2 and/or o2.
It is VERY possible I'm wrong. Can you show that I am?
John