---
title: Predicates
author: nbloomf
date: 2018-01-07
tags: arithmetic-made-difficult, literate-haskell
slug: predicates
---

> {-# LANGUAGE NoImplicitPrelude #-}
> module Predicates (
>   pnot, pand, por, ptrue, pfalse, _test_predicate, main_predicate
> ) where
> 
> import Testing
> import Booleans
> import Not
> import And
> import Or

In the last post we defined the algebra of boolean values, true and false. Today we'll look at *predicates* -- functions from some set $A$ to $\bool$. It turns out the algebra on $\bool$ can be lifted to predicates, and is useful enough to collect some definitions and properties in one place.

:::::: definition ::
[]{#def-ptrue}[]{#def-pfalse}
Let $A$ be a set. A *predicate* on $A$ is just a function $p : A \rightarrow \bool$. We define two special predicates, $\ptrue = \const(\btrue)$ and $\pfalse = \const(\bfalse)$.

In Haskell:

> ptrue :: (Boolean b) => a -> b
> ptrue _ = true
> 
> pfalse :: (Boolean b) => a -> b
> pfalse _ = false

::::::::::::::::::::

First, the basic logic operators lift.

:::::: definition ::
[]{#def-pnot}
Let $A$ be a set. We define $\pnot : \bool^A \rightarrow \bool^A$ by $$\pnot(p)(a) = \bnot(p(a)).$$

In Haskell:

> pnot :: (Boolean b) => (a -> b) -> a -> b
> pnot p a = not (p a)

::::::::::::::::::::

$\pnot$ is an involution.

:::::: theorem :::::
[]{#thm-pnot-involution}
Let $A$ be a set. For all $p : A \rightarrow \bool$, we have $$\pnot(\pnot(p)) = p.$$

::: proof ::::::::::
Let $a \in A$. Then we have
$$\begin{eqnarray*}
 &   & \pnot(\pnot(p))(a) \\
 &     \href{@predicates@#def-pnot}
   = & \bnot(\pnot(p)(a)) \\
 &     \href{@predicates@#def-pnot}
   = & \bnot(\bnot(p(a))) \\
 &     \href{@not@#thm-not-involution}
   = & p(a)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_pnot_involutive :: (Boolean b, Equal b)
>   => a -> b -> Test ((a -> b) -> a -> Bool)
> _test_pnot_involutive _ b =
>   testName "pnot(pnot(p)) == p" $
>   \p x -> eq (pnot (pnot p) x) ((p x) `withTypeOf` b)

::::::::::::::::::::
::::::::::::::::::::

Special cases.

:::::: theorem :::::
[]{#thm-pnot-ptrue}[]{#thm-pnot-pfalse}[]{#thm-compose-bnot-ptrue}[]{#thm-compose-bnot-pfalse}
Let $A$ be a set. Then we have the following.

1. $\pnot(\ptrue) = \pfalse$.
2. $\pnot(\pfalse) = \ptrue$.
3. $\compose(\bnot)(\ptrue) = \pfalse$.
4. $\compose(\bnot)(\pfalse) = \ptrue$.

::: proof ::::::::::
1. If $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pnot(\ptrue)(a) \\
 &     \href{@predicates@#def-pnot}
   = & \bnot(\ptrue(a)) \\
 &     \href{@predicates@#def-ptrue}
   = & \bnot(\const(\btrue)(a)) \\
 &     \href{@functions@#def-const}
   = & \bnot(\btrue) \\
 &     \href{@not@#thm-not-true}
   = & \bfalse \\
 &     \href{@functions@#def-const}
   = & \const(\bfalse)(a) \\
 &     \href{@predicates@#def-pfalse}
   = & \pfalse(a)
\end{eqnarray*}$$
as needed.
2. If $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pnot(\pfalse)(a) \\
 &     \href{@predicates@#def-pnot}
   = & \bnot(\pfalse(a)) \\
 &     \href{@predicates@#def-pfalse}
   = & \bnot(\const(\bfalse)(a)) \\
 &     \href{@functions@#def-const}
   = & \bnot(\bfalse) \\
 &     \href{@not@#thm-not-false}
   = & \btrue \\
 &     \href{@functions@#def-const}
   = & \const(\btrue)(a) \\
 &     \href{@predicates@#def-ptrue}
   = & \ptrue(a)
\end{eqnarray*}$$
as needed.
3. If $a \in A$, we have
$$\begin{eqnarray*}
 &   & \compose(\bnot)(\ptrue)(a) \\
 &     \href{@functions@#def-compose}
   = & \bnot(\ptrue(a)) \\
 &     \href{@predicates@#def-ptrue}
   = & \bnot(\const(\btrue)(a)) \\
 &     \href{@functions@#def-const}
   = & \bnot(\btrue) \\
 &     \href{@not@#thm-not-true}
   = & \bfalse \\
 &     \href{@functions@#def-const}
   = & \const(\bfalse)(a) \\
 &     \href{@predicates@#def-pfalse}
   = & \pfalse(a)
\end{eqnarray*}$$
as needed.
4. If $a \in A$, we have
$$\begin{eqnarray*}
 &   & \compose(\bnot)(\pfalse)(a) \\
 &     \href{@functions@#def-compose}
   = & \bnot(\pfalse(a)) \\
 &     \href{@predicates@#def-pfalse}
   = & \bnot(\const(\bfalse)(a)) \\
 &     \href{@functions@#def-const}
   = & \bnot(\bfalse) \\
 &     \href{@not@#thm-not-false}
   = & \btrue \\
 &     \href{@functions@#def-const}
   = & \const(\btrue)(a) \\
 &     \href{@predicates@#def-ptrue}
   = & \ptrue(a)
\end{eqnarray*}$$
::::::::::::::::::::

::: test :::::::::::

> _test_pnot_ptrue :: (Boolean b, Equal b)
>   => a -> b -> Test (a -> Bool)
> _test_pnot_ptrue _ b =
>   testName "pnot(ptrue) == pfalse" $
>   \a -> eq ((pnot ptrue) a) ((pfalse a) `withTypeOf` b)
> 
> 
> _test_pnot_pfalse :: (Boolean b, Equal b)
>   => a -> b -> Test (a -> Bool)
> _test_pnot_pfalse _ b =
>   testName "pnot(pfalse) == ptrue" $
>   \a -> eq ((pnot pfalse) a) ((ptrue a) `withTypeOf` b)
> 
> 
> _test_not_ptrue :: (Boolean b, Equal b)
>   => a -> b -> Test (a -> Bool)
> _test_not_ptrue _ b =
>   testName "(not . ptrue) == pfalse" $
>   \a -> eq ((not . ptrue) a) ((pfalse a) `withTypeOf` b)
> 
> 
> _test_not_pfalse :: (Boolean b, Equal b)
>   => a -> b -> Test (a -> Bool)
> _test_not_pfalse _ b =
>   testName "(not . pfalse) == ptrue" $
>   \a -> eq ((not . pfalse) a) ((ptrue a) `withTypeOf` b)

::::::::::::::::::::
::::::::::::::::::::

Next, $\pand$.

:::::: definition ::
[]{#def-pand}
Let $A$ be a set. We define $\pand : \bool^A \times \bool^A \rightarrow \bool^A$ by $$\pand(p,q)(a) = \band(p(a),q(a)).$$

In Haskell:

> pand :: (a -> Bool) -> (a -> Bool) -> a -> Bool
> pand p q a = and (p a) (q a)

::::::::::::::::::::

The usual properties of $\band$ lift to $\pand$.

:::::: theorem :::::
[]{#thm-pand-pfalse-left}[]{#thm-pand-pfalse-right}[]{#thm-pand-ptrue-left}[]{#thm-pand-ptrue-right}[]{#thm-pand-idempotent}[]{#thm-pand-commutative}[]{#thm-pand-associative}
Let $A$ be a set. The following hold for all p,q,r \in \bool^A$.

1. $\pand(\pfalse,p) = \pand(p,\pfalse) = \pfalse$.
2. $\pand(\ptrue,p) = \pand(p,\ptrue) = p$.
3. $\pand(p,p) = p$.
4. $\pand(p,q) = \pand(q,p)$.
5. $\pand(\pand(p,q),r) = \pand(p,\pand(q,r))$.

::: proof ::::::::::
1. For all $a \in A$ we have
$$\begin{eqnarray*}
 &   & \pand(\pfalse,p)(a) \\
 &     \href{@predicates@#def-pand}
   = & \band(\pfalse(a),p(a)) \\
 &     \href{@predicates@#def-pfalse}
   = & \band(\const(\bfalse)(a),p(a)) \\
 &     \href{@functions@#def-const}
   = & \band(\bfalse,p(a)) \\
 &     \href{@and@#thm-and-false-left}
   = & \bfalse \\
 &     \href{@functions@#def-const}
   = & \const(\bfalse)(a) \\
 &     \href{@predicates@#def-pfalse}
   = & \pfalse(a)
\end{eqnarray*}$$
as needed; similarly for the other equality.
2. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pand(\ptrue,p)(a) \\
 &     \href{@predicates@#def-pand}
   = & \band(\ptrue(a),p(a)) \\
 &     \href{@predicates@#def-ptrue}
   = & \band(\const(\btrue)(a),p(a)) \\
 &     \href{@functions@#def-const}
   = & \band(\btrue,p(a)) \\
 &     \href{@and@#thm-and-true-left}
   = & p(a)
\end{eqnarray*}$$
as needed.
3. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pand(p,p)(a) \\
 &     \href{@predicates@#def-pand}
   = & \band(p(a),p(a)) \\
 &     \href{@and@#thm-and-idempotent}
   = & p(a)
\end{eqnarray*}$$
as needed.
4. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pand(p,q)(a) \\
 &     \href{@predicates@#def-pand}
   = & \band(p(a),q(a)) \\
 &     \href{@and@#thm-and-commutative}
   = & \band(q(a),p(a)) \\
 &     \href{@predicates@#def-pand}
   = & \pand(q,p)(a)
\end{eqnarray*}$$
as needed.
5. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pand(\pand(p,q),r)(a) \\
 &     \href{@predicates@#def-pand}
   = & \band(\pand(p,q)(a),r(a)) \\
 &     \href{@predicates@#def-pand}
   = & \band(\band(p(a),q(a)),r(a)) \\
 &     \href{@and@#thm-and-associative}
   = & \band(p(a),\band(q(a),r(a))) \\
 &     \href{@predicates@#def-pand}
   = & \band(p(a),\pand(q,r)(a)) \\
 &     \href{@predicates@#def-pand}
   = & \pand(p,\pand(q,r))(a)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_pand_pfalse
>   :: a -> Test ((a -> Bool) -> a -> Bool)
> _test_pand_pfalse _ =
>   testName "pand(pfalse,p) == pfalse" $
>   \p a -> eq ((pand pfalse p) a) (pfalse a)
> 
> 
> _test_pand_ptrue
>   :: a -> Test ((a -> Bool) -> a -> Bool)
> _test_pand_ptrue _ =
>   testName "pand(ptrue,p) == p" $
>   \p a -> eq ((pand ptrue p) a) (p a)
> 
> 
> _test_pand_idempotent
>   :: a -> Test ((a -> Bool) -> a -> Bool)
> _test_pand_idempotent _ =
>   testName "pand(p,p) == p" $
>   \p a -> eq ((pand p p) a) (p a)
> 
> 
> _test_pand_commutative
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_pand_commutative _ =
>   testName "pand(p,q) == pand(q,p)" $
>   \p q a -> eq ((pand p q) a) ((pand q p) a)
> 
> 
> _test_pand_associative
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_pand_associative _ =
>   testName "pand(pand(p,q),r) == pand(p,pand(q,r))" $
>   \p q r a -> eq ((pand (pand p q) r) a) ((pand p (pand q r)) a)

::::::::::::::::::::
::::::::::::::::::::

Then $\por$.

:::::: definition ::
[]{#def-por}
Let $A$ be a set. We define $\por : \bool^A \times \bool^A \rightarrow \bool^A$ by $$\por(p,q)(a) = \bor(p(a),q(a)).$$

In Haskell:

> por :: (a -> Bool) -> (a -> Bool) -> a -> Bool
> por p q a = or (p a) (q a)

::::::::::::::::::::

The usual properties of $\bor$ lift to $\por$.

:::::: theorem :::::
[]{#thm-por-ptrue-left}[]{#thm-por-ptrue-right}[]{#thm-por-pfalse-left}[]{#thm-por-pfalse-right}[]{#thm-por-idempotent}[]{#thm-por-commutative}[]{#thm-por-associative}
Let $A$ be a set. The following hold for all $p,q,r \in \bool^A$.

1. $\por(\ptrue,p) = \por(p,\ptrue) = \ptrue$.
2. $\por(\pfalse,p) = \por(p,\pfalse) = p$.
3. $\por(p,p) = p$.
4. $\por(p,q) = \por(q,p)$.
5. $\por(\por(p,q),r) = \por(p,\por(q,r))$.

::: proof ::::::::::
1. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \por(\ptrue,p)(a) \\
 &     \href{@predicates@#def-por}
   = & \bor(\ptrue(a),p(a)) \\
 &     \href{@predicates@#def-ptrue}
   = & \bor(\const(\btrue)(a),p(a)) \\
 &     \href{@functions@#def-const}
   = & \bor(\btrue,p(a)) \\
 &     \href{@or@#thm-or-true-left}
   = & \btrue \\
 &     \href{@functions@#def-const}
   = & \const(\btrue)(a) \\
 &     \href{@predicates@#def-ptrue}
   = & \ptrue(a)
\end{eqnarray*}$$
as needed; the other equality is similar.
2. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \por(\pfalse,p)(a) \\
 &     \href{@predicates@#def-por}
   = & \bor(\pfalse(a),p(a)) \\
 &     \href{@predicates@#def-pfalse}
   = & \bor(\const(\bfalse)(a),p(a)) \\
 &     \href{@functions@#def-const}
   = & \bor(\bfalse,p(a)) \\
 &     \href{@or@#thm-or-false-left}
   = & p(a)
\end{eqnarray*}$$
as needed; the other equality is similar.
3. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \por(p,p)(a) \\
 &     \href{@predicates@#def-por}
   = & \bor(p(a),p(a)) \\
 &     \href{@or@#thm-or-idempotent}
   = & p(a)
\end{eqnarray*}$$
as needed.
4. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \por(p,q)(a) \\
 &     \href{@predicates@#def-por}
   = & \bor(p(a),q(a)) \\
 &     \href{@or@#thm-or-commutative}
   = & \bor(q(a),p(a)) \\
 &     \href{@predicates@#def-por}
   = & \por(q,p)(a)
\end{eqnarray*}$$
as needed.
5. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \por(\por(p,q),r)(a) \\
 &     \href{@predicates@#def-por}
   = & \bor(\por(p,q)(a),r(a)) \\
 &     \href{@predicates@#def-por}
   = & \bor(\bor(p(a),q(a)),r(a)) \\
 &     \href{@or@#thm-or-associative}
   = & \bor(p(a),\bor(q(a),r(a))) \\
 &     \href{@predicates@#def-por}
   = & \bor(p(a),\por(q,r)(a)) \\
 &     \href{@predicates@#def-por}
   = & \por(p,\por(q,r))(a)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_por_ptrue :: (Boolean b, Equal b)
>   => a -> b -> Test ((a -> Bool) -> a -> Bool)
> _test_por_ptrue _ _ =
>   testName "por(ptrue,p) == ptrue" $
>   \p a -> eq ((por ptrue p) a) (ptrue a)
> 
> 
> _test_por_pfalse :: (Boolean b, Equal b)
>   => a -> b -> Test ((a -> Bool) -> a -> Bool)
> _test_por_pfalse _ _ =
>   testName "por(pfalse,p) == p" $
>   \p a -> eq ((por pfalse p) a) (p a)
> 
> 
> _test_por_idempotent :: (Boolean b, Equal b)
>   => a -> b -> Test ((a -> Bool) -> a -> Bool)
> _test_por_idempotent _ _ =
>   testName "por(p,p) == p" $
>   \p a -> eq ((por p p) a) (p a)
> 
> 
> _test_por_commutative
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_por_commutative _ =
>   testName "por(p,q) == por(q,p)" $
>   \p q a -> eq ((por p q) a) ((por q p) a)
> 
> 
> _test_por_associative
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_por_associative _ =
>   testName "por(por(p,q),r) == por(p,por(q,r))" $
>   \p q r a -> eq ((por (por p q) r) a) ((por p (por q r)) a)

::::::::::::::::::::
::::::::::::::::::::

And $\pnot$, $\pand$, and $\por$ interact.

:::::: theorem :::::
[]{#thm-demorgan-pnot-pand}[]{#thm-demorgan-pnot-por}[]{#thm-pand-por-distribute}[]{#thm-por-pand-distribute}
Let $A$ be a set. The following hold for all $p,q,r \in \bool^A$.

1. $\pnot(\pand(p,q)) = \por(\pnot(p),\pnot(q))$.
2. $\pnot(\por(p,q)) = \pand(\pnot(p),\pnot(q))$.
3. $\pand(p,\por(q,r)) = \por(\pand(p,q),\pand(p,r))$.
4. $\bor(p,\pand(q,r)) = \pand(\por(p,q),\por(p,r))$.

::: proof ::::::::::
1. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pnot(\pand(p,q))(a) \\
 &     \href{@predicates@#def-pnot}
   = & \bnot(\pand(p,q)(a)) \\
 &     \href{@predicates@#def-pand}
   = & \bnot(\band(p(a),q(a))) \\
 &     \href{@or@#thm-demorgan-not-and}
   = & \bor(\bnot(p(a)),\bnot(q(a))) \\
 &     \href{@predicates@#def-pnot}
   = & \bor(\pnot(p)(a),\bnot(q(a))) \\
 &     \href{@predicates@#def-pnot}
   = & \bor(\pnot(p)(a),\pnot(q)(a)) \\
 &     \href{@predicates@#def-por}
   = & \por(\pnot(p),\pnot(q))(a)
\end{eqnarray*}$$
as needed.
2. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pnot(\por(p,q))(a) \\
 &     \href{@predicates@#def-pnot}
   = & \bnot(\por(p,q)(a)) \\
 &     \href{@predicates@#def-por}
   = & \bnot(\bor(p(a),q(a))) \\
 &     \href{@or@#thm-demorgan-not-or}
   = & \band(\bnot(p(a)),\bnot(q(a))) \\
 &     \href{@predicates@#def-pnot}
   = & \band(\pnot(p)(a),\bnot(q(a))) \\
 &     \href{@predicates@#def-pnot}
   = & \band(\pnot(p)(a),\pnot(q)(a)) \\
 &     \href{@predicates@#def-pand}
   = & \pand(\pnot(p),\pnot(q))(a)
\end{eqnarray*}$$
as needed.
3. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \pand(p,\por(q,r))(a) \\
 &     \href{@predicates@#def-pand}
   = & \band(p(a),\por(q,r)(a)) \\
 &     \href{@predicates@#def-por}
   = & \band(p(a),\bor(q(a),r(a))) \\
 &     \href{@or@#thm-and-or-distribute}
   = & \bor(\band(p(a),q(a)),\band(p(a),r(a))) \\
 &     \href{@predicates@#def-pand}
   = & \bor(\pand(p,q)(a),\band(p(a),r(a))) \\
 &     \href{@predicates@#def-pand}
   = & \bor(\pand(p,q)(a),\pand(p,r)(a)) \\
 &     \href{@predicates@#def-por}
   = & \por(\pand(p,q),\pand(p,r))(a)
\end{eqnarray*}$$
as needed.
4. For all $a \in A$, we have
$$\begin{eqnarray*}
 &   & \por(p,\pand(q,r))(a) \\
 &     \href{@predicates@#def-por}
   = & \bor(p(a),\pand(q,r)(a)) \\
 &     \href{@predicates@#def-pand}
   = & \bor(p(a),\band(q(a),r(a))) \\
 &     \href{@or@#thm-or-and-distribute}
   = & \band(\bor(p(a),q(a)),\bor(p(a),r(a))) \\
 &     \href{@predicates@#def-por}
   = & \band(\por(p,q)(a),\bor(p(a),r(a))) \\
 &     \href{@predicates@#def-por}
   = & \band(\por(p,q)(a),\por(p,r)(a)) \\
 &     \href{@predicates@#def-pand}
   = & \pand(\por(p,q),\por(p,r))(a)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _test_pnot_pand
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_pnot_pand _ =
>   testName "pnot(pand(p,q)) == por(pnot(p),pnot(q))" $
>   \p q a -> eq ((pnot (pand p q)) a) ((por (pnot p) (pnot q)) a)
> 
> 
> _test_pnot_por
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_pnot_por _ =
>   testName "pnot(por(p,q)) == pand(pnot(p),pnot(q))" $
>   \p q a -> eq ((pnot (por p q)) a) ((pand (pnot p) (pnot q)) a)
> 
> 
> _test_pand_por
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_pand_por _ =
>   testName "pand(p,por(q,r)) == por(pand(p,q),pand(p,r))" $
>   \p q r a -> eq ((pand p (por q r)) a) ((por (pand p q) (pand p r)) a)
> 
> 
> _test_por_pand
>   :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
> _test_por_pand _ =
>   testName "por(p,pand(q,r)) == pand(por(p,q),por(p,r))" $
>   \p q r a -> eq ((por p (pand q r)) a) ((pand (por p q) (por p r)) a)

::::::::::::::::::::
::::::::::::::::::::

Implication lifts to predicates.

:::::: definition ::
[]{#def-pimpl}
Let $A$ be a set. We define $\pimpl : \bool^A \times \bool^A \rightarrow \bool^A$ by $$\pimpl(p,q)(a) = \bimpl(p(a),q(a)).$$
::::::::::::::::::::


Testing
-------

Suite:

> _test_predicate ::
>   ( Equal a, Arbitrary a, CoArbitrary a, Show a, TypeName a
>   , TypeName b, Boolean b, Equal b, Arbitrary b
>   ) => a -> b -> Int -> Int -> IO ()
> _test_predicate x p size cases = do
>   testLabel1 "predicate" x
> 
>   let args = testArgs size cases
> 
>   runTest args (_test_pnot_involutive x p)
>   runTest args (_test_pnot_ptrue x p)
>   runTest args (_test_pnot_pfalse x p)
>   runTest args (_test_not_ptrue x p)
>   runTest args (_test_not_pfalse x p)
> 
>   runTest args (_test_pand_pfalse x)
>   runTest args (_test_pand_ptrue x)
>   runTest args (_test_pand_idempotent x)
>   runTest args (_test_pand_commutative x)
>   runTest args (_test_pand_associative x)
> 
>   runTest args (_test_por_ptrue x p)
>   runTest args (_test_por_pfalse x p)
>   runTest args (_test_por_idempotent x p)
>   runTest args (_test_por_commutative x)
>   runTest args (_test_por_associative x)
> 
>   runTest args (_test_pnot_pand x)
>   runTest args (_test_pnot_por x)
>   runTest args (_test_pand_por x)
>   runTest args (_test_por_pand x)

Main:

> main_predicate :: IO ()
> main_predicate = _test_predicate (true :: Bool) (true :: Bool) 20 100