[Agda] Defining subtraction for naturals

[Martin Escardo]

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.

(From a logical point of view, if you replace "and" by "plus", then 
implication gets replaced by truncated subtraction. A nice old paper by 
Lawvere on metric spaces is around ideas like this.)

Martin