Predicate Logic | Rod Carvalho

Posts Tagged ‘Predicate Logic’

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 »

Not all birds can fly

January 1, 2012

Consider the following declarative sentence

Not all birds can fly.

This sentence can be paraphrased as

It is not the case that all things which are birds can fly.

Let $\mathcal{X}$ be the set of all things of interest (i.e., the universe under discussion). We now introduce predicates $B : \mathcal{X} \to \{\text{True}, \text{False}\}$ and $F : \mathcal{X} \to \{\text{True}, \text{False}\}$ , defined by

$B (x) = \begin{cases} \text{True}, & x \textrm{ is a bird}\\ \text{False}, & x \textrm{ is not a bird}\end{cases}$

and

$F (x) = \begin{cases} \text{True}, & x \textrm{ can fly}\\ \text{False}, & x \textrm{ cannot fly}\end{cases}$

Finally, using (unary) predicates $B$ and $F$ , the declarative sentence “Not all birds can fly” can be encoded as follows

$\neg \left( \forall x \, ( B (x) \rightarrow F (x) ) \right)$

where we used negation ( $\neg$ ), universal quantification ( $\forall$ ), and material implication ( $\rightarrow$ ). The (well-formed) formula above should be read as: “it is not the case that for all $x \in \mathcal{X}$ , if $x$ is a bird, then $x$ can fly”. Whether the (universally quantified) formula evaluates to $\text{True}$ or $\text{False}$ depends on the set $\mathcal{X}$ we consider. For example, if $\mathcal{X}$ is the set of all living things on Earth on January 1, 2012, then the formula evaluates to $\text{True}$ because penguins are birds which cannot fly. However, if we spend the next century eradicating all birds that cannot fly, then on January 1, 2112, the formula might evaluate to $\text{False}$ .

__________

Technicalities

Let us consider the formula $\neg\left(\forall x \, \varphi (x)\right)$ , where $\varphi$ is a predicate. If this formula evaluates to $\text{True}$ , then it is not the case that for all $x \in \mathcal{X}$ we have that $\varphi (x) = \text{True}$ , which is the same as saying that there exists a $x \in \mathcal{X}$ for which $\varphi (x) = \text{False}$ or, in other words, for which $\neg \varphi (x) = \text{True}$ . Hence, formula $\neg\left(\forall x \, \varphi (x)\right)$ is equivalent (in some sense) to the formula $\exists x \, \neg \varphi (x)$ , where $\exists$ is the existential quantifier. We write $\neg\left(\forall x \, \varphi (x)\right) \equiv \exists x \, \neg \varphi (x)$ to denote this equivalence. Hence, we conclude that

$\neg \left( \forall x \, ( B (x) \rightarrow F (x) ) \right) \equiv \exists x \, \neg ( B (x) \rightarrow F (x) )$ .

Given propositional atoms $p$ and $q$ , we have that the formula $p \rightarrow q$ is semantically equivalent [1] to the formula $\neg p \lor q$ . We write $p \rightarrow q \equiv \neg p \lor q$ to denote this equivalence. Thus, we have that

$B (x) \rightarrow F (x) \equiv \neg B (x) \lor F (x)$

which allows us to conclude that

$\exists x \, \neg ( B (x) \rightarrow F (x) ) \equiv \exists x \, \neg ( \neg B (x) \lor F (x) )$ .

Using one of De Morgan’s laws, namely, $\neg (p \lor q) \equiv \neg p \land \neg q$ , we conclude that $\neg ( \neg B (x) \lor F (x) ) \equiv \neg \neg B (x) \land \neg F (x)$ . Eliminating the double negation (we can do that in Classical Logic, but not in Intuitionistic Logic), we obtain $\neg ( \neg B (x) \lor F (x) ) \equiv B (x) \land \neg F (x)$ . Without further ado, we have that

$\exists x \, \neg ( \neg B (x) \lor F (x) ) \equiv \exists x \, ( B (x) \land \neg F (x) )$ .

From all these equivalences, we finally conclude that

$\neg \left( \forall x \, ( B (x) \rightarrow F (x) ) \right) \equiv \exists x \, ( B (x) \land \neg F (x) )$ .

What does this equivalence say? It tells us that the declarative sentence “Not all birds can fly” can be paraphrased as follows

There exists a thing which is a bird and which cannot fly.

That “thing” could be, for example, a penguin. For the sake of convenience, let us introduce predicates $\varphi$ and $\psi$ , defined by

$\varphi (x) := B (x) \rightarrow F (x)$

$\psi (x) := B (x) \land \neg F (x)$

so that the last equivalence can be written more compactly as

$\neg \left( \forall x \, \varphi (x) \right) \equiv \exists x \, \psi (x)$

where $\varphi (x) \equiv \neg B (x) \lor F (x)$ . This will be useful later on.

__________

Creating our universe

Let us suppose that we do not know that penguins are birds and that they cannot fly. Evaluating the formula $\exists x \, ( B (x) \land \neg F (x) )$ using planet Earth’s fauna as the set of all things of interest would require us to consult quite a few Zoology books. However, it is Sunday night and the library is closed for the Winter break. And, to make matters worse, we are somewhat lazy.

Instead of bothering with the actual universe, let us create our own imaginary universe in which there are only three classes of animals: birds, cats, and dogs. Each class contains only three species each.

We construct this imaginary universe in Haskell:

-- create Animal data type
data Animal = Bird String |
              Cat String |
              Dog String deriving (Show, Eq)

-- create list of animals
animals = [Bird "Dove", Bird "Hawk", Bird "Penguin",
           Cat "Burmese", Cat "Persian", Cat "Siamese",
           Dog "Dalmatian", Dog "Husky", Dog "Terrier"]

-- define isBird predicate
isBird :: Animal -> Bool
isBird (Bird s) = True
isBird _ = False

-- define canFly predicate
canFly :: Animal -> Bool
canFly (Bird "Dove") = True
canFly (Bird "Hawk") = True
canFly _ = False

-- define phi predicate
phi :: Animal -> Bool
phi x = ((not . isBird) x) || (canFly x) 

-- define psi predicate
psi :: Animal -> Bool
psi x = (isBird x) && ((not . canFly) x)

Let us now play with these objects and predicates and evaluate the quantified formulas using the GHCi interpreter:

*Main> -- print list of animals
*Main> animals
[Bird "Dove",Bird "Hawk",Bird "Penguin",Cat "Burmese",Cat "Persian",
Cat "Siamese",Dog "Dalmatian",Dog "Husky",Dog "Terrier"]
*Main> -- test isBird predicate
*Main> map isBird animals
[True,True,True,False,False,False,False,False,False]
*Main> -- test canFly predicate
*Main> map canFly animals
[True,True,False,False,False,False,False,False,False]
*Main> -- test phi predicate
*Main> map phi animals
[True,True,False,True,True,True,True,True,True]
*Main> -- test psi predicate
*Main> map psi animals
[False,False,True,False,False,False,False,False,False]
*Main> -- evaluate universally quantified formula
*Main> not (all phi animals)
True
*Main> -- evaluate existentially quantified formula
*Main> any psi animals
True

where we used functions all and any to emulate the universal and existential quantifiers, respectively. Note that both formulas evaluate to $\text{True}$ , as expected.

__________

Caution: do not confuse the arrow used in the definition of the predicates with the arrow used in material implication. They look the same, but they are different $\LaTeX$ symbols and context should allow one to distinguish the two.

Remark: this post is based on an example in chapter 2 of Huth & Ryan [1].

__________

References

[1] Michael Huth, Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed., Cambridge University Press, June 2004.

Tags:Haskell, Logic, Predicate Logic
Posted in 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 ‘Predicate Logic’

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

Not all birds can fly

Pages

Categories

Top 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 ‘Predicate Logic’

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

Not all birds can fly

Pages

Categories

Top 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”