%Authors: Bas van Gijzel and Henrik Nilsson
%See: http://www.cs.nott.ac.uk/~bmv/Dung/index.html
%include arg-preamble.fmt
%including an algorithm for the grounded semantics and show
\section{An implementation of AFs in Haskell}
\label{sec:dung}
\label{sec:Dung}
The abstract argument system, or argumentation frameworks (AFs) as introduced
by Dung~\cite{Dung95} is a simple yet general model capable of capturing
various contemporary approaches to non-monotonic reasoning. It has been the
translation target for a number of modern structured argumentation
models~\cite{Prakken10, Gijzel12, Gijzel11, Brewka11, Modgil12}. This section
gives a large part of the standard definitions of Dung's AFs, including
an algorithm for what is termed the \emph{grounded semantics}, showing how
these definitions effectively can transliterated into (a slightly
stylised version) of Haskell%
\footnote{
The source code for this Section is written in literate Haskell and
can be run as is by a standard Haskell compiler. \\
\url{http://www.cs.nott.ac.uk/~bmv/Code/dunginhaskell_ifl.lhs}}.
The aim 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 in a way that facilitates proving properties about the
implementation. This section can also serve as a tutorial-like introduction to
the implementation of AFs up to grounded semantics. The implementation is
provided as a public library%
\footnote{
See
\url{http://hackage.haskell.org/package/Dung}.},
in the same way as the code for our earlier work discussed in Section 3. Those
interested in a more complete introduction to AFs and alternative semantics
can consult Baroni and Giacomin~\cite{Baroni09}.
An abstract argumentation framework consists of a set of abstract arguments and a binary relation on this set representing \emph{attack}: the notion of one argument conflicting with another. To keep the framework completely general, the notion of argument is abstract; i.e., no assumptions are made as to their nature and they may come from any domain, including informal ones such as ``if it rains you get wet''. Note that the attack relation is not assumed to be symmetric: an attacked argument does not necessarily constitute a counter-attack of the attacking argument.
%%Arguments are kept abstract to be kept completely general and can thus include legal arguments, or even informal arguments, e.g. if it rains you get wet. Attacks represent conflicts between arguments, possibly originating from a logical or intuitive conflict between parts of two arguments; note that this conflict/attack does not have to be symmetric.
%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 \mathit{Args}, \mathit{Att} \rangle$, such that $\mathit{Args}$ is a set of arguments and $\mathit{Att} \subseteq \mathit{Args} \times \mathit{Args}$ is an attack relation on the arguments in $\mathit{Args}$.
\end{definition}
%if False
\begin{code}
module AF where
import Data.List (intersect, (\\))
\end{code}
%endif
While the notion of argument is abstract, we need to assume that it is possible to determine if two arguments are the same or not. For now, we use |String|s to label arguments to that end.
%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 for ease of presentation.
%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 attacking its attacking argument $B$ is captured by $AF_1 = \langle \{A, B, C\}, \{ (A, B), (B, C) \} \rangle$; see Figure~\ref{fig:framework}.
\end{exmp}
\begin{figure}[H]%
\label{fig:framework}
\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}
\noindent
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 \mathit{Args}, attacks \rangle$.
%\end{rem}
The following are standard definitions for AFs such as the acceptability of arguments and admissibility of sets. We use an arbitrary but fixed argumentation framework $AF = \langle \mathit{Args}, \mathit{Att} \rangle$.
\begin{definition}[Set-attacks]
%A set $S \subseteq \mathit{Args}$ of arguments attacks an argument $A \in \mathit{Args}$ iff there exists a $B \in S$ such that $(B,A) \in \mathit{Att}$.
A set $S \subseteq \mathit{Args}$ of arguments attacks an argument $A \in \mathit{Args}$ iff there exists a $Y \in S$ such that $(Y,X) \in \mathit{Att}$.
\end{definition}
For example, in Figure~\ref{fig:reinstate}, $\{A,B\}$ set-attacks $C$, because $B$ attacks $C$ and $B \in \{A,B\}$.
\begin{definition}[Conflict-free]
%A set $S \subseteq \mathit{Args}$ of arguments is called \emph{conflict-free} iff there are no $A$, $B$ in $S$ such that $(A,B) \in \mathit{Att}$.
A set $S \subseteq \mathit{Args}$ of arguments is called \emph{conflict-free} iff there are no $X$, $Y$ in $S$ such that $(X,Y) \in \mathit{Att}$.
\end{definition}
Considering a set of arguments as a position an agent can take with regards to its knowledge, conflict-freeness is often taken as the minimal requirement for a reasonable position. For example, in Figure~\ref{fig:reinstate}, $\{A, C\}$ is a conflict-free set.
%set-attacks $C$, because $B$ attacks $C$ and $B \in \{A,B\}$.
%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 $X \in \mathit{Args}$ is acceptable with respect to a set $S$ of arguments, or alternatively $S$ \emph{defends} $X$, iff for all arguments $Y \in \mathit{Args}$: if $(Y,X) \in \mathit{Att}$ then there exists a $Z \in S$ for which $(Z,Y) \in \mathit{Att}$.
\end{definition}
An argument is acceptable (w.r.t. to some set $S$) if all its attackers are attacked in turn. (Note that although the acceptability is w.r.t. to a set $S$, \emph{all} attackers are taken in account.) For example, in Figure~\ref{fig:reinstate}, $C$ is acceptable w.r.t. $\{A,B,C\}$, because $A$ attacks the only attacker of $C$, i.e. $B$.
Dung defined the semantics of the argumentation frameworks by using the concept of \emph{extensions} and the \emph{characteristic function} of an $AF$. An extension is always a subset of $\mathit{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.
%The semantics Dung defined are defined using the \emph{characteristic function} of an $AF$.
\begin{definition}[Characteristic function]
The \emph{characteristic function} of $AF$, $F_{AF} : 2^{\mathit{Args}} \rightarrow 2^{\mathit{Args}}$, is a function, such that, given a set of arguments $S$, $F_{AF}(S) = \{X \mid X$ \text{is acceptable w.r.t. to} $S\}$.
\end{definition}
For example, in Figure~\ref{fig:reinstate}, $F_{AF}(\emptyset) = \{ A \}$, $F_{AF}(\{A\}) = \{A, C\}$ and $F_{AF}(\{A,B,C\}) = \{A, C\}$.
A conflict-free set of arguments is said to be \emph{admissible} if it is a defendable position, that is, it can defend itself from incoming attacks.
\begin{definition}[Admissibility]
A conflict-free set of arguments $S$ is admissible iff every argument $X$ in $S$ is acceptable with respect to $S$, i.e. $S \subseteq F_{AF}(S)$.
\end{definition}
Note that not every conflict-free set is necessarily admissible. For example, in Figure~\ref{fig:reinstate}, $\{C\}$ is conflict-free but is not an admissible set, since $(B,C) \in \mathit{Att}$ and there is no argument in $\{C\}$ that defends from this attack.
%$S$ is a \emph{complete extension} of a given argumentation framework $AF$ iff $S = F_{AF}(S)$.
Below we define the four standard semantics (extensions) as given by Dung~\cite{Dung95}. A \emph{complete extension} is a set of arguments that is able to defend itself, including all arguments it defends. It is mainly used to define the other extensions. The (unique) \emph{grounded extension} is a minimal standpoint, including only those arguments without attackers and those that are ``completely defended''. A \emph{stable extension} is an extension that is able to attack all arguments not included in it. A \emph{preferred extension} is a relaxation from that requirement, weakening it to an as large as possible set while still being able to defend itself from attacks.
\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 attacking all arguments in $\mathit{Args} \backslash S$.
\end{itemize*}
As proven in Dung~\cite{Dung95}, given that that the domain of $F$ is ordered w.r.t. to set inclusion, $F$ is monotonic. Furthermore, the grounded extension always exists and is unique and there always exists a preferred extension. 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, \mathit{Att} \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 \mathit{Att}$.
%%\item $S$ is called \emph{conflict-free} iff $\neg \exists A, B \in S$ such that $(A,B) \in \mathit{Att}$.
%%\item An argument $A \in Args$ is \emph{acceptable} w.r.t. $S$ iff $\forall B \in Args$, if $(B,A) \in \mathit{Att}$ then $\exists C \in S$ such that $(C,B) \in \mathit{Att}$.
%%\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
x `subset` y = null (x \\ y)
\end{code}
%endif
%%\end{code}
%%TODO: some text
%%\begin{code}
\begin{code}
setAttacks :: Eq arg => DungAF arg -> [arg] ->
arg -> Bool
setAttacks (AF _ att) args arg
= or [y == arg | (x, y) <- att, x `elem` args]
conflictFree :: Eq arg => DungAF arg -> [arg] -> Bool
conflictFree (AF _ att) args
= null [(x, y) | (x, y) <- att, x `elem` args, y `elem` args]
acceptable :: Eq arg => DungAF arg -> arg ->
[arg] -> Bool
acceptable af@(AF _ att) x args
= and [setAttacks af args y | (y, x') <- att, x == x']
f :: Eq arg => DungAF arg -> [arg] -> [arg]
f af@(AF args' _) args
= [x | x <- args', acceptable af x args]
faf :: [AbsArg] -> [AbsArg]
faf = f exampleAF
admissible :: Eq arg => DungAF arg -> [arg] -> Bool
admissible af args = conflictFree 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}
\noindent
The contexts |Eq arg| mean that these functions are only applicable
to types of arguments for which equality has been defined.
%%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.\
%is the approach taken, thus to correctly implement Dung's semantics we would not need a formalisation of fixpoints if we take the labelling based approach.
Given an argumentation framework, we can determine which arguments are
justified by applying an argumentation semantics. However, instead of the
extension based approach, we will take the \emph{labelling-based} approach to
grounded semantics. The labelling based approach is more commonly used in
actual implementations. Opting for this thus facilitates comparisons.
Furthermore, by using the grounded labelling we obviate the need to formalise
fixed points, significantly reducing the amount of work needed when
implementing everything in a theorem prover (see Section \ref{sec:agdadung}).
Formally, the labelling approach is a generalisation of the extension-based
approach~\cite{caminada2007algorithm}, permitting further possibilities than
arguments being either \emph{in} or \emph{out} of an extension; e.g. the state
of an argument might be \emph{undecided}. The grounded labelling can easily be
mapped back to a grounded extension by simply discarding all arguments not
labelled \emph{in}. The algorithm below is commonly used for computing the
grounded labelling~\cite{Modgil09AI}. However, for correctness, the ``if
then'' in the $\exists$ has been changed to ``and''. This small fix
in the algorithm is obvious and has, to our knowledge, always been adopted
in any actual implementation. However, given that formal specifications of
translations are hard to understand even for experts in the field, it does
already demonstrate the importance of formalising complex mathematics.
%such as a translation between argumentation models.
%compare to existing implementations, furthermore to achieve a formalisation in a theorem prover, we do not need a formalisation of fixpoints, severely lightening the work load.
%\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})}
\label{algorithm:grounded}
\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 _ att) arg =
let attackers = [x | (x, y) <- att, arg == y]
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 _ att) arg =
let attackers = [x | (x, y) <- att, arg == y]
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*}
%
Our implementation consists of two parts. The main function for the grounded
labelling, and a helper function implementing the actual algorithm. The latter
has two additional accumulation arguments for keeping track of 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}