back to root

back to Matryoshka

Skolemization and saturation framework

• Jasmin Blanchette

  2020-04-28 9:57:58 (GMT)

  It occurred to me that there's a slight complication that arises once we have a calculus whose core (mandatory) rules perform some form of Skolemization, in justifying static and dynamic completeness. Namely, when defining the inference system Inf, one doesn't know in advance which Skolem version to put in there (sk_1? sk_7?). For completeness, one should put all variants. (For soundness, or rather satisfiability preservation, one would then pick a fresh variant.) And Red_Inf has to be defined in such a way that as soon as one of the conclusions of the variants has been generated, the other variant inferences are redundant. This all seems doable but a bit involved.

  An alternative might be to use Hilbert choice and then to argue in a second step that all Hilbert choice terms can be replaced by Skolems. This could work if we use our own Hilbert choice, with no axiom. (Axioms would start messing with our choice terms, which we want to avoid so that we can represent them by Skolems.)

• Jasmin Blanchette

  2020-04-28 9:58:33 (GMT)

  I'm leaving the above as a puzzle to the Theoretiker (@Alexander Bentkamp @Sophie @Uwe Waldmann).

• Alexander Bentkamp

  2020-04-28 10:20:47 (GMT)

  I'd propose to index the skolems with terms rather than with numbers. For example, $\mathsf{sk}_{\exists x.\>t}$ could be used to represent a witness for ${\exists x.\>t}$. Then skolems would not need to be fresh because it would not be a problem to reuse the same skolem if it is supposed to witness the same term anyway. It is even desirable to reuse skolems in this way and Petar has already implemented this.

• Jasmin Blanchette

  2020-04-28 10:57:11 (GMT)

  Good. That basically amounts to Hilbert choice without axiom (the second para above). The inference rules are then even sound w.r.t. models where $(\exists x.\;t) \longrightarrow t[\mathsf{sk}_{\exists x.\;t}/x]$ holds for all $t$.

• Jasmin Blanchette

  2020-04-28 10:59:18 (GMT)

  ($\mathsf{sk}_{\exists x.\>t}$ being just another syntax for $\epsilon\> (\lambda x.\> t)$ or $\epsilon x.\> t$.)

• Jasmin Blanchette

  2020-04-28 11:16:30 (GMT)

  Actually, forget some of what I wrote. There is a difference with using a Skolem and some choice constant in the presence of variables. I guess your Skolem $\mathsf{sk}_{\exists x.\> t}$ would take all of $t$'s free variables as arguments. That would indeed mean the subscript remains unchanged under substitution (right?), which is good for Zip/Petar.

• Alexander Bentkamp

  2020-04-28 12:27:23 (GMT)

  Right.

• Alexander Bentkamp

  2020-04-28 12:28:13 (GMT)

  Using sk with subscripts also allows us to have an axiomatized choice function in addition to be complete w.r.t. choice.

• Jasmin Blanchette

  2020-04-28 12:34:6 (GMT)

  Well nobody would have forbidden us from having two choices, the official one and a special, not axiomatized one.

• Jasmin Blanchette

  2020-04-28 12:34:21 (GMT)

  That's what I meant by "our own Hilbert choice" above.

• Alexander Bentkamp

  2020-04-28 12:37:23 (GMT)

  ok, sure, I am just saying I am happy that one choice function is enough :-)

• Jasmin Blanchette

  2020-04-28 16:7:16 (GMT)

  Well $\mathsf{sk}$ is essentially an indexed family of choices, so you have $\omega$ of them instead...

• Jasmin Blanchette

  2020-04-28 16:10:13 (GMT)

  Seriously, maybe I am worrying for nothing, but I am wondering how you intend to connect the ground and nonground levels then. Normally, the ground level would have no free variables, so it would never generate, say, $\mathsf{sk}_{\exists x.\> x = \mathsf{fst}\>(\mathsf{pair}\>x\>y)}\>y$ -- which has a free variable in the label and an extra argument $y$.

• Petar Vukmirovic

  2020-04-28 16:50:17 (GMT)

  Jasmin Blanchette said:

  Seriously, maybe I am worrying for nothing, but I am wondering how you intend to connect the ground and nonground levels then. Normally, the ground level would have no free variables, so it would never generate, say, $\mathsf{sk}_{\exists x.\> x = \mathsf{fst}\>(\mathsf{pair}\>x\>y)}\>y$ -- which has a free variable in the label and an extra argument $y$.

  We can guarantee stability of those names under substitution. That should fix the problem, right?

• Jasmin Blanchette

  2020-04-28 17:50:59 (GMT)

  How can you do that?

• Alexander Bentkamp

  2020-04-28 18:2:29 (GMT)

  I think Petar misunderstood the issue. Let's look at an example: $C = \exists x.\>f(x,Y) \approx \top$. BoolRw will derive $f(x,sk_{\exists x.\>f(x,Y)}(Y)) \approx \top$. But on the ground instance $C\theta = \exists x.\>f(x,Y\theta) \approx \top$, BoolRw would derive $f(x,sk_{\exists x.\>f(x,Y\theta)}) \approx \top$. So not only is the skolem constant a different one, it also has a different number of arguments.

  This is indeed not easy to deal with, but it can be done with the intersection-mechanism of the saturation framework. In our previous papers, the intersection parameter q was the selection function. Now, q will get a second component $w$, which assigns witness terms $w(C, \exists x.\>t)$ to each pair of a ground clause C and ground term of the form $\exists x.\>t$ occurring in C. The ground inference system will not use the sk constants directly, but instead ask this function w for an appropriate term.

  For the lifting, we can then inject a function $w$ into the ground inference system that depends on the saturated set N of nonground clauses. If for example N contains a clause $C = \exists x.\>f(x,Y) \approx \top$ with the ground instance $C\theta = \exists x.\>f(x,Y\theta) \approx \top$, we can set $w(C\theta, \exists x.\>f(x,Y\theta)) = \mathsf{sk}_{\exists x.\>f(x,Y)}(Y\theta)$ to ensure that the ground inference is liftable to a nonground inference.

• Petar Vukmirovic

  2020-04-28 18:20:27 (GMT)

  You skolemized the second arg, but the first one should be skolemized, right?

• Petar Vukmirovic

  2020-04-28 18:21:52 (GMT)

  Apart from that, what I thought was that you can reuse the name, and pass the ground arg $Y \theta$ to the symbol

• Petar Vukmirovic

  2020-04-28 18:22:39 (GMT)

  I just realized that there is no guarantee whether you will reason about more or less general formula first, so Skolem renaming might not work properly

• Jasmin Blanchette

  2020-04-28 19:14:45 (GMT)

  Alex: Right. I guess this could work. An alternative would be to introduce schematic variables, like in Isabelle. In Inf, the inference would produce a clause with ?sk in it. No subscript. The semantics would be existential (there exists a skolem function ?sk such that the clause is true). A clause with a concrete Skolem term would entail this clause and make the inference redundant.

  Petar: Alex and I are merely discussing the completeness proof. The calculus wil simply use indexed Skolems $\mathsf{sk}_{...}$.

• Jasmin Blanchette

  2020-04-28 19:17:36 (GMT)

  Actually, the alternative probably doesn't prevent the intersection trick when grounding. Forget it.

• Alexander Bentkamp

  2020-04-29 14:49:21 (GMT)

  There is actually a problem with this witness function.

  Consider for example these clauses:
  $C = f (\exists x.\> g(x,x,Y)) \approx h(Y)$
  $C\theta = f (\exists x.\> g(x,x,\exists z. \>p(z))) \approx h(\exists z. \>p(z))$
  Then we would set $w(C\theta, \exists x.\> g(x,x,\exists z. \>p(z))) = \mathsf{sk}_{\exists x.\> g(x,x,Y)}(\exists z. \>p(z))$.
  But with this witness function, GBoolRw on $C\theta$ would produce
  $f (g(\mathsf{sk}_{\exists x.\> g(x,x,Y)}(\exists z. \>p(z)),\mathsf{sk}_{\exists x.\> g(x,x,Y)}(\exists z. \>p(z)),\exists z. \>p(z))) \approx h(\exists z. \>p(z))$
  And this conclusion is larger than the premise $C\theta$ because it has more $\exists$ s. Therefore it is useless for the completeness proof.

  This is not a fundamental problem. If we merge ground and nonground completeness proof, it would work out fine. But using the saturation framework is difficult. This is for similar reasons as for constraint superposition.

  Another option would be to change the calculus a bit. So far, I decided not to do inferences below quantifiers. Alternatively, we could add inferences below quantifiers, but in exchange restrict the $\forall$ and $\exists$-cases of BoolRw to apply only if the body of the quantifier does not contain any boolean subterms other than $\top$, $\bot$, or variables. I am not sure what would be better performancewise, but the inferences below quantifiers would solve the problem with the witness function.

• Petar Vukmirovic

  2020-04-29 16:36:10 (GMT)

  Ok I do not understand the problem 100%, but restricting the BoolRw rule to apply if the body of the quantifier contains only $\top$, $$\bot$$b or $x$ booleans boils down to quantifier having only those terms as the body, because the body of the quant has to be a Boolean, and only booleans allowed are those three

• Petar Vukmirovic

  2020-04-29 16:36:49 (GMT)

  This is very restrictive, since I have not seen $\forall x. x$ or $\forall x. y$ appear at all in practice

• Petar Vukmirovic

  2020-04-29 16:37:29 (GMT)

  and simplifier will simplify $\forall x. f$ where $f$ contains no $x$ into $f$, reducing $\forall x. \top (\bot)$ to $\top$ or $\bot$ in the remaining cases

• Petar Vukmirovic

  2020-04-29 16:38:39 (GMT)

  So, in principle, performing sups under quantifiers will not be the end of the world, because this BoolRw restriction is quite strong

• Petar Vukmirovic

  2020-04-29 16:40:11 (GMT)

  This means that BoolRw will (almost) ignore the quants, with the price of performing sups under quantifiers

• Petar Vukmirovic

  2020-04-29 16:40:26 (GMT)

  What about leaking variables bound in quantifiers?

• Alexander Bentkamp

  2020-04-29 16:44:43 (GMT)

  Right, I forgot one condition. I meant: Apply BoolRw for ∀/∃ only if each boolean subterm in the body is ⊤, ⊥, a variable, or contains the variable bound by the quantifier.

• Jasmin Blanchette

  2020-04-29 16:53:24 (GMT)

  I wouldn't change the calculus to please the completeness proof as long as we believe the calculus is complete and that there might be a reasonable solution.

  I have another idea, based on the schematic variable approach I was talking about earlier. The idea is to represent all Skolems by these schematic variables, even at the ground level. These schematic variables would behave like regular free variables w.r.t. alpha-equivalence and grounding. But unification would never instantiate them.

  Grounding of f (?SK Y) = h Y would yield e.g. {f (?SK a) = h a, f (?SK b) = h b, ...}, whereas the ground calculus would have, say, {f ?SK = h b}. Because all (1) occurrences of ?SK in the grounded clause have the same first argument, it makes no difference and can be pruned. Or, put another way, if we now instantiate the ?SK variables, we get the same ground clauses.

• Alexander Bentkamp

  2020-04-29 17:6:16 (GMT)

  But after some inferences, the same skolem might appear with different arguments in a clause.

• Jasmin Blanchette

  2020-04-29 17:8:11 (GMT)

  I'm not sure I'm following. Remember that these are schematic variables. So "?SK a b" and "?SK b a" just mean essentially the same thing (some term that contains a and b). Could you make your example concrete?

• Alexander Bentkamp

  2020-04-29 17:9:21 (GMT)

  Maybe I haven't understood your proposal well...

• Alexander Bentkamp

  2020-04-29 17:10:21 (GMT)

  I'll have dinner now, but we can talk about it later or tomorrow.

• Jasmin Blanchette

  2020-04-29 17:12:13 (GMT)

  Yes, maybe we should Skype.

• Petar Vukmirovic

  2020-04-29 17:44:54 (GMT)

  Alexander Bentkamp said:

  Right, I forgot one condition. I meant: Apply BoolRw for ∀/∃ only if each boolean subterm in the body is ⊤, ⊥, a variable, or contains the variable bound by the quantifier.

  You probably mean proper subterms, because if they are not proper then we are again in the same situation

• Alexander Bentkamp

  2020-04-29 18:40:34 (GMT)

  No, because in most cases, the body will contain the variable bound by the quantifier.

• Petar Vukmirovic

  2020-04-29 18:52:19 (GMT)

  ok.. so if I understand this correctly... $\forall x. \textsf{p}(\textsf{a})$ will not be OK

• Petar Vukmirovic

  2020-04-29 18:52:34 (GMT)

  but $\forall x. \textsf{p}(x)$

• Petar Vukmirovic

  2020-04-29 18:52:55 (GMT)

  is OK

• Alexander Bentkamp

  2020-04-29 19:34:42 (GMT)

  Right. And OK means only BoolRw at the top level. Not OK means inferences inside, but nor BoolRw on the top level.

• Alexander Bentkamp

  2020-04-29 19:35:48 (GMT)

  I would guess that the version that we currently have, i.e. no inferences below quantifiers ever, is more efficient. What do you think?