Data.TMS.ATMS.ATMST

Translation of Forbus and de Kleer's assumption-based truth maintenance systems (ATMSes) from Common Lisp to Haskell.

This is not a very "Haskelly" implementation; rather, it is a translation of the original code with minimal changes. Most of the deviations from the original are due to either Haskell's strong typing, which necessitates some additional tagging, and to the abomination which is Lisp's do macro. The translation relies on mutable data structures using STT state thread references. A more pure translation, possibly not relying on the ST monad/STT transformer, is a significant piece of future work.

Note also there are restrictions on the embedded monad m which can be wrapped in the STT transformer; see the Control.Monad.ST.Trans documentation for details.

See the LICENSE.txt and README-forbus-dekleer.txt files distributed with this work for a paragraph stating scope of permission and disclaimer of warranty, and for additional information regarding copyright ownership. The above copyright notice and that paragraph must be included in any separate copy of this file.

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, for NON-COMMERCIAL use. See the License for the specific language governing permissions and limitations under the License.

The ATMST monad

data Monad m => ATMST s m a

The process of building and using a mutable ATMS.

Instances

MonadTrans (ATMST s)

Defined in Data.TMS.ATMS.ATMST

Methods

lift :: Monad m => m a -> ATMST s m a

(Monad m, Functor m) => Monad (ATMST s m)

Defined in Data.TMS.ATMS.ATMST

Methods

(>>=) :: ATMST s m a -> (a -> ATMST s m b) -> ATMST s m b

(>>) :: ATMST s m a -> ATMST s m b -> ATMST s m b

return :: a -> ATMST s m a

Monad m => Functor (ATMST s m)

Defined in Data.TMS.ATMS.ATMST

Methods

fmap :: (a -> b) -> ATMST s m a -> ATMST s m b

(<$) :: a -> ATMST s m b -> ATMST s m a

Monad m => MonadFail (ATMST s m)

Defined in Data.TMS.ATMS.ATMST

Methods

fail :: String -> ATMST s m a

(Monad m, Functor m) => Applicative (ATMST s m)

Defined in Data.TMS.ATMS.ATMST

Methods

pure :: a -> ATMST s m a

(<*>) :: ATMST s m (a -> b) -> ATMST s m a -> ATMST s m b

liftA2 :: (a -> b -> c) -> ATMST s m a -> ATMST s m b -> ATMST s m c

(*>) :: ATMST s m a -> ATMST s m b -> ATMST s m b

(<*) :: ATMST s m a -> ATMST s m b -> ATMST s m a

MonadIO m => MonadIO (ATMST s m)

Defined in Data.TMS.ATMS.ATMST

Methods

liftIO :: IO a -> ATMST s m a

data AtmsErr

Errors which can arise from ATMS operations.

Constructors

CannotRemoveNodeWIthConsequences String Int

It is not possible to remove a Node from an ATMS after a JustRule which uses that Node is added to the ATMS.

InternalNoEmptyEnv

Internal error called when there is no internal default empty Env associated with this ATMS. Should never be signaled for an ATMS created with createATMS, since this latter function does set up the default empty environment before returning the new ATMS.

FromMonadFail String

Indicates a pattern-matching failure within an ATMST operation.

Instances

Show AtmsErr

Defined in Data.TMS.ATMS.ATMST

Methods

showsPrec :: Int -> AtmsErr -> ShowS

show :: AtmsErr -> String

showList :: [AtmsErr] -> ShowS

runATMST :: Monad m => (forall s. ATMST s m r) -> m (Either AtmsErr r)

Execute a computation in the ATMST monad transformer.

setInitialEnvTableAlloc :: Monad m => Int -> ATMST s m ()

Retrieve the current initial Env table size setting.

setEnvTableIncr :: Monad m => Int -> ATMST s m ()

Retrieve the current initial Env table size setting.

getInitialEnvTableAlloc :: Monad m => ATMST s m Int

Retrieve the current initial Env table size setting.

getEnvTableIncr :: Monad m => ATMST s m Int

Retrieve the current initial Env table size setting.

ATMS data structures

Component classes

class NodeDatum d

Class of type which can be used as the datum underlying Nodes in an ATMS.

Minimal complete definition

contradictionNodeDatum

Instances

NodeDatum String

Defined in Data.TMS.ATMS.ATMST

Methods

contradictionNodeDatum :: String

NodeDatum Symbol

Defined in Data.TMS.ATMS.ATMST

Methods

contradictionNodeDatum :: Symbol

contradictionNodeDatum :: NodeDatum d => d

The datum associated with the contradiction node in a newly-initialized ATMS with Node data of this type.

Top-level ATMS

data (Monad m, NodeDatum d) => ATMS d i r s m

Top-level representation of an assumption-based truth maintenance system.

createATMS :: (Debuggable m, NodeDatum d) => String -> ATMST s m (ATMS d i r s m)

Create a new, empty ATMS.

Translated from create-atms in atms.lisp.

atmsTitle :: ATMS d i r s m -> String

Name of this ATMS.

ATMS components

getNodes :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]

Return the ATMS's current Node list.

getJusts :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [JustRule d i r s m]

Return the ATMS's current JustRule list.

getContradictions :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]

Return the ATMS's current contradictions list.

getAssumptions :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m [Node d i r s m]

Return the ATMS's current assumptions list.

getContradictionNode :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Node d i r s m)

Return the ATMS's built-in contradiction node.

getEmptyEnvironment :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Env d i r s m)

Return the ATMS's built-in empty environment.

getNodeString :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (Node d i r s m -> String)

Return the ATMS's current Node formatter.

getJustString :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (JustRule d i r s m -> String)

Return the ATMS's current JustRule formatter.

getDatumString :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (d -> String)

Return the ATMS's current datum formatter.

getInformantString :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (i -> String)

Return the ATMS's current informant formatter.

getEnqueueProcedure :: (Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m (r -> ATMST s m ())

Return the ATMS's current rule-queueing procedure.

setDatumStringViaString :: Monad m => ATMS String i r s m -> ATMST s m ()

When the data associated with Nodes are all Strings, we can direct the ATMS to display each datum as itself.

setDatumStringViaShow :: (NodeDatum d, Show d, Monad m) => ATMS d i r s m -> ATMST s m ()

When the data associated with Nodes are of a type of class Show, we can direct the ATMS to display each datum using the show instance.

setInformantStringViaString :: (Monad m, NodeDatum d) => ATMS d String r s m -> ATMST s m ()

When the informants associated with JustRules are all Strings, we can direct the ATMS to display each informant as itself.

setInformantStringViaShow :: (Show i, Monad m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

When the informants associated with JustRules are of a type of class Show, we can direct the ATMS to display each datum using the show instance.

Nodes

data (Monad m, NodeDatum d) => Node d i r s m

Wrapper for the datum associated with a node of the ATMS.

Translated from (tms-node in atms.lisp.

Instances

(Monad m, NodeDatum d) => Eq (Node d i r s m)

Defined in Data.TMS.ATMS.ATMST

Methods

(==) :: Node d i r s m -> Node d i r s m -> Bool

(/=) :: Node d i r s m -> Node d i r s m -> Bool

(Monad m, NodeDatum d) => Ord (Node d i r s m)

Defined in Data.TMS.ATMS.ATMST

Methods

compare :: Node d i r s m -> Node d i r s m -> Ordering

(<) :: Node d i r s m -> Node d i r s m -> Bool

(<=) :: Node d i r s m -> Node d i r s m -> Bool

(>) :: Node d i r s m -> Node d i r s m -> Bool

(>=) :: Node d i r s m -> Node d i r s m -> Bool

max :: Node d i r s m -> Node d i r s m -> Node d i r s m

min :: Node d i r s m -> Node d i r s m -> Node d i r s m

(Monad m, NodeDatum d) => Show (Node d i r s m)

Defined in Data.TMS.ATMS.ATMST

Methods

showsPrec :: Int -> Node d i r s m -> ShowS

show :: Node d i r s m -> String

showList :: [Node d i r s m] -> ShowS

nodeDatum :: Node d i r s m -> d

Retrieve the datum associated with a Node.

createNode :: (Debuggable m, NodeDatum d) => ATMS d i r s m -> d -> Bool -> Bool -> ATMST s m (Node d i r s m)

Create a new Node in an ATMS.

Translated from create-node in atms.lisp.

Node components

nodeATMS :: Node d i r s m -> ATMS d i r s m

Retrieve the ATMS associated with a Node.

nodeString :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String

Shortcut for retrieving the Node formatter from an ATMS, and applying it to the given Node.

Translated from node-string in atms.lisp.

defaultNodeString :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String

Default formatter for the Nodes of an ATMS.

Translated from default-node-string in atms.lisp.

getNodeLabel :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [Env d i r s m]

Return the Node's label.

getNodeRules :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [r]

Return the Node's rules.

getNodeConsequences :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m [JustRule d i r s m]

Return the Node's consequences.

Setting node status

assumeNode :: (Debuggable m, NodeDatum d) => Node d i r s m -> ATMST s m ()

Mark the given Node as to be believed as an assumption by its ATMS.

Translated from assume-node in atms.lisp.

makeContradiction :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()

Mark the given Node as an additional contradiction node of the ATMS.

Translated from make-contradiction in atms.lisp.

removeNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m ()

Remove a Node from the ATMS.

Translated from remove-node in atms.lisp.

Justifications

data (Monad m, NodeDatum d) => JustRule d i r s m

The justification of one ATMS Node by zero or more others.

Constructors

JustRule Int i (Node d i r s m) [Node d i r s m]

Instances

(Monad m, NodeDatum d) => Eq (JustRule d i r s m)

Defined in Data.TMS.ATMS.ATMST

Methods

(==) :: JustRule d i r s m -> JustRule d i r s m -> Bool

(/=) :: JustRule d i r s m -> JustRule d i r s m -> Bool

justInformant :: JustRule d i r s m -> i

The informant associated with applying this inference rule.

justConsequence :: JustRule d i r s m -> Node d i r s m

The conclusion of this inference rule.

justAntecedents :: JustRule d i r s m -> [Node d i r s m]

The antecedents of this inference rule.

data Justification d i r s m

Description of why a Node may be believed by the ATMS.

data Explanation d i r s m

Explanation of why a Node may be believed by the ATMS for output to a query.

justifyNode :: (Debuggable m, NodeDatum d) => i -> Node d i r s m -> [Node d i r s m] -> ATMST s m ()

Direct the ATMS to believe a particular Node when all of the given list of Nodes are also believed. The first argument is the informant associated with this inference.

Translated from justify-node in atms.lisp.

Environments and tables

data (Monad m, NodeDatum d) => Env d i r s m

An environment of Nodes which may be used as the basis of reasoning in an ATMS.

Instances

(Monad m, NodeDatum d) => Eq (Env d i r s m)

Defined in Data.TMS.ATMS.ATMST

Methods

(==) :: Env d i r s m -> Env d i r s m -> Bool

(/=) :: Env d i r s m -> Env d i r s m -> Bool

(Monad m, NodeDatum d) => Show (Env d i r s m)

Defined in Data.TMS.ATMS.ATMST

Methods

showsPrec :: Int -> Env d i r s m -> ShowS

show :: Env d i r s m -> String

showList :: [Env d i r s m] -> ShowS

data EnvTable d i r s m

Type alias for the array storage of a table of Envs arranged by length.

envIndex :: Env d i r s m -> Int

The unique nomber of this Env within its ATMS.

envAssumptions :: Env d i r s m -> [Node d i r s m]

The assumptions contained within this Env.

getEnvNodes :: (Monad m, NodeDatum d) => Env d i r s m -> ATMST s m [Node d i r s m]

Shortcut for reading the Nodes of an Env.

Deduction and search utilities

Related to a node

isTrueNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool

Returns True if the given Node is axiomatic, following from the assumption of zero other nodes.

Translated from true-node? in atms.lisp.

isInNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool

Returns True if the given Node is justified by some labelling Environment of Nodes in the ATMS.

Translated from in-node? in atms.lisp.

isInNodeByEnv :: (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool

Returns True if the given Node is justified by some subset of the given environment in the ATMS.

Translated from in-node? in atms.lisp.

isOutNode :: (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool

Returns True if the given Node is justified by no labelling Environment of Nodes in the ATMS.

Translated from out-node? in atms.lisp.

isNodeConsistentWith :: (Monad m, NodeDatum d) => Node d i r s m -> Env d i r s m -> ATMST s m Bool

Returns True if some environment justifying the given Node is consistent with the given environment, where two environments are consistent when their union is not no-good.

Translated from node-consistent-with? in atms.lisp.

getNodeIsAssumption :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool

Return whether the Node's is currently markable as an assumption.

getNodeIsContradictory :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m Bool

Return whether the Node's is currently contradictory.

Related to environments

envIsNogood :: (Monad m, NodeDatum d) => Env d i r s m -> ATMST s m Bool

Shortcut for testing whether an Env is nogood.

Printing and debugging

Functions prefixed format build a computation returning a String. Functions prefixed debug or print build a unit computation printing the artifact in question to standard output; those with prefix debug are generally more verbose.

debugAtms :: (MonadIO m, NodeDatum d) => String -> ATMS d i r s m -> ATMST s m ()

Give a verbose printout of an ATMS.

printAtms :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

Print the internal title signifying an ATMS.

Translated from print-atms in atms.lisp.

debugAtmsEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

Give a verbose printout of the Environments of an ATMS.

printAtmsStatistics :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

Print statistics about an ATMS.

Translated from print-atms-statistics in atms.lisp.

Nodes and node lists

formatNode :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String

Computation returning a one-line summary of one Node of an ATMS.

formatNodes :: (Monad m, NodeDatum d) => String -> [Node d i r s m] -> ATMST s m String

Computation returning a one-line summary of the Nodes of an ATMS.

debugNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()

Give a verbose printout of a Node of an ATMS.

printNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()

Print a verbose summary of a Node of an ATMS.

Translated from print-tms-node in atms.lisp.

whyNodes :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

Print the justifying Environments which label each Node of an ATMS.

Translated from why-nodes in atms.lisp.

whyNode :: (MonadIO m, NodeDatum d) => Node d i r s m -> ATMST s m ()

Print the justifying Environments which label a Node.

Translated from why-node in atms.lisp.

Environments, labels, and tables

debugEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()

Give a verbose printout of one Environment of an ATMS.

debugEnvTable :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> EnvTable d i r s m -> ATMST s m ()

Give a verbose printout of the Environments of an EnvTable of an ATMS.

formatNodeLabel :: (Monad m, NodeDatum d) => Node d i r s m -> ATMST s m String

Computation returning a one-line summary of the label of a Node of an ATMS.

debugNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

Give a verbose printout of the no-good Environments of an ATMS.

printEnv :: (MonadIO m, NodeDatum d) => Env d i r s m -> ATMST s m ()

Print an environment.

Translated from print-env in atms.lisp.

printNogoods :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

List the nogood Environments of an ATMS.

Translated from print-nogoods in atms.lisp.

printEnvs :: (MonadIO m, NodeDatum d) => ATMS d i r s m -> ATMST s m ()

Print the Environments of an ATMS.

Translated from print-envs in atms.lisp.

printEnvTable :: (MonadIO m, NodeDatum d) => EnvTable d i r s m -> ATMST s m ()

Print the Environments contained in the given EnvTable.

Translated from print-env-table in atms.lisp.

printTable :: (MonadIO m, NodeDatum d) => String -> EnvTable d i r s m -> ATMST s m ()

Print the entries of an EnvTable.

Translated from print-table in atms.lisp.

Justifications

debugJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()

Give a verbose printout of one Justification rule of an ATMS.

printJust :: (MonadIO m, NodeDatum d) => JustRule d i r s m -> ATMST s m ()

Print a more verbose description of a Justification rule of an ATMS.

Translated from print-just in atms.lisp.

formatJustification :: (Monad m, NodeDatum d) => Justification d i r s m -> ATMST s m String

Computation returning a one-line summary of the reason an ATMS may believe a Node.

Orphan instances

MonadIO m => MonadIO (STT s m)

Methods

liftIO :: IO a -> STT s m a