CarneadesDSL.lhs

%include arg-preamble.fmt

\begin{code}
module Language.Carneades.CarneadesDSL where

import Prelude hiding (negate)
import Data.Graph.Inductive
import Data.Graph.Analysis
import Data.Map (Map)
import Data.List(nub)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe (fromJust)
\end{code}



As our ultimate goal is a DSL for argumentation theory, we strive for a
realisation in Haskell that mirrors the mathematical model of Carneades
argumentation framework as closely as possible. Ideally, there would be little
more to a realisation than a transliteration. We will thus proceed by
stating the central definitions of Carneades along with our realisation
of them in Haskell. 

\begin{definition}[Arguments]
\label{def:carneadesargs}
Let $\mathcal{L}$ be a propositional language. An \emph{argument} is a
tuple $\langle P, E, c \rangle$ where $P \subset \mathcal{L}$ are its
\emph{premises}, $E \subset \mathcal{L}$ with $P \cap E = \emptyset$
are its \emph{exceptions} and $c \in \mathcal{L}$ is its
\emph{conclusion}. For simplicity, $c$ and all members of $P$ and $E$
must be literals, i.e. either an atomic proposition or a negated
atomic proposition. Let $p$ be a literal. If $p$ is $c$, then the
argument is an argument \emph{pro} $p$. If $p$ is the complement of
$c$, then the argument is an argument \emph{con} $p$.

\end{definition}

In Carneades all logical formulae are literals in propositional logic;
i.e., all propositions are either positive or negative atoms. Taking
atoms to be strings suffice in the following, and propositions can
then be formed by pairing this atom with a Boolean to denote whether
it is negated or not: 
\begin{code} 
type Proposition = (Bool, String)
\end{code} Negation of a proposition is now trivial: 
\begin{code}
negate :: Proposition -> Proposition 
negate (b, p) = (not b, p)
\end{code}

We chose to realise an \emph{argument} as two lists of propositions, its
\emph{premises} and its \emph{exceptions}, and a proposition that
denotes the \emph{conclusion}. 


Arguments are considered equal if their premises, exceptions and
conclusion are equal; thus arguments are identified by their logical
content. The equality instance for |Argument| takes
this into account by comparing the lists as sets.

\begin{code}
data Argument = Arg [Proposition] [Proposition] Proposition
\end{code}  

\begin{code}
--Manual Eq instance for set equality on premises and exceptions
instance Eq Argument where
 (Arg prems excs c) == (Arg prems' excs' c') =  Set.fromList prems == Set.fromList prems' && 
                                                Set.fromList excs == Set.fromList excs' && 
                                                c == c'


showProp :: Proposition -> String
showProp (True, c)   = c
showProp (_    , c)  = '-' : c


instance Show Argument where 
 show (Arg prems excs (True, c))  = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show c
 show (Arg prems excs (_    , c)) = show (map showProp prems) ++ ' ' : '~' : show (map showProp excs) ++ "=>" ++ show ('-' : c)
\end{code}


A set of arguments determines how propositions depend on each other.
Carneades requires that there are no cycles among these dependencies. 
Following Brewka and Gordon~\cite{Brewka10a}, we use a dependency
graph to determine acyclicity of a set of arguments.

\begin{definition}[Acyclic set of arguments]
\label{def:carneadesacyclic}
A set of \emph{arguments} is \emph{acyclic} iff its corresponding
dependency graph is acyclic. The corresponding dependency graph has a
node for every literal appearing in the set of arguments. A node $p$
has a link to node $q$ whenever $p$ depends on $q$ in the sense that
there is an argument pro or con $p$ that has $q$ or $\overline{q}$ in
its set of premises or exceptions.
\end{definition}

Our realisation of a set of arguments is considered abstract for DSL
purposes, only providing a check for acyclicity and a function to
retrieve arguments pro a proposition. We use FGL \cite{Erwig2001} to
implement the dependency graph, forming nodes for propositions and edges
for the dependencies. For simplicity, we opt to keep the graph
also as the representation of a set of arguments.

\begin{code}
-- Note that for practical purposes we do not need to know the following 
-- implementation but can use the abstraction further below
type ArgSet = Gr (Proposition, [Argument]) ()
\end{code}


\begin{spec}
-- abstraction of ArgSet and the operating functions on it
type ArgSet = ...

getArgs     :: Proposition -> ArgSet -> [Argument]  
checkCycle  :: ArgSet -> Bool
\end{spec}


\subsection{Carneades Argument Evaluation Structure}

The main structure of the argumentation model is called a Carneades
Argument Evaluation Structure (CAES):
\begin{definition}[Carneades Argument Evaluation Structure (CAES)] A
\emph{Carneades Argument Evaluation Structure} (CAES) is a triple
\[
\langle arguments, audience, standard \rangle
\]
where $arguments$ is an acyclic set of arguments, and \emph{standard}
is a total function mapping each propositions to to its specific proof
standard. 
\end{definition}
Note that propositions may be associated with \emph{different} proof
standards. This is considered a particular strength of the Carneades
framework. The transliteration into Haskell is immediate:
\begin{code}
newtype CAES = CAES (ArgSet, Audience, PropStandard)
\end{code}

\begin{definition}[Audience]
\label{def:carneadesaudience}
Let $\mathcal{L}$ be a propositional language. An \emph{audience} is a
tuple $\langle$\emph{assumptions}, \emph{weight}$\rangle$, where
$assumptions \subset \mathcal{L}$ is a consistent set of literals
assumed to be acceptable by the audience and \emph{weight} is a 
function mapping arguments to a real-valued weight in the range $[0,1]$.
\end{definition}

This definition is captured by the following Haskell definitions:
\begin{code}
type Audience = (Assumptions, ArgWeight)
type Assumptions = [Proposition]
type ArgWeight = Argument -> Weight
type Weight = Double
\end{code}

Further, as each proposition is associated with a specific proof standard,
we need a mapping from propositions to proof standards:
\begin{code}
type PropStandard = Proposition -> ProofStandard
\end{code}


A proof standard is a function that given a proposition $p$, aggregates
arguments pro and con $p$ and decides whether it is acceptable or not:
\begin{code}
type ProofStandard = Proposition -> CAES -> Bool
\end{code}


This aggregation process will be defined in detail in the next section,
but note that it is done relative to a specific CAES, and note the
cyclic dependence at the type level between |CAES| and |ProofStandard|.

The above definition of proof standard also demonstrates that
implementation in a typed language such as Haskell is a useful way of
verifying definitions from argumentation theoretic models. Our
implementation effort revealed that the original definition as given
in~\cite{Gordon09a} could not be realised as stated, because proof standards
in general not only depend on a set of arguments and the audience,
but may need the whole CAES.



\subsection{Evaluation}

Central to the evaluation of a CAES are the concepts of
\emph{applicability of arguments}, which arguments that should be
taken into account, and \emph{acceptability of propositions}, which
conclusions can be reached under the relevant proof standards, given
the beliefs of a specific audience.


\begin{definition}[Applicability of arguments]
Given a set of arguments and a set of assumptions (in an audience) in a CAES
$C$, then an argument $a = \langle prems, excs, conc \rangle$ is
\emph{applicable} iff
\begin{itemize}
\item
    $p \in prems$ implies $p$ is an assumption or [\,$\overline{p}$ is
    not an assumption and $p$ is acceptable in $C$\,] and
\item
    $e \in excs$ implies $e$ is not an assumption and [\,$\overline{e}$
    is an assumption or $e$ is not acceptable in $C$\,].
\end{itemize}
\end{definition}


\begin{definition}[Acceptability of propositions]
Given a CAES $C$ a proposition $p$ is \emph{acceptable} in $C$ iff
$s(p, C)$ is $true$, where $s$ is the proof standard for $p$.
\end{definition}


Note that these two definitions in general are mutually dependent
because acceptability depends on proof standards, and most sensible
proof standards depend on the applicability of arguments. This is the
reason that Carneades restricts the set of arguments to be acyclic. 
(Specific proof standards are considered in the next section.)
The realisation of applicability and acceptability in Haskell is
straightforward:


\begin{code}
applicable :: Argument -> CAES -> Bool
applicable (Arg prems excns _) caes@(CAES (_, (assumptions, _), _)) 
  = and  $  [(p `elem` assumptions)  ||     (p `acceptable` caes)  |  p <- prems  ]
            ++
            [(e `elem` assumptions)  `nor`  (e `acceptable` caes)  |  e <- excns  ]
      where
          x `nor` y = not (x || y)

acceptable :: Proposition -> CAES -> Bool
acceptable c caes@(CAES (_, _, standard))  
  = c `s` caes 
  where s = standard c
\end{code}



\subsection{Proof standards}

Carneades predefines five proof standards, originating from the work of
Freeman and Farley \cite{Freeman96,Farley95}: \emph{scintilla of
evidence}, \emph{preponderance of the evidence}, \emph{clear and convincing
evidence}, \emph{beyond reasonable doubt} and \emph{dialectical
validity}. Some proof standards depend on constants such as $\alpha$, 
$\beta$, $\gamma$; these are assumed to be defined once and globally.
This time, we proceed to give the definitions directly in Haskell,
as they really only are translitarations of the original definitions.


For a proposition $p$ to satisfy the weakest proof standard, scintilla of
evidence, there should be at least one applicable argument pro $p$ in the CAES:

\begin{code}
scintilla :: ProofStandard
scintilla p caes@(CAES (g, _, _))
 = any (`applicable` caes) (getArgs p g)  
\end{code}


Preponderance of the evidence additionally requires that the maximum weight of
the applicable arguments pro $p$ is greater than the maximum weight of the
applicable arguments con $p$. The weight of zero arguments is taken to
be 0. As the maximal weight of applicable arguments pro and con is a recurring
theme in the definitions of several of the proof standards, we start by
defining those notions:

\begin{code}
maxWeightApplicable :: [Argument] -> CAES -> Weight
maxWeightApplicable as caes@(CAES (_, (_, argWeight), _))
 = foldl max 0 [argWeight a | a <- as, a `applicable` caes] 

maxWeightPro :: Proposition -> CAES -> Weight
maxWeightPro p caes@(CAES (g, _, _))
 = maxWeightApplicable (getArgs p g) caes

maxWeightCon :: Proposition -> CAES -> Weight
maxWeightCon p caes@(CAES (g, _, _))
 = maxWeightApplicable (getArgs (negate p) g) caes
\end{code}


We can then define the proof standard preponderance:

\begin{code}
preponderance :: ProofStandard 
preponderance p caes = maxWeightPro p caes > maxWeightCon p caes   
\end{code}


Clear and convincing evidence strengthen the preponderance constraints by
insisting that the difference between the maximal weights of the pro and con
arguments must be greater than a given positive constant $\beta$, and there
should furthermore be at least one applicable argument pro $p$ that is
stronger than a given positive constant $\alpha$:

\begin{code}
clear_and_convincing :: ProofStandard 
clear_and_convincing p caes
 =  (mwp > alpha) && (mwp - mwc > beta)
  where 
    mwp  =  maxWeightPro p caes
    mwc  =  maxWeightCon p caes
\end{code}


Beyond reasonable doubt has one further requirement still: the maximal
strength of an argument con $p$ needs to be less than a given positive
constant $\gamma$; i.e., there must be no reasonable doubt:

\begin{code}
beyond_reasonable_doubt :: ProofStandard 
beyond_reasonable_doubt p caes
 = clear_and_convincing p caes && (maxWeightCon p caes < gamma)
\end{code}


Finally dialectical validity requires at least one applicable argument pro $p$
and no applicable arguments con $p$:

\begin{code}
dialectical_validity :: ProofStandard 
dialectical_validity p caes   
  = scintilla p caes && not (scintilla (negate p) caes)
\end{code}


\subsection{Convenience functions}
Instead of having to access the data types directly, we provide a set
of functions to provide easy construction of propositions, arguments,
argument sets and sets of assumptions. Together with the definitions
covered so far, this constitute our DSL for constructing Carneades
argumentation models.

\begin{spec}
mkProp         :: String -> Proposition                        
mkArg          :: [String] -> [String] -> String -> Argument   
mkArgSet       :: [Argument] -> ArgSet
mkAssumptions  :: [String] -> [Proposition]
\end{spec}

To construct an audience, we can use native Haskell tupling to combine
a set of assumptions and a weight function, exactly how it would be
done in the Carneades model.

\begin{spec}
audience :: Audience
audience = (assumptions, weight) 
\end{spec}

Similar methods can be employed to define a CAES or the weight
function, as will be shown in the next subsection.

Finally, we provide a set of functions to retrieve arguments for a
specific proposition or all arguments/propositions from a given
argument sets; and functions to retrieve the (not) applicable
arguments or (not) acceptable propositions from a CAES.

\begin{spec}
getArgs             :: Proposition  -> ArgSet  ->  [Argument]
getAllArgs          :: ArgSet                  ->  [Argument]
getProps            :: ArgSet                  ->  [Proposition]
applicableArgs      :: CAES                    ->  [Argument]
nonApplicableArgs   :: CAES                    ->  [Argument]
acceptableProps     :: CAES                    ->  [Proposition]
nonAcceptableProps  :: CAES                    ->  [Proposition]
\end{spec}

\begin{code}
getAllArgs :: ArgSet -> [Argument]
getAllArgs g = nub $ concatMap (snd . snd) (labNodes g)

getProps :: ArgSet -> [Proposition]
getProps g = map (fst . snd) (labNodes g)

applicableArgs :: CAES -> [Argument]
applicableArgs caes@(CAES (argSet, _, _)) = filter (`applicable` caes) (getAllArgs argSet)  

nonApplicableArgs :: CAES -> [Argument]
nonApplicableArgs caes@(CAES (argSet, _, _)) = filter (not . (`applicable` caes)) (getAllArgs argSet)

acceptableProps :: CAES  -> [Proposition]
acceptableProps c@(CAES (argSet, _, _)) = filter (`acceptable` c) (getProps argSet)

nonAcceptableProps :: CAES  -> [Proposition]
nonAcceptableProps c@(CAES (argSet, _, _)) = filter (not . (`acceptable` c)) (getProps argSet)
\end{code}


\begin{code}
contextP :: Proposition -> AGraph -> [Context (Proposition, [Argument]) ()]
contextP p = gsel (\ (_, _, a, _) -> fst a == p) 
     
getArgs :: Proposition -> AGraph -> [Argument]  
getArgs p g 
  =  case contextP p g of
       []                          -> []
       ((_, _, (_, args), _) : _)  -> args
\end{code}



\subsection{Graph construction}
We associate a graph along with a |Map| that stores the node number for every |Proposition| to make construction of the |AGraph| easier.

\begin{code}
type AGraph = ArgSet
type PropNode = LNode (Proposition, [Argument])
type AssociatedGraph = (AGraph, Map Proposition Node)
\end{code}

An argument graph is then constructed as following:
\begin{code}
mkArgSet :: [Argument] -> ArgSet
mkArgSet = mkArgGraph

mkArgGraph :: [Argument] -> AGraph
mkArgGraph = fst . foldr addArgument (empty, Map.empty)
\end{code}

Carneades uses the following definition for acyclicity:
\begin{definition}[Acyclic set of arguments]
\label{def:carneadesacyclic}
A list of arguments is acyclic iff its corresponding dependency graph is acyclic. The corresponding dependency graph has nodes for every literal appearing in the list of arguments. A node $p$ has a directed link to node $q$ whenever $p$ depends on $q$ in the sense that there is an argument pro or con $p$ that has $q$ or $\overline{q}$ in its list of premises or exceptions.
\end{definition}

So when we add an argument |(Arg premises exceptions conclusion)| to our graph, we need to add both the conclusion and its negate to the graph, adding edges for both to all premises and exceptions while adding the argument to the list of arguments for |conclusion| as well. 

\begin{code}
addArgument :: Argument -> AssociatedGraph -> AssociatedGraph
addArgument arg@(Arg prem exc c) gr  = 
  let  deps             =  prem ++ exc
       (gr',  nodeNr)   =  addArgument' arg gr
       (gr'', nodeNr')  =  addNode (negate c) gr'
  in addEdges nodeNr' deps $ addEdges nodeNr deps gr'' 
\end{code}


\begin{code}
addToContext :: Argument -> (Context (Proposition, [Argument]) (), AGraph) -> AGraph
addToContext arg ((adjb, n, (p, args), adja), g') = (adjb, n, (p, arg:args), adja) & g'

unsafeMatch :: Graph gr => Node -> gr a b -> (Context a b, gr a b)
unsafeMatch n g = mapFst fromJust $ match n g
\end{code}

Add an argument to the graph. If there is no node present yet for the conclusion insert it, in both cases add the argument to the context of the conclusion.
\begin{code}
addArgument' :: Argument -> AssociatedGraph -> (AssociatedGraph, Node)
addArgument' arg@(Arg _ _ c) (g, m) 
 = case Map.lookup c m of 
       Nothing  ->  ((insNode (nodeNr, (c, [arg])) g, 
                       Map.insert c nodeNr m), 
                         nodeNr)
       Just n   ->  ((addToContext arg (unsafeMatch n g), 
                       m), 
                         n) 
  where nodeNr = Map.size m + 1
\end{code}

Add a proposition to the graph.
\begin{code}
addNode :: Proposition -> AssociatedGraph -> (AssociatedGraph, Node)
addNode p gr@(g,m) 
 =  case Map.lookup p m of 
       Nothing -> ((insNode (nodeNr, (p, [])) g, Map.insert p nodeNr m), nodeNr)
       Just n  -> (gr, n)
    where nodeNr = Map.size m + 1
\end{code}

For a specific node, add an edge for every |Proposition| in the list for the given graph.
\begin{code}
addEdges :: Node -> [Proposition] -> AssociatedGraph -> AssociatedGraph
addEdges n ps (g, m) = addEdges' n (map (fromJust . flip Map.lookup m') ps)  (g', m')-- addEdges' c n ps (g', m')
 where  nodeNr    = Map.size m + 1 
        newProps  = filter ( (== Nothing) . flip Map.lookup m) ps  
        g'        = insNodes (propsToNodes newProps nodeNr) g
        m'        = Map.union m . Map.fromList $ zip newProps [nodeNr..]
\end{code}


Generate unlabelled edges from a |Node| to a list of |Node|s and add it to the graph.
\begin{code}
addEdges' :: Node -> [Node] -> AssociatedGraph -> AssociatedGraph
addEdges' c ps (g, m) = (insEdges edges' g, m)
 where  edges' = map (genEdge c) ps
        genEdge k l = (k, l, ())

\end{code}

Some useful functions.
\begin{code}
propsToNodes :: [Proposition] -> Node -> [PropNode]
propsToNodes ps n = zip [n..] (map (\ p -> (p, [])) ps)

checkCycle :: AGraph -> Bool
checkCycle = not . null . cyclesIn

mkProp :: String -> Proposition
mkProp ('-':s)  = mapFst not (mkProp s)
mkProp s        = (True, s)

mkAssumptions :: [String] -> [Proposition]
mkAssumptions = map mkProp

mkArg :: [String] -> [String] -> String -> Argument
mkArg ps es c = Arg (map mkProp ps) (map mkProp es) (mkProp c)
\end{code}

Globally predefined alpha, beta and gamma. 
\begin{code}
alpha, beta, gamma :: Double
alpha  =  0.4
beta   =  0.3
gamma  =  0.2
\end{code}