diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 5f76eca..d653954 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -145,9 +145,9 @@ } protected List repetitionAssumptionGenerate(int i) { - if (i == 0) { - return new ArrayList<>(this.repetitionAssumptions); - } +// if (i == 0) { +// return new ArrayList<>(this.repetitionAssumptions); +// } List result = new ArrayList<>(); for (MetaFormula metaFormula : this.repetitionAssumptions) { Map mapping = new HashMap<>(); diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 566c628..61391fb 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,10 +12,16 @@ import java.util.Set; import java.util.stream.Collectors; +import inference.axioms.ArgumentDependencyExtraction; import inference.axioms.CompositeMapping; +import inference.axioms.Constantness; +import inference.axioms.MapComposition; import inference.axioms.RedundancyElimination; +import inference.axioms.RightNormalization; import inference.axioms.RightSubstitution; import inference.axioms.UncurriedMapping; +import inference.axioms.Uncurrying; +import models.algebra.Constant; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -26,6 +32,7 @@ import models.terms.RDLTerm; import models.terms.meta.MetaDependencyTerm; import models.terms.meta.MetaDependencyVariable; +import models.terms.meta.MetaDynamicDependency; import models.terms.meta.MetaDynamicDependencyTerm; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; @@ -110,15 +117,9 @@ @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 1; - if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("re")); - } if (curIndex % 2 == 0) { return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); } - if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("ue")); - } return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); } }, @@ -129,15 +130,9 @@ @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 1; - if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("re")); - } if (curIndex % 2 == 0) { return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); } - if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("ue")); - } return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); } }, @@ -155,7 +150,7 @@ "Identity", List.of(), List.of( - new MetaEquationFormula( + new MetaEquationFormula( new MetaDependencyTerm( new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("x")), @@ -170,22 +165,16 @@ @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 1; - if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("se")); - } if (curIndex % 2 == 0) { return new MetaEvaluatableTermVariable(new Variable("se" + curIndex / 2)); } - if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("te")); - } return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); } }, - new MetaEvaluatableTermVariable(new Variable("se")) + new MetaEvaluatableTermVariable(new Variable("se0")) ), - new MetaEvaluatableTermVariable(new Variable("te")) + new MetaEvaluatableTermVariable(new Variable("te0")) ), null, (assumptions) -> assumptions.size() * 2 + 1, @@ -193,18 +182,39 @@ (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 ); - public static final InferenceRule mapComposition = new EquationAxiom( - "Map Composition", + public static final InferenceRule mapComposition = new MapComposition(); + + public static final InferenceRule constantness = new Constantness(); + + public static final InferenceRule rightNormalization = new RightNormalization(); + + public static final InferenceRule pseudoConstantness = new InferenceRule( + "Pseudo-Constantness", + List.of( + new MetaDependencyFormula( + new MetaDynamicDependency( + (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1)), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + ) + ), List.of(), - List.of(), - null, - null, - null, - null, - null + new MetaEquationFormula( + new MetaDynamicDependencyTerm( + (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1) / 2), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new InferenceOrderConstraint(new Constant("0"), OrderConstraint.GT, new Variable("n")), + (assumptions) -> (((DependencyFormula)assumptions.get(0)).getDependency().getMaxIndex() - 1) * 2 + 1, + (assumptions) -> 1, + (term) -> (term.getMaxIndex() - 1) / 2 + 1 ); + public static final InferenceRule uncurrying = new Uncurrying(); + public static final InferenceRule argumentDependencyExtraction = new ArgumentDependencyExtraction(); // diff --git a/src/main/java/inference/axioms/ArgumentDependencyExtraction.java b/src/main/java/inference/axioms/ArgumentDependencyExtraction.java new file mode 100644 index 0000000..f160716 --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentDependencyExtraction.java @@ -0,0 +1,93 @@ +package inference.axioms; +import java.util.Map; + +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +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 ArgumentDependencyExtraction extends EquationAxiom { + + public ArgumentDependencyExtraction() { + super("Argument Dependency Extraction"); + 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("firstAssumptionIndex", curIndex + 2); + return new MetaEvaluatableTermVariable(new Variable("t" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ) + ); + 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("t" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ) + ); + assumptions.add( + 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("t" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("t")), + new MetaEvaluatableTermVariable(new Variable("x")) + ), + new MetaEvaluatableTermVariable(new Variable("c")) + ) + ); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); + curIndex -= 1; + if (curIndex >= firstAssumptionIndex) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("t" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("t")) + ), + new MetaEvaluatableTermVariable(new Variable("x")) + ); + conclusionMaxIndexCalculator = (assumptions) -> ((EquationFormula) assumptions.get(2)).getLeftSideHand().getMaxIndex() - 3 + 1; + } + +} diff --git a/src/main/java/inference/axioms/Constantness.java b/src/main/java/inference/axioms/Constantness.java new file mode 100644 index 0000000..7f5380f --- /dev/null +++ b/src/main/java/inference/axioms/Constantness.java @@ -0,0 +1,11 @@ +package inference.axioms; +import inference.EquationAxiom; + +public class Constantness extends EquationAxiom { + + public Constantness() { + super("Constantness"); + + } + +} diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java index 42186f9..78296f1 100644 --- a/src/main/java/inference/axioms/MapComposition.java +++ b/src/main/java/inference/axioms/MapComposition.java @@ -1,72 +1,10 @@ package inference.axioms; -import java.util.Map; - import inference.EquationAxiom; -import models.algebra.Variable; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.meta.MetaDependencyTerm; -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( - (ci, cd, mi, md, context) -> ci - 2 == 0 ? new MetaEvaluatableTermVariable(new Variable("u")) : new MetaEvaluatableTermVariable(new Variable("u" + (ci - 2))), - new MetaEvaluatableTermVariable(new Variable("s")), - new MetaEvaluatableTermVariable(new Variable("t")) - ) - ) - ); - assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency( - (ci, cd, mi, md, context) -> ci - 1 == 0 ? new MetaEvaluatableTermVariable(new Variable("v")) : new MetaEvaluatableTermVariable(new Variable("v" + (ci - 1))), - new MetaEvaluatableTermVariable(new Variable("t")) - ) - ) - ); - repetitionAssumptions.add( - new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("v")), - new MetaEvaluatableTermVariable(new Variable("xxx")), - new MetaEvaluatableTermVariable(new Variable("yyy")) - ), - new MetaEvaluatableTermVariable(new Variable("x")) - ) - ); - - conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - - return null; - }}, - new MetaEvaluatableTermVariable(new Variable("s")), - new MetaEvaluatableTermVariable(new Variable("t")) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - return null; - } - }, - new MetaEvaluatableTermVariable(new Variable("s")) - ) - ); - } } diff --git a/src/main/java/inference/axioms/RightNormalization.java b/src/main/java/inference/axioms/RightNormalization.java new file mode 100644 index 0000000..5d6f893 --- /dev/null +++ b/src/main/java/inference/axioms/RightNormalization.java @@ -0,0 +1,12 @@ +package inference.axioms; +import inference.EquationAxiom; + +public class RightNormalization extends EquationAxiom { + + public RightNormalization() { + super("RIght Normalization"); + + + } + +} diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java index f3219d0..2af7896 100644 --- a/src/main/java/inference/axioms/RightSubstitution.java +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -27,8 +27,8 @@ this.assumptions = new ArrayList<>(); this.repetitionAssumptions = new ArrayList<>(); assumptions.add(new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) + new MetaEvaluatableTermVariable(new Variable("te0")), + new MetaEvaluatableTermVariable(new Variable("ue0")) )); repetitionAssumptions.add(new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), @@ -48,38 +48,29 @@ @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 1; - if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("re")); - } - if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("te")); - } if (curIndex % 2 == 0) { return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); } return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); } }, - new MetaEvaluatableTermVariable(new Variable("se")) + new MetaEvaluatableTermVariable(new Variable("se0")) ), new MetaDynamicDependencyTerm( new MetaTermGenerator() { @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 1; - if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("re")); - } if (curIndex % 2 == 0) { return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); } if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("ue")); + return new MetaEvaluatableTermVariable(new Variable("ue0")); } return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); } }, - new MetaEvaluatableTermVariable(new Variable("se")) + new MetaEvaluatableTermVariable(new Variable("se0")) ) ); conclusionMaxIndexCalculator = (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1; diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java new file mode 100644 index 0000000..86d4780 --- /dev/null +++ b/src/main/java/inference/axioms/Uncurrying.java @@ -0,0 +1,9 @@ +package inference.axioms; +import inference.EquationAxiom; + +public class Uncurrying extends EquationAxiom { + public Uncurrying() { + super("Uncurrying"); + } + +} diff --git a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java index 8a55608..bf0f69e 100644 --- a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java @@ -1,5 +1,7 @@ package models.terms.meta; +import com.google.common.collect.TreeMultiset; + import java.util.ArrayList; import java.util.Arrays; import java.util.List; @@ -8,8 +10,6 @@ import java.util.stream.Collectors; import java.util.stream.IntStream; -import com.google.common.collect.TreeMultiset; - import exceptions.SubstituteFailedException; import exceptions.SyntaxException; import models.algebra.Variable; @@ -80,11 +80,11 @@ } } for (int i = 0; i < (maxIndex - index) / 2; i++) { - RDLTerm dependedTerm = generator.generate(i * 2 + 1, depth, maxIndex, maxDepth, context); + RDLTerm dependedTerm = generator.generate(i * 2 + index, depth, maxIndex, maxDepth, context); if (dependedTerm == null) { break; } - RDLTerm argTerm = generator.generate(i * 2 + 2, depth, maxIndex, maxDepth, context); + RDLTerm argTerm = generator.generate(i * 2 + index + 1, depth, maxIndex, maxDepth, context); if (argTerm == null) { break; } diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 198fb85..70c3a8a 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,11 +1,11 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; +import org.junit.jupiter.api.Test; + import java.util.List; import java.util.Set; -import org.junit.jupiter.api.Test; - import inference.ProofSystem; import inference.axioms.RightSubstitution; import models.formulas.DependencyFormula; @@ -13,6 +13,7 @@ import models.formulas.Formula; import models.terms.DependencyTerm; import models.terms.Resource; +import models.terms.ResourceConstant; public class EqualityAxiomTest { @@ -91,4 +92,22 @@ assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d, e, h), d))); } + @Test + void PseudoConstantnessTest() { + Set result = ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b)); + assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b), a))); + + result = ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b, c, d)); + assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b, c, c, d, d), a))); + } + + @Test + void ArgumentDependencyExtractionTest() { + Set result = ProofSystem.argumentDependencyExtraction.apply( + new DependencyFormula(a, b, c), + new DependencyFormula(b, c), + new EquationFormula(new DependencyTerm(a, b, d, c, e), new ResourceConstant("ccc"))); + assertTrue(result.contains(new EquationFormula(new DependencyTerm(b, c, e), d))); + } + }