diff --git a/src/Main.java b/src/Main.java index 85f114c..37bea9c 100644 --- a/src/Main.java +++ b/src/Main.java @@ -1,5 +1,6 @@ import java.util.List; +import inference.ProofSystem; import inference.equivalence.SemanticEquivalenceProofSystem; import inference.equivalence.SemanticEquivalenceRelation; import lombok.SneakyThrows; @@ -7,9 +8,14 @@ import models.algebra.Type; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; +import models.formulas.DependencyFormula; import models.formulas.EquationFormula; +import models.formulas.InFormula; +import models.terms.Dependency; import models.terms.DependencyTerm; +import models.terms.ResourceConstant; import models.terms.ResourceVariable; +import models.terms.SetEvaluatableTerm; import parser.Parser; import parser.Parser.TokenStream; import tests.Utils; @@ -24,6 +30,11 @@ public static void main(String[] args) { +// sandbox2(); + sandbox3(); + } + + static void sandbox1() { ResourceVariable A = new ResourceVariable("A", Utils.INT, 2); ResourceVariable Ap = new ResourceVariable("A'", Utils.INT, 2); ResourceVariable B = new ResourceVariable("B", Utils.INT, 2); @@ -49,26 +60,36 @@ // System.out.println(conclusionFormula.linearRightNormalized()); System.out.println(proofSystem.proof()); -// sandbox2(); } static void sandbox2() { - 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(t1, B, E); - System.out.println(t2); - System.out.println(t2.isLinearRightNormalized()); - t2.selfLinearRightNormalize(); - System.out.println(t2); + ProofSystem.debug(); + } + + static void sandbox3() { + ResourceVariable followee = new ResourceVariable("followee", INT, 2); + ResourceVariable fno = new ResourceVariable("fno", INT, 2); + ResourceConstant one = new ResourceConstant("1"); + ResourceConstant A = new ResourceConstant("A"); + ResourceConstant C = new ResourceConstant("C"); + ResourceVariable aid = new ResourceVariable("aid", INT, 1); + DependencyTerm t1 = new DependencyTerm(followee, fno, one); + Dependency d1 = new Dependency(t1, aid); + DependencyTerm t2 = new DependencyTerm(one, aid, A); + DependencyTerm t3 = new DependencyTerm(new SetEvaluatableTerm(fno), aid, A); + DependencyTerm t4 = new DependencyTerm(t1, aid, A); + + DependencyFormula f1 = new DependencyFormula(d1); + InFormula f2 = new InFormula(t2, t3); + EquationFormula f3 = new EquationFormula(t4, C); + InFormula conclusion = new InFormula(C, new SetEvaluatableTerm(new SetEvaluatableTerm(followee))); + + System.out.println(f1); + System.out.println(f2); + System.out.println(f3); + System.out.println(conclusion); + boolean result = ProofSystem.check(List.of(f1, f2, f3), conclusion); + System.out.println(result); } diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java index c10c5d1..ccbdd84 100644 --- a/src/inference/InferenceRule.java +++ b/src/inference/InferenceRule.java @@ -13,13 +13,16 @@ import models.formulas.meta.MetaFormula; import models.terms.RDLTerm; import models.terms.meta.OrderVariableConstraint; +import utils.Permutation; public class InferenceRule { @Getter private final String name; + @Getter private final List assumptions; + @Getter private final MetaFormula conclusion; private final InferenceOrderConstraint defaultOrderConstraint; @@ -112,6 +115,47 @@ } + public Formula apply(List assumptions) { + if (assumptions.size() != getAssumptionSize()) { + return null; + } + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + for (int i = 0; i < getAssumptionSize(); i++) { + if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraint)) { + return null; + } + } + return conclusion.substitution(binding); + } + + public Formula apply(Collection assumptions) { + if (assumptions.size() != getAssumptionSize()) { + return null; + } + for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { + boolean matchFailed = false; + for (int i = 0; i < getAssumptionSize(); i++) { + if (! this.assumptions.get(i).isMatchedBy(assumptionList.get(i))) { + matchFailed = true; + break; + } + } + if (matchFailed) { + continue; + } else { + return apply(assumptionList); + } + } + return null; + } + + + public int getAssumptionSize() { + return this.assumptions.size(); + } + + public String toString() { StringBuilder sb = new StringBuilder(); for (int i = 0; i < assumptions.size(); i++) { @@ -122,7 +166,7 @@ } String assumpStr = sb.toString(); String concluStr = conclusion.toString(); - String line = "-".repeat(Math.max(assumpStr.length(), concluStr.length())); + String line = "-".repeat(Math.max(assumpStr.length(), concluStr.length())) + " (" + this.name + ")"; sb = new StringBuilder(); sb.append(assumpStr); sb.append("\n"); diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java index f3c89d2..be922d1 100644 --- a/src/inference/ProofSystem.java +++ b/src/inference/ProofSystem.java @@ -10,17 +10,322 @@ import java.util.Map; import java.util.Set; +import models.algebra.Variable; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.formulas.meta.MetaInFormula; import models.terms.EvaluatableTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; +import utils.Product; public class ProofSystem { - public static boolean check(Collection assumptions, Formula conclusion) { - if (equationTransitionCheck(assumptions, conclusion)) { - return true; + private static final InferenceRule reflexivity = new InferenceRule( + "Reflexivity", + List.of(), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + private static final InferenceRule symmetry = new InferenceRule( + "Symmetry", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + private static final InferenceRule transitivity = new InferenceRule( + "Transitivity", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ); + + private static final InferenceRule rightSubstitution = new InferenceRule( + "Right Substitution", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")) + ), + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("r"))) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ); + + private 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 MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")) + ), + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("ue")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("r"))) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ); + + private static final InferenceRule identity = new InferenceRule( + "Identity", + List.of( + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("r"))) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaResourceVariable(new Variable("r")), + new MetaResourceVariable(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + private static final InferenceRule mapComposition = new InferenceRule( + "Map Composition", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")) + ), + new MetaDependencyFormula( + new MetaResourceVariable(new Variable("r")), + new MetaResourceVariable(new Variable("p")) + ), + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("p"))) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r")), + new MetaRDLTerm( + new MetaResourceVariable(new Variable("r")), + new MetaResourceVariable(new Variable("p")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("p")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + + private static final InferenceRule memberSubstitution = new InferenceRule( + "Member Substitution", + List.of( + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ); + + private static final InferenceRule membershipChain = new InferenceRule( + "Membership Chain", + List.of( + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaInFormula( + 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 codomainMembership = new InferenceRule( + "Codomain Membership", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r1")), + new MetaEvaluatableTermVariable(new Variable("t1")) + ), + new MetaResourceVariable(new Variable("r2")) + ), + 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")) + ) + ) + ), + new MetaInFormula( + 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 MetaRDLTerm( + new MetaRDLTerm( + new MetaResourceVariable(new Variable("se")) + ), + new MetaResourceVariable(new Variable("r2")), + new MetaEvaluatableTermVariable(new Variable("t2")) + ) + ) + ); + + private static final List axioms = List.of( + reflexivity, + symmetry, + transitivity, + rightSubstitution, + leftSubstitution, + identity, + mapComposition, + memberSubstitution, + membershipChain, + codomainMembership + ); + + public static void debug() { + for (var axiom : axioms) { + System.out.println(axiom); + System.out.println("=================================================================================================="); } - return false; + } + + + public static boolean check(Collection assumptions, Formula conclusion) { +// if (equationTransitionCheck(assumptions, conclusion)) { +// return true; +// } + + Set appearFormulas = new HashSet<>(assumptions); + int prevAppearFormulasSize = appearFormulas.size(); + while (! appearFormulas.contains(conclusion)) { + Set derivedFormulas = new HashSet<>(); + System.out.println("========================================="); + System.out.println(appearFormulas); + for(InferenceRule axiom : axioms) { + derivedFormulas.addAll(applyAxiom(axiom, appearFormulas)); + } + if (derivedFormulas.size() == 0) { + return false; + } + appearFormulas.addAll(derivedFormulas); + if (appearFormulas.size() == prevAppearFormulasSize) { + return false; + } + prevAppearFormulasSize = appearFormulas.size(); + } + + return true; + } + + private static Set applyAxiom(InferenceRule axiom, Set formulas) { + Set result = new HashSet<>(); + List> matchedFormulas = new ArrayList<>(); + for (int i = 0; i < axiom.getAssumptionSize(); i++) { + matchedFormulas.add(new ArrayList<>()); + for (Formula formula : formulas) { + if (axiom.getAssumptions().get(i).isMatchedBy(formula)) { + matchedFormulas.get(i).add(formula); + } + } + } + for(List applyFormulas : Product.product(matchedFormulas)) { + result.add(axiom.apply(applyFormulas)); + } + if (result.size() != 0) { + System.out.println(axiom.getName()); + System.out.println(result); + } + return result; } private static boolean equationTransitionCheck(Collection assumptions, Formula conclusion) { diff --git a/src/models/formulas/meta/MetaDependencyFormula.java b/src/models/formulas/meta/MetaDependencyFormula.java index ea72f2f..12dd807 100644 --- a/src/models/formulas/meta/MetaDependencyFormula.java +++ b/src/models/formulas/meta/MetaDependencyFormula.java @@ -7,6 +7,7 @@ import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.Formula; +import models.terms.Dependency; import models.terms.RDLTerm; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; @@ -44,6 +45,13 @@ } + @Override + public DependencyFormula substitution(Map binding) { + return new DependencyFormula((Dependency) dependency.substitute(binding)); + } + + + public String toString() { return dependency.toString(); } diff --git a/src/models/formulas/meta/MetaEquationFormula.java b/src/models/formulas/meta/MetaEquationFormula.java index 9c4ddd9..7f27ff5 100644 --- a/src/models/formulas/meta/MetaEquationFormula.java +++ b/src/models/formulas/meta/MetaEquationFormula.java @@ -7,6 +7,7 @@ import models.algebra.Variable; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.meta.MetaRDLTerm; import models.terms.meta.OrderVariableConstraint; @@ -39,6 +40,10 @@ return leftSideHand.isMatchedBy(eq.getLeftSideHand(), binding, orderConstraint) && rightSideHand.isMatchedBy(eq.getRightSideHand(), binding, orderConstraint); } + @Override + public EquationFormula substitution(Map binding) { + return new EquationFormula((EvaluatableTerm) leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding)); + } public String toString() { return leftSideHand.toString() + " = " + rightSideHand.toString(); diff --git a/src/models/formulas/meta/MetaFormula.java b/src/models/formulas/meta/MetaFormula.java index cd43fbd..6115a2b 100644 --- a/src/models/formulas/meta/MetaFormula.java +++ b/src/models/formulas/meta/MetaFormula.java @@ -16,6 +16,8 @@ public abstract boolean isMatchedBy(Formula formula, Map binding, Map orderConstraint); + public abstract Formula substitution(Map binding); + public abstract String toString(); public abstract boolean equals(Object another); public abstract int hashCode(); diff --git a/src/models/formulas/meta/MetaInFormula.java b/src/models/formulas/meta/MetaInFormula.java index d446557..900faff 100644 --- a/src/models/formulas/meta/MetaInFormula.java +++ b/src/models/formulas/meta/MetaInFormula.java @@ -7,6 +7,7 @@ import models.algebra.Variable; import models.formulas.Formula; import models.formulas.InFormula; +import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.meta.MetaRDLTerm; import models.terms.meta.OrderVariableConstraint; @@ -38,6 +39,12 @@ return leftSideHand.isMatchedBy(inFormula.getLeftSideHand(), binding, orderConstraint) && rightSideHand.isMatchedBy(inFormula.getRightSideHand(), binding, orderConstraint); } + + @Override + public InFormula substitution(Map binding) { + return new InFormula((EvaluatableTerm) leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding)); + } + @Override public String toString() { diff --git a/src/models/terms/meta/MetaRDLTerm.java b/src/models/terms/meta/MetaRDLTerm.java index efb0d65..17ae060 100644 --- a/src/models/terms/meta/MetaRDLTerm.java +++ b/src/models/terms/meta/MetaRDLTerm.java @@ -157,7 +157,7 @@ } return new Dependency(dependingTerm, (ResourceVariable) dependedVariable); } - if (isDependencyTerm()) { + else if (isDependencyTerm()) { RDLTerm dependingTerm = (RDLTerm) getChild(0); RDLTerm dependedVariable = (RDLTerm) getChild(1); RDLTerm argumentTerm = (RDLTerm) getChild(2); @@ -171,6 +171,12 @@ argumentTerm = ((MetaRDLTerm) argumentTerm).substitute(binding); } return new DependencyTerm((EvaluatableTerm) dependingTerm, (ResourceVariable) dependedVariable, (EvaluatableTerm) argumentTerm); + } else if (isSetTerm()) { + RDLTerm term = (RDLTerm) getChild(0); + if (term instanceof MetaRDLTerm) { + term = ((MetaRDLTerm) term).substitute(binding); + } + return new SetEvaluatableTerm((EvaluatableTerm) term); } throw new SubstituteFailedException(); } @@ -226,6 +232,10 @@ return checkTermType(DependencyTerm.class); } + public boolean isSetTerm() { + return checkTermType(SetEvaluatableTerm.class); + } + public boolean isResourceVariable() { return checkTermType(ResourceVariable.class); } @@ -266,6 +276,8 @@ return "[" + getChild(0).toString() + "]"; case META_DEPENDENCY_TERM: return "[" + getChild(0).toString() + " : " + getChild(1).toString() + " -> " + getChild(2).toString() + "]"; + case META_EVALUATABLE_TERM_SET: + return "{" + getChild(0).toString() + "}"; default: return ""; } diff --git a/src/models/terms/meta/MetaResourceVariable.java b/src/models/terms/meta/MetaResourceVariable.java index ad665dd..19be600 100644 --- a/src/models/terms/meta/MetaResourceVariable.java +++ b/src/models/terms/meta/MetaResourceVariable.java @@ -1,10 +1,15 @@ package models.terms.meta; +import java.util.Map; + import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; import models.algebra.Symbol; import models.algebra.Variable; +import models.terms.RDLTerm; +import models.terms.ResourceConstant; +import models.terms.ResourceVariable; @Getter public class MetaResourceVariable extends MetaVariable { @@ -20,4 +25,26 @@ public MetaResourceVariable(Variable variableName, Expression order) { super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, OrderConstraint.EQ, order); } + + @Override + public boolean isMatchedBy(RDLTerm another, Map binding, + Map orderConstraint) { + if ((! (another instanceof ResourceVariable)) && (! (another instanceof ResourceConstant))) { + return false; + } + + if (! orderConstraintCheck(another, orderConstraint)) { + return false; + } + + if (! islinearRightNormalizedMatchedBy(another)) { + return false; + } + + if (! binding.containsKey(this.variableName)) { + binding.put(this.variableName, another); + return true; + } + return binding.get(this.variableName).equals(another); + } } diff --git a/src/models/terms/meta/MetaVariable.java b/src/models/terms/meta/MetaVariable.java index ed96b12..27e13db 100644 --- a/src/models/terms/meta/MetaVariable.java +++ b/src/models/terms/meta/MetaVariable.java @@ -103,7 +103,7 @@ throw new SubstituteFailedException(); } - private boolean orderConstraintCheck(RDLTerm another, Map orderConstraints) { + protected boolean orderConstraintCheck(RDLTerm another, Map orderConstraints) { if (orderVariable == null) { switch (constraint) { case ANY: diff --git a/src/tests/utils/ProductTest.java b/src/tests/utils/ProductTest.java new file mode 100644 index 0000000..0747642 --- /dev/null +++ b/src/tests/utils/ProductTest.java @@ -0,0 +1,33 @@ +package tests.utils; + +import static org.junit.Assert.*; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import utils.Product; + +public class ProductTest { + + @Test + void product() { + List> input = List.of( + List.of(1, 2), + List.of(3, 4), + List.of(5) + ); + + List> result = Product.product(input); + + List> expected = List.of( + List.of(1, 3, 5), + List.of(1, 4, 5), + List.of(2, 3, 5), + List.of(2, 4, 5) + ); + + assertEquals(expected, result); + } + +} diff --git a/src/utils/Product.java b/src/utils/Product.java new file mode 100644 index 0000000..89238fb --- /dev/null +++ b/src/utils/Product.java @@ -0,0 +1,37 @@ +package utils; + +import java.util.ArrayList; +import java.util.List; + +public class Product { + + public static List> product(List> lists) { + List> result = new ArrayList<>(); + + if (lists == null || lists.isEmpty()) { + return result; + } + + backtrack(lists, result, 0, new ArrayList<>()); + return result; + } + + private static void backtrack( + List> lists, + List> result, + int depth, + List current) { + + if (depth == lists.size()) { + result.add(new ArrayList<>(current)); + return; + } + + for (T element : lists.get(depth)) { + current.add(element); + backtrack(lists, result, depth + 1, current); + current.remove(current.size() - 1); + } + } + +}