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!

About these ads

Tags: Data.List, Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Injectivity, Logic, Predicate Logic

This entry was posted on March 7, 2012 at 01:10 and is filed under Haskell, Logic, Mathematics. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

5 Responses to “Deciding the injectivity of finite functions”

Rod Carvalho Says:
March 7, 2012 at 12:14 | Reply
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.
Shubhendu Trivedi Says:
March 7, 2012 at 12:38 | Reply
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:
  March 7, 2012 at 12:46 | Reply
  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.
  - Shubhendu Trivedi Says:
    March 7, 2012 at 13:21 | Reply
    Woah. Well. Embarrassingly obvious now that you mention it. But I am glad I asked anyway. Thanks!
Rod Carvalho Says:
March 7, 2012 at 14:07 | Reply
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)]
```

Rod Carvalho

Deciding the injectivity of finite functions

Like this:

5 Responses to “Deciding the injectivity of finite functions”

Leave a Reply Cancel reply

Follow “Rod Carvalho”