diff --git a/src/main/java/Main.java b/src/main/java/Main.java index e7242df..fac8790 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,13 +1,17 @@ -import com.google.common.collect.TreeMultimap; - import java.util.HashMap; import java.util.Map; +import com.google.common.collect.TreeMultimap; + import constants.Types; import models.algebra.Constant; import models.algebra.Expression; import models.algebra.Type; import models.algebra.Variable; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.MetaTermGenerator; public class Main { @@ -17,6 +21,7 @@ // sandbox(); sandbox2(); + sandbox3(); } @@ -43,4 +48,17 @@ System.out.println(tmp.get(1)); } + static void sandbox3() { + MetaDynamicDependency d1 = new MetaDynamicDependency((ci, cd, mi, md, context) -> new MetaResource(new Variable("x" + ci))); + MetaDynamicDependency d2 = new MetaDynamicDependency(new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + if (curIndex == 0 && curDepth < maxDepth) return new MetaDynamicDependency(this); + else return new MetaResource(new Variable("x" + curIndex + "_" + curDepth)); + } + }); + d2.generate(0, 2, 2, null); + System.out.println(d2.generate(0, 2, 2, null)); + } + } diff --git a/src/main/java/inference/Constantness.java b/src/main/java/inference/Constantness.java deleted file mode 100644 index bb8d00d..0000000 --- a/src/main/java/inference/Constantness.java +++ /dev/null @@ -1,113 +0,0 @@ -package inference; - -import java.util.HashSet; -import java.util.List; -import java.util.Set; - -import exceptions.SubstituteFailedException; -import models.algebra.Variable; -import models.formulas.Formula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.RDLTerm; -import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.OrderConstraint; -import models.terms.meta.OrderVariableConstraint; -import utils.ExpressionUitls; -import utils.Permutation; - -public class Constantness extends InferenceRule{ - - public Constantness() { - //todo - super("composite mapping", List.of(), null, new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))); - } - - - @Override - public Set apply(List assumptions, Set existTerms) { - Set result = new HashSet<>(); - for (List perm : Permutation.permutation(assumptions, assumptions.size())) { - Set matchResult = assumptionMatch(perm); - for (MatchConstraint constraint: matchResult) { - int m = constraint.getOrderConstraint().get(new Variable("m")).getOrder(); - int n = m - perm.size(); - - - if (! constraint.getOrderConstraint().containsKey(new Variable("n"))) { - constraint.putOrderConstraint(new Variable("n"), new OrderVariableConstraint()); - } - constraint.setOrderConstraint(new Variable("n"), OrderConstraint.EQ, n); - - if (! this.defaultOrderConstraint.check(constraint.getOrderConstraint())) { - continue; - } - - MetaRDLTerm conclusionLsh = createMetaConclusionLsh(0, m-n); - MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); - MetaEquationFormula conclusion = new MetaEquationFormula(conclusionLsh, se); - - for (RDLTerm term : existTerms) { - if (! se.isMatchedBy(term).isEmpty()) { - constraint.setBinding(new Variable("se"), term); - try { - result.add(conclusion.substitution(constraint.getBinding())); - } catch(SubstituteFailedException e) { - continue; - } - } - } - } - } - return result; - } - - private Set assumptionMatch(List assumptions) { - Set result = new HashSet<>(); - result = generateAssumption(0, false).isMatchedBy(assumptions.get(0)); - for (int i = 1; i < assumptions.size(); i++) { - result = generateAssumption(i, i == assumptions.size() - 1).isMatchedBy(assumptions.get(i), result); - } - - return result; - } - - private MetaEquationFormula generateAssumption(int i, boolean isLast) { - if (isLast) { - MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm( - new MetaResource(new Variable("r" + i), ExpressionUitls.parse("n + 1")), - new MetaEvaluatableTermVariable(new Variable("x" + i)), - new MetaEvaluatableTermVariable(new Variable("y" + i)) - ); - MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i)); - return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh); - } else { - MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm( - new MetaResource(new Variable("r" + i), ExpressionUitls.parse("m - " + i)), - new MetaEvaluatableTermVariable(new Variable("x" + i)), - new MetaEvaluatableTermVariable(new Variable("y" + i)) - ); - MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i)); - return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh); - } - } - - private MetaRDLTerm createMetaConclusionLsh(int depth, int maxRecursion) { - int i = maxRecursion - depth - 1; - if (depth == maxRecursion - 1) { - return new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaResource(new Variable("r" + i), new Variable("m")), - new MetaEvaluatableTermVariable(new Variable("t" + i)) - ); - } - return new MetaRDLTerm( - createMetaConclusionLsh(depth + 1, maxRecursion), - new MetaResource(new Variable("r" + i),ExpressionUitls.parse("m - " + i)), - new MetaEvaluatableTermVariable(new Variable("t" + i)) - ); - } - -} diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 03eaacc..26eaad3 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,24 +12,14 @@ import java.util.Set; import java.util.stream.Collectors; -import models.algebra.Constant; 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.EvaluatableTerm; import models.terms.RDLTerm; -import models.terms.meta.MetaDynamicTerm; import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.MetaTermGenerator; -import models.terms.meta.MetaTermPairGenerator; -import models.terms.meta.MetaTermPairGenerator.TermPair; -import models.terms.meta.OrderConstraint; -import utils.ExpressionUitls; import utils.Product; public class ProofSystem { @@ -40,7 +30,7 @@ "Reflexivity", List.of(), new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te")) ) ); @@ -49,12 +39,12 @@ "Symmetry", List.of( new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("se")) ) ), new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")) ) ); @@ -63,373 +53,24 @@ "Transitivity", List.of( new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")) ), new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")) ) ), new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")) ) - ); - - public static final InferenceRule rightSubstitution = new InferenceRule( - "Right Substitution", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te0")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaDependencyFormula( - new MetaDynamicTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - (MetaTermGenerator) (index, depth, isLast) -> new MetaEvaluatableTermVariable(new Variable("re" + index)) - ) - ) - ), - (i) -> new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("re" + i)), - new MetaEvaluatableTermVariable(new Variable("x" + i)), - new MetaEvaluatableTermVariable(new Variable("y" + i)) - ), - new MetaEvaluatableTermVariable(new Variable("te" + i)) - ), - new MetaEquationFormula( - new MetaDynamicTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - (MetaTermPairGenerator) (index, depth, isLast) -> new TermPair( - new MetaEvaluatableTermVariable(new Variable("re" + index)), - new MetaEvaluatableTermVariable(new Variable("te" + index)) - ) - ), - new MetaDynamicTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - (MetaTermPairGenerator) (index, depth, isLast) -> new TermPair( - new MetaEvaluatableTermVariable(new Variable("re" + index)), - index == 0 ? new MetaEvaluatableTermVariable(new Variable("ue")) : new MetaEvaluatableTermVariable(new Variable("te" + index)) - ) - ) - ) - ); - - public static final InferenceRule leftSubstitution = new InferenceRule( - "Left Substitution", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaDependencyFormula( - new MetaDynamicTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - (MetaTermGenerator) (index, depth, isLast) -> new MetaEvaluatableTermVariable(new Variable("re" + index)) - ) - ) - ), - (i) -> new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("re" + i)), - new MetaEvaluatableTermVariable(new Variable("x" + i)), - new MetaEvaluatableTermVariable(new Variable("y" + i)) - ), - new MetaEvaluatableTermVariable(new Variable("ue" + i)) - ), - new MetaEquationFormula( - new MetaDynamicTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - (MetaTermPairGenerator) (index, depth, isLast) -> new TermPair( - new MetaEvaluatableTermVariable(new Variable("re" + index)), - new MetaEvaluatableTermVariable(new Variable("ue" + index)) - ) - ), - new MetaDynamicTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - (MetaTermPairGenerator) (index, depth, isLast) -> new TermPair( - new MetaEvaluatableTermVariable(new Variable("re" + index)), - new MetaEvaluatableTermVariable(new Variable("ue" + index)) - ) - ) - ) - ); - - public static final InferenceRule identity = new InferenceRule( - "Identity", - List.of( - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("x")), - new MetaEvaluatableTermVariable(new Variable("y")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ); - - public static final InferenceRule mapComposition = new InferenceRule( - "Map Composition", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("re")), - new MetaEvaluatableTermVariable(new Variable("pe")) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("pe")), - new MetaEvaluatableTermVariable(new Variable("x")), - new MetaEvaluatableTermVariable(new Variable("y")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re")), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("re")), - new MetaEvaluatableTermVariable(new Variable("pe")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("pe")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ); - - public static final InferenceRule constantness = new Constantness(); - - public static final InferenceRule rightNormalization = new InferenceRule( - "Right Normalization", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")) - ) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("qe"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - public static final InferenceRule pseudoConstantness = new InferenceRule( - "Pseudo-Constantness", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) - ), - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - public static final InferenceRule uncurrying = new InferenceRule( - "Uncurrying", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")) - ), - new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), - new MetaEvaluatableTermVariable(new Variable("x")), - new MetaEvaluatableTermVariable(new Variable("y")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")), - new MetaEvaluatableTermVariable(new Variable("x2")), - new MetaEvaluatableTermVariable(new Variable("y2")) - ), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")) - ), - new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("qe"), ExpressionUitls.parse("n-1")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) + ); // // //======================Dependency Axioms============================= // - public static final InferenceRule identityMapping = new InferenceRule( - "Identity Mapping", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")) - ) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")) - ) - ); - - public static final InferenceRule compositeMapping = new InferenceRule( - "Composite Mapping", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int i, int depth, boolean isLast) { - return new MetaEvaluatableTermVariable(new Variable("te" + i)); - }} - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te0")), - new MetaEvaluatableTermVariable(new Variable("ue0")) - ) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int i, int depth, boolean isLast) { - if (i == 0) { - return new MetaResource(new Variable("ue0")); - } - return new MetaResource(new Variable("te" + i)); - }} - ) - ); - - public static final InferenceRule constantMapping = new InferenceRule( - "Constant Mapping", - List.of(), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("m")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) - ); - - public static final InferenceRule slicedMapping = new InferenceRule( - "Sliced Mapping", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ), - new MetaResource(new Variable("p")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("p")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaResource(new Variable("p")) - ) - ); - - public static final InferenceRule uncurriedMapping = new InferenceRule( - "Uncurried Mapping", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re")) - ), - new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re")), - new MetaEvaluatableTermVariable(new Variable("te"), ExpressionUitls.parse("n-1")) - ), - new MetaEvaluatableTermVariable(new Variable("pe"), ExpressionUitls.parse("n-1")), - new MetaEvaluatableTermVariable(new Variable("te"), ExpressionUitls.parse("n-1")) - ) - ); private static final List axioms = List.of( diff --git a/src/main/java/models/terms/meta/MetaDependency.java b/src/main/java/models/terms/meta/MetaDependency.java index fba6677..7053d66 100644 --- a/src/main/java/models/terms/meta/MetaDependency.java +++ b/src/main/java/models/terms/meta/MetaDependency.java @@ -18,6 +18,13 @@ public class MetaDependency extends MetaRDLTerm{ + protected RDLTerm dependingTerm; + protected List dependedTerms; + + protected MetaDependency() { + super(new Symbol(":", -1), TermType.META_DEPENDENCY, -1); + } + public MetaDependency(RDLTerm dependingTerm, List dependedTerms) { super(new Symbol(":", -1), TermType.META_DEPENDENCY, -1); int size = dependingTerm.getSize(); @@ -27,6 +34,8 @@ size += term.getSize(); } this.size = size; + this.dependingTerm = dependingTerm; + this.dependedTerms = dependedTerms; } public MetaDependency(RDLTerm dependingTerm, RDLTerm ...dependedTerms) { diff --git a/src/main/java/models/terms/meta/MetaDynamicDependency.java b/src/main/java/models/terms/meta/MetaDynamicDependency.java new file mode 100644 index 0000000..97b02d3 --- /dev/null +++ b/src/main/java/models/terms/meta/MetaDynamicDependency.java @@ -0,0 +1,72 @@ +package models.terms.meta; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import models.algebra.Variable; +import models.terms.RDLTerm; + +public class MetaDynamicDependency extends MetaDependency implements MetaDynamicTerm { + + private final MetaTermGenerator termGenerator; + + public MetaDynamicDependency(MetaTermGenerator termGenerator) { + this.termGenerator = termGenerator; + } + + public MetaDynamicDependency(MetaTermGenerator termGenerator, List terms) { + this.termGenerator = termGenerator; + this.dependingTerm = terms.size() > 0 ? terms.get(0) : null; + this.dependedTerms = terms.size() > 1 ? terms.stream().skip(1).toList() : List.of(); + } + + public MetaDynamicDependency(MetaTermGenerator termGenerator, RDLTerm ...terms) { + this(termGenerator, Arrays.asList(terms)); + } + + @Override + public MetaRDLTerm generate(int depth, Map context) { + // TODO 自動生成されたメソッド・スタブ + return null; + } + + @Override + public MetaDependency generate(int depth, int maxIndex, int maxDepth, Map context) { + if (maxIndex < 2) return null; + RDLTerm dependingTerm = this.dependingTerm == null ? termGenerator.generate(0, depth, maxIndex, maxDepth, context) : this.dependingTerm; + while (dependingTerm instanceof MetaDynamicTerm dynamicTerm) { + dependingTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + List dependedTerms = new ArrayList<>(); + int staticSize = this.dependedTerms == null ? 0 : this.dependedTerms.size(); + for (int i = 0; i < Math.min(maxIndex - 1, staticSize); i++) { + dependedTerms.add(this.dependedTerms.get(i)); + } + for (int i = staticSize; i < maxIndex - 1; i++) { + RDLTerm generatedTerm = termGenerator.generate(i + 1, depth, maxIndex, maxDepth, context); + while (generatedTerm instanceof MetaDynamicTerm dynamicTerm) { + generatedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + dependedTerms.add(generatedTerm); + } + return new MetaDependency(dependingTerm, dependedTerms); + } + + + @Override + protected Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { + // TODO 自動生成されたメソッド・スタブ + return null; + } + + @Override + protected RDLTerm substitute(Map binding, int depth) { + // TODO 自動生成されたメソッド・スタブ + return null; + } + + +} diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java index 505beb0..db8f017 100644 --- a/src/main/java/models/terms/meta/MetaDynamicTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java @@ -1,319 +1,12 @@ package models.terms.meta; -import com.google.common.collect.TreeMultiset; - -import java.util.ArrayList; -import java.util.HashSet; -import java.util.List; import java.util.Map; -import java.util.Set; -import models.algebra.Symbol; import models.algebra.Variable; -import models.terms.Dependency; -import models.terms.DependencyTerm; -import models.terms.EvaluatableTerm; -import models.terms.RDLTerm; -import models.terms.Resource; -import models.terms.ResourceConstant; -import models.terms.meta.MetaTermPairGenerator.TermPair; -import utils.Permutation; -public class MetaDynamicTerm extends MetaRDLTerm { - - private MetaTermGenerator dependingTermGenerator; - private MetaTermGenerator dependedTermGenerator; - private MetaTermPairGenerator termPairGenerator; - private boolean isStaticSize = false; - - public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaTermGenerator dependedTermGenerator) { - super(new Symbol("", -1), TermType.META_DEPENDENCY, -1); - this.dependingTermGenerator = dependingTermGenerator; - this.dependedTermGenerator = dependedTermGenerator; - } - - public MetaDynamicTerm(MetaRDLTerm dependingTerm, MetaTermGenerator dependedTermGenerator) { - this((index, depth, isLast) -> dependingTerm, dependedTermGenerator); - } - - public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaRDLTerm dependedTerm) { - this(dependingTermGenerator, (MetaTermGenerator) (index, depht, isLast) -> dependedTerm); - isStaticSize = true; - } - - public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaTermPairGenerator termPairGenerator) { - super(new Symbol("", -1), TermType.META_DEPENDENCY_TERM, -1); - this.dependingTermGenerator = dependingTermGenerator; - this.termPairGenerator = termPairGenerator; - } - - public MetaDynamicTerm(MetaRDLTerm dependingTerm, MetaTermPairGenerator termPairGenerator) { - this((index, depth, isLast) -> dependingTerm, termPairGenerator); - } - - public MetaDynamicTerm(MetaTermGenerator dependingTermGenerator, MetaRDLTerm dependedTerm, MetaRDLTerm argTerm) { - this(dependingTermGenerator, (MetaTermPairGenerator)(index, depht, isLast) -> new TermPair(dependedTerm, argTerm)); - isStaticSize = true; - } - - @Override - public RDLTerm substitute(Map binding, int depth) { - switch (this.termType) { - case META_DEPENDENCY: - return dependencyGenerate(binding).substitute(binding); - case META_DEPENDENCY_TERM: - return dependencyTermGenerate(binding).substitute(binding); - default: - break; - } - return null; - } - - @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { - Set result = new HashSet<>(); - if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { - return result; - } - switch (this.termType) { - case META_DEPENDENCY: - return dependencyMatch((Dependency) another, constraint, depth); - case META_DEPENDENCY_TERM: - return dependencyTermMatch((DependencyTerm) another, constraint, depth); - default: - break; - } - return result; - } - - private Set dependencyMatch(Dependency another, MatchConstraint constraint, int depth) { - Set result = new HashSet<>(); - Set tmpRes = new HashSet<>(); - RDLTerm anotherDependingTerm = another.getDependingTerm(); - TreeMultiset anotherDependedTerms = another.getDependedTerms(); - boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant; - MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast); - tmpRes = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); - if (tmpRes.isEmpty()) { - return result; - } - for (List perm: Permutation.permutation(anotherDependedTerms.size())) { - Set localResult = new HashSet<>(tmpRes); - boolean flg = true; - for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { - int anotherTermIndex = perm.get(metaTermIndex); - EvaluatableTerm anotherDependedTerm = anotherDependedTerms.stream().skip(anotherTermIndex).findFirst().orElse(null); - isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; - MetaRDLTerm metaDependedTerm = dependedTermGenerator.generate(metaTermIndex, depth, isLast); - localResult = metaDependedTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1); - if (localResult.isEmpty()) { - flg = false; - break; - } - } - if (flg) { - result.addAll(localResult); - } - } - return result; - } - - private Set dependencyTermMatch(DependencyTerm another, MatchConstraint constraint, int depth) { - Set result = new HashSet<>(); - Set tmpRes = new HashSet<>(); - RDLTerm anotherDependingTerm = another.getDependingTerm(); - List anotherDependedTerms = another.getDependedTerms(); - List anotherArgumentTerms = another.getArgumentTerms(); - boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant; - MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast); - tmpRes = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); - if (tmpRes.isEmpty()) { - return tmpRes; - } - for (List perm: Permutation.permutation(anotherDependedTerms.size())) { - Set localResult = new HashSet<>(tmpRes); - boolean flg = true; - for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { - int anotherTermIndex = perm.get(metaTermIndex); - EvaluatableTerm anotherDependedTerm = anotherDependedTerms.get(anotherTermIndex); - EvaluatableTerm anotherArgTerm = anotherArgumentTerms.get(anotherTermIndex); - TermPair metaTermPair = termPairGenerator.generate(metaTermIndex, depth, isLast); - isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; - localResult = metaTermPair.dependedTerm().isMatchedBy(anotherDependedTerm, localResult, depth + 1); - if (localResult.isEmpty()) { - flg = false; - break; - } - - isLast = anotherArgTerm instanceof Resource || anotherArgTerm instanceof ResourceConstant; - localResult = metaTermPair.argTerm().isMatchedBy(anotherArgTerm, localResult, depth + 1); - if (localResult.isEmpty()) { - flg = false; - break; - } - } - if (flg) { - result.addAll(localResult); - } - } - return result; - } - - private MetaRDLTerm dependencyRecursionGenerate(int maxRecursion, int depth) { - MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1); - MetaRDLTerm dependedTerm = dependedTermGenerator.generate(0, depth, depth == maxRecursion - 1); - if (depth == maxRecursion - 1) { - return new MetaDependency(dependingTerm, dependedTerm); - } - if (dependingTerm instanceof MetaDynamicTerm generator) { - return new MetaDependency(generator.dependencyRecursionGenerate(maxRecursion, depth + 1), dependedTerm); - } else if (dependedTerm instanceof MetaDynamicTerm generator) { - return new MetaDependency(dependedTerm, generator.dependencyRecursionGenerate(maxRecursion, depth + 1)); - } - return null; - } - - private MetaRDLTerm dependencyRecursionGenerate(Map binding, int maxRecursion, int depth) { - MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1); - List dependedTerms = new ArrayList<>(); - MetaRDLTerm dependedTerm = dependedTermGenerator.generate(0, depth, depth == maxRecursion - 1); - dependedTerms.add(dependedTerm); - for (int i = 0; i < searchMaxTermIndex(binding, depth, depth == maxRecursion - 1); i++) { - dependedTerms.add(dependedTermGenerator.generate(i + 1, depth, depth == maxRecursion - 1)); - } - if (depth == maxRecursion - 1) { - return new MetaDependency(dependingTerm, dependedTerms); - } - if (dependingTerm instanceof MetaDynamicTerm generator) { - return new MetaDependency(generator.dependencyRecursionGenerate(binding, maxRecursion, depth + 1), dependedTerms); - } else if (dependedTerm instanceof MetaDynamicTerm generator) { - return new MetaDependency(dependedTerm, generator.dependencyRecursionGenerate(binding, maxRecursion, depth + 1)); - } - return null; - } - - private MetaRDLTerm dependencyTermRecursionGenerate(int maxRecursion, int depth) { - MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1); - TermPair termPair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1); - MetaRDLTerm dependedTerm = termPair.dependedTerm(); - MetaRDLTerm argTerm = termPair.argTerm(); - if (depth == maxRecursion - 1) { - return new MetaDependencyTerm(dependingTerm, dependedTerm, argTerm); - } - if (dependingTerm instanceof MetaDynamicTerm generator) { - return new MetaDependencyTerm(generator.dependencyTermRecursionGenerate(maxRecursion, depth + 1), dependedTerm, argTerm); - } else if (dependedTerm instanceof MetaDynamicTerm generator) { - return new MetaDependencyTerm(dependedTerm, generator.dependencyTermRecursionGenerate(maxRecursion, depth + 1), argTerm); - } else if (argTerm instanceof MetaDynamicTerm generator) { - return new MetaDependencyTerm(dependedTerm, dependedTerm, generator.dependencyTermRecursionGenerate(maxRecursion, depth + 1)); - } - return null; - } - - private MetaRDLTerm dependencyTermRecursionGenerate(Map binding, int maxRecursion, int depth) { - MetaRDLTerm dependingTerm = dependingTermGenerator.generate(0, depth, depth == maxRecursion - 1); - List termPairs = new ArrayList<>(); - TermPair termPair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1); - termPairs.add(termPair.dependedTerm()); - termPairs.add(termPair.argTerm()); - for (int i = 1; i <= searchMaxTermPairIndex(binding, depth, depth == maxRecursion - 1); i++) { - TermPair pair = termPairGenerator.generate(i, depth, depth == maxRecursion - 1); - termPairs.add(pair.dependedTerm()); - termPairs.add(pair.argTerm()); - } - if (depth == maxRecursion - 1) { - return new MetaDependencyTerm(dependingTerm, termPairs); - } - List resTerms = new ArrayList<>(); - for (MetaRDLTerm term : termPairs) { - if (term instanceof MetaDynamicTerm generator) { - resTerms.add(generator.dependencyTermRecursionGenerate(binding, maxRecursion, depth+1)); - } else { - resTerms.add(term); - } - } - if (dependingTerm instanceof MetaDynamicTerm generator) { - return new MetaDependencyTerm(generator.dependencyTermRecursionGenerate(binding, maxRecursion, depth + 1), resTerms); - } - return new MetaDependencyTerm(dependingTerm, resTerms); - } - - private int searchMaxTermIndex(Map binding, int depth, boolean isLast) { - if (isStaticSize) return 0; - int ok = -1; - int ng = 100; - while (Math.abs(ok - ng) > 1) { - int mid = (ok + ng) / 2; - MetaRDLTerm generatedTerm = dependedTermGenerator.generate(mid, depth, isLast); - Set variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList()); - variables.removeAll(binding.keySet()); - if (variables.isEmpty()) { - ok = mid; - } else { - ng = mid; - } - } - return ok; - } - - private int searchMaxTermPairIndex(Map binding, int depth, boolean isLast) { - if (isStaticSize) return 0; - int ok = -1; - int ng = 100; - while (Math.abs(ok - ng) > 1) { - int mid = (ok + ng) / 2; - TermPair generatedTerm = termPairGenerator.generate(mid, depth, isLast); - Set variables = new HashSet<>(generatedTerm.dependedTerm().getAllVariables().stream().map(v -> v.getVariableName()).toList()); - variables.removeAll(binding.keySet()); - if (variables.isEmpty()) { - ok = mid; - } else { - ng = mid; - } - } - return ok; - } - - public MetaRDLTerm dependencyGenerate(Map binding) { - int ok = 0; - int ng = 100; - while (Math.abs(ok - ng) > 1) { - int mid = (ok + ng) / 2; - MetaRDLTerm generatedTerm = dependencyRecursionGenerate(mid, 0); - if (generatedTerm == null) { - ng = mid; - continue; - } - Set variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList()); - variables.removeAll(binding.keySet()); - if (variables.isEmpty()) { - ok = mid; - } else { - ng = mid; - } - } - return dependencyRecursionGenerate(binding, ok, 0); - } - - public MetaRDLTerm dependencyTermGenerate(Map binding) { - int ok = 0; - int ng = 100; - while (Math.abs(ok - ng) > 1) { - int mid = (ok + ng) / 2; - MetaRDLTerm generatedTerm = dependencyTermRecursionGenerate(mid, 0); - if (generatedTerm == null) { - ng = mid; - continue; - } - Set variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList()); - variables.removeAll(binding.keySet()); - if (variables.isEmpty()) { - ok = mid; - } else { - ng = mid; - } - } - return dependencyTermRecursionGenerate(binding, ok, 0); - } +public interface MetaDynamicTerm { + + public MetaRDLTerm generate(int depth, Map context); + public MetaRDLTerm generate(int depth, int maxIndex, int maxDepth, Map context); } diff --git a/src/main/java/models/terms/meta/MetaTermGenerator.java b/src/main/java/models/terms/meta/MetaTermGenerator.java index 36d7db5..44a5c36 100644 --- a/src/main/java/models/terms/meta/MetaTermGenerator.java +++ b/src/main/java/models/terms/meta/MetaTermGenerator.java @@ -1,8 +1,12 @@ package models.terms.meta; +import java.util.Map; + +import models.algebra.Variable; + @FunctionalInterface public interface MetaTermGenerator { - MetaRDLTerm generate(int index, int depth, boolean isLast); + MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context); } diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index e693aa8..49890af 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -1,17 +1,4 @@ package inferencerule; -import static org.junit.jupiter.api.Assertions.*; - -import org.junit.jupiter.api.Test; - -import java.util.List; -import java.util.Set; - -import inference.ProofSystem; -import models.formulas.DependencyFormula; -import models.formulas.EquationFormula; -import models.formulas.Formula; -import models.terms.Dependency; -import models.terms.DependencyTerm; import models.terms.Resource; import utils.Utils; @@ -26,59 +13,4 @@ Resource g = new Resource("g", Utils.INT, 2); Resource h = new Resource("h", Utils.INT, 2); - @Test - void IdentityMappingTest() { - EquationFormula ef1 = new EquationFormula(a, b); - DependencyFormula df1 = new DependencyFormula(a, b); - boolean tmp = ProofSystem.identityMapping.check(List.of(ef1), df1); - assertTrue(tmp); - Formula conclusion = ProofSystem.identityMapping.apply(List.of(ef1)); - assertEquals(df1, conclusion); - - DependencyTerm t1 = new DependencyTerm(a, b, c); - EquationFormula ef2 = new EquationFormula(t1, d); - DependencyFormula df2 = new DependencyFormula(t1, d); - assertTrue(ProofSystem.identityMapping.check(List.of(ef2), df2)); - assertEquals(df2, ProofSystem.identityMapping.apply(ef2)); - } - - @Test - void CompositeMappingTest() { - DependencyFormula df1 = new DependencyFormula(a, b, c); - DependencyFormula df2 = new DependencyFormula(c, d); - DependencyFormula df3 = new DependencyFormula(a, d, b); - assertTrue(ProofSystem.compositeMapping.check(List.of(df1, df2), df3)); - assertEquals(df3, ProofSystem.compositeMapping.apply(List.of(df1, df2))); - - DependencyFormula df4 = new DependencyFormula(a, b); - DependencyFormula df5 = new DependencyFormula(b, c); - DependencyFormula df6 = new DependencyFormula(a, c); - assertTrue(ProofSystem.compositeMapping.check(List.of(df4, df5), df6)); - assertEquals(df6, ProofSystem.compositeMapping.apply(List.of(df4, df5))); - } - - @Test - void ConstantMapping() { - Resource aa = new Resource("aa", Utils.INT, 1); - Resource bb = new Resource("bb", Utils.INT, 2); - Resource cc = new Resource("cc", Utils.INT, 1); - DependencyFormula d1 = new DependencyFormula(aa, bb); - DependencyFormula d3 = new DependencyFormula(aa, cc); - Set result = ProofSystem.constantMapping.apply(List.of(), Set.of(aa, bb, cc)); - assertTrue(result.contains(d1)); - assertFalse(result.contains(d3)); - } - - @Test - void UncurriedMappingTest() { - Dependency d1 = new Dependency(f, g); - Dependency d2 = new Dependency(d1, a); - DependencyTerm t1 = new DependencyTerm(f, g, b); - Dependency d3 = new Dependency(t1, a, b); - DependencyFormula df1 = new DependencyFormula(d2); - DependencyFormula df2 = new DependencyFormula(d3); - Set results = ProofSystem.uncurriedMapping.apply(List.of(df1), Set.of(b)); - assertTrue(results.contains(df2)); - } - } diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index d92d06e..fe75f26 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,18 +1,4 @@ package inferencerule; -import static org.junit.jupiter.api.Assertions.*; - -import org.junit.jupiter.api.Test; - -import java.util.List; -import java.util.Set; - -import inference.ProofSystem; -import models.formulas.DependencyFormula; -import models.formulas.EquationFormula; -import models.formulas.Formula; -import models.terms.Dependency; -import models.terms.DependencyTerm; -import models.terms.RDLTerm; import models.terms.Resource; import utils.Utils; @@ -31,191 +17,4 @@ Resource k = new Resource("k", Utils.INT, 2); Resource l = new Resource("l", Utils.INT, 1); - @Test - void ReflexivityTest() { - EquationFormula f = new EquationFormula(a, a); - Set results = ProofSystem.reflexivity.apply(List.of(), Set.of(a)); - assertTrue(results.contains(f)); - } - - @Test - void SymmetryTest() { - EquationFormula f1 = new EquationFormula(a, b); - EquationFormula f2 = new EquationFormula(b, a); - assertFalse(f1.equals(f2)); - - Formula result = ProofSystem.symmetry.apply(List.of(f1)); - assertTrue(f2.equals(result)); - } - - @Test - void TransitivitiyTest() { - EquationFormula ab = new EquationFormula(a, b); - EquationFormula bc = new EquationFormula(b, c); - EquationFormula ac = new EquationFormula(a, c); - - Formula result = ProofSystem.transitivity.apply(List.of(ab, bc)); - assertEquals(ac, result); - } - - @Test - void RightSubstitutionTest() { - EquationFormula f1 = new EquationFormula(a, b); - DependencyFormula d1 = new DependencyFormula(c, d); - DependencyTerm t1 = new DependencyTerm(d, f, g); - EquationFormula f2 = new EquationFormula(t1, a); - DependencyTerm t2 = new DependencyTerm(c, d, a); - DependencyTerm t3 = new DependencyTerm(c, d, b); - EquationFormula f3 = new EquationFormula(t2, t3); - Formula result = ProofSystem.rightSubstitution.apply(List.of(f1, d1, f2)); - assertEquals(result, f3); - - Resource te0 = new Resource("te0", Utils.INT, 1); - Resource te1 = new Resource("te1", Utils.INT, 1); - Resource te2 = new Resource("te2", Utils.INT, 1); - Resource ue = new Resource("ue", Utils.INT, 1); - Resource se = new Resource("se", Utils.INT, 1); - Resource re0 = new Resource("re0", Utils.INT, 1); - Resource re1 = new Resource("r1", Utils.INT, 1); - Resource re2 = new Resource("r2", Utils.INT, 1); - EquationFormula eq1 = new EquationFormula(te0, ue); - DependencyFormula df1 = new DependencyFormula(se, re0, re1, re2); - EquationFormula eq2 = new EquationFormula(new DependencyTerm(re0, a, b), te0); - EquationFormula eq21 = new EquationFormula(new DependencyTerm(re1, c, d), te1); - EquationFormula eq22 = new EquationFormula(new DependencyTerm(re2, e, f), te2); - DependencyTerm dt1 = new DependencyTerm(se, re0, te0, re1, te1, re2, te2); - DependencyTerm dt2 = new DependencyTerm(se, re0, ue, re1, te1, re2, te2); - EquationFormula eq3 = new EquationFormula(dt1, dt2); - RDLTerm result2 = ProofSystem.rightSubstitution.generateRightSideHand(List.of(eq1, df1, eq2, eq21, eq22), eq3.getLeftSideHand()); - assertEquals(result2, eq3.getRightSideHand()); - - } - - @Test - void LeftSubstituitionTest() { - EquationFormula f1 = new EquationFormula(a, b); - DependencyFormula d1 = new DependencyFormula(a, c); - DependencyTerm t1 = new DependencyTerm(c, f, g); - EquationFormula f2 = new EquationFormula(t1, d); - DependencyTerm t2 = new DependencyTerm(a, c, d); - DependencyTerm t3 = new DependencyTerm(b, c, d); - EquationFormula f3 = new EquationFormula(t2, t3); - Formula result = ProofSystem.leftSubstitution.apply(List.of(f1, d1, f2)); - assertEquals(result, f3); - } - - @Test - void IdentityTest() { - DependencyTerm t1 = new DependencyTerm(a, f, g); - DependencyTerm t2 = new DependencyTerm(a, a, b); - EquationFormula f1 = new EquationFormula(t1, b); - EquationFormula f2 = new EquationFormula(t2, b); - - Formula result = ProofSystem.identity.apply(List.of(f1)); - assertEquals(f2, result); - } - - @Test - void MapCompositionTest() { - DependencyFormula d1 = new DependencyFormula(a, b); - DependencyFormula d2 = new DependencyFormula(b, c); - DependencyTerm t1 = new DependencyTerm(c, f, g); - EquationFormula f1 = new EquationFormula(t1, d); - - DependencyTerm t2 = new DependencyTerm(b, c, d); - DependencyTerm t3 = new DependencyTerm(a, b, t2); - DependencyTerm t4 = new DependencyTerm(a, c, d); - EquationFormula f2 = new EquationFormula(t3, t4); - - Formula result = ProofSystem.mapComposition.apply(List.of(d1, d2, f1)); - assertEquals(f2, result); - } - - @Test - void ConstantnessTest() { - Resource a = new Resource("a", Utils.INT, 3); - Resource b = new Resource("b", Utils.INT, 3); - Resource c = new Resource("c", Utils.INT, 2); - Resource d = new Resource("d", Utils.INT, 2); - Resource e = new Resource("e", Utils.INT, 2); - Resource f = new Resource("f", Utils.INT, 2); - Resource g = new Resource("g", Utils.INT, 1); - Resource h = new Resource("h", Utils.INT, 1); - - DependencyTerm t1 = new DependencyTerm(a, b, c); - DependencyTerm t2 = new DependencyTerm(e, f, g); - EquationFormula eq1 = new EquationFormula(t1, d); - EquationFormula eq2 = new EquationFormula(t2, h); - - Resource x = new Resource("x", Utils.INT, 2); - DependencyTerm t3 = new DependencyTerm(x, a, d); - DependencyTerm t4 = new DependencyTerm(t3, e, h); - EquationFormula eq3 = new EquationFormula(t4, x); - - - Set f1 = ProofSystem.constantness.apply(List.of(eq1, eq2), Set.of(x)); - assertTrue(f1.contains(eq3)); - - Resource aa = new Resource("a", Utils.INT, 1); - Resource bb = new Resource("b", Utils.INT, 1); - Resource cc = new Resource("c", Utils.INT, 0); - Resource dd = new Resource("d", Utils.INT, 0); - Resource yy = new Resource("x", Utils.INT, 0); - DependencyTerm t5 = new DependencyTerm(aa, bb, cc); - EquationFormula eq4 = new EquationFormula(t5, dd); - DependencyTerm t6 = new DependencyTerm(yy, aa, dd); - EquationFormula eq5 = new EquationFormula(t6, yy); - Set f2 = ProofSystem.constantness.apply(List.of(eq4), Set.of(yy)); - assertTrue(f2.contains(eq5)); - } - - @Test - void RightNormalizationTest() { - Dependency d1 = new Dependency(a, b); - Dependency d2 = new Dependency(c, d); - DependencyTerm t1 = new DependencyTerm(a, b, c); - DependencyTerm t2 = new DependencyTerm(t1, d, e); - DependencyTerm t3 = new DependencyTerm(c, d, e); - DependencyTerm t4 = new DependencyTerm(a, b, t3); - - DependencyFormula df1 = new DependencyFormula(d1); - DependencyFormula df2 = new DependencyFormula(d2); - EquationFormula eq1 = new EquationFormula(t2, t4); - Set result = ProofSystem.rightNormalization.apply(List.of(df1, df2), Set.of(e)); - assertTrue(result.contains(eq1)); - - } - - @Test - void PseudoConstantnessTest() { - Dependency d1 = new Dependency(a, b); - DependencyTerm t1 = new DependencyTerm(a, b, b); - DependencyFormula df1 = new DependencyFormula(d1); - EquationFormula eq1 = new EquationFormula(t1, a); - Formula result = ProofSystem.pseudoConstantness.apply(List.of(df1)); - assertEquals(eq1, result); - } - - @Test - void UncurryingTest() { - Dependency d1 = new Dependency(h, i); - Dependency d2 = new Dependency(d1, a); - DependencyTerm t1 = new DependencyTerm(a, b, c); - DependencyTerm t2 = new DependencyTerm(d, e, f); - DependencyFormula df1 = new DependencyFormula(d2); - EquationFormula eq1 = new EquationFormula(t1, f); - EquationFormula eq2 = new EquationFormula(t2, l); - - DependencyTerm t3 = new DependencyTerm(h, i, l); - DependencyTerm t4 = new DependencyTerm(t3, a, f); - DependencyTerm t5 = new DependencyTerm(h, i, d); - DependencyTerm t6 = new DependencyTerm(t5, a, f, d, l); - EquationFormula eq3 = new EquationFormula(t4, t6); - - - Formula result = ProofSystem.uncurrying.apply(List.of(df1, eq1, eq2)); - assertEquals(result, eq3); - - } - } diff --git a/src/test/java/inferencerule/InferenceRuleTest.java b/src/test/java/inferencerule/InferenceRuleTest.java index c6ea6b0..57deb71 100644 --- a/src/test/java/inferencerule/InferenceRuleTest.java +++ b/src/test/java/inferencerule/InferenceRuleTest.java @@ -1,78 +1,5 @@ package inferencerule; -import static org.junit.jupiter.api.Assertions.*; -import static utils.Utils.*; - -import org.junit.jupiter.api.Test; - -import java.util.List; - -import inference.InferenceRule; -import models.algebra.Variable; -import models.formulas.DependencyFormula; -import models.formulas.EquationFormula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.Dependency; -import models.terms.DependencyTerm; -import models.terms.Resource; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; public class InferenceRuleTest { - @Test - void InferenceRuleTerst1() { - MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); - MetaResource v = new MetaResource(new Variable("v")); - MetaResource w = new MetaResource(new Variable("w")); - MetaRDLTerm metaD1 = new MetaRDLTerm(te, v); - MetaRDLTerm metaD2 = new MetaRDLTerm(v, w); - MetaRDLTerm metaD3 = new MetaRDLTerm(te, w); - MetaDependencyFormula metaDf1 = new MetaDependencyFormula(metaD1); - MetaDependencyFormula metaDf2 = new MetaDependencyFormula(metaD2); - MetaDependencyFormula metaDf3 = new MetaDependencyFormula(metaD3); - InferenceRule goseShazo = new InferenceRule(List.of(metaDf1, metaDf2), metaDf3); - - Resource a = new Resource("a", INT, 0); - Resource b = new Resource("b", INT, 0); - Resource c = new Resource("c", INT, 0); - Dependency d1 = new Dependency(a, b); - Dependency d2 = new Dependency(b, c); - Dependency d3 = new Dependency(a, c); - DependencyFormula df1 = new DependencyFormula(d1); // a : b - DependencyFormula df2 = new DependencyFormula(d2); // b : c - DependencyFormula df3 = new DependencyFormula(d3); // a : c - assertTrue(goseShazo.check(List.of(df1, df2), df3)); - - } - - @Test - void InferencuRuleTest2() { - MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); - MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue")); - MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se")); - MetaResource v = new MetaResource(new Variable("v")); - MetaEquationFormula assump1 = new MetaEquationFormula(te, ue); - MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue)); - /* - * te = ue - * ---------------------------------------- - * [se : v -> te] = [se : v -> ue] - */ - InferenceRule rightReplacement = new InferenceRule(List.of(assump1), concl1); - - Resource a = new Resource("a", INT, 0); - Resource c = new Resource("c", INT, 0); - Resource d = new Resource("d", INT, 0); - Resource x = new Resource("x", INT, 0); - Resource y = new Resource("y", INT, 0); - Resource z = new Resource("z", INT, 0); - DependencyTerm xyz = new DependencyTerm(x, y, z); - EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z] - EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]] - - assertTrue(rightReplacement.check(List.of(assump2), concl2)); - } - }