1

I've never seen before the following function definition.

Image taken from Ch. 2 of the book "Principles of Eventual Consistency"

What does it try to convey in this specific form and how does it differ from the commonly used notation?

(The book is freely accesible from https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/final-printversion-10-5-14.pdf)

Curious
  • 11
  • Be careful. The author is defining a partial function, not a function. Partial functions don't have to be defined on every point in the domain. – John Douma Mar 10 '21 at 19:47

1 Answers1

1

I’ve not seen the notation before, but it appears that:

  • $(A\to B)$ is the set of all functions from $A$ to $B$;
  • $(A\rightharpoonup B)$ is the set of partial functions from $A$ to $B$, i.e., the set of all functions whose domains are subsets of $A$ and whose ranges are subsets of $B$; and
  • $(A\times B)$ is the set of all relations from $A$ to $B$, so that it is simply $\wp(A\times B)$.

Thus, $(A\to B)\subseteq(A\rightharpoonup B)\subseteq(A\times B)$: every function from $A$ to $B$ is a partial function, and every partial function is a relation.

Finally, if $f:A\rightharpoonup B$ is a partial function (and I’m including the possibility that $f$ is a total function, i.e., with domain all of $A$), $a\in A$, and $b\in B$, we can define a new function $f[a\mapsto b]$ whose domain is $\{a\}\cup\operatorname{dom}(f)$:

$$f[a\mapsto b](x)=\begin{cases} b,&\text{if }a=b\\ f(x),&\text{otherwise.} \end{cases}$$

This function sends $a$ to $b$ but otherwise acts exactly as $f$ does.

Brian M. Scott
  • 616,228