diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,7 @@ +0.9 => 1.0 +============= +This package version is updated with a command line utility. + +* Make use of the CarneadesDSL Input and Dung Output modules to provide a + command line interface reading a Carneades Argument Evaluation Structure + and possible give the evaluation result or output in CEGARTIX format. diff --git a/CarneadesIntoDung.cabal b/CarneadesIntoDung.cabal --- a/CarneadesIntoDung.cabal +++ b/CarneadesIntoDung.cabal @@ -1,6 +1,6 @@ name: CarneadesIntoDung category: Argumentation, Embedded, AI -version: 0.9 +version: 1.0 license: BSD3 cabal-version: >= 1.6 license-file: LICENSE @@ -8,29 +8,42 @@ maintainer: Bas van Gijzel stability: experimental homepage: http://www.cs.nott.ac.uk/~bmv/CarneadesIntoDung/ -copyright: Copyright (C) 2013 Bas van Gijzel +copyright: Copyright (C) 2014 Bas van Gijzel synopsis: A translation from the Carneades argumentation model into Dung's AFs. description: A translation from the Carneades argumentation model - (http://hackage.haskell.org/package/CarneadesDSL) into Dung's - argumentation frameworks (http://hackage.haskell.org/package/Dung). + () into Dung's + argumentation frameworks (). This package provides a translation function and correspondence - properties. See "Towards a framework for the implementation and - verification of translations between argumentation models" by - Bas van Gijzel and Henrik Nilsson or the package's homepage. + properties. For the papers accompanying this library see + \"Towards a framework for the implementation and verification of + translations between argumentation models\" and \"A principled + approach to the implementation of argumentation models\", + available at . build-type: Simple +Extra-Source-Files: + CHANGELOG + examplecaes.txt + Library build-depends: base >= 4 && < 5, containers >= 0.3 && < 0.6, - fgl >= 5.4.2.4 && < 5.5, - CarneadesDSL >= 1.2, - Dung >= 0.9 + fgl >= 5.4.2.4, + cmdargs >= 0.10.2, + CarneadesDSL >= 1.3, + Dung >= 1.0.0.1 + hs-source-dirs: + src exposed-modules: - Language.CarneadesIntoDung.Translation - Language.CarneadesIntoDung.Examples + Language.CarneadesIntoDung.Translation + Language.CarneadesIntoDung.Examples + +Executable caell + main-Is: Main.hs + hs-source-dirs: src source-repository head Type: git diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c)2013, Bas van Gijzel +Copyright (c)2014, Bas van Gijzel All rights reserved. diff --git a/Language/CarneadesIntoDung/Examples.hs b/Language/CarneadesIntoDung/Examples.hs deleted file mode 100644 --- a/Language/CarneadesIntoDung/Examples.hs +++ /dev/null @@ -1,107 +0,0 @@ --- | This is the examples module accompanying the implementation of the --- translation from the Carneades argumentation model into Dung's --- argumentation frameworks. --- --- This module contains a collection of examples, showing how to translate --- an existing Carneades Argument Evaluation Structure (CAES) into an argumentation --- framework. --- --- To run these examples, or your own: start GHCi and do the following: --- --- @\:l Language.CarneadesIntoDung.Examples@ --- - -module Language.CarneadesIntoDung.Examples - ( - -- *Example translation - -- |We use the example CAES as defined in "Language.Carneades.ExampleCAES". - caes, - exTrans, exTrans', - -- *Correspondence properties - corProp, - ) - where -import Language.CarneadesIntoDung.Translation -import Language.Dung.AF -import Language.Carneades.CarneadesDSL -import Language.Carneades.ExampleCAES - --- |Translation of the example CAES 'caes'. --- The following is the prettified output of the translation, where --- the five propositions in the middle are the assumptions and 'defeater'. --- --- >>> translate caes --- AF [ --- Left (True,"murder"), --- Left (False,"murder"), --- Right ["kill","intent"] ~[]=>"murder", --- Left (False,"intent"), --- Left (True,"intent"), --- Right ["witness2"] ~["unreliable2"]=>"-intent", --- Right ["witness"] ~["unreliable"]=>"intent", --- Left (True,"unreliable"), --- Left (False,"unreliable") --- , --- Left (True,"defeater"), --- Left (True,"kill"), --- Left (True,"witness"), --- Left (True,"witness2"), --- Left (True,"unreliable2")] --- [ --- (Left (True,"defeater"), Left (True,"murder")), --- (Left (True,"defeater"), Left (False,"murder")), --- (Left (True,"defeater"), Right ["kill","intent"] ~[]=>"murder"), --- (Left (True,"defeater"), Left (False,"intent")), --- (Left (True,"defeater"),Left (True,"intent")), --- (Left (True,"unreliable2"),Right ["witness2"] ~["unreliable2"]=>"-intent"), --- (Left (True,"defeater"),Left (True,"unreliable")), --- (Left (True,"defeater"),Left (False,"unreliable")) --- ] -exTrans :: ConcreteAF -exTrans = translate caes - - - --- |Translation of the example CAES 'caes', keeping labels. --- The following is the prettified output of the translation, where --- the five propositions in the middle are the assumptions and 'defeater'. --- --- >>> translate' caes --- AF [ --- (False,Left (True,"murder")), --- (False,Left (False,"murder")), --- (False,Right ["kill","intent"] ~[]=>"murder"), --- (False,Left (False,"intent")), --- (False,Left (True,"intent")), --- (False,Right ["witness2"] ~["unreliable2"]=>"-intent"), --- (True,Right ["witness"] ~["unreliable"]=>"intent"), --- (False,Left (True,"unreliable")), --- (False,Left (False,"unreliable")) --- , --- (True,Left (True,"defeater")), --- (True,Left (True,"kill")), --- (True,Left (True,"witness")), --- (True,Left (True,"witness2")), --- (True,Left (True,"unreliable2"))] --- [ --- ((True,Left (True,"defeater")),(False,Left (True,"murder"))), --- ((True,Left (True,"defeater")),(False,Left (False,"murder"))), --- ((True,Left (True,"defeater")), (False,Right ["kill","intent"] ~[]=>"murder")), --- ((True,Left (True,"defeater")),(False,Left (False,"intent"))), --- ((True,Left (True,"defeater")),(False,Left (True,"intent"))), --- ((True,Left (True,"unreliable2")),(False,Right ["witness2"] ~["unreliable2"]=>"-intent")), --- ((True,Left (True,"defeater")),(False,Left (True,"unreliable"))), --- ((True,Left (True,"defeater")),(False,Left (False,"unreliable"))) -exTrans' :: LConcreteAF -exTrans' = translate' caes - - - --- |Combining the correspondence properties. --- --- And as expected: --- --- >>> corApp caes && corAcc caes --- True -corProp :: CAES -> Bool -corProp caes = corApp caes && corAcc caes diff --git a/Language/CarneadesIntoDung/Translation.hs b/Language/CarneadesIntoDung/Translation.hs deleted file mode 100644 --- a/Language/CarneadesIntoDung/Translation.hs +++ /dev/null @@ -1,230 +0,0 @@ --- |This module implements a translation from the Carneades argumentation model --- into Dung's argumentation frameworks. Any cycle-free Carneades Argument --- Evaluation Structure (CAES) is handled. We also give a Haskell implementation of --- correspondence properties. --- --- Translation is done according to the following algorithm (see also \"Towards a --- framework for the implementation and verification of translations between --- argumentation models\" by Bas van Gijzel and Henrik Nilsson) --- --- 1. generatedArgs = /emptyset/. --- --- 2. sortedArgs = Topological sort of arguments on its dependency graph. --- --- 3. while sortedArgs != /emptyset/: --- --- * Pick the first argument in sortedArgs. --- Remove all arguments from sortedArgs that have the same conclusion, --- c, and put them in argSet. --- --- * Translate applicability part of arguments argSet, building on previously --- generatedArgs and put the generated arguments in tempArgs. --- --- * argSet = /emptyset/ --- --- * Repeat the above three steps for the arguments for the opposite conclusion. --- --- * Translate the acceptability part of c and the opposite conclusion based on --- arguments in tempArgs. Add the results and tempArgs to generatedArgs. --- --- * tempArgs = /emptyset/ -module Language.CarneadesIntoDung.Translation - ( - -- * Basic types - ConcreteArg, LConcreteArg, - ConcreteAF, LConcreteAF, - -- * Translation functions - translate, translate', - -- * Correspondence properties - -- | Informally, the correspondence properties below state that every - -- argument and proposition in a CAES, after translation, will have a - -- corresponding argument and keep the same acceptability status. - -- - -- If the translation function is a correct implementation, the Haskell - -- implementation of the correspondence properties should always return - -- 'True'. However to constitute an actual (mechanised) proof we would - -- need to convert the translation and the implementation of the - -- correspondence properties in Haskell to a theorem prover like Agda. - -- - -- See Section 4.4 of the paper for the formally stated properties. - - - corApp, corAcc) - where -import Language.Dung.AF hiding (acceptable) -import Language.Carneades.CarneadesDSL -import Language.Carneades.Cyclic -import Data.Graph.Inductive -import Data.List(find, delete, intersect) -import Data.Maybe(fromMaybe) -import Data.Either(lefts, rights) -import Data.Set(fromList) -import Prelude hiding (negate) - --- |A concrete argument (in an argumentation framework) is either a Carneades --- propositional literal, or a Carneades argument. -type ConcreteArg = Either PropLiteral Argument - --- |A labelled version of the concrete argument allowing a more efficient --- translation by keeping track of the translation status. -type LConcreteArg = (Bool, ConcreteArg) - --- |An argumentation framework (AF) instantiated with 'ConcreteArg'. -type ConcreteAF = DungAF ConcreteArg - --- |An argumentation framework (AF) instantiated with 'LConcreteArg'. -type LConcreteAF = DungAF LConcreteArg - --- |Assumed true argument in the translated AF. It is used to attack arguments --- that do not uphold their proof standard or have unacceptable premises. -defeater :: LConcreteArg -defeater = (True, Left $ mkProp "defeater") - - --- | Topological sort of the dependency graph --- The result is a list, pairing a proposition with all its pro arguments -topSort :: ArgSet -> [(PropLiteral, [Argument])] -topSort g | cyclic g = error "Argumentation graph is cyclic!" - | otherwise = reverse $ topsort' g - --- |Transforms a Carneades proposition into a Dung argument and labels it 'True'. -propToLArg :: PropLiteral -> LConcreteArg -propToLArg p = (True, Left p) - --- |Strips the label of both the 'LConcreteArg's in the attack. -stripAttack :: (LConcreteArg, LConcreteArg) -> (ConcreteArg, ConcreteArg) -stripAttack (a, b) = (snd a, snd b) - --- |Translation function. It translate an arbitrary /cycle-free/ Carneades argument --- Evaluation Structure (CAES) into a Dung argumentation framework (instantiated --- with a ConcreteArg) -translate :: CAES -> ConcreteAF -translate caes@(CAES (argSet, (assumptions, _), _)) - = AF (map snd args) (map stripAttack attacks) - where AF args attacks = argsToAF (topSort argSet) - caes - (AF (defeater : map propToLArg assumptions) []) - - --- |Mainly, for testing purposes. This function behaves exactly like 'translate', --- but retains the labels. -translate' :: CAES -> LConcreteAF -translate' caes@(CAES (argSet, (assumptions, _), _)) - = AF args attacks - where AF args attacks = argsToAF (topSort argSet) - caes - (AF (defeater : map propToLArg assumptions) []) - - --- |Retrieves the arguments con the given proposition 'p'. -conArgs :: PropLiteral -> [(PropLiteral, [Argument])] -> (PropLiteral, [Argument]) -conArgs p argList = fromMaybe (negate p, []) (find ((== negate p) . fst) argList) - --- |Corresponds to the whole of 3. of the above algorithm (or Algorithm 4.1 in --- the paper) --- --- If there are no more arguments to process, the translated AF is returned. - --- If there is a propositional literal left, but it is an assumption, it has --- already been translated and does not need to be considered. --- --- Otherwise, collect all pro and con arguments for p (con arguments are obtained --- by calling 'conArgs') and remove them from @argList@. The translation is then --- done in four steps. 'transApps' is called to translate the applicability part of --- the pro and con arguments. 'transAcc' is called to translate the acceptability of --- p and the opposite of p (note that the order of applicable arguments is switched --- for translating the acceptability of the opposite of p). The results of these --- four calls are collected and used in the recursive step of 'argsToAF'. -argsToAF :: [(PropLiteral, [Argument])] -> CAES -> LConcreteAF -> LConcreteAF -argsToAF [] _ transAF = transAF -argsToAF (pro@(p, proArgs) : argList) caes@(CAES (_, (assumptions, _), _)) (AF args defs) - | p `elem` assumptions = argsToAF argList caes (AF args defs) - | otherwise = - let con = conArgs p argList - (proAppArgs, proDefs) = transApps args pro - (conAppArgs, conDefs) = transApps args con - (newArgPro, proDefs') = transAcc p proAppArgs conAppArgs caes - (newArgCon, conDefs') = transAcc (negate p) conAppArgs proAppArgs caes - argList' = delete con argList - in argsToAF argList' caes - (AF (newArgPro : newArgCon : proAppArgs ++ conAppArgs ++ args) - (proDefs' ++ conDefs' ++ proDefs ++ conDefs ++ defs)) - --- |Filters out propositional literals that have been labelled 'True'. -accProps :: [LConcreteArg] -> [PropLiteral] -accProps [] = [] -accProps ((True, Left p) : ls) = p : accProps ls -accProps ((True, Right _) : ls) = accProps ls -accProps ((False, _) : ls) = accProps ls - --- |This function takes two arguments, a list of already translated arguments --- (including the translated premises and exceptions) and a proposition --- paired with its to be translated arguments. It collects the results --- of the transApp function, which does the main work. -transApps :: [LConcreteArg] -> (PropLiteral, [Argument]) -> ([LConcreteArg], [(LConcreteArg, LConcreteArg)]) -transApps tArgs (p, args) = - let tr = map (transApp tArgs p) args - in (map fst tr, concatMap snd tr) - --- |Given a list of already translated arguments and a propositional literal, --- an argument (pro the propositional literal) is translated into a Dung argument --- and a possibly empty list of attackers. -transApp :: [LConcreteArg] -> PropLiteral -> Argument -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) -transApp tArgs p a@(Arg (prems, excs, c)) - | accProps tArgs `intersect` prems /= prems = ((False, Right a), [(defeater, (False, Right a))]) - | otherwise = - let acceptableExceptions = filter (\ (b, arg) -> b && either (`elem` excs) (const False) arg) tArgs - applicableArg = (null acceptableExceptions, Right a) - defeats = map (\ argExc -> (argExc, applicableArg)) acceptableExceptions - in (applicableArg, defeats) - --- |Determines the maximum weight of a list of applicable arguments (assumed --- to have the same conclusion). -maxWeight :: [LConcreteArg] -> CAES -> Double -maxWeight as caes@(CAES (_, (_, argWeight), _)) - = foldl max 0 [argWeight a | (True, Right a) <- as] - - --- |This function expects the following arguments: a propositional literal at --- question, a list of pro arguments (labelled 'True', and thus acceptable in --- the current AF), a list of con arguments (acceptable in the current AF) and --- a CAES. The result will be an argument corresponding to the proposition and --- a list of attacks. -transAcc :: PropLiteral -> [LConcreteArg] -> [LConcreteArg] -> CAES -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) -transAcc c [] conArgs caes = ((False, Left c), [(defeater, (False, Left c))]) -- no applicable argument for p -transAcc c ((_, Left _): proArgs) conArgs caes = error "Proposition in the list of applicable arguments" -transAcc c ((False, _) : proArgs) conArgs caes = transAcc c proArgs conArgs caes -transAcc c proArgs@((True, _) : proArgs') conArgs caes@(CAES (_, _, standard)) - | standard c == Scintilla = ((True, Left c), []) -- there is an applicable argument for p, thus acceptable under Scintilla - | standard c == Preponderance && - maxWeight proArgs caes > maxWeight conArgs caes = ((True, Left c), []) - | standard c == ClearAndConvincing && - maxWeight proArgs caes > alpha && - maxWeight proArgs caes > maxWeight conArgs caes + beta = ((True, Left c), []) - | standard c == BeyondReasonableDoubt && - maxWeight proArgs caes > alpha && - maxWeight proArgs caes > maxWeight conArgs caes + beta && - maxWeight conArgs caes < gamma = ((True, Left c), []) - | standard c == DialecticalValidity && null conArgs = ((True, Left c), []) - | otherwise = ((False, Left c), [(defeater, (False, Left c))]) - --- |Correspondence of the applicability of arguments. -corApp :: CAES -> Bool -corApp caes@(CAES (argSet, _, _)) = - let translatedCAES = translate caes - applicableArgs = filter (`applicable` caes) - (getAllArgs argSet) - transArgs = rights $ groundedExt translatedCAES - in fromList applicableArgs == fromList transArgs - --- |Correspondence of the acceptability of propositional literals, including --- assumptions. -corAcc :: CAES -> Bool -corAcc caes@(CAES (argSet, (assumptions, _), _)) = - let translatedCAES = translate caes - acceptableProps = filter (\ p -> p `acceptable` caes || - p `elem` assumptions) - (getProps argSet) - transProps = lefts $ delete (Left $ mkProp "defeater") - (groundedExt translatedCAES ) - in fromList acceptableProps == fromList transProps diff --git a/examplecaes.txt b/examplecaes.txt new file mode 100644 --- /dev/null +++ b/examplecaes.txt @@ -0,0 +1,25 @@ +argument arg1 ["kill", "intent"] [ ] "murder" +argument arg2 ["witness"] ["unreliable"] "intent" +argument arg3 ["witness2"] ["unreliable2"] "-intent" + +weight arg1 0.8 +weight arg2 0.3 +weight arg3 0.8 + +assumptions ["kill", "witness", "witness2", "unreliable2"] + + +-- Comments are allowed +-- also valid: standard "intent" BeyondReasonableDoubt +-- Propositions either as string literals or plain identifiers +standard "kill" scintilla +standard "intent" beyond_reasonable_doubt +standard "-intent" scintilla +standard murder scintilla +standard "-murder" scintilla +standard "unreliable" scintilla +standard "unreliable2" scintilla +standard witness scintilla +standard witness2 scintilla + + diff --git a/src/Language/CarneadesIntoDung/Examples.hs b/src/Language/CarneadesIntoDung/Examples.hs new file mode 100644 --- /dev/null +++ b/src/Language/CarneadesIntoDung/Examples.hs @@ -0,0 +1,107 @@ +-- | This is the examples module accompanying the implementation of the +-- translation from the Carneades argumentation model into Dung's +-- argumentation frameworks. +-- +-- This module contains a collection of examples, showing how to translate +-- an existing Carneades Argument Evaluation Structure (CAES) into an argumentation +-- framework. +-- +-- To run these examples, or your own: start GHCi and do the following: +-- +-- @\:l Language.CarneadesIntoDung.Examples@ +-- + +module Language.CarneadesIntoDung.Examples + ( + -- *Example translation + -- |We use the example CAES as defined in "Language.Carneades.ExampleCAES". + caes, + exTrans, exTrans', + -- *Correspondence properties + corProp, + ) + where +import Language.CarneadesIntoDung.Translation +import Language.Dung.AF +import Language.Carneades.CarneadesDSL +import Language.Carneades.ExampleCAES + +-- |Translation of the example CAES 'caes'. +-- The following is the prettified output of the translation, where +-- the five propositions in the middle are the assumptions and 'defeater'. +-- +-- >>> translate caes +-- AF [ +-- Left (True,"murder"), +-- Left (False,"murder"), +-- Right ["kill","intent"] ~[]=>"murder", +-- Left (False,"intent"), +-- Left (True,"intent"), +-- Right ["witness2"] ~["unreliable2"]=>"-intent", +-- Right ["witness"] ~["unreliable"]=>"intent", +-- Left (True,"unreliable"), +-- Left (False,"unreliable") +-- , +-- Left (True,"defeater"), +-- Left (True,"kill"), +-- Left (True,"witness"), +-- Left (True,"witness2"), +-- Left (True,"unreliable2")] +-- [ +-- (Left (True,"defeater"), Left (True,"murder")), +-- (Left (True,"defeater"), Left (False,"murder")), +-- (Left (True,"defeater"), Right ["kill","intent"] ~[]=>"murder"), +-- (Left (True,"defeater"), Left (False,"intent")), +-- (Left (True,"defeater"),Left (True,"intent")), +-- (Left (True,"unreliable2"),Right ["witness2"] ~["unreliable2"]=>"-intent"), +-- (Left (True,"defeater"),Left (True,"unreliable")), +-- (Left (True,"defeater"),Left (False,"unreliable")) +-- ] +exTrans :: ConcreteAF +exTrans = translate caes + + + +-- |Translation of the example CAES 'caes', keeping labels. +-- The following is the prettified output of the translation, where +-- the five propositions in the middle are the assumptions and 'defeater'. +-- +-- >>> translate' caes +-- AF [ +-- (False,Left (True,"murder")), +-- (False,Left (False,"murder")), +-- (False,Right ["kill","intent"] ~[]=>"murder"), +-- (False,Left (False,"intent")), +-- (False,Left (True,"intent")), +-- (False,Right ["witness2"] ~["unreliable2"]=>"-intent"), +-- (True,Right ["witness"] ~["unreliable"]=>"intent"), +-- (False,Left (True,"unreliable")), +-- (False,Left (False,"unreliable")) +-- , +-- (True,Left (True,"defeater")), +-- (True,Left (True,"kill")), +-- (True,Left (True,"witness")), +-- (True,Left (True,"witness2")), +-- (True,Left (True,"unreliable2"))] +-- [ +-- ((True,Left (True,"defeater")),(False,Left (True,"murder"))), +-- ((True,Left (True,"defeater")),(False,Left (False,"murder"))), +-- ((True,Left (True,"defeater")), (False,Right ["kill","intent"] ~[]=>"murder")), +-- ((True,Left (True,"defeater")),(False,Left (False,"intent"))), +-- ((True,Left (True,"defeater")),(False,Left (True,"intent"))), +-- ((True,Left (True,"unreliable2")),(False,Right ["witness2"] ~["unreliable2"]=>"-intent")), +-- ((True,Left (True,"defeater")),(False,Left (True,"unreliable"))), +-- ((True,Left (True,"defeater")),(False,Left (False,"unreliable"))) +exTrans' :: LConcreteAF +exTrans' = translate' caes + + + +-- |Combining the correspondence properties. +-- +-- And as expected: +-- +-- >>> corApp caes && corAcc caes +-- True +corProp :: CAES -> Bool +corProp caes = corApp caes && corAcc caes diff --git a/src/Language/CarneadesIntoDung/Translation.hs b/src/Language/CarneadesIntoDung/Translation.hs new file mode 100644 --- /dev/null +++ b/src/Language/CarneadesIntoDung/Translation.hs @@ -0,0 +1,230 @@ +-- |This module implements a translation from the Carneades argumentation model +-- into Dung's argumentation frameworks. Any cycle-free Carneades Argument +-- Evaluation Structure (CAES) is handled. We also give a Haskell implementation of +-- correspondence properties. +-- +-- Translation is done according to the following algorithm (see also \"Towards a +-- framework for the implementation and verification of translations between +-- argumentation models\" by Bas van Gijzel and Henrik Nilsson) +-- +-- 1. generatedArgs = /emptyset/. +-- +-- 2. sortedArgs = Topological sort of arguments on its dependency graph. +-- +-- 3. while sortedArgs != /emptyset/: +-- +-- * Pick the first argument in sortedArgs. +-- Remove all arguments from sortedArgs that have the same conclusion, +-- c, and put them in argSet. +-- +-- * Translate applicability part of arguments argSet, building on previously +-- generatedArgs and put the generated arguments in tempArgs. +-- +-- * argSet = /emptyset/ +-- +-- * Repeat the above three steps for the arguments for the opposite conclusion. +-- +-- * Translate the acceptability part of c and the opposite conclusion based on +-- arguments in tempArgs. Add the results and tempArgs to generatedArgs. +-- +-- * tempArgs = /emptyset/ +module Language.CarneadesIntoDung.Translation + ( + -- * Basic types + ConcreteArg, LConcreteArg, + ConcreteAF, LConcreteAF, + -- * Translation functions + translate, translate', + -- * Correspondence properties + -- | Informally, the correspondence properties below state that every + -- argument and proposition in a CAES, after translation, will have a + -- corresponding argument and keep the same acceptability status. + -- + -- If the translation function is a correct implementation, the Haskell + -- implementation of the correspondence properties should always return + -- 'True'. However to constitute an actual (mechanised) proof we would + -- need to convert the translation and the implementation of the + -- correspondence properties in Haskell to a theorem prover like Agda. + -- + -- See Section 4.4 of the paper for the formally stated properties. + + + corApp, corAcc) + where +import Language.Dung.AF hiding (acceptable) +import Language.Carneades.CarneadesDSL +import Language.Carneades.Cyclic +import Data.Graph.Inductive +import Data.List(find, delete, intersect) +import Data.Maybe(fromMaybe) +import Data.Either(lefts, rights) +import Data.Set(fromList) +import Prelude hiding (negate) + +-- |A concrete argument (in an argumentation framework) is either a Carneades +-- propositional literal, or a Carneades argument. +type ConcreteArg = Either PropLiteral Argument + +-- |A labelled version of the concrete argument allowing a more efficient +-- translation by keeping track of the translation status. +type LConcreteArg = (Bool, ConcreteArg) + +-- |An argumentation framework (AF) instantiated with 'ConcreteArg'. +type ConcreteAF = DungAF ConcreteArg + +-- |An argumentation framework (AF) instantiated with 'LConcreteArg'. +type LConcreteAF = DungAF LConcreteArg + +-- |Assumed true argument in the translated AF. It is used to attack arguments +-- that do not uphold their proof standard or have unacceptable premises. +defeater :: LConcreteArg +defeater = (True, Left $ mkProp "defeater") + + +-- | Topological sort of the dependency graph +-- The result is a list, pairing a proposition with all its pro arguments +topSort :: ArgSet -> [(PropLiteral, [Argument])] +topSort g | cyclic g = error "Argumentation graph is cyclic!" + | otherwise = reverse $ topsort' g + +-- |Transforms a Carneades proposition into a Dung argument and labels it 'True'. +propToLArg :: PropLiteral -> LConcreteArg +propToLArg p = (True, Left p) + +-- |Strips the label of both the 'LConcreteArg's in the attack. +stripAttack :: (LConcreteArg, LConcreteArg) -> (ConcreteArg, ConcreteArg) +stripAttack (a, b) = (snd a, snd b) + +-- |Translation function. It translate an arbitrary /cycle-free/ Carneades argument +-- Evaluation Structure (CAES) into a Dung argumentation framework (instantiated +-- with a ConcreteArg) +translate :: CAES -> ConcreteAF +translate caes@(CAES (argSet, (assumptions, _), _)) + = AF (map snd args) (map stripAttack attacks) + where AF args attacks = argsToAF (topSort argSet) + caes + (AF (defeater : map propToLArg assumptions) []) + + +-- |Mainly, for testing purposes. This function behaves exactly like 'translate', +-- but retains the labels. +translate' :: CAES -> LConcreteAF +translate' caes@(CAES (argSet, (assumptions, _), _)) + = AF args attacks + where AF args attacks = argsToAF (topSort argSet) + caes + (AF (defeater : map propToLArg assumptions) []) + + +-- |Retrieves the arguments con the given proposition 'p'. +conArgs :: PropLiteral -> [(PropLiteral, [Argument])] -> (PropLiteral, [Argument]) +conArgs p argList = fromMaybe (negate p, []) (find ((== negate p) . fst) argList) + +-- |Corresponds to the whole of 3. of the above algorithm (or Algorithm 4.1 in +-- the paper) +-- +-- If there are no more arguments to process, the translated AF is returned. + +-- If there is a propositional literal left, but it is an assumption, it has +-- already been translated and does not need to be considered. +-- +-- Otherwise, collect all pro and con arguments for p (con arguments are obtained +-- by calling 'conArgs') and remove them from @argList@. The translation is then +-- done in four steps. 'transApps' is called to translate the applicability part of +-- the pro and con arguments. 'transAcc' is called to translate the acceptability of +-- p and the opposite of p (note that the order of applicable arguments is switched +-- for translating the acceptability of the opposite of p). The results of these +-- four calls are collected and used in the recursive step of 'argsToAF'. +argsToAF :: [(PropLiteral, [Argument])] -> CAES -> LConcreteAF -> LConcreteAF +argsToAF [] _ transAF = transAF +argsToAF (pro@(p, proArgs) : argList) caes@(CAES (_, (assumptions, _), _)) (AF args defs) + | p `elem` assumptions = argsToAF argList caes (AF args defs) + | otherwise = + let con = conArgs p argList + (proAppArgs, proDefs) = transApps args pro + (conAppArgs, conDefs) = transApps args con + (newArgPro, proDefs') = transAcc p proAppArgs conAppArgs caes + (newArgCon, conDefs') = transAcc (negate p) conAppArgs proAppArgs caes + argList' = delete con argList + in argsToAF argList' caes + (AF (newArgPro : newArgCon : proAppArgs ++ conAppArgs ++ args) + (proDefs' ++ conDefs' ++ proDefs ++ conDefs ++ defs)) + +-- |Filters out propositional literals that have been labelled 'True'. +accProps :: [LConcreteArg] -> [PropLiteral] +accProps [] = [] +accProps ((True, Left p) : ls) = p : accProps ls +accProps ((True, Right _) : ls) = accProps ls +accProps ((False, _) : ls) = accProps ls + +-- |This function takes two arguments, a list of already translated arguments +-- (including the translated premises and exceptions) and a proposition +-- paired with its to be translated arguments. It collects the results +-- of the transApp function, which does the main work. +transApps :: [LConcreteArg] -> (PropLiteral, [Argument]) -> ([LConcreteArg], [(LConcreteArg, LConcreteArg)]) +transApps tArgs (p, args) = + let tr = map (transApp tArgs p) args + in (map fst tr, concatMap snd tr) + +-- |Given a list of already translated arguments and a propositional literal, +-- an argument (pro the propositional literal) is translated into a Dung argument +-- and a possibly empty list of attackers. +transApp :: [LConcreteArg] -> PropLiteral -> Argument -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) +transApp tArgs p a@(Arg (prems, excs, c)) + | accProps tArgs `intersect` prems /= prems = ((False, Right a), [(defeater, (False, Right a))]) + | otherwise = + let acceptableExceptions = filter (\ (b, arg) -> b && either (`elem` excs) (const False) arg) tArgs + applicableArg = (null acceptableExceptions, Right a) + defeats = map (\ argExc -> (argExc, applicableArg)) acceptableExceptions + in (applicableArg, defeats) + +-- |Determines the maximum weight of a list of applicable arguments (assumed +-- to have the same conclusion). +maxWeight :: [LConcreteArg] -> CAES -> Double +maxWeight as caes@(CAES (_, (_, argWeight), _)) + = foldl max 0 [argWeight a | (True, Right a) <- as] + + +-- |This function expects the following arguments: a propositional literal at +-- question, a list of pro arguments (labelled 'True', and thus acceptable in +-- the current AF), a list of con arguments (acceptable in the current AF) and +-- a CAES. The result will be an argument corresponding to the proposition and +-- a list of attacks. +transAcc :: PropLiteral -> [LConcreteArg] -> [LConcreteArg] -> CAES -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) +transAcc c [] conArgs caes = ((False, Left c), [(defeater, (False, Left c))]) -- no applicable argument for p +transAcc c ((_, Left _): proArgs) conArgs caes = error "Proposition in the list of applicable arguments" +transAcc c ((False, _) : proArgs) conArgs caes = transAcc c proArgs conArgs caes +transAcc c proArgs@((True, _) : proArgs') conArgs caes@(CAES (_, _, standard)) + | standard c == Scintilla = ((True, Left c), []) -- there is an applicable argument for p, thus acceptable under Scintilla + | standard c == Preponderance && + maxWeight proArgs caes > maxWeight conArgs caes = ((True, Left c), []) + | standard c == ClearAndConvincing && + maxWeight proArgs caes > alpha && + maxWeight proArgs caes > maxWeight conArgs caes + beta = ((True, Left c), []) + | standard c == BeyondReasonableDoubt && + maxWeight proArgs caes > alpha && + maxWeight proArgs caes > maxWeight conArgs caes + beta && + maxWeight conArgs caes < gamma = ((True, Left c), []) + | standard c == DialecticalValidity && null conArgs = ((True, Left c), []) + | otherwise = ((False, Left c), [(defeater, (False, Left c))]) + +-- |Correspondence of the applicability of arguments. +corApp :: CAES -> Bool +corApp caes@(CAES (argSet, _, _)) = + let translatedCAES = translate caes + applicableArgs = filter (`applicable` caes) + (getAllArgs argSet) + transArgs = rights $ groundedExt translatedCAES + in fromList applicableArgs == fromList transArgs + +-- |Correspondence of the acceptability of propositional literals, including +-- assumptions. +corAcc :: CAES -> Bool +corAcc caes@(CAES (argSet, (assumptions, _), _)) = + let translatedCAES = translate caes + acceptableProps = filter (\ p -> p `acceptable` caes || + p `elem` assumptions) + (getProps argSet) + transProps = lefts $ delete (Left $ mkProp "defeater") + (groundedExt translatedCAES ) + in fromList acceptableProps == fromList transProps diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,100 @@ +-- |This module implements a command-line interface to the implementation of +-- Carneades. CAES + Haskell = caell +-- +-- Code in this module partly taken from/inspired by Shinobu +-- See: http://zuttobenkyou.wordpress.com/2011/04/19/haskell-using-cmdargs-single-and-multi-mode/ +-- and http://listx.github.com/ +{-# LANGUAGE DeriveDataTypeable, RecordWildCards #-} +module Main + ( + main + ) + where +import Language.CarneadesIntoDung.Translation +import Language.Carneades.CarneadesDSL(CAES(..), getAllArgs, applicable, + getProps, acceptable) +import Language.Carneades.Input +import Language.Dung.AF(groundedExt, preferredExt, stableExt, semiStableExt, + DungAF(..)) +import Language.Dung.Output + +import System.Console.CmdArgs +import System.Environment (getArgs, withArgs) +import System.Exit +import Control.Monad (when, unless) + +data MyOptions = MyOptions { + cegartix :: Bool, + laxCegartix :: Bool, + fileName :: String, + outputFile :: String, + correspondence :: Bool, + extension :: Bool, + xSemantics :: Bool + } deriving (Show, Data, Typeable) + +myProgOpts :: MyOptions +myProgOpts = MyOptions + { cegartix = True &= help "Output in strict CEGARTIX/PrefSat format (standard)" + , laxCegartix = False &= help "Output in lax CEGARTIX/PrefSat format (+parentheses)" + , fileName = def &= typFile &= help "Name of the file to be read" + , outputFile = def &= typFile &= help "Name of the file to be written" + , extension = True &= help "Output unique complete extension for the translated CAES (standard)" + , correspondence = False &= help "Display satisfaction of correspondence result" + , xSemantics = False &= help "Output evaluation of the original Carneades semantics" + } + +getOpts :: IO MyOptions +getOpts = cmdArgs $ myProgOpts + &= versionArg [explicit, name "version", name "v", summary _PROGRAM_INFO] + &= summary (_PROGRAM_INFO ++ ", " ++ _COPYRIGHT) + &= help _PROGRAM_ABOUT + &= helpArg [explicit, name "help", name "h"] + &= program _PROGRAM_NAME + +_PROGRAM_NAME = "caell" +_PROGRAM_VERSION = "1.0" +_PROGRAM_INFO = _PROGRAM_NAME ++ " version " ++ _PROGRAM_VERSION +_PROGRAM_ABOUT = "An implementation of Carneades in Haskell" +_COPYRIGHT = "(C) Bas van Gijzel 2014" + + +main :: IO () +main = do + args <- getArgs + opts <- (if null args then withArgs ["--help"] else id) getOpts + optionHandler opts + +-- |Check any malformed arguments/missing arguments. +optionHandler :: MyOptions -> IO () +optionHandler opts@MyOptions{..} = do + when (null fileName) $ putStrLn "--fileName is blank!" >> exitWith (ExitFailure 1) + input <- readFile fileName + let opts' = opts {cegartix = not laxCegartix} + caes <- case parseCAES input of + Left err -> putStrLn "Parsing error: " >> print err >> exitWith (ExitFailure 1) + Right caes -> return caes + exec opts' caes + +-- |Execute supplied options +exec :: MyOptions -> CAES -> IO () +exec opts@MyOptions{..} caes@(CAES (argSet, (assumptions, _), _)) = do + let args = getAllArgs argSet + let transCaes = translate caes + putStrLn $ "Argument set: " ++ show args + when xSemantics $ + putStrLn "Evaluation under original semantics:" >> + putStrLn "Applicable arguments:" >> + print (filter (`applicable` caes) args) >> + putStrLn "Acceptable propositions:" >> + print (filter (\ p -> p `acceptable` caes + || p `elem` assumptions) + (getProps argSet)) + when extension $ putStrLn "Extension after translation: " + >> print (groundedExt transCaes) + when correspondence $ putStrLn ("Correspondence of applicability is: " ++ show (corApp caes)) + >> putStrLn ("Correspondence of acceptability is: " ++ show (corAcc caes)) + unless (null outputFile) + $ if cegartix + then writeFile outputFile (toStrictCegartix transCaes) >> putStrLn "File outputted." + else writeFile outputFile (toCegartix transCaes) >> putStrLn "File outputted."