Monus

Notation

A use of the monus symbol is seen in Dennis Ritchie's PhD Thesis from 1968.

Definition

Let (M, +, 0) be a commutative monoid. Define a binary relation \leq on this monoid as follows: for any two elements a and b, define a \leq b if there exists an element c such that a + c = b. It is easy to check that \leq is reflexive and that it is transitive. M is called naturally ordered if the \leq relation is additionally antisymmetric and hence a partial order. Further, if for each pair of elements a and b, a unique smallest element c_0 exists such that a \leq b + c_0, then M is called a commutative monoid with monus and the monus a \mathbin{\dot{-}} b of any two elements a and b can be defined as this unique smallest element c_0 such that a \leq b + c_0.

An example of a commutative monoid that is not naturally ordered is (\mathbb{Z}, +, 0), the commutative monoid of the integers with usual addition, as for any a, b \in \mathbb{Z} there exists c such that a + c = b, so a \leq b holds for any a, b \in \mathbb{Z}, so \leq is not antisymmetric and therefore not a partial order. There are also examples of monoids that are naturally ordered but are not semirings with monus.

Other structures

Beyond monoids, the notion of monus can be applied to other structures. For instance, a naturally ordered semiring (sometimes called a dioid) is a semiring where the commutative monoid induced by the addition operator is naturally ordered. When this monoid is a commutative monoid with monus, the semiring is called a semiring with monus, or m-semiring.

Examples

If M is an ideal in a Boolean algebra, then M is a commutative monoid with monus under a + b = a \vee b and a \mathbin{\dot{-}} b = a \wedge \neg b .

Natural numbers

The natural numbers including 0 form a commutative monoid with monus, with their ordering being the usual order of natural numbers and the monus operator being a saturating variant of standard subtraction, variously referred to as truncated subtraction, limited subtraction, proper subtraction, doz (difference or zero), and monus. Truncated subtraction is usually defined as :a \mathbin{\dot{-}} b = \begin{cases} 0 & \mbox{if } a a - b & \mbox{if } a \ge b, \end{cases} where − denotes standard subtraction. For example, 5 - 3 = 2 and 3 - 5 = -2 in regular subtraction, whereas in truncated subtraction 3 \mathbin{\dot{-}} 5 = 0. Truncated subtraction may also be defined as :a \mathbin{\dot{-}} b = \max(a - b, 0).

In Peano arithmetic, truncated subtraction is defined in terms of the predecessor function P (the inverse of the successor function): : \begin{align} P(0) &= 0 \ P(S(a)) &= a \ a \mathbin{\dot{-}} 0 &= a \ a \mathbin{\dot{-}} S(b) &= P(a \mathbin{\dot{-}} b). \end{align}

A definition that does not need the predecessor function is: : \begin{align} a \mathbin{\dot{-}} 0 &= a \ 0 \mathbin{\dot{-}} b &= 0 \ S(a) \mathbin{\dot{-}} S(b) &= a \mathbin{\dot{-}} b. \end{align}

Truncated subtraction is useful in contexts such as primitive recursive functions, which are not defined over negative numbers. Truncated subtraction is also used in the definition of the multiset difference operator.

Properties

The class of all commutative monoids with monus form a variety. The equational basis for the variety of all CMMs consists of the axioms for commutative monoids, as well as the following axioms:

\begin{align} a + (b \mathbin{\dot{-}} a) &= b + (a \mathbin{\dot{-}} b),\ (a \mathbin{\dot{-}} b) \mathbin{\dot{-}} c &= a \mathbin{\dot{-}} (b + c),\ (a \mathbin{\dot{-}} a) &= 0,\ (0 \mathbin{\dot{-}} a) &= 0.\ \end{align}

Notes

References

• {{cite journal

• {{cite conference | editor1-last = Wigington | editor1-first = Curtis | editor2-last = Hardy | editor2-first = Matthew | editor3-last = Bagley | editor3-first = Steven R. | editor4-last = Simske | editor4-first = Steven J. | contribution-url = https://www.cs.princeton.edu/~bwk/dmr/doceng22.pdf

• {{cite book |editor-last = Wirsing |editor-first = Martin |editor-last2 = Nivat |editor-first2 = Maurice |chapter-url = https://www.cs.ru.nl/B.Jacobs/PAPERS/AMAST96.ps |chapter-format=PS

• {{cite web

• {{cite web

• {{cite book

• {{cite book

References

1. [[Character (computing). Character]]s in Unicode are referenced in prose via the "U+" notation. The [[hexadecimal]] number after the "U+" is the character's Unicode code point.
2. taking $c$ to be the [[neutral element]] of the monoid
3. if $a\; \backslash leq\; b$ with witness $d$ and $b\; \backslash leq\; c$ with witness $d\text{'}$ then $d\; +\; d\text{'}$ witnesses that $a\; \backslash leq\; c$