CarneadesDSL (empty) → 0.9

raw patch · 5 files changed

+731/−0 lines, 5 filesdep +Graphalyzedep +basedep +containerssetup-changed

Dependencies added: Graphalyze, base, containers, fgl

Files

• CarneadesDSL.cabal +32/−0
• LICENSE +30/−0
• Language/Carneades/CarneadesDSL.lhs +521/−0
• Language/Carneades/ExampleCAES.lhs +146/−0
• Setup.hs +2/−0

@@ -0,0 +1,32 @@+name:          CarneadesDSL+category:      Argumentation, Embedded, AI+version:       0.9+license:       BSD3+cabal-version: >= 1.2+license-file:  LICENSE+author:        Bas van Gijzel, Henrik Nilsson+maintainer:    Bas van Gijzel <bmv@cs.nott.ac.uk>+stability:     experimental+homepage:      http://www.cs.nott.ac.uk/~bmv/CarneadesDSL/+copyright:     Copyright (C) 2012 Bas van Gijzel+synopsis:      An implementation and DSL for the Carneades argumentation model.+description:   An implementation and domain specific language for the Carneades+               argumentation model. See Haskell Gets Argumentative in the +               Proceedings of Symposium on Trends in Functional Programming +               (TFP 2012) by Bas van Gijzel and Henrik Nilsson or the +               maintainer's website. +build-type:    Simple++Library+  build-depends:+    base                   >= 4        && < 5,+    containers             >= 0.3      && < 0.6,+    fgl                    >= 5.4.2.4  && < 5.5, +    Graphalyze             >= 0.13.0.1 && < 0.14+    ++  exposed-modules:+    Language.Carneades.CarneadesDSL+    Language.Carneades.ExampleCAES+    +

@@ -0,0 +1,30 @@+Copyright (c)2012, Bas van Gijzel, Henrik Nilsson++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Bas van Gijzel, Henrik Nilsson, nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,521 @@+%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}

@@ -0,0 +1,146 @@+%include arg-preamble.fmt++\begin{code}+module Language.Carneades.ExampleCAES where++import Prelude hiding (negate)+import Language.Carneades.CarneadesDSL+\end{code}++++\subsection{Implementing a CAES}++This subsection shows how an argumentation theorist given the+Carneades DSL developed in this section quickly and at a high level of+abstraction can implement a Carneades argument evaluation structure+and evaluate it as well. We revisit the arguments from Section+\ref{sec:background} and assume the following:++\begin{align*}+\mathit{arguments} &= \{\mathit{arg1}, \mathit{arg2}, \mathit{arg3} \}, \\+\mathit{assumptions} &= \{\mathit{kill}, \mathit{witness}, \mathit{witness2}, \mathit{unreliable2} \},\\+\mathit{standard(intent)} &= \mathit{beyond}\textit{-}\mathit{reasonable}\textit{-}\mathit{doubt}, \\+\mathit{standard(x)} &= \mathit{scintilla},\ \textrm{for any other proposition x}, \\+\alpha &= 0.4,\ \beta = 0.3,\ \gamma = 0.2.+\end{align*}++Note that since alpha, beta and gamma are assumed they are global, they are predefined in |CarneadesDSL.lhs|.+++++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%Start example code%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+\begin{spec}+alpha, beta, gamma :: Double+alpha  =  0.4+beta   =  0.3+gamma  =  0.2+\end{spec}+++Arguments and the argument graph are constructed by calling |mkArg| and+|mkArgSet| respectively:+\begin{code}+arg1, arg2, arg3 :: Argument +arg1 = mkArg ["kill", "intent"] [] "murder"+arg2 = mkArg ["witness"] ["unreliable"] "intent"+arg3 = mkArg ["witness2"] ["unreliable2"] "-intent"++argSet :: ArgSet+argSet = mkArgSet [arg1, arg2, arg3]+\end{code}++The audience is implemented by defining the |weight| function and calling+|mkAssumptions| on the propositions which are to be assumed. The audience is+just a pair of these:+++\begin{code}+weight :: ArgWeight+weight  arg  |  arg == arg1  = 0.8+weight  arg  |  arg == arg2  = 0.3+weight  arg  |  arg == arg3  = 0.8+weight  _                    = error "no weight assigned"++assumptions :: [Proposition]+assumptions = mkAssumptions ["kill", "witness", "witness2","unreliable2"] ++audience :: Audience+audience = (assumptions, weight) +\end{code}++Finally, after assigning proof standards in the |standard| function, we form+the CAES from the argument graph, audience and function |standard|:+\begin{code}+standard :: PropStandard +standard  (_, "intent")  = beyond_reasonable_doubt+standard  _              = scintilla ++caes :: CAES +caes = CAES (argSet, audience, standard)+\end{code}++We can now try out the argumentation structure. ++\begin{spec}+getAllArgs argSet+ > [  ["witness2"]       ~["unreliable2"]   =>  "-intent",+      ["witness"]        ~["unreliable"]    =>  "intent",+      ["kill","intent"]  ~[]                =>  "murder"]+\end{spec}++Then, as expected, there are no applicable arguments for $\mathit{-intent}$, +since $\mathit{unreliable2}$ is an exception, but there is an applicable +argument for $\mathit{intent}$, namely $\mathit{arg2}$:+++\begin{spec}+filter (`applicable` caes) $ getArgs (mkProp "intent") argSet+ > [["witness"]=>"intent"]++filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet+ >  []+\end{spec}++Despite the applicable argument $\mathit{arg2}$ for $\mathit{intent}$,+$\mathit{murder}$ should not be acceptable, because the weight of+$\mathit{arg2} < \alpha$. However, note that we can't reach the opposite+conclusion either:++\begin{spec}+acceptable (mkProp "murder") caes+ > False+acceptable (mkProp "-murder") caes+ > False+\end{spec}++As a further extension, one could for example imagine giving an+argumentation theorist the means to see a trace of the derivation of+acceptability. It would be straightforward to add further primitives+to the DSL and keeping track of intermediate results for+acceptability and applicability to achieve this.++\begin{code}+testAppIntent :: [Argument]+testAppIntent = filter (`applicable` caes) $ getArgs (mkProp "intent") argSet        ++testAppNotIntent :: [Argument]+testAppNotIntent = filter (`applicable` caes) $ getArgs (mkProp "-intent") argSet        ++testAppMurder :: [Argument]+testAppMurder = filter (`applicable` caes) $ getArgs (mkProp "murder") argSet        ++testAppNotMurder :: [Argument]+testAppNotMurder = filter (`applicable` caes) $ getArgs (mkProp "-murder") argSet        ++testMurder  :: Bool+testMurder  = acceptable (mkProp "murder") caes++testNotMurder  :: Bool+testNotMurder  = acceptable (mkProp "-murder") caes+\end{code}+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%End example code%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain