Ordered monoid with partial subtraction: Is there a name for this?

Question

I've come across the following structure as being useful to represent various kinds of resources (e.g., fungible things like money, nonfungible things like deeds, etc.), and I was curious if there's a name for this structure already/hopefully there is some part of a book or paper that discusses these objects.

Def: A resource $\mathcal{R}$ is a tuple $(R, +, 0, \leq, -)$ where

1. $(R, +, 0, \leq)$ is an ordered monoid.
2. $- : R \times R \to R$ is a partial function so that for any $x,y \in R$ such that $y \leq x$, we have $(x - y) + y = x$.

For example:

1. The natural numbers with the standard operations is a resource $(\mathbb{N}, +, 0, \leq, -)$.
2. For any set $A$, we can build the resource $(\mathcal{P}(A), \cup, \emptyset, \subseteq, \setminus)$, where $X \setminus Y$ is the set difference operation.
3. The set of strings on an alphabet $\Sigma$ can be made into a "prefix resource" $(\Sigma^*, \epsilon, \cdot, \leq_p, -_p)$ or a "suffix resource" $(\Sigma^*, \epsilon, \cdot, \leq_s, -_s)$, where $\cdot$ is concatenation, $x \leq_p y$ if $x$ is a prefix of $y$ and similarly $x \leq_s y$ if $x$ is a suffix of $y$. The functions $-_p$ and $-_s$ are defined so $(x \cdot y) -_p x = y$ and $(x \cdot y) -_s y = x$. \end{enumerate}

Answer 1

Your additive notation may suggest that you are considering commutative monoids, but your example 3 is not commutative. Thus I will not assume commutativity, but I will switch to a multiplicative notation.

Let $M$ be an ordered monoid. Your condition 2 can be rephrased as follows:

(2') if $y \leqslant x$, then $x \leqslant_{\cal L} y$,

where the $\leqslant_{\cal L}$ preorder is defined as follows: $x \leqslant_{\cal L} y$ if and only if there exists $z \in M$ such that $zy = x$. It gives rise to the Green's relation $\cal L$.

I don't think there is a specific name for this property. However, you might be interested in a related property. The maximal $z$ such that $zy \leqslant x$, if it exists, is called the left residual of $x$ by $y$. A monoid is left residuated if the left residual exists for any pair $x,y$ such that $y \leqslant x$.