diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java index 9d85181..64a89b0 100644 --- a/src/main/java/inference/EquationAxiom.java +++ b/src/main/java/inference/EquationAxiom.java @@ -27,27 +27,27 @@ super(name, assumptions, conclusion); } - public Set apply(Listassumptions, EvaluatableTerm leftSideHand) { + protected EquationAxiom(String name) { + super(name); + } + + public Set apply(List assumptions, EvaluatableTerm term) { + return apply(assumptions, term, MatchConstraint.createDefault()); + } + + public Set apply(Listassumptions, EvaluatableTerm leftSideHand, MatchConstraint constraint) { Set result = new HashSet<>(); boolean isLeft = true; if (assumptions.size() < this.assumptions.size()) { return new HashSet<>(); } - Set matchResult = new HashSet<>(); - matchResult.add(MatchConstraint.createDefault()); - for (int i = 0; i < assumptions.size(); i++) { - Formula assumption = assumptions.get(i); - MetaFormula metaAssumption = this.assumptions.get(i); - matchResult = metaAssumption.isMatchedBy(assumption, matchResult); - if (matchResult.isEmpty()) { - return new HashSet<>(); - } - } + Set matchResult = assumptionMatch(assumptions, constraint); + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - Set conclusionMatchResult = ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(leftSideHand, matchResult); + Set conclusionMatchResult = conclusionLeftSideHandMatch(leftSideHand, matchResult); if (conclusionMatchResult.isEmpty()) { isLeft = false; - conclusionMatchResult = ((MetaRDLTerm) metaConclusion.getRightSideHand()).isMatchedBy(leftSideHand, matchResult); + conclusionMatchResult = conclusionRightSideHandMatch(leftSideHand, matchResult); if (conclusionMatchResult.isEmpty()) { return new HashSet<>(); } @@ -67,9 +67,32 @@ return result; } + protected Set assumptionMatch(Listassumptions, MatchConstraint constraint) { + Set matchResult = new HashSet<>(); + matchResult.add(constraint); + for (int i = 0; i < assumptions.size(); i++) { + Formula assumption = assumptions.get(i); + MetaFormula metaAssumption = this.assumptions.get(i); + matchResult = metaAssumption.isMatchedBy(assumption, matchResult); + if (matchResult.isEmpty()) { + return new HashSet<>(); + } + } + return matchResult; + } + + protected Set conclusionLeftSideHandMatch(EvaluatableTerm term, Set matchResult) { + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + return ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(term, matchResult); + } + + protected Set conclusionRightSideHandMatch(EvaluatableTerm term, Set matchResult) { + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + return ((MetaRDLTerm) metaConclusion.getRightSideHand()).isMatchedBy(term, matchResult); + } - private static Set requiredAssumptions(EvaluatableTerm term) { + protected static Set requiredAssumptions(EvaluatableTerm term) { if (term instanceof Resource) { return new HashSet<>(); } @@ -95,7 +118,7 @@ return result; } - private static boolean conclusionCheck(EvaluatableTerm leftSideHand, Set formulas) { + protected static boolean conclusionCheck(EvaluatableTerm leftSideHand, Set formulas) { for (Formula formula: requiredAssumptions(leftSideHand)) { if (! formulas.contains(formula)) { return false; diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index c7a2f34..5ab033f 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -2,21 +2,19 @@ import java.util.HashSet; import java.util.List; -import java.util.Map; import java.util.Set; +import inference.axioms.Identity; +import inference.axioms.LeftSubstitution; +import inference.axioms.MapComposition; +import inference.axioms.RightSubstitution; 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.RDLTerm; -import models.terms.meta.MetaDynamicDependency; -import models.terms.meta.MetaDynamicDependencyTerm; import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaTermGenerator; public class ProofSystem { @@ -64,203 +62,16 @@ ); - public static final EquationAxiom rightSubstitution = new EquationAxiom( - "Right Substitution", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("ue")), - new MetaEvaluatableTermVariable(new Variable("ve")) - ), - new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 2; - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 3; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 3; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ve")) - ) - ) - ); + public static final EquationAxiom rightSubstitution = new RightSubstitution(); - public static final InferenceRule leftSubstitution = new EquationAxiom( - "Left Substitution", - List.of( - new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))) - ), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ); + public static final EquationAxiom leftSubstitution = new LeftSubstitution(); - public static final EquationAxiom identity = new EquationAxiom( - "Identity", - List.of(), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("ue")); - } - return new MetaEvaluatableTermVariable(new Variable("ve")); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ); + public static final EquationAxiom identity = new Identity(); - public static final EquationAxiom mapComposition = new EquationAxiom( - "Map Composition", - List.of( - new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 2; - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - context.put("uIndex", curIndex); - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); - } - }, - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 3; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } else { - return new MetaEvaluatableTermVariable(new Variable("tex" + curIndex / 2)); - } - } - }, - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); - } else { - return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); - } - } - }, - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - int uIndex = (Integer) context.get("uIndex"); - if (curIndex % 2 == 0 && curIndex < uIndex) { - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); - } else if (curIndex < uIndex ){ - return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); - } else if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } else { - return new MetaEvaluatableTermVariable(new Variable("tex" + curIndex / 2)); - } - } - }, - new MetaEvaluatableTermVariable(new Variable("se")) - ) - ) - ); + public static final EquationAxiom mapComposition = new MapComposition(); // // public static final InferenceRule constantness = new Constantness(); // diff --git a/src/main/java/inference/axioms/Constantness.java b/src/main/java/inference/axioms/Constantness.java new file mode 100644 index 0000000..d22fe54 --- /dev/null +++ b/src/main/java/inference/axioms/Constantness.java @@ -0,0 +1,44 @@ +package inference.axioms; + +import java.util.Map; + +import inference.EquationAxiom; +import inference.InferenceOrderConstraint; +import models.algebra.Variable; +import models.formulas.meta.MetaEquationFormula; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import models.terms.meta.OrderConstraint; +import utils.ExpressionUtils; + +public class Constantness extends EquationAxiom{ + + public Constantness() { + super("Constantness"); + defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + if (curDepth == maxDepth && curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("m-" + (maxDepth - curDepth))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2)); + } + } + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ); + } + +} diff --git a/src/main/java/inference/axioms/Identity.java b/src/main/java/inference/axioms/Identity.java new file mode 100644 index 0000000..8566314 --- /dev/null +++ b/src/main/java/inference/axioms/Identity.java @@ -0,0 +1,68 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class Identity extends EquationAxiom{ + + public Identity() { + super("Identity"); + this.conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ); + } + + @Override + public Set apply(Listassumptions, EvaluatableTerm term) { + Set result = new HashSet<>(); + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = new HashSet<>(); + matchResult.add(MatchConstraint.createDefault()); + Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + return new HashSet<>(); + } + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + MetaEvaluatableTermVariable right = (MetaEvaluatableTermVariable) metaConclusion.getRightSideHand(); + for (MatchConstraint matchRes: conclusionMatchResult) { + try { + result.add((EvaluatableTerm) right.substitute(matchRes.getBinding(), matchRes.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/LeftSubstitution.java b/src/main/java/inference/axioms/LeftSubstitution.java new file mode 100644 index 0000000..8588ecd --- /dev/null +++ b/src/main/java/inference/axioms/LeftSubstitution.java @@ -0,0 +1,94 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class LeftSubstitution extends EquationAxiom { + + public LeftSubstitution() { + super("Left Substitution"); + assumptions.add(new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + )); + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + } + + @Override + public Set apply(Listassumptions, EvaluatableTerm term) { + Set result = new HashSet<>(); + boolean isLeft = true; + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + isLeft = false; + conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + return new HashSet<>(); + } + } + for (MatchConstraint matchRes: conclusionMatchResult) { + matchRes.getContext().put("maxIndex", term.getMaxIndex()); + matchRes.getContext().put("maxDepth", term.getMaxDepth()); + try { + EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()); + if (isLeft) { + result.add(eq.getRightSideHand()); + } else { + result.add(eq.getLeftSideHand()); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java new file mode 100644 index 0000000..f8a3ce3 --- /dev/null +++ b/src/main/java/inference/axioms/MapComposition.java @@ -0,0 +1,154 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class MapComposition extends EquationAxiom { + + public MapComposition() { + super("Map Composition"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + context.put("tIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("uIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + int tIndex = (Integer) context.get("tIndex"); + if (curIndex >= tIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int uIndex = (Integer) context.get("uIndex"); + if (curIndex >= uIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int uIndex = (Integer) context.get("uIndex"); + int tIndex = (Integer) context.get("tIndex"); + if (curIndex >= uIndex * 2 + tIndex * 2) { + return null; + } + if (curIndex % 2 == 0 && curIndex < uIndex * 2) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } else if (curIndex < uIndex * 2) { + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); + } + curIndex -= uIndex * 2; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + } + + @Override + public Set apply(Listassumptions, EvaluatableTerm term) { + Set result = new HashSet<>(); + boolean isLeft = true; + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + isLeft = false; + conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + return new HashSet<>(); + } + } + for (MatchConstraint matchRes: conclusionMatchResult) { + matchRes.getContext().put("maxIndex", 10000); + matchRes.getContext().put("maxDepth", 1); + try { + EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()); + if (isLeft) { + result.add(eq.getRightSideHand()); + } else { + result.add(eq.getLeftSideHand()); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java new file mode 100644 index 0000000..41c7d01 --- /dev/null +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -0,0 +1,115 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class RightSubstitution extends EquationAxiom { + + public RightSubstitution() { + super("Right Substitution"); + assumptions.add(new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("ue")), + new MetaEvaluatableTermVariable(new Variable("ve")) + )); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex)); + } + + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + this.conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ve")) + ) + ); + } + + + @Override + public Set apply(Listassumptions, EvaluatableTerm term) { + Set result = new HashSet<>(); + boolean isLeft = true; + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + isLeft = false; + conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + return new HashSet<>(); + } + } + for (MatchConstraint matchRes: conclusionMatchResult) { + matchRes.getContext().put("maxIndex", term.getMaxIndex()); + matchRes.getContext().put("maxDepth", term.getMaxDepth()); + try { + EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()); + if (isLeft) { + result.add(eq.getRightSideHand()); + } else { + result.add(eq.getLeftSideHand()); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/models/terms/meta/MetaDependencyTerm.java b/src/main/java/models/terms/meta/MetaDependencyTerm.java index 3adedb8..cd06b0d 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDependencyTerm.java @@ -65,8 +65,11 @@ if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) { return result; } + if (another.getChildren().size() != this.getChildren().size()) { + return new HashSet<>(); + } result = dependingTermMatch(another, constraint); - return termPairsMatch(another, result); + return termPairsMatch((DependencyTerm) another, result); } private Set dependingTermMatch(RDLTerm another, MatchConstraint constraint) { @@ -83,7 +86,7 @@ return new HashSet<>(); } - private Set termPairsMatch(RDLTerm another, Set constraint) { + private Set termPairsMatch(DependencyTerm another, Set constraint) { Set result = new HashSet<>(); for (List perm : Permutation.permutation((another.getChildren().size() - 1) / 2)) { Set localResult = new HashSet<>(constraint); diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 48f1eaa..eca1496 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,12 +1,12 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; -import org.junit.jupiter.api.Test; - import java.util.HashSet; import java.util.List; import java.util.Set; +import org.junit.jupiter.api.Test; + import inference.ProofSystem; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -65,14 +65,30 @@ @Test void LeftSubTest() { + EquationFormula eq1 = new EquationFormula(a, b); + Set formulas = ProofSystem.leftSubstitution.apply(List.of(eq1), new DependencyTerm(a, c, d)); + assertTrue(formulas.contains(new DependencyTerm(b, c, d))); + formulas = ProofSystem.leftSubstitution.apply(List.of(eq1), new DependencyTerm(b, c, d)); + assertTrue(formulas.contains(new DependencyTerm(a, c, d))); + } @Test void IdentityTest() { + Set terms = ProofSystem.identity.apply(List.of(), new DependencyTerm(a, a, b)); + assertTrue(terms.contains(b)); } @Test void MapCompositionTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyFormula d2 = new DependencyFormula(b, d, e); + DependencyTerm dt1 = new DependencyTerm(a, d, f, e, g, c, h); + DependencyTerm dt2 = new DependencyTerm(a, b, new DependencyTerm(b, d, f, e, g), c, h); + Set terms = ProofSystem.mapComposition.apply(List.of(d1, d2), dt1); + assertTrue(terms.contains(dt2)); + terms = ProofSystem.mapComposition.apply(List.of(d1, d2), dt2); + assertTrue(terms.contains(dt1)); } @Test