Decision Procedures | Rod Carvalho

Posts Tagged ‘Decision Procedures’

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 surjectivity of finite functions

March 19, 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 two weeks ago, function $f$ is surjective if and only if

$\forall y \exists x \left( f (x) = y \right)$

where $x$ and $y$ range over sets $\mathcal{X}$ and $\mathcal{Y}$ , respectively. We now introduce the surjectivity predicate $\varphi : \mathcal{X} \times \mathcal{Y} \to \{\text{True}, \text{False}\}$ , defined by $\varphi (x, y) =\left( f (x) = y\right)$ so that function $f$ is surjective if and only if $\forall y \exists x \, \varphi (x, y)$ evaluates to $\text{True}$ .

Let $m := |\mathcal{X}|$ and $n := |\mathcal{Y}|$ denote the cardinalities of sets $\mathcal{X}$ and $\mathcal{Y}$ , respectively. Deciding $\forall y \exists x \, \varphi (x, y)$ should then require a total of $m n$ evaluations of predicate $\varphi$ . Let us write $\mathcal{X} = \{x_1, x_2, \dots, x_m\}$ and $\mathcal{Y} = \{y_1, y_2, \dots, y_n\}$ , and introduce $\Phi \in \{\text{True}, \text{False}\}^{m \times n}$ , a Boolean matrix defined as follows

$\Phi = \left[\begin{array}{cccc} \varphi (x_1,y_1) & \varphi (x_1,y_2) & \ldots & \varphi (x_1,y_n)\\ \varphi (x_2,y_1) & \varphi (x_2,y_2) & \ldots & \varphi (x_2,y_n)\\ \vdots & \vdots & \ddots & \vdots\\ \varphi (x_m,y_1) & \varphi (x_m,y_2) & \ldots & \varphi (x_m,y_n)\\\end{array}\right]$

Stating that $f$ is surjective, i.e., $\forall y \exists x \, \varphi (x, y)$ evaluates to $\text{True}$ , is equivalent to saying that every column of matrix $\Phi$ contains at least one entry that evaluates to $\text{True}$ . We now introduce a new predicate, $\psi : \mathcal{Y} \to \{\text{True}, \text{False}\}$ , defined by

$\psi (y) = \exists x \, \varphi (x,y)$

so that $\forall y \exists x \, \varphi (x, y)$ can be rewritten in the form $\forall y \, \psi (y)$ , where $y$ ranges over set $\mathcal{Y}$ . Note that $\psi (y)$ can be viewed as the disjunction of the $m$ atoms $\varphi (x_1, y), \varphi (x_2, y), \dots, \varphi (x_m, y)$ , i.e.,

$\psi (y) = \displaystyle\bigvee_{i =1}^m \varphi (x_i, y)$ .

Note also that $\forall y \, \psi (y)$ can be viewed as the conjunction of the $n$ atoms $\psi (y_1), \psi (y_2), \dots, \psi (y_n)$ . Thus, we can decide surjectivity using the following procedure:

Compute $\psi (y) = \exists x \, \varphi (x,y)$ for all $y \in \mathcal{Y}$ .
Compute the conjunction $\bigwedge_{j=1}^n \psi (y_j)$ . If its truth value is $\text{True}$ , then the function is surjective.

Let us now consider two simple examples and implement this decision procedure in Haskell.

__________

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. Note that $f (0) = 0$ , $f (1) = 3$ , $f (2) = 2$ , and $f (3) = 1$ . Hence, we easily conclude that $f$ is both injective and surjective (and, thus, is bijective). In Haskell:

Prelude> let f n = (3 * n) `mod` 4
Prelude> let xs = [0..3]
Prelude> let ys = [0..3]
Prelude> let psi y = or [(f x == y) | x <- xs]
Prelude> all psi ys
True

which allows us to conclude that $f$ is surjective. Note that we used function or to perform disjunction, and function all to perform universal quantification.

__________

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

Note that $g (0) = g (2) = 0$ and $g (1) = g (3) = 2$ . Hence, function $g$ is neither injective nor surjective. In Haskell, we have the following:

Prelude> let g n = (2 * n) `mod` 4
Prelude> let xs = [0..3]
Prelude> let ys = [0..3]
Prelude> let psi y = or [(g x == y) | x <- xs]
Prelude> all psi ys
False

which allows us to conclude that $g$ is not surjective. Why? The following code returns a list of lists of Booleans where each sublist is a column of matrix $\Phi$ (where each entry is $\Phi_{ij} = (g(x_i) = y_j)$ )

Prelude> [[(g x == y) | x <- xs] | y <- ys]
[[True,False,True,False],[False,False,False,False],
[False,True,False,True],[False,False,False,False]]

Note that the 2nd and 4th sublists contain only $\text{False}$ truth values. Hence, it is not the case that every column of matrix $\Phi$ contains at least one entry that evaluates to $\text{True}$ . Thus, $g$ is not surjective.

Tags:Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Logic, Predicate Logic, Surjectivity
Posted in Haskell, Logic, Mathematics | 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 »

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 ‘Decision Procedures’

Deciding the bijectivity of finite functions

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

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 ‘Decision Procedures’

Deciding the bijectivity of finite functions

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

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”