diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 369868b..8f6caf8 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -8,7 +8,9 @@ import inference.axioms.Identity; import inference.axioms.LeftSubstitution; import inference.axioms.MapComposition; +import inference.axioms.PseudoConstantness; import inference.axioms.RightSubstitution; +import inference.axioms.Uncurrying; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -78,33 +80,10 @@ // // 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(), -// 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 EquationAxiom pseudoConstantness = new PseudoConstantness(); -// public static final InferenceRule uncurrying = new Uncurrying(); -// -// public static final InferenceRule argumentDependencyExtraction = new ArgumentDependencyExtraction(); + public static final EquationAxiom uncurrying = new Uncurrying(); // diff --git a/src/main/java/inference/axioms/PseudoConstantness.java b/src/main/java/inference/axioms/PseudoConstantness.java new file mode 100644 index 0000000..fbbe179 --- /dev/null +++ b/src/main/java/inference/axioms/PseudoConstantness.java @@ -0,0 +1,64 @@ +package inference.axioms; + +import java.util.List; +import java.util.Map; +import java.util.Set; + +import inference.EquationAxiom; +import inference.InferenceOrderConstraint; +import models.algebra.Constant; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +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; +import models.terms.meta.OrderConstraint; + +public class PseudoConstantness extends EquationAxiom { + + public PseudoConstantness() { + super("Pseudo-Constantness"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + )); + defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ); + } + + @Override + public Set apply(List assumptions, EvaluatableTerm term, MatchConstraint constraint) { + constraint.getContext().put("maxIndex", ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() * 2 - 1); + constraint.getContext().put("maxDepth", 1); + return super.apply(assumptions, term, constraint); + } + +} diff --git a/src/main/java/inference/axioms/RightNormalization.java b/src/main/java/inference/axioms/RightNormalization.java new file mode 100644 index 0000000..b285fb4 --- /dev/null +++ b/src/main/java/inference/axioms/RightNormalization.java @@ -0,0 +1,11 @@ +package inference.axioms; + +import inference.EquationAxiom; + +public class RightNormalization extends EquationAxiom { + + public RightNormalization() { + super("Right Normalization"); + } + +} diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java new file mode 100644 index 0000000..7fb928a --- /dev/null +++ b/src/main/java/inference/axioms/Uncurrying.java @@ -0,0 +1,119 @@ +package inference.axioms; + +import java.util.List; +import java.util.Map; +import java.util.Set; + +import inference.EquationAxiom; +import models.algebra.Variable; +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; +import utils.ExpressionUtils; + +public class Uncurrying extends EquationAxiom { + + public Uncurrying() { + super("Uncurrying"); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + context.put("" + curDepth, maxIndex + 1); + context.put("i", Math.max(maxDepth - curDepth, (Integer) context.getOrDefault("i", 0))); + if (curDepth == maxDepth && curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curDepth == maxDepth && curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); + } + } + ) + )); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + maxIndex = (Integer) context.get(""+curDepth); + int i = (Integer) context.get("i"); + if (curDepth == maxDepth) { + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } else if (curIndex == 2) { + return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); + } + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex >= maxIndex * 2) { + if (i == maxDepth - curDepth && curIndex == maxIndex * 2) { + return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); + } else if (i == maxDepth - curDepth && curIndex == maxIndex * 2 + 1) { + return new MetaEvaluatableTermVariable(new Variable("we")); + } + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2)); + } + } + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + maxIndex = (Integer) context.get(""+curDepth); + if (curDepth == maxDepth) { + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } else if (curIndex == 2) { + return new MetaEvaluatableTermVariable(new Variable("we")); + } + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex >= maxIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2)); + } + } + ) + ); + } + + @Override + public Set apply(List assumptions, EvaluatableTerm term, MatchConstraint constraint) { + constraint.getContext().put("maxIndex", 10000); + constraint.getContext().put("maxDepth", term.getMaxDepth()); + return super.apply(assumptions, term, constraint); + } + + + +} diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index 513dad9..4e7c6c4 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,15 +1,14 @@ package models.terms; -import com.google.common.collect.TreeMultiset; - import java.util.ArrayList; import java.util.Arrays; import java.util.List; import java.util.stream.Collectors; +import com.google.common.collect.TreeMultiset; + import exceptions.SyntaxException; import lombok.Getter; -import models.algebra.Symbol; @Getter public class Dependency extends RDLTerm{ diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 1985275..dc070f5 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -10,6 +10,7 @@ import inference.ProofSystem; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; +import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; @@ -32,6 +33,8 @@ Resource m = new Resource("m", 2); Resource n = new Resource("n", 2); Resource o = new Resource("o", 3); + Resource p = new Resource("p", 3); + Resource q = new Resource("q", 3); @Test void ReflexivityTest() { @@ -108,14 +111,23 @@ @Test void PseudoConstantnessTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyTerm dt1 = new DependencyTerm(a, b, b, c, c); + Set terms = ProofSystem.pseudoConstantness.apply(List.of(d1), dt1); + assertTrue(terms.contains(a)); + terms = ProofSystem.pseudoConstantness.apply(List.of(d1), a); + assertTrue(terms.contains(dt1)); } @Test void UncurryingTest() { - } - - @Test - void ArgumentDependencyExtractionTest() { + DependencyFormula d1 = new DependencyFormula(new Dependency(new Dependency(o, p, q), n, m), a, b, c); + DependencyTerm dt1 = new DependencyTerm(new DependencyTerm(new DependencyTerm(o, p, d, q, e), n, f, m ,g), a, h, b, i, c, j); + DependencyTerm dt2 = new DependencyTerm(new DependencyTerm(new DependencyTerm(o, p, k, q, e), n, f, m ,g), a, h, b, i, c, j, k, d); + Set terms = ProofSystem.uncurrying.apply(List.of(d1), dt1); + assertTrue(terms.contains(dt2)); + terms = ProofSystem.uncurrying.apply(List.of(d1), dt2); + assertTrue(terms.contains(dt1)); } } diff --git a/src/test/java/terms/meta/MetaDynamicDependencyTest.java b/src/test/java/terms/meta/MetaDynamicDependencyTest.java index ed8ce54..5cc7994 100644 --- a/src/test/java/terms/meta/MetaDynamicDependencyTest.java +++ b/src/test/java/terms/meta/MetaDynamicDependencyTest.java @@ -15,6 +15,7 @@ import models.terms.meta.MetaDependency; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaRDLTermVariable; import models.terms.meta.MetaResource; @@ -113,4 +114,25 @@ assertFalse(md1.isMatchedBy(d3).isEmpty()); } + @Test + void DynamicMatchTest2() { + MetaDynamicDependency md1 = 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 MetaEvaluatableTermVariable(new Variable("se")); + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex)); + } + } + ); + Dependency d1 = new Dependency(new Dependency(a, b, c), d, e); + assertFalse(md1.isMatchedBy(d1).isEmpty()); + Dependency d2 = new Dependency(new Dependency(a, b, c, d), e); + assertFalse(md1.isMatchedBy(d2).isEmpty()); + } + }