Decision Problems | Rod Carvalho

Posts Tagged ‘Decision Problems’

Deciding the convexity of semialgebraic sets II

June 23, 2012

Let $S_3 \subset \mathbb{R}^{3 \times 3}$ denote the set of real symmetric $3 \times 3$ matrices. We introduce a matrix-valued function $A: \mathbb{R}^3 \to S_3$ defined by

$A (x) = \left[\begin{array}{ccc} 1 & x_1 & x_2\\ x_1 & 1 & x_3\\ x_2 & x_3 & 1\end{array}\right]$

The elliptope $E_3 \subset \mathbb{R}^3$ is defined by

$E_3 = \left\{ x \in \mathbb{R}^3 \mid A (x) \succeq 0 \right\}$

where $A (x) \succeq 0$ means that matrix $A (x)$ is positive semidefinite. Since the elliptope $E_3$ is defined by the linear matrix inequality (LMI) $A (x) \succeq 0$ , we can conclude that $E_3$ is a spectrahedron and, therefore, we have that $E_3$ is convex.

The $E_3$ elliptope (also known as “inflated tetrahedron”) is the yellow part (surface and interior) of the Cayley’s cubic surface plotted below

[ source ]

__________

$E_3$ is a semialgebraic set

Saying that $A (x)$ is positive semidefinite is equivalent to saying that the $2^3 - 1 = 7$ principal minors of $A (x)$ are nonnegative. If $A (x) \succeq 0$ , then the three 1st order principal minors (which are the diagonal entries of $A (x)$ ) lead to the following three (admittedly uninteresting) inequalities

$1 \geq 0$ , $1 \geq 0$ , $1 \geq 0$

which we can discard. The three 2nd order principal minors (determinants of $2 \times 2$ submatrices of $A (x)$ ) and the 3rd order principal minor (the determinant of $A (x)$ ) can be computed using the following Python 2.5 + SymPy script:

from sympy import *

# symbolic variables
x1 = Symbol('x1')
x2 = Symbol('x2')
x3 = Symbol('x3')

# build matrix A(x)
A = Matrix([[1,x1,x2],
            [x1,1,x3],
            [x2,x3,1]])

print "\nMatrix A(x):"
print A

print "\n2nd order principal minors:"
print A.extract([0,1],[0,1]).det()
print A.extract([0,2],[0,2]).det()
print A.extract([1,2],[1,2]).det()

print "\n3rd order principal minor:"
print A.det()

which produces the following output:

Matrix A(x):
[ 1, x1, x2]
[x1,  1, x3]
[x2, x3,  1]

2nd order principal minors:
-x1**2 + 1
-x2**2 + 1
-x3**2 + 1

3rd order principal minor:
-x1**2 + 2*x1*x2*x3 - x2**2 - x3**2 + 1

Hence, the 2nd order principal minors yield the following inequalities

$1 - x_1^2 \geq 0$ , $1 - x_2^2 \geq 0$ , $1 - x_3^2 \geq 0$

which define the $3$ -dimensional cube $[-1,1]^3 \subset \mathbb{R}^3$ . The 3rd order principal minor (i.e., the determinant) yields the inequality

$1 + 2 x_1 x_2 x_3 - (x_1^2 + x_2^2 + x_3^3) \geq 0$ .

We can thus conclude that $E_3$ is a basic closed semialgebraic set.

__________

Deciding the convexity of $E_3$

In my last post, I used quantifier elimination to decide the convexity of two semialgebraic sets in $\mathbb{R}^2$ . Let us now decide the convexity of $E_3$ , which is of higher “complexity” than the sets I considered last time. What is the goal? The goal is to find out whether REDLOG can decide the convexity of $E_3$ in less than 10 minutes.

Based on the scripts in my previous post, we write the following REDUCE + REDLOG script to decide the convexity of $E_3$ :

% decide the convexity of the elliptope E3

load_package redlog;
rlset ofsf;

% define predicates in antecedent
p1 := (1-x1^2>=0) and (1-x2^2>=0) and (1-x3^2>=0) and 
      (1-x1^2-x2^2-x3^2+2*x1*x2*x3>=0);
p2 := (1-y1^2>=0) and (1-y2^2>=0) and (1-y3^2>=0) and 
      (1-y1^2-y2^2-y3^2+2*y1*y2*y3>=0);
p3 := (theta>=0) and (theta<=1);

% define predicate in the consequent
z1 := theta*x1+(1-theta)*y1;
z2 := theta*x2+(1-theta)*y2;
q  := (1-z1^2>=0) and (1-z2^2>=0) and (1-z3^2>=0) and 
      (1-z1^2-z2^2-z3^2+2*z1*z2*z3>=0);

% define universal formula
phi := all({x1,x2,x3,y1,y2,y3,theta}, (p1 and p2 and p3) impl q);

% perform quantifier elimination
rlqe phi;

end;

After 30 minutes (!!!) waiting for the decision procedure to terminate, I killed the reduce.exe process (which was eating all my machine’s CPU cycles and RAM memory). This is disappointing…

Tags:Convex Algebraic Geometry, Convexity, Decision Problems, Linear Matrix Inequalities, Python, Quantifier Elimination, REDLOG, REDUCE, Semialgebraic Geometry, Semialgebraic Sets, Spectrahedra, SymPy
Posted in Algebraic Geometry, Python | Leave a Comment »

Deciding the convexity of semialgebraic sets

June 16, 2012

Given a basic closed semialgebraic set [1], $S \subset \mathbb{R}^n$ , defined by

$S = \{ x \in \mathbb{R}^n \mid g_1 (x) \geq 0 \land \dots \land g_m (x) \geq 0\}$

where $m \in \mathbb{N}$ and $g_1, \dots, g_m \in \mathbb{R}[x]$ , how can one decide if set $S$ is convex? Can one use quantifier elimination?

__________

Convexity

Let us recall the definition of convexity [2]:

Definition: A set $S$ is convex if the line segment between any two points in $S$ lies in $S$ , i.e., if for any $x, y \in S$ and any $\theta$ with $0 \leq \theta \leq 1$ , we have $\theta x + (1-\theta) y \in S$ .

Let us introduce a predicate $p : \mathbb{R}^n \to \{\text{True}, \text{False}\}$ , defined by

$\displaystyle p (x) = \bigwedge_{i = 1}^m g_i (x) \geq 0$

so that we can write $S$ in the more parsimonious form

$S = \{ x \in \mathbb{R}^n \mid p (x) \}$ .

Hence, writing $x \in S$ is equivalent to asserting that $p (x) = \text{True}$ . From the definition above, it follows that set $S$ is convex if and only if the following universally quantified formula

$\forall x \, \forall y \, \forall \theta \, \left[ \, p(x) \land p(y) \land (\theta \geq 0 \land \theta \leq 1) \implies p (\theta x + (1-\theta) y) \, \right]$

where $x, y$ range over $\mathbb{R}^n$ and $\theta$ ranges over $\mathbb{R}$ , evaluates to $\text{True}$ . Since $g_1, \dots, g_m$ are polynomials, the formula above can be decided using quantifier elimination software like QEPCAD or REDLOG. Unfortunately, decidability does not imply that real quantifier elimination will decide the formula in an expedite manner. Let us now consider two instances of the decision problem under study.

__________

Example #1

Consider the following semialgebraic set

$S_1 := \{ x \in \mathbb{R}^2 \mid x_1 - x_2^2 + 3 \geq 0 \land -x_1 - x_2^2 + 3 \geq 0\}$

which we depict below

Visual inspection of the plot above allows us to conclude that set $S_1$ is convex. However, relying on the human visual system is extremely limiting. Therefore, we would like to automate the decision. We decide the convexity of $S_1$ via quantifier elimination using the following REDUCE + REDLOG script:

% decide the convexity of a semialgebraic set

load_package redlog;
rlset ofsf;

% define predicates in antecedent
p1 := (x1-x2^2+3>=0) and (-x1-x2^2+3>=0);
p2 := (y1-y2^2+3>=0) and (-y1-y2^2+3>=0);
p3 := (theta>=0) and (theta<=1);

% define predicate in the consequent
z1 := theta*x1+(1-theta)*y1;
z2 := theta*x2+(1-theta)*y2;
q  := (z1-z2^2+3>=0) and (-z1-z2^2+3>=0); 

% define universal formula
phi := all({x1,x2,y1,y2,theta}, (p1 and p2 and p3) impl q);

% perform quantifier elimination
rlqe phi;

end;

This script returns the truth value $\text{True}$ and, hence, $S_1$ is, indeed, convex. However, it took REDLOG approximately 60 seconds to decide the convexity of $S_1$ , which is considerably longer than any of my previous experiments with REDLOG. Since we are performing quantifier elimination on a formula with five universal quantifiers, I am not incredibly surprised that it takes a while to obtain an answer.

__________

Example #2

Consider now the following semialgebraic set

$S_2 := \{ x \in \mathbb{R}^2 \mid x_1 - x_2^2 + 3 \geq 0 \land x_1 - x_2^2 + 1 \leq 0\}$

part of which we depict below

Visual inspection of the plot above allows us to conclude that set $S_2$ is not convex. We decide the convexity of $S_2$ using the following REDUCE + REDLOG script:

% decide the convexity of a semialgebraic set

load_package redlog;
rlset ofsf;

% define predicates in antecedent
p1 := (x1-x2^2+3>=0) and (x1-x2^2+1<=0);
p2 := (y1-y2^2+3>=0) and (y1-y2^2+1<=0);
p3 := (theta>=0) and (theta<=1);

% define predicate in the consequent
z1 := theta*x1+(1-theta)*y1;
z2 := theta*x2+(1-theta)*y2;
q  := (z1-z2^2+3>=0) and (z1-z2^2+1<=0); 

% define universal formula
phi := all({x1,x2,y1,y2,theta}, (p1 and p2 and p3) impl q);

% perform quantifier elimination
rlqe phi;

end;

This script returns the truth value $\text{False}$ and, hence, $S_2$ is, indeed, not convex. Interestingly, it took REDLOG less than one second to decide the formula. That is over two orders of magnitude faster than in example #1.

__________

References

[1] Markus Schweighofer, Describing convex semialgebraic sets by linear matrix inequalities, International Symposium on Symbolic and Algebraic Computation, Korea Institute for Advanced Study, Seoul, July 2009.

[2] Stephen Boyd, Lieven Vandenberghe, Convex Optimization.

Tags:Convex Algebraic Geometry, Convexity, Decision Problems, Quantifier Elimination, Real Algebraic Geometry, REDLOG, REDUCE, Semialgebraic Geometry, Semialgebraic Sets
Posted in Algebraic Geometry | Leave a Comment »

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:Haskell, Decision Problems, Injectivity, Functionology, Surjectivity, Finite Functions, Decision Procedures, Bijectivity
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:Logic, Haskell, Predicate Logic, Decision Problems, Functionology, Surjectivity, Finite Functions, Decision Procedures
Posted in Mathematics, Haskell, Logic | 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:Logic, Haskell, Predicate Logic, Decision Problems, Injectivity, Functionology, Finite Functions, Decision Procedures
Posted in Mathematics, Haskell, Logic | 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 ‘Decision Problems’

Deciding the convexity of semialgebraic sets II

Deciding the convexity of semialgebraic sets

Deciding the bijectivity of finite functions

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

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 Problems’

Deciding the convexity of semialgebraic sets II

Deciding the convexity of semialgebraic sets

Deciding the bijectivity of finite functions

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

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”