Injectivity | Rod Carvalho

Posts Tagged ‘Injectivity’

Deciding the bijectivity of finite functions

March 31, 2012

Consider a function $f : \mathcal{X} \to \mathcal{Y}$ . Function $f$ is bijective if and only if it is both injective and surjective. We say that $f$ is a finite function if and only if both $\mathcal{X}$ and $\mathcal{Y}$ are finite sets.

In this post, we will restrict our attention to finite functions. For finite functions, we already know how to decide injectivity and surjectivity. Hence, deciding the bijectivity of finite functions is now trivial. In Haskell, we create the following three predicates:

isInjective :: (Eq a, Eq b) => (a -> b) -> [a] -> Bool
isInjective f xs = all phi [(x1,x2) | x1 <- xs, x2 <- xs]
                   where phi (x1,x2) = (f x1 /= f x2) || (x1 == x2)

isSurjective :: Eq b => (a -> b) -> [a] -> [b] -> Bool
isSurjective f xs ys = all psi ys
                       where psi y = or [(f x == y) | x <- xs]

isBijective :: (Eq a, Eq b) => (a -> b) -> [a] -> [b] -> Bool
isBijective f xs ys = (isInjective f xs) && (isSurjective f xs ys)

Note that predicate isInjective takes as inputs a function and a list (the domain), whereas predicate isSurjective takes as inputs a function and two lists (the domain and the codomain). Both return either True or False. Predicate isBijective is defined using the conjunction of the other two predicates. In this implementation, we separated the decision procedure from the definition of $f$ .

__________

Example #1

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. We know that this function is both injective and surjective. Hence, it is bijective. Here’s a GHCi session (after running the Haskell script above):

*Main> let f n = (3 * n) `mod` 4
*Main> isInjective f [0..3]
True
*Main> isSurjective f [0..3] [0..3]
True
*Main> isBijective f [0..3] [0..3]
True

__________

Example #2

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}$

We already know that function $g$ is neither injective nor surjective. Hence, it is not bijective. Here’s a GHCi session:

*Main> let g n = (2 * n) `mod` 4
*Main> isInjective g [0..3]
False
*Main> isSurjective g [0..3] [0..3]
False
*Main> isBijective g [0..3] [0..3]
False

Tags:Bijectivity, Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Injectivity, Surjectivity
Posted in Haskell | Leave a Comment »

Deciding the injectivity of finite functions II

March 17, 2012

Last week we considered the following finite function

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

where $\mathbb{Z}_4 := \{0, 1, 2, 3\}$ and $\pmod{4}$ denotes modulo 4 arithmetic. We know that 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 $\mathbb{Z}_4$ . We introduce the injectivity predicate $\varphi : \mathbb{Z}_4 \times \mathbb{Z}_4 \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 the universally-quantified sentence $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ evaluates to $\text{True}$ .

__________

A naive decision procedure

We can determine the truth value of $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ by evaluating the predicate $\varphi$ at all $(x_1, x_2) \in \mathbb{Z}_4 \times \mathbb{Z}_4$ , which will require a total of $|\mathbb{Z}_4|^2 = 4^2 = 16$ evaluations. We implemented this decision procedure in Haskell last week. Here’s a rather brief GHCi session:

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

which allows us to conclude that $f$ is injective. Note that we used the following equivalence

$\left( f (x_1) = f (x_2) \implies x_1 = x_2\right) \equiv \left( f (x_1) \neq f (x_2) \lor x_1 = x_2\right)$

to implement $\varphi$ . Can we do better than this? In fact, we can.

__________

A better decision procedure

We introduce matrix $\Phi \in \{\text{True}, \text{False}\}^{4 \times 4}$ , defined by

$\Phi = \left[\begin{array}{cccc} \varphi (0,0) & \varphi (0,1) & \varphi (0,2) & \varphi (0,3)\\ \varphi (1,0) & \varphi (1,1) & \varphi (1,2) & \varphi (1,3)\\ \varphi (2,0) & \varphi (2,1) & \varphi (2,2) & \varphi (2,3)\\ \varphi (3,0) & \varphi (3,1) & \varphi (3,2) & \varphi (3,3)\\\end{array}\right]$

Stating that $f$ is injective, i.e., $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ evaluates to $\text{True}$ , is equivalent to saying that all the $4^2 = 16$ entries of matrix $\Phi$ evaluate to $\text{True}$ . Note, however, that the four entries on the main diagonal of $\Phi$ will always evaluate to $\text{True}$ , as the implication

$f (x) = f (x) \implies x = x$

evaluates to $\text{True}$ for every $x$ . Moreover, from the equivalence

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

we can conclude that $\varphi (x_1, x_2) = \varphi (x_2, x_1)$ for all $x_1$ and $x_2$ , which tells us that matrix $\Phi$ is symmetric (i.e., $\Phi = \Phi^T$ ). Therefore, we do not need to evaluate all entries of matrix $\Phi$ , only the ones above the main diagonal, as illustrated below

$\left[\begin{array}{cccc} \ast & \varphi (0,1) & \varphi (0,2) & \varphi (0,3)\\ \ast & \ast & \varphi (1,2) & \varphi (1,3)\\ \ast & \ast & \ast & \varphi (2,3)\\ \ast & \ast & \ast & \ast\\\end{array}\right]$

where the symbol $\ast$ denotes “don’t care”, i.e., entries we do not need to evaluate. Hence, instead of evaluating the predicate $\varphi$ a total of $4^2 = 16$ times, we now only need to evaluate it ${4 \choose 2} = 6$ times, which is $37.5 \%$ of the original total. We can generate all pairs $(x_1, x_2)$ with $x_2 > x_1$ using the following Haskell code:

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

We thus implement a more efficient decision procedure as follows:

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

which requires less than half of the number of evaluations required by the previous (naive) procedure.

__________

Conclusions

Given a finite function $f : \mathcal{X} \to \mathcal{Y}$ , we 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 (finite) function $f$ is injective if and only if $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ evaluates to $\text{True}$ . Let $n := |\mathcal{X}|$ denote the cardinality of set $\mathcal{X}$ . Deciding $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ using the naive procedure will require a total of $n^2$ evaluations of the predicate $\varphi$ . Since $\varphi (x,x) = \text{True}$ for every $x$ , and taking into account that $\varphi (x_1,x_2) = \varphi (x_2,x_1)$ , using the improved procedure we can decide injectivity at a cost of only ${n \choose 2} = \frac{n (n-1)}{2}$ evaluations of the predicate $\varphi$ . As $n$ approaches infinity, the ratio ${n \choose 2} / n^2$ approaches $1/2$ . Hence, for “large” problems, the improved procedure will require approximately half the number of evaluations required by the naive procedure.

Tags:Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Injectivity, Logic, Predicate Logic
Posted in Haskell, Logic, Mathematics | Leave a Comment »

Deciding the injectivity of finite functions

March 7, 2012

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!

Tags:Data.List, Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Injectivity, Logic, Predicate Logic
Posted in Haskell, Logic, Mathematics | 5 Comments »

Deciding injectivity

February 28, 2012

Consider a function $f : \mathcal{X} \to \mathcal{Y}$ . We say that $f$ is injective if and only if it maps distinct inputs to distinct outputs [1]. More formally, $f$ is injective if and only if

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

where $x_1$ and $x_2$ range over set $\mathcal{X}$ . Note that the inequations $x_1 \neq x_2$ and $f (x_1) \neq f (x_2)$ are equivalent to $\neg (x_1 = x_2)$ and $\neg \left(f (x_1) = f (x_2)\right)$ , respectively. The universally-quantified formula above can be rewritten as follows

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

which looks a bit messy. Contrapositively,

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

In this post, we will restrict our attention to real-valued functions of a real variable (i.e., functions from $\mathbb{R}$ to $\mathbb{R}$ ). For polynomial functions from reals to reals, we can use quantifier elimination to determine the truth values of the universally-quantified formulas above, thereby deciding injectivity.

__________

Example

We would like to decide the injectivity of the following functions

$\begin{array}{rl} f : \mathbb{R} &\to \mathbb{R}\\ x &\mapsto x^2\end{array}$ $\begin{array}{rl} g : \mathbb{R} &\to \mathbb{R}\\ x &\mapsto x^3\end{array}$

which we plot below (using Wolfram Alpha)

In high school we all learned to use the infamous horizontal line test to determine whether a function is injective. Let us use something more powerful this time, namely, the following REDUCE + REDLOG script:

% decide the injectivity of f(x) = x^2 and g(x) = x^3

load_package redlog;
rlset ofsf;

% define universally-quantified formulas
phi := all({x1,x2}, x1**2=x2**2 impl x1=x2);
psi := all({x1,x2}, x1**3=x2**3 impl x1=x2);

% perform quantifier elimination
rlqe phi;
rlqe psi;

end;

which decides that $f$ is not injective and that $g$ is injective.

__________

References

[1] David Makinson, Sets, Logic and Maths for Computing, Springer, 2008.

Tags:Decision Problems, Functionology, Injectivity, Quantifier Elimination, Real Functions, REDLOG, REDUCE
Posted in Mathematics | Leave a Comment »

S	M	T	W	T	F	S
« Dec
			1	2	3	4
5	6	7	8	9	10	11
12	13	14	15	16	17	18
19	20	21	22	23	24	25
26	27	28	29	30	31

Rod Carvalho

Posts Tagged ‘Injectivity’

Deciding the bijectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

Deciding injectivity

Pages

Categories

Top Posts

Recent Posts

Recent Comments

Tag Cloud

Archives

Blog Stats

Artists

Blogs

Haskell

Math Blogs

MATLAB

Python

Robotics

Software

Symbolic Computation

Powered by FeedBurner

Meta

Follow “Rod Carvalho”

Rod Carvalho

Posts Tagged ‘Injectivity’

Deciding the bijectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

Deciding injectivity

Pages

Categories

Top Posts

Recent Posts

Recent Comments

Tag Cloud

Archives

Blog Stats

Artists

Blogs

Haskell

Math Blogs

MATLAB

Python

Robotics

Software

Symbolic Computation

Category Cloud

Powered by FeedBurner

Meta

Follow “Rod Carvalho”