On 3/17/11 4:22 PM, Martin Escardo wrote:

On 17/03/11 18:35, wren ng thornton wrote:

...

(2) Use saturating subtraction, i.e. if the result would drop below zero then return zero;

This is what people working with quantales do.

Subtraction y-z, when it exists, is the solution in s to the equation s+z =y.

Truncated subtraction y - z is the supremum of the set of solutions s to the inequality s+z <= y, when this supremum exists. (In your example, when z>y, the set of solutions is empty, and the empty set has supremum zero.)

This amounts to saying that the truncated subtraction function (-) - z is the right adjoint to the addition function (-) + z.

So (2) is very natural.

Thanks! That's exactly the kind of thing I was looking for. I'd been needlessly thinking of it as a hack :) -- Live well, ~wren