diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 63b0c9e..85ce966 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,10 +1,15 @@ import java.util.HashMap; import java.util.Map; +import java.util.Set; import constants.Types; +import inference.ProofSystem; import models.algebra.Type; import models.algebra.Variable; +import models.formulas.DependencyFormula; import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; import models.terms.Resource; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaDynamicDependency; @@ -18,9 +23,25 @@ public static void main(String[] args) { // - sandBox8(); + sandbox2(); } + static void sandbox() { + EvaluatableTerm t = new DependencyTerm(new Resource("a", 1), new Resource("b", 1), new Resource("c", 1)); + System.out.println(t.getSubTerms(EvaluatableTerm.class).values()); + } + + static void sandbox2() { + Resource a = new Resource("a", 1); + Resource b = new Resource("b", 1); + Resource c = new Resource("c", 1); + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(b, c); + DependencyFormula d3 = new DependencyFormula(a, c); + ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); + ps.dependencyInference(); + System.out.println(ps.getState().getHistory().getHistoryString(d3)); + } static void sandBox8() { MetaDynamicDependency md = new MetaDynamicDependency( diff --git a/src/main/java/inference/InferenceHistory.java b/src/main/java/inference/InferenceHistory.java new file mode 100644 index 0000000..95a0db3 --- /dev/null +++ b/src/main/java/inference/InferenceHistory.java @@ -0,0 +1,49 @@ +package inference; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Deque; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; + +import models.formulas.Formula; + +public class InferenceHistory { + + private Map> inferenceHistory; + + public InferenceHistory() { + inferenceHistory = new HashMap<>(); + } + + public void addHistory(Formula conclusion, InferenceHistoryNode node) { + this.inferenceHistory.computeIfAbsent(conclusion, k -> new HashSet<>()).add(node); + } + + public String getHistoryString(Formula conclusion) { + List result = new ArrayList<>(); + Deque q = new ArrayDeque<>(); + q.add(conclusion); + while (! q.isEmpty()) { + Formula formula = q.pollFirst(); + if (! inferenceHistory.containsKey(formula)) { + continue; + } + InferenceHistoryNode node = inferenceHistory.get(formula).iterator().next(); + result.add(conclusion.toString()); + result.add("--------------------------------" + node.getUsedRule().getName()); + result.add(node.getAssumptions().stream().map(v -> v.toString()).collect(Collectors.joining(", "))); + for (Formula f: node.getAssumptions()) { + q.add(f); + } + } + Collections.reverse(result); + return result.stream().collect(Collectors.joining("\n")); + } + +} diff --git a/src/main/java/inference/InferenceHistoryNode.java b/src/main/java/inference/InferenceHistoryNode.java new file mode 100644 index 0000000..fab43be --- /dev/null +++ b/src/main/java/inference/InferenceHistoryNode.java @@ -0,0 +1,35 @@ +package inference; +import com.google.common.base.Objects; + +import java.util.List; + +import lombok.Getter; +import models.formulas.Formula; + +@Getter +public class InferenceHistoryNode { + + private final List assumptions; + private final Formula conclusion; + private final InferenceRule usedRule; + + public InferenceHistoryNode(List assumptions, InferenceRule usedRule, Formula conclusion) { + this.assumptions = assumptions; + this.usedRule = usedRule; + this.conclusion = conclusion; + } + + @Override + public boolean equals(Object another) { + if (another instanceof InferenceHistoryNode node) { + return Objects.equal(node.assumptions, this.assumptions) && Objects.equal(node.usedRule, this.usedRule) && Objects.equal(this.conclusion, node.conclusion); + } + return false; + } + + @Override + public int hashCode() { + return Objects.hashCode(assumptions, conclusion, usedRule); + } + +} diff --git a/src/main/java/inference/ProofState.java b/src/main/java/inference/ProofState.java new file mode 100644 index 0000000..880bd70 --- /dev/null +++ b/src/main/java/inference/ProofState.java @@ -0,0 +1,165 @@ +package inference; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import lombok.Getter; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.Dependency; +import models.terms.EvaluatableTerm; +import models.terms.meta.MetaRDLTerm; + +@Getter +public class ProofState { + + private Set dependencies = new HashSet<>(); + private Set evaluatableTerms = new HashSet<>(); + private Set formulas = new HashSet<>(); + private Set dependencyFormulas = new HashSet<>(); + private Set equationFormulas = new HashSet<>(); + private Map>> matchedFormulas = new HashMap<>(); + private Map matchedTerms = new HashMap<>(); + private InferenceHistory history = new InferenceHistory(); + + public ProofState(Set existFormulas) { + for (Formula formula: existFormulas) { + formulas.add(formula); + if (formula instanceof DependencyFormula df) { + this.dependencyFormulas.add(df); + this.dependencies.add(df.getDependency()); + this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values()); + } else if (formula instanceof EquationFormula eq) { + this.equationFormulas.add(eq); + this.evaluatableTerms.addAll(eq.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); + this.evaluatableTerms.addAll(eq.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); + } + } + for (InferenceRule rule: ProofSystem.dependencyAxioms) { + List> terms = new ArrayList<>(); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + terms.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + terms.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + terms.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, terms); + } + for (EquationAxiom rule: ProofSystem.equationAxioms) { + List> formulas = new ArrayList<>(); + MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftSideHand(); + MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightSideHand(); + Set lhs = new HashSet<>(); + Set rhs = new HashSet<>(); + for (EvaluatableTerm term : evaluatableTerms) { + try { + if (! conclusionLeft.isMatchedBy(term).isEmpty()) { + lhs.add(term); + } + } catch (RuntimeException e) {} + try { + if (! conclusionRight.isMatchedBy(term).isEmpty()) { + rhs.add(term); + } + } catch(RuntimeException e) {} + } + matchedTerms.put(rule, new ConclusionMatchedTerm(lhs, rhs)); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + formulas.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + formulas.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + formulas.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, formulas); + } + } + + public void addFormuals(Set existFormulas) { + for (Formula formula: existFormulas) { + formulas.add(formula); + if (formula instanceof DependencyFormula df) { + this.dependencyFormulas.add(df); + this.dependencies.add(df.getDependency()); + this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values()); + } else if (formula instanceof EquationFormula eq) { + this.equationFormulas.add(eq); + this.evaluatableTerms.addAll(eq.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); + this.evaluatableTerms.addAll(eq.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); + } + } + for (InferenceRule rule: ProofSystem.dependencyAxioms) { + List> terms = new ArrayList<>(); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + terms.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + terms.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + terms.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, terms); + } + for (EquationAxiom rule: ProofSystem.equationAxioms) { + List> formulas = new ArrayList<>(); + MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftSideHand(); + MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightSideHand(); + Set lhs = new HashSet<>(); + Set rhs = new HashSet<>(); + for (EvaluatableTerm term : evaluatableTerms) { + if (! conclusionLeft.isMatchedBy(term).isEmpty()) { + lhs.add(term); + } + if (! conclusionRight.isMatchedBy(term).isEmpty()) { + rhs.add(term); + } + } + matchedTerms.put(rule, new ConclusionMatchedTerm(lhs, rhs)); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + formulas.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + formulas.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + formulas.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, formulas); + } + } + + public void addHistory(List assumptions, InferenceRule usedAxiom, Formula conclusion) { + InferenceHistoryNode node = new InferenceHistoryNode(assumptions, usedAxiom, conclusion); + this.history.addHistory(conclusion, node); + } + + record ConclusionMatchedTerm(Set leftSideHands, Set rightSideHands) {}; + +} diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 51fda3f..f96eb7b 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -1,5 +1,6 @@ package inference; +import java.util.ArrayList; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -18,14 +19,18 @@ import inference.axioms.RightSubstitution; import inference.axioms.UncurriedMapping; import inference.axioms.Uncurrying; +import lombok.Getter; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; +import models.terms.Dependency; +import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.meta.MetaEvaluatableTermVariable; +import utils.Product; public class ProofSystem { @@ -120,78 +125,129 @@ public static final InferenceRule compositeMapping = new CompositeMapping(); - public static final InferenceRule constatnMapping = new ConstantMapping(); + public static final InferenceRule constantMapping = new ConstantMapping(); public static final InferenceRule uncurriedMapping = new UncurriedMapping(); public static final InferenceRule dependencyExtension = new DependencyExtension(); - /* - * new InferenceRule( - "", - List.of(), - List.of(), - null, - null, - null, - null, - null - ); - */ - - - private static final List axioms = List.of( -// reflexivity, -// symmetry, -// transitivity, -// rightSubstitution, -// leftSubstitution, -// identity, -// mapComposition, -// constantness, -// rightNormalization, -// pseudoConstantness, -// identityMapping, -// compositeMapping, -// constantMapping, -// slicedMapping, -// memberSubstitution, -// membershipChain, -// collectionSubstitution, -// setEquivelence, -// setHomomorphism, -// leftProjection, -// rightProjection, -// domainMembership, -// codomainMembership, -// codomainMembership2 + public static final List axioms = List.of( + reflexivity, + symmetry, + transitivity, + rightSubstitution, + leftSubstitution, + identity, + mapComposition, + constantness, + pseudoConstantness, + uncurrying, + identityMapping, + argumentExtension, + argumentReduction, + compositeMapping, + constantMapping, + uncurriedMapping, + dependencyExtension ); - - private Set dependencyFormulas = new HashSet<>(); - private Set equationFormulas = new HashSet<>(); - private Set terms = new HashSet<>(); + public static final List equationAxioms = List.of( + reflexivity, + symmetry, + transitivity, + rightSubstitution, + leftSubstitution, + identity, + mapComposition, + constantness, + pseudoConstantness, + uncurrying + ); - public void addDependencyFormula(DependencyFormula dep) { - dependencyFormulas.add(dep); - addExistTerms(dep); + public static final List dependencyAxioms = List.of( + identityMapping, + argumentExtension, + argumentReduction, + compositeMapping, + constantMapping, + uncurriedMapping, + dependencyExtension + ); + + private Set assumptions; + private Formula conclusion; + @Getter + private ProofState state; + + + public ProofSystem(Set assumptions, Formula conclusion) { + state = new ProofState(assumptions); + this.assumptions = assumptions; + this.conclusion = conclusion; } - public void addEquationFormula(EquationFormula eq) { - equationFormulas.add(eq); - addExistTerms(eq); + public void inference() { } - private void addExistTerms(Formula formula) { - if (formula instanceof EquationFormula) { - RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand(); - RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand(); - terms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values()); - terms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values()); - } else if (formula instanceof DependencyFormula) { - RDLTerm dependency = ((DependencyFormula) formula).getDependency(); - terms.addAll(dependency.getSubTerms(RDLTerm.class).values()); - } + public void dependencyInference() { + if (conclusion instanceof EquationFormula eq) { + RDLTerm lhs = eq.getLeftSideHand(); + RDLTerm rhs = eq.getRightSideHand(); + Dependency leftDependency = lhs.getDependency(); + Dependency rightDependency = rhs.getDependency(); + while((! state.getDependencies().contains(leftDependency)) && (! state.getDependencies().contains(rightDependency))) { + state.addFormuals(dependencyInferenceStep()); + } + } else if (conclusion instanceof DependencyFormula dep) { + while((! state.getDependencyFormulas().contains(dep))) { + state.addFormuals(dependencyInferenceStep()); + } + } + } + + public Set dependencyInferenceStep() { + Set result = new HashSet<>(); + for (InferenceRule rule: dependencyAxioms) { + List> matchedFormulas = new ArrayList<>(); + for (Set formulas: state.getMatchedFormulas().get(rule)) { + matchedFormulas.add(new ArrayList<>(formulas)); + } + for (List formulas: Product.product(matchedFormulas)) { + Set results = rule.derive(formulas); + for (Formula res: results) { + state.addHistory(formulas, rule, res); + } + result.addAll(results); + } + } + return result; + } + + public Set equationInferenceStep() { + Set result = new HashSet<>(); + for (EquationAxiom rule: equationAxioms) { + List> matchedFormulas = new ArrayList<>(); + for (Set formulas: state.getMatchedFormulas().get(rule)) { + matchedFormulas.add(new ArrayList<>(formulas)); + } + for (EvaluatableTerm left: state.getMatchedTerms().get(rule).leftSideHands()) { + for (List formulas: Product.product(matchedFormulas)) { + for (EvaluatableTerm right: rule.apply(formulas, left)) { + result.add(new EquationFormula(left, right)); + state.addHistory(formulas, rule, new EquationFormula(left, right)); + } + } + } + for (EvaluatableTerm right: state.getMatchedTerms().get(rule).rightSideHands()) { + for (List formulas: Product.product(matchedFormulas)) { + for (EvaluatableTerm left: rule.apply(formulas, right)) { + result.add(new EquationFormula(left, right)); + state.addHistory(formulas, rule, new EquationFormula(left, right)); + } + } + } + } + return result; } } diff --git a/src/main/java/inference/axioms/ArgumentReduction.java b/src/main/java/inference/axioms/ArgumentReduction.java index 40b47ec..28b3e3d 100644 --- a/src/main/java/inference/axioms/ArgumentReduction.java +++ b/src/main/java/inference/axioms/ArgumentReduction.java @@ -65,6 +65,7 @@ } + public Set derive(List assumptions, MatchConstraint constraint) { Set result = new HashSet<>(); if (this.assumptions.size() != assumptions.size()) { diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index 4e7c6c4..8a25375 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,12 +1,12 @@ package models.terms; +import com.google.common.collect.TreeMultiset; + import java.util.ArrayList; import java.util.Arrays; import java.util.List; import java.util.stream.Collectors; -import com.google.common.collect.TreeMultiset; - import exceptions.SyntaxException; import lombok.Getter; @@ -37,6 +37,11 @@ } @Override + public Dependency getDependency() { + return this; + } + + @Override public int getMaxIndex() { return 1 + dependedTerms.size(); } diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index e9fa90c..1acfd5b 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -92,6 +92,21 @@ this(dependingTerm, Arrays.asList(terms)); } + @Override + public Dependency getDependency() { + RDLTerm dependingTerm; + List dependedTerms = new ArrayList<>(); + if (this.dependingTerm instanceof Resource || this.dependingTerm instanceof ResourceConstant) { + dependingTerm = this.dependingTerm; + } else { + dependingTerm = this.dependingTerm.getDependency(); + } + for (EvaluatableTerm dependedTerm: this.termPairs.keySet()) { + dependedTerms.add(dependedTerm); + } + return new Dependency(dependingTerm, dependedTerms); + } + @Override public int getMaxIndex() { diff --git a/src/main/java/models/terms/PrimedTerm.java b/src/main/java/models/terms/PrimedTerm.java deleted file mode 100644 index 44be53e..0000000 --- a/src/main/java/models/terms/PrimedTerm.java +++ /dev/null @@ -1,74 +0,0 @@ -package models.terms; - -import lombok.Getter; - -@Getter -public class PrimedTerm extends EvaluatableTerm { - - private EvaluatableTerm primedTerm; - private boolean isResource; - - public PrimedTerm(EvaluatableTerm term) { - super(term.getOrder(), term.getSize()); - this.primedTerm = term; - this.isResource = term instanceof Resource; - } - - @Override - public int getMaxIndex() { - return primedTerm.getMaxIndex(); - } - - @Override - public int getMaxDepth() { - return primedTerm.getMaxDepth(); - } - - @Override - public String toString() { - return primedTerm.toString() + "'"; - } - - @Override - public String toStringWithOrder() { - return toString() + "(" + primedTerm.getOrder() + ")"; - } - - @Override - public int hashCode() { - return toStringWithOrder().hashCode(); - } - - @Override - public boolean equals(Object other) { - if (! (other instanceof PrimedTerm)) { - return false; - } - PrimedTerm otherPrimed = (PrimedTerm) other; - EvaluatableTerm otherTerm = otherPrimed.getPrimedTerm(); - return this.primedTerm.equals(otherTerm); - } - - @Override - public Object clone() { - return new PrimedTerm(primedTerm); - } - - @Override - public boolean isLinearRightNormalized() { - return primedTerm.isLinearRightNormalized(); - } - - @Override - public EvaluatableTerm linearRightNormalize() { - return new PrimedTerm(primedTerm.linearRightNormalize()); - } - - @Override - public void selfLinearRightNormalize() { - primedTerm.selfLinearRightNormalize(); - } - - - -} diff --git a/src/main/java/models/terms/RDLTerm.java b/src/main/java/models/terms/RDLTerm.java index e45cd6b..4c30b56 100644 --- a/src/main/java/models/terms/RDLTerm.java +++ b/src/main/java/models/terms/RDLTerm.java @@ -20,6 +20,8 @@ return getOrder(); } + public abstract Dependency getDependency(); + public abstract int getMaxIndex(); public abstract int getMaxDepth(); diff --git a/src/main/java/models/terms/Resource.java b/src/main/java/models/terms/Resource.java index 8e0597c..5603097 100644 --- a/src/main/java/models/terms/Resource.java +++ b/src/main/java/models/terms/Resource.java @@ -13,6 +13,11 @@ } @Override + public Dependency getDependency() { + return null; + } + + @Override public int getMaxIndex() { return 1; } diff --git a/src/main/java/models/terms/ResourceConstant.java b/src/main/java/models/terms/ResourceConstant.java index 48755a2..105590b 100644 --- a/src/main/java/models/terms/ResourceConstant.java +++ b/src/main/java/models/terms/ResourceConstant.java @@ -1,7 +1,6 @@ package models.terms; import lombok.Getter; -import models.algebra.Symbol; import models.algebra.Type; @Getter @@ -23,6 +22,11 @@ } @Override + public Dependency getDependency() { + return null; + } + + @Override public int getMaxIndex() { return 1; } diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index e262457..2ef365c 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -82,7 +82,7 @@ constraint.setBinding(new Variable("te0"), l); constraint.setBinding(new Variable("te1"), m); constraint.getContext().put("maxDepth", 1); - Set res = ProofSystem.constatnMapping.derive(List.of(), constraint); + Set res = ProofSystem.constantMapping.derive(List.of(), constraint); assertTrue(res.contains(new DependencyFormula(a, l, m))); }