[Agda] Defining subtraction for naturals

[wren ng thornton]

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