%include arg-preamble.fmt
\section{An implementation of AFs\\ in Haskell}
The abstract argument system, or argumentation framework (AF) as introduced by Dung~\cite{Dung95} is a very simple, but general model that is able to capture various contemporary approaches to non-monotonic reasoning. It has also been the translation target for many modern structured argumentation models~\cite{Prakken10, Gijzel12, Gijzel11, Brewka11, Modgil12} that have been introduced later in the literature. In this section we will give a significant part of the standard definitions of Dung's AFs, including an algorithm for the grounded semantics and show how these definitions can be almost immediately translated into (a slightly stylised version) of the functional programming language, Haskell\footnote{The source code of this Section, see\\ \texttt{http://www.cs.nott.ac.uk/\~{}bmv/Code/dunginhaskell_away_day.lhs}, is written in literate Haskell and can immediately be run by a standard Haskell compiler.}. The purpose of this section is to show how a functional programming language such as Haskell can be used to quickly implement a prototype of an argumentation model and to set up the possibility for proving properties of this implementation. This section can also serve as a tutorial like introduction to the implementation of AFs up to grounded semantics.
%Text of the actual paper:
%We will not be able to fully discuss AFs nor can we handle Haskell syntax, so for a more in depth introduction to abstract argumentation see Baroni and Giacomin~\cite{Baroni09} and for Haskell one can consult one of the standard textbooks~\cite{Hutton07, Lipovaca11}.
An abstract argumentation framework consists of abstract arguments and a binary relation representing attack.
%The argument's internal structure is kept open for different instantiations; allowing arguments to be internally structured as graphs or trees, and allowing to use different types of inferences in the arguments. Moreover, the attack relation can be instantiated when interpreted as abstracting from the use of preferences, leading to a notion of defeat between arguments\footnote{For an overview of the use of preferences in determining the attack relation cf. Section 3.3 of Prakken~\cite{Prakken10}.}.
\begin{definition}{Abstract argumentation framework}
An \emph{abstract argumentation framework} is a tuple $ \langle Args, Def \rangle$, such that $Args$ is a set of arguments and $Def \subseteq Args \times Args$ is a defeat relation on the arguments in $Args$.
\end{definition}
%if False
\begin{code}
module AF where
import Data.List (intersect, (\\))
\end{code}
%endif
It is important to note that the type of argument is left abstract in the definition above, allowing for possible instantiations of argument by other frameworks such as ASPIC$^+$~\cite{Prakken10}. Several of the following definitions however, will need to have some notion of equality on arguments to be able to make the needed comparisons. For now, we use |String|s to just label arguments.
%deriving (Eq, Show)
\begin{code}
data DungAF arg = AF [arg] [(arg, arg)]
deriving (Show)
type AbsArg = String
\end{code}
Note that we use lists instead of sets to allow for an easier presentation.
%In an AF, arguments and attacks are sets, we however chose to encode both as lists to allow for an easier presentation.
\begin{exmp}
An example (abstract) argumentation framework containing three arguments where the argument $C$ \emph{reinstates} the argument $A$ by defeating its defeating argument $B$ is captured by $AF_1 = \langle \{a,b,c\}, \{ (a,b), (b, c) \} \rangle$.
\end{exmp}
%\begin{figure}[H]%
%\centering
\begin{center}
$\xymatrix@@1{
A\ar[r] & B \ar[r] & C }$
%\caption{An (abstract) argumentation framework}%demonstrating reinstatement
%\label{fig:reinstate}%
\end{center}
%\end{figure}
And in Haskell:
%-- Example AF: |A -> B -> C|
\begin{code}
a, b, c :: AbsArg
a = "A"
b = "B"
c = "C"
exampleAF :: DungAF AbsArg
exampleAF = AF [a, b, c] [(a, b), (b, c)]
\end{code}
%if False
\begin{code}
-- Example AF: |A <-> B|
exampleAF2 :: DungAF AbsArg
exampleAF2 = AF [a, b] [(a, b), (b, a)]
\end{code}
%endif
%\begin{rem}
%In the following definitions we will use an arbitrary but fixed argumentation framework $AF = \langle Args, defeats \rangle$.
%\end{rem}
We now quickly give a few standard definitions for AFs such as the acceptability of arguments and admissibility of sets. We will use an arbitrary but fixed argumentation framework $AF = \langle Args, defeats \rangle$.
\begin{definition}[Conflict-free]
A set $S \subseteq Args$ of arguments attacks an argument $A \in Args$ iff there exists a $B \in S$ such that $(B,A) \in Def$.
\end{definition}
\begin{definition}[Conflict-free]
A set $S \subseteq Args$ of arguments is called \emph{conflict-free} iff there is no $A$, $B$ in $S$ such that $(A,B) \in Def$.
\end{definition}
%An argument is acceptable w.r.t. a set of arguments $S$ if it can defend itself from
\begin{definition}[Acceptability]
\label{def:dungaccept}
An argument $A \in Args$ is acceptable with respect to a set $S$ of arguments, or alternatively $S$ \emph{defends} $A$, iff for all arguments $B \in S$: if $(B,A) \in Def$ then there is a $C \in S$ for which $(C,B) \in Def$.
\end{definition}
The semantics Dung defined for an argumentation framework can be defined by using the \emph{characteristic function} of an $AF$.
\begin{definition}[Characteristic function]
The \emph{characteristic function} of $AF$, $F_{AF} : 2^{Args} \rightarrow 2^{Args}$, is a function, such that, given a conflict-free set of arguments $S$, $F_{AF}(S) = \{A \mid A$ \text{is acceptable w.r.t. to} $S\}$.
\end{definition}
A conflict-free set of arguments is said to be \emph{admissible} if it is a defendable position.
\begin{definition}[Admissibility]
A conflict-free set of arguments $S$ is admissible iff every argument $A$ in $S$ is acceptable with respect to $S$, i.e. $S \subseteq F_{AF}(S)$.
\end{definition}
Dung defined the semantics of the argumentation frameworks by using the concept of \emph{extensions}. An extension is always a subset of $Args$, and can intuitively be seen as a set of arguments that are acceptable when taken together. We will just discuss the grounded extension, but for completeness we give the four standard semantics defined by Dung.
%$S$ is a \emph{complete extension} of a given argumentation framework $AF$ iff $S = F_{AF}(S)$.
\begin{definition}[Extensions]
Given a conflict-free set of arguments $S$, argumentation framework $AF$ and if the domain of $F$ is ordered with respect to set inclusion then:
\begin{itemize*}
\item $S$ is a \emph{complete extension} iff $S = F_{AF}(S)$.
\item $S$ is a \emph{grounded extension} iff it is the least fixed point of $F_{AF}$.
\item $S$ is a \emph{preferred extension} iff it is a maximal fixed point of $F_{AF}$.
\item $S$ is a \emph{stable extension} iff it is a preferred extension defeating all arguments in $Args \backslash S$.
\end{itemize*}
Alternatively, the grounded and preferred extensions can respectively be characterised as the smallest and a maximal complete extension.
\end{definition}
%%\begin{definition}
%%\label{def:dungaccept}
%%Let $AF = \langle Args, Def \rangle$ and $S \subseteq Args$.
%%\begin{enumerate*}
%%\item $S$ attacks an argument $A \in Args$ iff $\exists B \in S$ such that $(B,A) \in Def$.
%%\item $S$ is called \emph{conflict-free} iff $\neg \exists A, B \in S$ such that $(A,B) \in Def$.
%%\item An argument $A \in Args$ is \emph{acceptable} w.r.t. $S$ iff $\forall B \in Args$, if $(B,A) \in Def$ then $\exists C \in S$ such that $(C,B) \in Def$.
%%\item The \emph{characteristic function} of an $AF$, $F_{AF}$ is a function such that:
%%\begin{itemize}
%%\item $F_{AF} : 2^{Args} \rightarrow 2^{Args}$,
%%\item $F_{AF}(S) = \{A \mid A$ is acceptable w.r.t. to $S\}$.
%%\end{itemize}
%%\item A conflict-free set of arguments $S$ is \emph{admissible} iff every argument $A \in S$ is acceptable w.r.t. $S$, i.e. $S \subseteq F_{AF}(S)$.
%%\end{enumerate*}
%%\end{definition}
%%
In our Haskell implementation of these definitions we resort to a few standard library functions: |null| is a function takes a list as an argument and returns a |True| if it is empty and |False| otherwise, |and| is the equivalent to $\bigwedge$ on lists, while |or| is the equivalent to $\bigvee$ on lists.
%%\begin{spec}
%%-- 'and' returns the conjunction of a Boolean list. For the result to be
%%-- 'True', the list must be finite; 'False', however, results from a 'False'
%%-- value at a finite index of a finite or infinite list.
%%and :: [Bool] -> Bool
%%and [] = True
%%and (x:xs) = x && and xs
%%
%%-- 'or' returns the disjunction of a Boolean list. For the result to be
%%-- 'False', the list must be finite; 'True', however, results from a 'True'
%%-- value at a finite index of a finite or infinite list.
%%or :: [Bool] -> Bool
%%or [] = False
%%or (x:xs) = x || or xs
%%
%%-- Test whether a list is empty.
%%null :: [a] -> Bool
%%null [] = True
%%null (_:_) = False
%%
%%
%%\end{spec}
%if False
\begin{code}
subset :: Eq a => [a] -> [a] -> Bool
a `subset` b = null (a \\ b)
\end{code}
%endif
%%\end{code}
%%TODO: some text
%%\begin{code}
\begin{code}
setAttacks :: Eq arg => DungAF arg -> [arg] ->
arg -> Bool
setAttacks (AF _ def) args arg
= or [b == arg | (a, b) <- def, a `elem` args]
conflictFree :: Eq arg => DungAF arg -> [arg] -> Bool
conflictFree (AF _ def) args
= null [(a,b) | (a, b) <- def, a `elem` args, b `elem` args]
acceptable :: Eq arg => DungAF arg -> arg ->
[arg] -> Bool
acceptable af@(AF _ def) a args
= and [setAttacks af args b | (b, a') <- def, a == a']
f :: Eq arg => DungAF arg -> [arg] -> [arg]
f af@(AF args' _) args
= [a | a <- args', acceptable af a args]
faf :: [AbsArg] -> [AbsArg]
faf = f exampleAF
admissible :: Eq arg => DungAF arg -> [arg] -> Bool
admissible af args = args `subset` f af args
groundedF :: Eq arg => ([arg] -> [arg]) -> [arg]
groundedF f = groundedF' f []
where groundedF' f args
| f args == args = args
| otherwise = groundedF' f (f args)
\end{code}
Then as expected:
\begin{spec}
groundedF faf
> ["A","C"]
\end{spec}
Note that by the required |Eq arg =>|, Haskell forces us to see that we need an equality on arguments to be able implement these functions.
%%1.\ &\LA_0 = (\emptyset, \emptyset, \emptyset) \\
%%2.\ &\textbf{repeat} \\
%%3.\ &in(\LA_{i+1}) = in(\LA_i) \cup \{ x \mid &&x \text{ is not labelled in } \LA_i, \\
%% & &&\forall y : \text{if } y \R x \text{ then } y \in out(\LA_i) \} \\
%%4.\ &out(\LA_{i+1}) = out(\LA_i) \cup \{ x \mid &&x \text{ is not labelled in } \LA_i, \\
%% & &&\exists y : \text{if } y \R x \text{ then } y \in in(\LA_{i+1}) \} \\
%%5.\ &\textbf{until }\LA_{i+1} = \LA_i\\
%%6.\
Given an argumentation framework, we can determine which arguments are justified by applying an argumentation semantics. However in contrast to the succise extension based approach, we will take the \emph{labelling-based} approach to grounded semantics. The labelling based approach is more commonly used in actual implementation and to correctly formalise Dung's semantics we would not need a formalisation of fixpoints if we take the labelling based approach. In the below algorithm, for correctness, the ``if then'' in the $\exists$ has been changed to ``and''. Although the fix here is obvious, it does make a case in point for formalisation of more complex mathematics such as a translation between argumentation models.
%\begin{algorithm}{Algorithm for grounded labelling}
%\begin{algorithmic}[1]% Taken from the algorithmicx package documentation
% $\LA_0 = (\emptyset, \emptyset, \emptyset)$
% \Repeat
% \State $in(\LA_{i+1})\gets in(\LA_i) \cup $ \\
% \State $\{ x \mid x \text{ is not labelled in } \LA_i, \forall y : \text{if } y \R x \text{ then } y \in out(\LA_i) \}$
% \Until{$\LA_{i+1} = \LA_i$}
%\end{algorithmic}
%\end{algorithm}
%\text{if } y \R x \text{ then } y \in \mathrm{in}(\LA_{i+1}) \}$
\begin{algorithm}{Algorithm for grounded labelling (Algorithm 6.1 of~\cite{Modgil09AI})}
\begin{enumerate*}
\item $\LA_0 = (\emptyset, \emptyset, \emptyset)$
\item \textbf{repeat}
\item $\mathrm{in}(\LA_{i+1}) = \mathrm{in}(\LA_i) \cup \{ x \mid x \text{ is not labelled in } \LA_i,$ \\
$\forall y : \text{if } y \R x \text{ then } y \in \mathrm{out}(\LA_i) \} $
\item $\mathrm{out}(\LA_{i+1}) = \mathrm{out}(\LA_i) \cup \{ x \mid x \text{ is not labelled in } \LA_i,$ \\
$\exists y : y \R x \text{ and } y \in \mathrm{in}(\LA_{i+1}) \}$
\item \textbf{until }$\LA_{i+1} = \LA_i$
\item $\LA_{\G} = (\mathrm{in}(\LA_i), \mathrm{out}(\LA_i), \A - (\mathrm{in}(\LA_i) \cup \mathrm{out}(\LA_i)))$
\end{enumerate*}
%From Chapter 6.4.1, Algorithm 6.1: Proof Theories and Algorithms for Abstract Argumentation Frameworks, of Argumentation in AI~\cite{Modgil09AI}.
\end{algorithm}
The Haskell equivalent to a labelling:
%-- Labelling:
\begin{code}
data Status = In | Out | Undecided
deriving (Eq, Show)
\end{code}
For our Haskell implementation, we will first translate the two conditions for $x$ containing quantifiers in line 3 and 4.
%, can intuitively be seen as $x$ is unattacked/$x$ is attacked respectively.
\begin{code}
-- if all attackers are |Out|
unattacked :: Eq arg => [arg] ->
DungAF arg -> arg -> Bool
unattacked outs (AF _ def) arg =
let attackers = [a | (a, b) <- def, arg == b]
in null (attackers \\ outs)
\end{code}
%in null $ attacker \\ outs
%Similarly,
\begin{code}
-- if there exists an attacker that is |In|
attacked :: Eq arg => [arg] ->
DungAF arg -> arg -> Bool
attacked ins (AF _ def) arg =
let attackers = [a | (a, b) <- def, arg == b]
in not (null (attackers `intersect` ins))
\end{code}
% in not . null $ attackers `intersect` ins
%1.\ &\\
%2.\ & \\
%3.\ &in(\LA_{i+1}) = &in(\LA_i) \cup \\
% &\ &\{ x \mid &&x \text{ is not labelled in } \LA_i, forall y : \text{if } y \R x \text{ then } y \in out(\LA_i) \} \\
%\end{align*}
%
We split the implementation in two parts. A function for the grounded labelling which can immediately be applied to an AF, and a function actually implementing the algorithm, which has an additional two arguments that accumulate the |In|s and |Out|s.
%Compute the grounded labelling for a Dung argumentation framework, returning a list of arguments with respective statuses.
%Based on section 4.1 of Proof Theories and Algorithms for Abstract Argumentation Frameworks by Modgil and Caminada in ...
\begin{code}
grounded :: Eq arg => DungAF arg -> [(arg, Status)]
grounded af@(AF args _) = grounded' [] [] args af
\end{code}
\begin{code}
grounded' :: Eq a => [a] -> [a] ->
[a] -> DungAF a -> [(a, Status)]
grounded' ins outs [] _
= map (\ x -> (x, In)) ins
++ map (\ x -> (x, Out)) outs
grounded' ins outs args af =
let newIns = filter (unattacked outs af) args
newOuts = filter (attacked ins af) args
in if null (newIns ++ newOuts)
then map (\ x -> (x, In)) ins
++ map (\ x -> (x, Out)) outs
++ map (\ x -> (x, Undecided)) args
else grounded' (ins ++ newIns)
(outs ++ newOuts)
(args \\ (newIns ++ newOuts))
af
\end{code}
Then as expected:
\begin{spec}
grounded exampleAF
> [("A",In),("C",In),("B",Out)]
\end{spec}
%if False
\begin{spec}
grounded exampleAF2
> [("A",Undecided),("B",Undecided)]
\end{spec}
%endif
Finally, the grounded extension can be defined by returning only those arguments that are In from the grounded labelling.
\begin{code}
groundedExt :: Eq arg => DungAF arg -> [arg]
groundedExt af = [arg | (arg, In) <- grounded af]
\end{code}