-- Authors: Bas van Gijzel and Henrik Nilsson
-- See: http://www.cs.nott.ac.uk/~bmv/CarneadesIntoDung/index.html
module AF2 where
import Data.List as List
open import Data.List using (List ; _∷_ ; [] ; any ; null ; filter ) renaming (_++_ to _++L_)
open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ)
open import Data.String using (String)
import Data.String as String using (_==_)
open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Function
open import Data.Vec hiding ([_])
open import Data.Nat
open import Data.Nat.Properties
open import Algebra
open SemiringSolver
private module CS = CommutativeSemiring commutativeSemiring
data DungAF (A : Set) : Set where
AF : List A → List (A × A) → DungAF A
-- The simplest type of argument is an argument just identifiable by its name
-- equivalent to |type AbsArg = String| in Haskell
AbsArg = String
a : AbsArg
a = "A"
b : AbsArg
b = "B"
c : AbsArg
c = "C"
-- an AF such that: a1 → a2 → a3
exampleAF : DungAF AbsArg
exampleAF = AF (a ∷ b ∷ c ∷ []) ( (a , b) ∷ (b , c) ∷ [])
-- an AF such that: a1 ↔ a2
exampleAF2 : DungAF AbsArg
exampleAF2 = AF (a ∷ b ∷ []) ( (a , b) ∷ (b , a) ∷ [])
-- When computing extension using labelling we use In, Out and Undecided as the labels.
data Status : Set where
In : Status
Out : Status
Undecided : Status
-- Given an equality function on its elements, compute the intersection of 2 lists.
intersectBy : {A : Set} → (A → A → Bool) → List A → List A → List A
intersectBy _ [] _ = []
intersectBy _ _ [] = []
intersectBy eq xs ys = filter (λ x → any (eq x) ys) xs
-- Given an equality function on its elements, delete the first occurence of x in a given list.
deleteBy : {A : Set} → (A → A → Bool) → A → List A → List A
deleteBy _ _ [] = []
deleteBy _≡_ x (y ∷ ys) = if x ≡ y then ys else y ∷ deleteBy _≡_ x ys
-- | The 'deleteFirstsBy' function takes a predicate and two lists and
-- returns the first list with the first occurrence of each element of
-- the second list removed.
deleteFirstsBy : {A : Set} → (A → A → Bool) → List A → List A → List A
deleteFirstsBy _≡_ = List.foldl (flip (deleteBy _≡_))
-- Given an equality function, a list of arguments (from a certain AF) that are already considered In,
-- compute whether an argument (arg) is attacked.
attacked : {A : Set} → (A → A → Bool) → List A → DungAF A → A → Bool
attacked _≡_ ins (AF _ def) arg = not
(null
(intersectBy _≡_
(List.map proj₁ (filter ((λ x → x ≡ arg) ∘ proj₂) def)) ins))
-- Given an equality function, a list of arguments (from a certain AF) that are already considered,
-- compute whether an argument (arg) is attacked.
unattacked : {A : Set} → (A → A → Bool) → List A → DungAF A → A → Bool
unattacked _≡_ outs (AF _ def) arg = null
(deleteFirstsBy _≡_
(List.map proj₁ (filter ((λ x → x ≡ arg) ∘ proj₂) def)) outs)
-- Grounded labelling helper function using Lists.
-- 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
-- The Agda termination checker marks it as possibly non-terminating.
-- Problem here is the following:
-- ins, outs keep track of the currently already status assigned arguments
-- args contains the arguments still to be assigned a status (if possible)
-- However, when having decided the status of a few arguments, we want to remove it from args,
-- however it is not clear to Agda that args is structurally decreasing (we do not match structurally on args).
groundedList : {A : Set} → (A → A → Bool) → List A → List A → List A → DungAF A → List (A × Status)
groundedList _ ins outs [] _ = List.map (λ x → (x , In)) ins ++L List.map (λ x → (x , Out)) outs
groundedList _≡_ ins outs args af with filter (unattacked _≡_ outs af) args |
filter (attacked _≡_ ins af) args |
filter (unattacked _≡_ outs af) args ++L
filter (attacked _≡_ ins af) args
... | _ | _ | [] = List.map (λ x → x , In) ins ++L List.map (λ x → x , Out) outs
++L List.map (λ x → x , Undecided) args
... | ins' | outs' | (x ∷ xs) = groundedList _≡_ (ins ++L ins') (outs ++L outs') (deleteFirstsBy _≡_ args (x ∷ xs)) af
-- The actual grounded labelling function for List.
-- This function calls groundedList with the correct arguments.
groundedL : {A : Set} → (A → A → Bool) → DungAF A → List (A × Status)
groundedL _≡_ (AF args def) = groundedList _≡_ [] [] args (AF args def)
-- My solution does the following.
-- Instead of fiddling with loads of properties of lists I decided to use Vectors.
-- Vectors keep track of their length so I don't have to do this explicity.
-- However, filter can not be sensibly defined for Vectors (the resulting lengths are unknown).
-- Thus, based on Ulf Norell's tutorial:
-- I first introduce the All predicate and Find view based on his notes (but using the modern version of inspect)
-- Find either finds that none of the elements matches a predicate, or returns proof that some element
-- does satisfy it and keeps track of where it is in the list.
-- I then adapt both All and Find to a version for Vectors.
-- False as the empty Type
data False : Set where
-- True as the Unit Type (using a record allows Agda to automatically infer the only allowed value)
record True : Set where
-- going from a decidable predicate to a Type
isTrue : Bool → Set
isTrue true = True
isTrue false = False
-- going from a decidable predicate to a Type
isFalse : Bool → Set
isFalse true = False
isFalse false = True
trueIsTrue : {x : Bool} → x ≡ true → isTrue x
trueIsTrue refl = _
falseIsFalse : {x : Bool} → x ≡ false → isFalse x
falseIsFalse refl = _
-- from decidable predicate to predicate on types
satisfies : {A : Set} → (A → Bool) → A → Set
satisfies p x = isTrue (p x)
infixr 30 _:all:_
data All {A : Set}(P : A → Set) : List A → Set where
all[] : All P []
_:all:_ : forall {x xs} → P x → All P xs → All P (x ∷ xs)
-- A simple lemma to transform to transform isFalse to isTrue
lemma : {x : Bool} → isFalse x → isTrue (not x)
lemma {true} ()
lemma {false} prf = prf
data Find {A : Set}(p : A → Bool) : List A → Set where
found : (xs : List A)(y : A) → satisfies p y → (ys : List A) → Find p (xs ++L (y ∷ ys))
not-found : forall {xs} → All (satisfies (not ∘ p)) xs → Find p xs
find : {A : Set}(p : A → Bool)(xs : List A) → Find p xs
find p [] = not-found all[]
find p (x ∷ xs) with p x | inspect p x
... | true | [ prf ] = found [] x (trueIsTrue prf) xs
... | false | _ with find p xs
find p (x ∷ ._) | false | [ prf ] | found xs y py ys = found (x ∷ xs) y py ys
find p (x ∷ xs) | false | [ prf ] | not-found npxs = not-found (lemma (falseIsFalse prf) :all: npxs)
exampleList : List AbsArg
exampleList = a ∷ b ∷ c ∷ []
{-
p : AbsArg → AbsArg → Bool
p = String._==_
-}
-- String_==_ is primitive equality on Strings
exampleFind : Find (String._==_ a) exampleList
exampleFind = find (String._==_ a) exampleList
-- after executing/normalising:
-- found [] "A" (record { }) ("B" ∷ "C" ∷ [])
-- Now to adapt the All and Find to Vectors:
infixr 30 _:allV:_
data AllV {A : Set}(P : A → Set) : {n : ℕ} → Vec A n → Set where
allV[] : AllV P []
_:allV:_ : {x : A}{n : ℕ}{xs : Vec A n} → P x → AllV P xs → AllV P (x ∷ xs)
data FindV {A : Set}(p : A → Bool) : {n : ℕ} → Vec A n → Set where
foundV : {k : ℕ}{m : ℕ}(xs : Vec A k)(y : A) → satisfies p y → (ys : Vec A m) → FindV p (xs ++ y ∷ ys)
not-foundV : {n : ℕ} {xs : Vec A n} → AllV (satisfies (not ∘ p)) xs → FindV p xs
findV : {A : Set}{n : ℕ}(p : A → Bool)(xs : Vec A n) → FindV p xs
findV p [] = not-foundV allV[]
findV p (x ∷ xs) with p x | inspect p x
... | true | [ prf ] = foundV [] x (trueIsTrue prf) xs
... | false | _ with findV p xs
findV p (x ∷ ._) | false | [ prf ] | foundV xs y py ys = foundV (x ∷ xs) y py ys
findV p (x ∷ xs) | false | [ prf ] | not-foundV npxs = not-foundV (lemma (falseIsFalse prf) :allV: npxs)
-- Simple arithmetic lemmas automatically solved by the RingSolver
-- (This is done by giving a syntactical representation of the theorem
-- and letting the RingSolver rewrite this. This is successful since
-- I was able to use refl)
lemma3 : {m n k l : ℕ} → (suc (m + n + (k + l))) ≡ (m + n + (k + suc l))
lemma3 {m} {n} {k} {l}= solve 4
(λ m' n' k' l' →
con 1 :+ (m' :+ n' :+ (k' :+ l')) :=
m' :+ n' :+ (k' :+ (con 1 :+ l')))
refl m n k l
-- Again a simple lemma needed in the grounded' function
lemma4 : {m n k l : ℕ} → (m + suc n + (k + l)) ≡ (m + n + (k + suc l))
lemma4 {m} {n} {k} {l} = solve 4
(λ m' n' k' l' →
m' :+ (con 1 :+ n') :+ (k' :+ l') :=
m' :+ n' :+ (k' :+ (con 1 :+ l')))
refl m n k l
lemma5 : {a k l : ℕ} → a ≡ k + suc l → a ≡ suc (k + l)
lemma5 {a} {k} {l} p = trans p
(solve 2 (λ k' l' → k' :+ (con 1 :+ l') := con 1 :+ (k' :+ l'))
refl k l)
lemma6 : {a k l : ℕ} → suc a ≡ k + suc l → a ≡ k + l
lemma6 {a} {k} {l} p = cong pred
(lemma5 {suc a} {k} {l} p)
-- grounded' helper function for grounded defined below (now using Vectors)
-- grounded' takes 3 Vectors. The current ins and outs (starting empty),
-- the arguments to process (args), a Dung AF (af)
-- a predicate on the arguments allowing for comparison (_≡_)
-- and a proof that there is a number equal to the length of args (p)
grounded' : {A : Set} → {m n o : ℕ} → (Σ ℕ λ k → k ≡ o) → (A → A → Bool) → Vec A m → Vec A n → Vec A o → DungAF A → Vec (A × Status) (m + n + o)
-- Base case:
-- We have no more arguments to process.
grounded' _ _ ins outs [] _ = (map (λ x → (x , In)) ins ++ map (λ x → (x , Out)) outs) ++ []
-- Inductive cases:
-- Otherwise, we can possibly find an unattacked/attacked argument
grounded' _ _≡_ ins outs args af with findV (unattacked _≡_ (toList outs) af) args |
findV (attacked _≡_ (toList ins) af) args
-- Two impossible cases:
-- The length of args is zero, while we did manage to find an unattacked/attacked element
-- Thus we use lemma5 to rewrite o so we can match on suc using lemma5 (and suc _ ≢ zero)
grounded' {o = .(k + suc l)} (zero , p) _≡_ _ _ ._ af | foundV {k} {l} _ _ _ _ | _ with lemma5 {zero} {k} {l} p
... | ()
grounded' {o = .(k + suc l)} (zero , p) _≡_ _ _ ._ af | not-foundV _ | foundV {k} {l} _ _ _ _ with lemma5 {zero} {k} {l} p
... | ()
-- Two cases:
-- We have found an unattacked/attacked element.
-- The Vector we try to return is of the "wrong" length, so we need to rewrite it using the basic lemma4
-- and substitute this value in the Vector constructur
-- Similarly we need to rewrite the proof of the length of o, using lemma6
grounded' {_} {m} {n} {o = .(k + suc l)} (suc a , p) _≡_ ins outs .(xs ++ y ∷ ys) af | foundV {k} {l} xs y _ ys | _ = subst (Vec _) (lemma3 {m} {n} {k} {l})
(grounded' (a , lemma6 {a} {k} {l} p) _≡_ (y ∷ ins) outs (xs ++ ys) af)
grounded' {_} {m} {n} {o = .(k + suc l)} (suc a , p) _≡_ ins outs .(xs ++ y ∷ ys) af | not-foundV _ | foundV {k} {l} xs y _ ys = subst (Vec _) (lemma4 {m} {n} {k} {l})
(grounded' (a , lemma6 {a} {k} {l} p) _≡_ ins (y ∷ outs) (xs ++ ys) af)
-- Final case (fixpoint):
-- We haven't found any unattacked/attacked element and thus are done.
grounded' _ _ ins outs args _ | not-foundV _ | not-foundV _ = (map (λ x → (x , In)) ins ++ map (λ x → (x , Out)) outs) ++ map (λ x → (x , Undecided)) args
-- length of Vectors
length : {A : Set} {n : ℕ} → Vec A n → ℕ
length {n = n} _ = n
-- The actual grounded labelling function.
-- This function calls grounded' with the correct Vectors and lengths.
grounded : {A : Set} → (A → A → Bool) → DungAF A → List (A × Status)
grounded _≡_ (AF args def) = toList
(grounded' ((length (fromList args)) , refl)
_≡_ [] [] (fromList args) (AF args def))
testGrounded1 : List (AbsArg × Status)
testGrounded1 = grounded String._==_ exampleAF
-- ("C" , In) ∷ ("A" , In) ∷ ("B" , Out) ∷ []
testGrounded2 : List (AbsArg × Status)
testGrounded2 = grounded String._==_ exampleAF2
-- ("A" , Undecided) ∷ ("B" , Undecided) ∷ []
-- Trivial equality function for Status
_==S_ : Status -> Status -> Bool
_==S_ In In = true
_==S_ Out Out = true
_==S_ Undecided Undecided = true
_==S_ _ _ = false
-- Defining the grounded extension using the grounded labelling is trivial,
-- we just need to keep all the arguments with an In label
groundedExt : {A : Set} → (A → A → Bool) → DungAF A → List A
groundedExt _≡_ (AF args def) = List.map proj₁((filter ((_==S_ In) ∘ proj₂) (grounded _≡_ (AF args def))))
elem : {A : Set} → (A → A → Bool) → A → List A → Bool
elem _≡_ x = any (_≡_ x)
setAttacks : {A : Set} → (A → A → Bool) → DungAF A -> List A -> A -> Bool
setAttacks _≡_ (AF args def) args' arg = setAttacks' _≡_ (AF args def) args' arg def
where
setAttacks' : {A : Set} → (A → A → Bool) → DungAF A -> List A -> A -> List (A × A) → Bool
setAttacks' _≡_ _ args arg [] = true
setAttacks' _≡_ (AF args' def) args arg ((a , b) ∷ xs) = elem _≡_ a args ∧
b ≡ arg ∧ setAttacks' _≡_ (AF args' def) args arg xs
conflictFree : {A : Set} → (A → A → Bool) → DungAF A → List A → Bool
conflictFree _≡_ (AF args def) args' = conflictFree' _≡_ (AF args def) args' def
where
conflictFree' : {A : Set} → (A → A → Bool) → DungAF A → List A → List (A × A) → Bool
conflictFree' _≡_ (AF args def) args' [] = true
conflictFree' _≡_ (AF args def) args' ((a , b) ∷ xs) = if elem _≡_ a args ∧ elem _≡_ b args then false else
conflictFree' _≡_ (AF args def) args' xs
-- null [(a,b) | (a, b) <- def, a `elem` args, b `elem` args]
acceptable : {A : Set} → (A → A → Bool) → DungAF A → A → List A → Bool
acceptable _≡_ (AF args' def) a args = acceptable' _≡_ (AF args' def) a args def
where
acceptable' : {A : Set} → (A → A → Bool) → DungAF A → A → List A → List (A × A) → Bool
acceptable' _≡_ (AF args' def) a args [] = true
acceptable' _≡_ (AF args' def) a args (( a' , b ) ∷ xs) = if a ≡ a' then setAttacks _≡_ (AF args' def) args b ∧ acceptable' _≡_ (AF args' def) a args xs else acceptable' _≡_ (AF args' def) a args xs
f : {A : Set} → (A → A → Bool) → DungAF A → List A → List A
f _≡_ af args = f' _≡_ af args args
where
f' : {A : Set} → (A → A → Bool) → DungAF A → List A → List A → List A
f' _≡_ af args [] = []
f' _≡_ af args (a ∷ xs) = if acceptable _≡_ af a args then a ∷ f' _≡_ af args xs else f' _≡_ af args xs
-- [a | a <- args, acceptable af a args]
_⊆_ : {A : Set} → (A → A → Bool) → List A → List A → Bool
_⊆_ _≡_ xs ys = null (deleteFirstsBy _≡_ xs ys)
admissible : {A : Set} → (A → A → Bool) → DungAF A → List A → Bool
admissible _≡_ af args = (_⊆_ _≡_) args (f _≡_ af args)
-- foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
groundedFix : {A : Set} → (A → A → Bool) → DungAF A → List A
groundedFix _≡_ (AF args def) = {!foldr !}
{-
faf :: [AbsArg] -> [AbsArg]
faf = f exampleAF
-}