diff --git a/src/Main.java b/src/Main.java index c82aa22..4156845 100644 --- a/src/Main.java +++ b/src/Main.java @@ -1,22 +1,18 @@ -import java.util.ArrayList; import java.util.List; -import inference.ProofSystem; +import inference.equivalence.SemanticEquivalenceProofSystem; +import inference.equivalence.SemanticEquivalenceRelation; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; -import models.formulas.DependencyFormula; import models.formulas.EquationFormula; -import models.formulas.Formula; -import models.terms.Dependency; import models.terms.DependencyTerm; -import models.terms.EvaluatableTerm; -import models.terms.ResourceConstant; import models.terms.ResourceVariable; import parser.Parser; import parser.Parser.TokenStream; +import tests.Utils; public class Main { @@ -28,92 +24,33 @@ public static void main(String[] args) { - List initialConditions = new ArrayList<>(); - ResourceVariable A = new ResourceVariable("A", INT, 2); - ResourceVariable B = new ResourceVariable("B", INT, 2); - ResourceVariable C = new ResourceVariable("C", INT, 2); - ResourceVariable D = new ResourceVariable("D", INT, 2); - ResourceVariable E = new ResourceVariable("E", INT, 1); - ResourceVariable F = new ResourceVariable("F", INT, 1); - ResourceVariable G = new ResourceVariable("G", INT, 0); - - ResourceVariable Ap = new ResourceVariable("A'", INT, 2); - ResourceVariable Bp = new ResourceVariable("B'", INT, 2); - ResourceVariable Cp = new ResourceVariable("C'", INT, 2); - ResourceVariable Dp = new ResourceVariable("D'", INT, 2); - ResourceVariable Fp = new ResourceVariable("F'", INT, 1); - - initialConditions.add(new DependencyFormula(new Dependency(new Dependency(A, B), D), F)); - initialConditions.add(new DependencyFormula(new Dependency(new Dependency(Ap, Bp), Dp), Fp)); - initialConditions.add(new EquationFormula(new DependencyTerm(A, B, C), new DependencyTerm(Ap, Bp, Cp))); - EquationFormula conclusion = new EquationFormula( - new DependencyTerm(new DependencyTerm(new DependencyTerm(A, B, C), D, E), F, G), - new DependencyTerm(new DependencyTerm(new DependencyTerm(Ap, Bp, Cp), D, E), F, G) + ResourceVariable A = new ResourceVariable("A", Utils.INT, 2); + ResourceVariable Ap = new ResourceVariable("A'", Utils.INT, 2); + ResourceVariable B = new ResourceVariable("B", Utils.INT, 2); + ResourceVariable Bp = new ResourceVariable("B'", Utils.INT, 2); + ResourceVariable C = new ResourceVariable("C", Utils.INT, 2); + ResourceVariable Cp = new ResourceVariable("C'", Utils.INT, 2); + ResourceVariable D = new ResourceVariable("D", Utils.INT, 2); + ResourceVariable E = new ResourceVariable("E", Utils.INT, 1); + ResourceVariable F = new ResourceVariable("F", Utils.INT, 1); + ResourceVariable G = new ResourceVariable("G", Utils.INT, 0); + DependencyTerm t1 = new DependencyTerm(A, B, C); + DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); + EquationFormula assumptionFormula = new EquationFormula(t1, t2); + EquationFormula conclusionFormula = new EquationFormula( + new DependencyTerm(new DependencyTerm(A, B, new DependencyTerm(C, D, E)),F, G), + new DependencyTerm(new DependencyTerm(Ap, Bp, new DependencyTerm(Cp, D, E)),F, G) ); - for(var cond : initialConditions) { - System.out.println(cond.toString()); - } - System.out.println(conclusion.toString()); - ProofSystem.check(initialConditions, conclusion); - System.out.println("======================="); - EvaluatableTerm lrn = conclusion.getLeftSideHand().linearRightNormalize(); - var subTerms = lrn.getSubTerms(EvaluatableTerm.class); - System.out.println(conclusion.getLeftSideHand().linearRightNormalize().toString()); - for(var sub: subTerms.keySet()) { - System.out.println(sub.getOrders().toString()); - System.out.println(subTerms.get(sub).toString()); - } - System.out.println("=================="); - System.out.println(conclusion.getRightSideHand().linearRightNormalize().toString()); - - sandbox1(); - sandbox2(); + SemanticEquivalenceProofSystem proofSystem = new SemanticEquivalenceProofSystem( + List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)), + conclusionFormula + ); + proofSystem.proof(); } - static void sandbox1() { - System.out.println("------------------------------------------------------------sandbox1"); - ResourceVariable a = new ResourceVariable("A", INT, 2); - ResourceVariable b = new ResourceVariable("B", INT, 2); - ResourceVariable c = new ResourceVariable("C", INT, 2); - ResourceVariable ap = new ResourceVariable("A'", INT, 2); - ResourceVariable bp = new ResourceVariable("B'", INT, 2); - ResourceVariable cp = new ResourceVariable("C'", INT, 2); - - DependencyTerm d1 = new DependencyTerm(a, b, c); - DependencyTerm d11 = new DependencyTerm(a, b, c); - DependencyTerm d2 = new DependencyTerm(ap, bp, cp); - EquationFormula conclu1 = new EquationFormula(d1, d11); - boolean tmp1 = ProofSystem.REFLEXIVE_LAW.check(List.of(), conclu1); - d11.setDependingTerm(ap); - boolean tmp2 = ProofSystem.LEFT_REPLACEMENT.check(List.of(new EquationFormula(a, ap)), conclu1); - d11.setDependingTerm(a); - d11.setDependedVariable(bp); - boolean tmp3 = ProofSystem.CENTER_REPLACEMENT.check(List.of(new EquationFormula(b, bp)), conclu1); - d11.setDependedVariable(b); - d11.setArgumentTerm(cp); - boolean tmp4 = ProofSystem.RIGHT_REPLACEMENT.check(List.of(new EquationFormula(c, cp)), conclu1); - d11.setArgumentTerm(c); - System.out.println(tmp2); - System.out.println(tmp3); - System.out.println(tmp4); - } - static void sandbox2() { - ResourceVariable A = new ResourceVariable("A", INT, 1); - ResourceVariable N = new ResourceVariable("N", INT, 1); - ResourceVariable X = new ResourceVariable("X", INT, 1); - ResourceVariable S = new ResourceVariable("S", INT, 1); - ResourceVariable S1 = new ResourceVariable("S1", INT, 1); - ResourceConstant zero = new ResourceConstant("0"); - DependencyTerm t1 = new DependencyTerm(S, S1, zero); - DependencyTerm t2 = new DependencyTerm(S, S1, X); - DependencyTerm t3 = new DependencyTerm(A, N, t2); - DependencyTerm t4 = new DependencyTerm(t3, X, t1); - System.out.println(t4); - System.out.println(t4.linearRightNormalize()); - - } + @SneakyThrows static Expression parse(String expr) { diff --git a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java index 05941ee..3e0c395 100644 --- a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java +++ b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java @@ -63,21 +63,31 @@ public Set substitute(Map binding, Map orderConstraint, Collection existedTerms) { Set result = new HashSet<>(); - Set allVariables = new HashSet<>(); + Map allVariables = new HashMap<>(); for(MetaVariable variable : leftSideHand.getAllVariables()) { - allVariables.add(variable.getVariableName()); + allVariables.put(variable.getVariableName(), variable); } for(MetaVariable variable : rightSideHand.getAllVariables()) { - allVariables.add(variable.getVariableName()); + allVariables.put(variable.getVariableName(), variable); } - allVariables.removeAll(binding.keySet()); - List leftVariables = new ArrayList<>(allVariables); + for (Variable variable : binding.keySet()) { + allVariables.remove(variable); + } + List leftVariables = new ArrayList<>(allVariables.keySet()); for(List useTerms: Permutation.permutation(existedTerms, leftVariables.size())) { Map tempBinding = new HashMap<>(); tempBinding.putAll(binding); + boolean flg = false; for (int i = 0; i < leftVariables.size(); i++) { + if (!allVariables.get(leftVariables.get(i)).isMatchedBy(useTerms.get(i))) { + flg = true; + break; + } tempBinding.put(leftVariables.get(i), useTerms.get(i)); } + if (flg) { + continue; + } RDLTerm leftTerm = leftSideHand.substitute(tempBinding); RDLTerm rightTerm = rightSideHand.substitute(tempBinding); Map tempOrderConstraint = new HashMap<>(); diff --git a/src/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/inference/equivalence/SemanticEquivalenceProofSystem.java index 7c1d04a..a865300 100644 --- a/src/inference/equivalence/SemanticEquivalenceProofSystem.java +++ b/src/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -12,6 +12,7 @@ import models.algebra.Term; import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; +import models.formulas.EquationFormula; import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.meta.MetaEvaluatableTermVariable; @@ -23,7 +24,7 @@ public class SemanticEquivalenceProofSystem { private Map> assumptions; - private SemanticEquivalenceRelation conclusion; + private EquationFormula conclusion; int maxOrder = -1; private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation( @@ -56,18 +57,22 @@ new Variable("n") ); - public SemanticEquivalenceProofSystem(Collection assumptions, SemanticEquivalenceRelation conclusion) { + public SemanticEquivalenceProofSystem(Collection assumptions, EquationFormula conclusion) { + this.assumptions = new HashMap<>(); for(SemanticEquivalenceRelation assumption : assumptions) { maxOrder = Math.max(maxOrder, assumption.getOrder()); if (! this.assumptions.containsKey(assumption.getOrder())) { this.assumptions.put(assumption.getOrder(), new ArrayList<>()); } + this.assumptions.get(assumption.getOrder()).add(assumption); } this.conclusion = conclusion; } public boolean proof() { Set existTerms = new HashSet<>(); + existTerms.addAll(conclusion.getLeftSideHand().getSubTerms(RDLTerm.class).values()); + existTerms.addAll(conclusion.getRightSideHand().getSubTerms(RDLTerm.class).values()); for(int key : assumptions.keySet()) { for(SemanticEquivalenceRelation relation : assumptions.get(key)) { existTerms.addAll(relation.getLeftSideHand().getSubTerms(RDLTerm.class).values()); @@ -77,11 +82,20 @@ } } for (int i = maxOrder; i > 0; i--) { + if (i == 1) { + System.out.println("aaa"); + } for (SemanticEquivalenceRelation relation : assumptions.get(i)) { applyRule4(relation, existTerms); } } - System.out.println(assumptions); + for(int order : assumptions.keySet()) { + System.out.println(order); + for(SemanticEquivalenceRelation relation : assumptions.get(order)) { + System.out.println(relation); + } + System.out.println("============================"); + } return false; } diff --git a/src/inference/equivalence/SemanticEquivalenceRelation.java b/src/inference/equivalence/SemanticEquivalenceRelation.java index f21698a..2a15bf9 100644 --- a/src/inference/equivalence/SemanticEquivalenceRelation.java +++ b/src/inference/equivalence/SemanticEquivalenceRelation.java @@ -1,6 +1,7 @@ package inference.equivalence; import lombok.Getter; +import models.formulas.EquationFormula; import models.terms.RDLTerm; @Getter @@ -15,6 +16,12 @@ rightSideHand = rsh; this.order = order; } + + public SemanticEquivalenceRelation(EquationFormula formula, int order) { + leftSideHand = formula.getLeftSideHand(); + rightSideHand = formula.getRightSideHand(); + this.order = order; + } @Override diff --git a/src/models/terms/DependencyTerm.java b/src/models/terms/DependencyTerm.java index 153c5d7..bef9d63 100644 --- a/src/models/terms/DependencyTerm.java +++ b/src/models/terms/DependencyTerm.java @@ -26,7 +26,7 @@ @Override public boolean isLinearRightNormalized() { - return isLinearRightNormal(0); + return isLinearRightNormaled(0); } @Override @@ -60,13 +60,13 @@ } - private boolean isLinearRightNormal(int depth) { + private boolean isLinearRightNormaled(int depth) { if(dependingTerm instanceof ResourceVariable || dependingTerm instanceof SetEvaluatableTerm) { return dependingTerm.getOrder() == dependedVariable.getOrder(); } DependencyTerm dependencyTerm = (DependencyTerm) dependingTerm; if( - dependencyTerm.isLinearRightNormal(depth + 1) && + dependencyTerm.isLinearRightNormaled(depth + 1) && dependencyTerm.getDependedVariable().getOrder() - 1 == dependedVariable.getOrder() && dependencyTerm.getOrder() == dependedVariable.getOrder() && argumentTerm.getOrder() <= dependencyTerm.getOrder() && @@ -75,7 +75,7 @@ return true; } if( - dependencyTerm.isLinearRightNormal(depth + 1) && + dependencyTerm.isLinearRightNormaled(depth + 1) && dependencyTerm.getDependedVariable().getOrder() - 1 == dependedVariable.getOrder() && dependencyTerm.getOrder() == dependedVariable.getOrder() && argumentTerm.getOrder() < dependencyTerm.getOrder()