diff --git a/src/Main.java b/src/Main.java index 72f2f12..5e92af1 100644 --- a/src/Main.java +++ b/src/Main.java @@ -29,9 +29,10 @@ static Type INT = DataConstraintModel.typeInt; public static void main(String[] args) { - +// sandbox1(); // sandbox2(); - sandbox3(); +// sandbox3(); + ProofSystem.debug(); } static void sandbox1() { @@ -57,7 +58,10 @@ List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)), conclusionFormula ); - + SemanticEquivalenceProofSystem.debug(); + System.out.println(); + System.out.println(assumptionFormula); + System.out.println(conclusionFormula); // System.out.println(conclusionFormula.linearRightNormalized()); System.out.println(proofSystem.proof()); } @@ -92,6 +96,7 @@ System.out.println(conclusion); System.out.println(); boolean result = ProofSystem.check(List.of(f1, f2, f3, f4, f5), conclusion); + System.out.println(); System.out.println(result); } diff --git a/src/inference/InferenceOrderConstraint.java b/src/inference/InferenceOrderConstraint.java index 6c789e9..e74b9dc 100644 --- a/src/inference/InferenceOrderConstraint.java +++ b/src/inference/InferenceOrderConstraint.java @@ -80,4 +80,26 @@ } } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + if (this.leftSideHandVariable != null) { + sb.append(this.leftSideHandVariable.toString()); + } else { + sb.append(this.leftSideHandConstant); + } + sb.append(" "); + sb.append(operator.getOperator()); + sb.append(" "); + if (this.rightSideHandVariable != null) { + sb.append(this.rightSideHandVariable.toString()); + } else { + sb.append(this.rightSideHandConstant); + } + + return sb.toString(); + + } + } diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java index 3a369f6..fb29d37 100644 --- a/src/inference/InferenceRule.java +++ b/src/inference/InferenceRule.java @@ -158,6 +158,10 @@ public String toString() { StringBuilder sb = new StringBuilder(); + if (defaultOrderConstraint != null) { + sb.append(defaultOrderConstraint); + sb.append(", "); + } for (int i = 0; i < assumptions.size(); i++) { sb.append(assumptions.get(i).toString()); if (i != assumptions.size() - 1) { diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java index 261f200..8d57806 100644 --- a/src/inference/ProofSystem.java +++ b/src/inference/ProofSystem.java @@ -12,6 +12,7 @@ import java.util.Set; import java.util.stream.Collectors; +import models.algebra.Constant; import models.algebra.Variable; import models.formulas.EquationFormula; import models.formulas.Formula; @@ -22,10 +23,16 @@ import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResourceVariable; +import models.terms.meta.OrderConstraint; import utils.Product; public class ProofSystem { + //MetaExistFormulaのような存在が必要ということを示すFormulaを作ってもいいかも + //あるいはチェックの時にconclusionのほうから必要なものをあらかじめ抽出しておく + + //======================Equality Axioms============================= + private static final InferenceRule reflexivity = new InferenceRule( "Reflexivity", List.of(), @@ -179,6 +186,156 @@ ) ); + private static final InferenceRule constantness = new InferenceRule( + "Constantness", + List.of( + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("t1")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("r1"), new Variable("m"))) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaResourceVariable(new Variable("r1"), new Variable("m")), + new MetaEvaluatableTermVariable(new Variable("t1")) + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + ); + + private static final InferenceRule rightNormalization = new InferenceRule( + "Right Normalization", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r"), new Variable("n")) + ) + ), + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("q"), new Variable("n")) + ) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaResourceVariable(new Variable("q"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r"), new Variable("n")), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("q"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + ); + + private static final InferenceRule pseudoConstantness = new InferenceRule( + "Pseudo-Constantness", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("r"), new Variable("n")) + ) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("r"), new Variable("n")), + new MetaResourceVariable(new Variable("r"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + ); + + //======================Dependency Axioms============================= + + private static final InferenceRule identityMapping = new InferenceRule( + "Identity Mapping", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r")) + ) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r")) + ) + ); + + private static final InferenceRule compositeMapping = new InferenceRule( + "Composite Mapping", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("r")), + new MetaResourceVariable(new Variable("q")) + ) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("q")) + ) + ); + + private static final InferenceRule constantMapping = new InferenceRule( + "Constant Mapping", + List.of(), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("r"), new Variable("m")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + ); + + private static final InferenceRule slicedMapping = new InferenceRule( + "Sliced Mapping", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")) + ), + new MetaResourceVariable(new Variable("p")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("p")) + ) + ), + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaResourceVariable(new Variable("p")) + ) + ); + + //======================Set-Theoretic Axioms============================= + private static final InferenceRule memberSubstitution = new InferenceRule( "Member Substitution", List.of( @@ -215,6 +372,127 @@ ) ); + private static final InferenceRule collectionSubstitution = new InferenceRule( + "Collection Substitution", + List.of( + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ), + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ); + + private static final InferenceRule setEquivelence = new InferenceRule( + "Set Equivelence", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))), + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + ); + + private static final InferenceRule setHomomorphism = new InferenceRule( + "Set Homomorphism", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) + ), + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ) + ); + + private static final InferenceRule leftProjection = new InferenceRule( + "Left Projection", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("r"), new Variable("m")) + ), + new MetaResourceVariable(new Variable("q"), new Variable("l")) + ) + ), + new MetaDependencyFormula( + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), + new MetaResourceVariable(new Variable("q"), new Variable("l")) + ) + ); + + private static final InferenceRule rightProjection = new InferenceRule( + "Right Projection", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("r"), new Variable("m")) + ), + new MetaResourceVariable(new Variable("q"), new Variable("l")) + ) + ), + new MetaDependencyFormula( + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), + new MetaResourceVariable(new Variable("q"), new Variable("l")) + ) + ); + + private static final InferenceRule domainMembership = new InferenceRule( + "Domain Membership", + List.of( + new MetaEquationFormula( + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r1")), + new MetaEvaluatableTermVariable(new Variable("t1")) + ), + new MetaResourceVariable(new Variable("r2")), + new MetaEvaluatableTermVariable(new Variable("t2")) + ), + new MetaResourceVariable(new Variable("c")) + ) + ), + new MetaInFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("t1")), + new MetaResourceVariable(new Variable("r2")), + new MetaEvaluatableTermVariable(new Variable("t2")) + ), + new MetaRDLTerm( + new MetaRDLTerm(new MetaResourceVariable(new Variable("r1"))), + new MetaResourceVariable(new Variable("r2")), + new MetaEvaluatableTermVariable(new Variable("t2")) + ) + ) + ); + private static final InferenceRule codomainMembership = new InferenceRule( "Codomain Membership", List.of( @@ -295,8 +573,21 @@ leftSubstitution, identity, mapComposition, + constantness, + rightNormalization, + pseudoConstantness, + identityMapping, + compositeMapping, + constantMapping, + slicedMapping, memberSubstitution, membershipChain, + collectionSubstitution, + setEquivelence, + setHomomorphism, + leftProjection, + rightProjection, + domainMembership, codomainMembership, codomainMembership2 ); diff --git a/src/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/inference/equivalence/SemanticEquivalenceProofSystem.java index 4472553..d75b77c 100644 --- a/src/inference/equivalence/SemanticEquivalenceProofSystem.java +++ b/src/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -121,6 +121,11 @@ } + public static void debug() { + System.out.println(rule4_1); + System.out.println(rule4_2); + } + private Set applyRule4(SemanticEquivalenceRelation relation, Set existTerms) { Map binding = new HashMap<>(); Map orderConstraint = new HashMap<>(); diff --git a/src/models/terms/meta/OrderConstraint.java b/src/models/terms/meta/OrderConstraint.java index 74824a7..fbd7320 100644 --- a/src/models/terms/meta/OrderConstraint.java +++ b/src/models/terms/meta/OrderConstraint.java @@ -2,11 +2,21 @@ public enum OrderConstraint { - EQ, - LT, - LE, - GT, - GE, - ANY; + EQ("=="), + LT("<"), + LE("<="), + GT(">"), + GE(">="), + ANY(""); + + private final String operator; + + private OrderConstraint(String operator) { + this.operator = operator; + } + + public String getOperator() { + return this.operator; + } }