## Deciding the injectivity of finite functions

Consider a function $f : \mathcal{X} \to \mathcal{Y}$.  We say that $f$ is a finite function if and only if both $\mathcal{X}$ and $\mathcal{Y}$ are finite sets. As mentioned last week, function $f$ is injective if and only if

$\forall x_1 \forall x_2 \left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

where $x_1$ and $x_2$ range over set $\mathcal{X}$. We now introduce the injectivity predicate $\varphi : \mathcal{X} \times \mathcal{X} \to \{\text{True}, \text{False}\}$, defined by

$\varphi (x_1, x_2) =\left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

so that function $f$ is injective if and only if $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ is true. In this post we will restrict our attention to finite functions, for which it is fairly straightforward to devise a decision procedure to decide injectivity. Let $n := |\mathcal{X}|$ denote the cardinality of set $\mathcal{X}$. Then, determining the truth value of $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ will require a total of $n^2$  evaluations of the predicate $\varphi$.

__________

Example

Let us define $\mathbb{Z}_4 := \{0, 1, 2, 3\}$. Consider the finite function

$\begin{array}{rl} f : \mathbb{Z}_4 &\to \mathbb{Z}_4\\ n &\mapsto 3 n \pmod{4}\end{array}$

where $\pmod{4}$ denotes modulo 4 arithmetic. Is $f$ injective? Note that $f (0) = 0$, $f (1) = 3$, $f (2) = 2$, and $f (3) = 1$. Hence, we easily conclude that $f$ is injective. Suppose that we do not want to enumerate the images of the elements of $\mathbb{Z}_4$ under $f$; in that case, we can use the following Haskell script to decide that $f$ is injective:

-- define function f
f :: Integral a => a -> a
f n = (3 * n) mod 4

-- define disjunction
(\/) :: Bool -> Bool -> Bool
p \/ q = p || q

-- define implication
(==>) :: Bool -> Bool -> Bool
p ==> q = (not p) \/ q

-- define injectivity predicate
phi :: Integral a => (a,a) -> Bool
phi (x1,x2) = (f x1 == f x2) ==> (x1 == x2)

where we used the fact that $p \implies q$ is semantically equivalent to $\neg p \lor q$. Let us carry out some testing:

*Main> -- test function f
*Main> [ f n | n <- [0..3]]
[0,3,2,1]
*Main> -- test disjunction
*Main> [ p \/ q | p <-[True, False], q <- [True, False]]
[True,True,True,False]
*Main> -- test implication
*Main> [ p ==> q | p <-[True, False], q <- [True, False]]
[True,False,True,True]

So far, so good. Finally, we can determine the truth value of the sentence $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ using function all, as follows:

*Main> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
True

which allows us to conclude that $f$ is injective.

An alternative procedure would be to use function nub from library Data.List to remove duplicates from a given list. Note that $f$ is injective if and only if the list of the images of the elements of $\mathbb{Z}_4$ under $f$ contains no duplicates. Hence, we obtain:

*Main> let images = [ f n | n <- [0..3]]
*Main> import Data.List
*Main Data.List> length (nub images) == length images
True

What a hack! This second procedure might seem much terser than the first one. But if we do away with type declarations and refrain from re-defining disjunction and defining implication, the first procedure can be made quite succinct as well:

Prelude> let f n = (3 * n) mod 4
Prelude> let phi (x1,x2) = not (f x1 == f x2) || (x1 == x2)
Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
True

which includes the definition of function $f$. Three lines only! Three!

### 5 Responses to “Deciding the injectivity of finite functions”

1. Rod Carvalho Says:

Using anonymous functions, we can decide injectivity as follows:

Prelude> let f n = (3 * n) mod 4
Prelude> let pairs = [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
Prelude> all (\(x1,x2)-> (f x1 /= f x2) || (x1 == x2)) pairs
True


which could be compressed into one line of code if we also made $f$ anonymous.

2. Shubhendu Trivedi Says:

Rod,
Nice set of posts. I have a minor unrelated question – How do you get code with a grey background like in this blog-post? I haven’t posted code in a long time, the last time I did so it was colourful and ugly. This is pretty elegant.

• Rod Carvalho Says:

I use preformatted text. The following HTML code:

<pre style="padding-left: 30px; background: #EEEEEE;">
f :: Integral a => a -> a
f n = (3 * n) mod 4
</pre>


will then look like this:

f :: Integral a => a -> a
f n = (3 * n) mod 4


If you want a white background instead, then just replace #EEEEEE with #FFFFFF.

3. Rod Carvalho Says:

Consider now the following finite function

$\begin{array}{rl} g : \mathbb{Z}_4 &\to \mathbb{Z}_4\\ n &\mapsto 2 n \pmod{4}\end{array}$

Note that $g (0) = g (2) = 0$ and $g (1) = g (3) = 2$. Hence, function $g$ is not injective. We can arrive at the same conclusion using the Haskell code:

Prelude> let g n = (2 * n) mod 4
Prelude> let phi (x1,x2) = (g x1 /= g x2) || (x1 == x2)
Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
False


And we can easily find the pairs $(x_1, x_2)$ for which the predicate $\varphi$ is false:


Prelude> filter (not . phi) [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
[(0,2),(1,3),(2,0),(3,1)]


Note that pairs $(0,2)$ and $(2,0)$ evaluate to the same value. Moreover, it does not make sense to evaluate pairs of the form $(x,x)$. Hence, instead of $n^2$ evaluations of the predicate $\varphi$, we should have only $n(n-1) / 2$ evaluations. A more efficient decision procedure would be:


Prelude> let g n = (2 * n) mod 4
Prelude> let phi (x1,x2) = (g x1 /= g x2) || (x1 == x2)
Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [(x1+1)..3]]
False


We can now find the pairs for which the predicate is false:


Prelude> filter (not . phi) [(x1,x2) | x1 <- [0..3], x2 <- [(x1+1)..3]]
[(0,2),(1,3)]


Note that the set of pairs now contains only 6 elements:


Prelude> [(x1,x2) | x1 <- [0..3], x2 <- [(x1+1)..3]]
[(0,1),(0,2),(0,3),(1,2),(1,3),(2,3)]