{-# LANGUAGE FlexibleInstances, UndecidableInstances #-} -------------------------------------------------------------------------------- -- See end of this file for licence information. -------------------------------------------------------------------------------- -- | -- Module : RDFProof -- Copyright : (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke -- License : GPL V2 -- -- Maintainer : Douglas Burke -- Stability : experimental -- Portability : FlexibleInstances, UndecidableInstances -- -- This module instantiates the 'Proof' framework for -- constructing proofs over 'RDFGraph' expressions. -- The intent is that this can be used to test some -- correspondences between the RDF Model theory and -- corresponding proof theory based on closure rules -- applied to the graph, per . -- -------------------------------------------------------------------------------- module Swish.RDF.RDFProof ( RDFProof, RDFProofStep , makeRDFProof, makeRDFProofStep , makeRdfInstanceEntailmentRule , makeRdfSubgraphEntailmentRule , makeRdfSimpleEntailmentRule ) where import Swish.RDF.RDFQuery ( rdfQueryInstance , rdfQuerySubs ) import Swish.RDF.RDFRuleset ( RDFFormula, RDFRule, RDFRuleset ) import Swish.RDF.RDFGraph ( RDFLabel(..), RDFGraph --, makeBlank , merge , allLabels , remapLabelList {-, newNode, newNodes , toRDFGraph -}, emptyRDFGraph ) import Swish.RDF.VarBinding (makeVarBinding) import Swish.RDF.Proof ( Proof(..), Step(..) ) import Swish.RDF.Rule ( Expression(..), Rule(..) ) import Swish.Utils.Namespace (ScopedName) import Swish.RDF.GraphClass ( Label(..), LDGraph(..), replaceArcs ) import Swish.Utils.LookupMap ( makeLookupMap, mapFind ) import Swish.Utils.ListHelpers ( subset , powerSet , powerSequencesLen , flist ) ------------------------------------------------------------ -- Type instantiation of Proof framework for RDFGraph data ------------------------------------------------------------ -- -- This is a partial instantiation of the proof framework. -- Details for applying inference rules are specific to the -- graph instance type. ------------------------------------------------------------ -- Proof datatypes for graph values ------------------------------------------------------------ -- The following is an orphan instance -- |Instances of 'LDGraph' are also instance of the -- @Expression@ class, for which proofs can be constructed. -- The empty RDF graph is always @True@ (other enduring -- truths are asserted as axioms). instance (Label lb, LDGraph lg lb) => Expression (lg lb) where isValid = null . getArcs ------------------------------------------------------------ -- Define RDF-specific types for proof framework ------------------------------------------------------------ type RDFProof = Proof RDFGraph type RDFProofStep = Step RDFGraph ------------------------------------------------------------ -- Helper functions for constructing proofs on RDF graphs ------------------------------------------------------------ -- |Make an RDF graph proof step. -- makeRDFProofStep :: RDFRule -- ^ rule to use for this step -> [RDFFormula] -- ^ antecedent RDF formulae for this step -> RDFFormula -- ^ RDF formula that is the consequent for this step -> RDFProofStep makeRDFProofStep rul ants con = Step { stepRule = rul , stepAnt = ants , stepCon = con } -- |Make an RDF proof. -- makeRDFProof :: [RDFRuleset] -- ^ RDF rulesets that constitute a proof context for this proof -> RDFFormula -- ^ initial statement from which the goal is claimed to be proven -> RDFFormula -- ^ statement that is claimed to be proven -> [RDFProofStep] -> RDFProof makeRDFProof rsets base goal steps = Proof { proofContext = rsets , proofInput = base , proofResult = goal , proofChain = steps } ------------------------------------------------------------ -- RDF instance entailment inference rule ------------------------------------------------------------ -- |Make an inference rule dealing with RDF instance entailment; -- i.e. entailments that are due to replacement of a URI or literal -- node with a blank node. -- -- The part of this rule expected to be useful is 'checkInference'. -- The 'fwdApply' and 'bwdApply' functions defined here may return -- rather large results if applied to graphs with many variables or -- a large vocabulary, and are defined for experimentation. -- -- Forward and backward chaining is performed with respect to a -- specified vocabulary. In the case of backward chaining, it would -- otherwise be impossible to bound the options thus generated. -- In the case of forward chaining, it is often not desirable to -- have the properties generalized. If forward or backward backward -- chaining will not be used, supply an empty vocabulary. -- Note: graph method 'allNodes' can be used to obtain a list of all -- the subjects and objuects used ina graph, not counting nested -- formulae; use a call of the form: -- -- > allNodes (not . labelIsVar) graph -- makeRdfInstanceEntailmentRule :: ScopedName -- ^ name -> [RDFLabel] -- ^ vocabulary -> RDFRule makeRdfInstanceEntailmentRule name vocab = newrule where newrule = Rule { ruleName = name , fwdApply = rdfInstanceEntailFwdApply vocab , bwdApply = rdfInstanceEntailBwdApply vocab , checkInference = rdfInstanceEntailCheckInference } -- Instance entailment forward chaining -- -- Note: unless the initial graph is small, the total result -- here could be very large. The existential generalizations are -- sequenced in increasing number of substitutions applied. -- This sequencing is determined by the powerset function used, -- which generates subsets in increasing order of size -- (see module 'ListHelpers'). -- -- The instances generated are all copies of the merge of the -- supplied graphs, with some or all of the non-variable nodes -- replaced by blank nodes. rdfInstanceEntailFwdApply :: [RDFLabel] -> [RDFGraph] -> [RDFGraph] rdfInstanceEntailFwdApply vocab ante = let -- Merge antecedents to single graph, renaming bnodes if needed. -- (Null test and using 'foldl1' to avoid merging if possible.) mergeGraph = if null ante then emptyRDFGraph else foldl1 merge ante -- Obtain lists of variable and non-variable nodes -- (was: nonvarNodes = allLabels (not . labelIsVar) mergeGraph) nonvarNodes = vocab varNodes = allLabels labelIsVar mergeGraph -- Obtain list of possible remappings for non-variable nodes mapList = remapLabelList nonvarNodes varNodes mapSubLists = powerSet mapList mapGr ls = fmap (\l -> mapFind l l (makeLookupMap ls)) in -- Return all remappings of the original merged graph flist (map mapGr mapSubLists) mergeGraph -- Instance entailment backward chaining (for specified vocabulary) -- -- [[[TODO: this is an incomplete implementation, there being no -- provision for instantiating some variables and leaving others -- alone. This can be overcome in many cases by combining instance -- and subgraph chaining. -- Also, there is no provision for instantiating some variables in -- a triple and leaving others alone. This may be fixed later if -- this function is really needed to be completely faithful to the -- precise notion of instance entailment.]]] rdfInstanceEntailBwdApply :: [RDFLabel] -> RDFGraph -> [[RDFGraph]] rdfInstanceEntailBwdApply vocab cons = let -- Obtain list of variable nodes varNodes = allLabels labelIsVar cons -- Generate a substitution for each combination of variable -- and vocabulary node. varBindings = map (makeVarBinding . zip varNodes) vocSequences vocSequences = powerSequencesLen (length varNodes) vocab in -- Generate a substitution for each combination of variable -- and vocabulary: [ rdfQuerySubs [v] cons | v <- varBindings ] -- Instance entailment inference checker rdfInstanceEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool rdfInstanceEntailCheckInference ante cons = let mante = if null ante then emptyRDFGraph -- merged antecedents else foldl1 merge ante qvars = rdfQueryInstance cons mante -- all query matches bsubs = rdfQuerySubs qvars cons -- all back substitutions in -- Return True if any back-substitution matches the original -- merged antecendent graph. any (mante ==) bsubs -- Instance entailment notes. -- -- Relation to simple entailment (s-entails): -- -- (1) back-substitution yields original graph -- ex:s1 ex:p1 ex:o1 s-entails ex:s1 ex:p1 _:o1 by [_:o1/ex:o1] -- -- (2) back-substitution yields original graph -- ex:s1 ex:p1 ex:o1 s-entails ex:s1 ex:p1 _:o2 by [_:o2/ex:o1] -- ex:s1 ex:p1 _:o1 ex:s1 ex:p1 _:o3 [_:o3/_:o1] -- -- (3) back-substitution does not yield original graph -- ex:s1 ex:p1 ex:o1 s-entails ex:s1 ex:p1 _:o2 by [_:o2/ex:o1] -- ex:s1 ex:p1 _:o1 ex:s1 ex:p1 _:o3 [_:o3/ex:o1] -- -- (4) consider -- ex:s1 ex:p1 ex:o1 s-entails ex:s1 ex:p1 ex:o1 -- ex:s1 ex:p1 ex:o2 ex:s1 ex:p1 ex:o2 -- ex:s1 ex:p1 ex:o3 ex:s1 ex:p1 _:o1 -- ex:s1 ex:p1 _:o2 -- where [_:o1/ex:o1,_:o2/ex:o2] yields a simple entailment but not -- an instance entailment, but [_:o1/ex:o3,_:o2/ex:o3] is also -- (arguably) an instance entailment. Therefore, it is not sufficient -- to look only at the "largest" substitutions to determine instance -- entailment. -- -- All this means that when checking for instance entailment by -- back substitution, all of the query results must be checked. -- This seems clumsy. If this function is heavily used with -- multiple query matches, a modified query that uses each -- triple of the target graph exactly once may be required. ------------------------------------------------------------ -- RDF subgraph entailment inference rule ------------------------------------------------------------ -- |Make an inference rule dealing with RDF subgraph entailment. -- The part of this rule expected to be useful is 'checkInference'. -- The 'fwdApply' function defined here may return rather large -- results. But in the name of completeness and experimentation -- with the possibilities of lazy evaluation, it has been defined. -- -- Backward chaining is not performed, as there is no reasonable way -- to choose a meaningful supergraph of that supplied. makeRdfSubgraphEntailmentRule :: ScopedName -> RDFRule makeRdfSubgraphEntailmentRule name = newrule where newrule = Rule { ruleName = name , fwdApply = rdfSubgraphEntailFwdApply , bwdApply = const [] , checkInference = rdfSubgraphEntailCheckInference } -- Subgraph entailment forward chaining -- -- Note: unless the initial graph is small, the total result -- here could be very large. The subgraphs are sequenced in -- increasing size of the sub graph. This sequencing is determined -- by the 'powerSet' function used which generates subsets in -- increasing order of size (see module 'ListHelpers'). rdfSubgraphEntailFwdApply :: [RDFGraph] -> [RDFGraph] rdfSubgraphEntailFwdApply ante = let -- Merge antecedents to single graph, renaming bnodes if needed. -- (Null test and using 'foldl1' to avoid merging if possible.) mergeGraph = if null ante then emptyRDFGraph else foldl1 merge ante in -- Return all subgraphs of the full graph constructed above map (replaceArcs mergeGraph) (init $ powerSet $ getArcs mergeGraph) -- Subgraph entailment inference checker -- -- This is of dubious utiltiy, as it doesn't allow for node renaming. -- The simple entailment inference rule is probably more useful here. rdfSubgraphEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool rdfSubgraphEntailCheckInference ante cons = let -- Combine antecedents to single graph, renaming bnodes if needed. -- (Null test and using 'foldl1' to avoid merging if possible.) fullGraph = if null ante then emptyRDFGraph else foldl1 add ante in -- Check each consequent graph arc is in the antecedent graph getArcs cons `subset` getArcs fullGraph ------------------------------------------------------------ -- RDF simple entailment inference rule ------------------------------------------------------------ -- |Make an inference rule dealing with RDF simple entailment. -- The part of this rule expected to be useful is 'checkInference'. -- The 'fwdApply' and 'bwdApply' functions defined return null -- results, indicating that they are not useful for the purposes -- of proof discovery. makeRdfSimpleEntailmentRule :: ScopedName -> RDFRule makeRdfSimpleEntailmentRule name = newrule where newrule = Rule { ruleName = name , fwdApply = const [] , bwdApply = const [] , checkInference = rdfSimpleEntailCheckInference } -- Simple entailment inference checker -- -- Note: antecedents here are presumed to share bnodes. -- (Use 'merge' instead of 'add' for non-shared bnodes) -- rdfSimpleEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool rdfSimpleEntailCheckInference ante cons = let agr = if null ante then emptyRDFGraph else foldl1 add ante in not $ null $ rdfQueryInstance cons agr {- original.. not $ null $ rdfQueryInstance cons (foldl1 merge ante) -} -------------------------------------------------------------------------------- -- -- Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke -- All rights reserved. -- -- This file is part of Swish. -- -- Swish is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2 of the License, or -- (at your option) any later version. -- -- Swish is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with Swish; if not, write to: -- The Free Software Foundation, Inc., -- 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- --------------------------------------------------------------------------------