back to root

back to Matryoshka

DupSup and completeness

• Jasmin Blanchette

  2020-05-25 14:10:24 (GMT)

  I've been trying to prove the conjecture in our JAR submission, about the completeness of DupSup. I think it's more complicated than that. Consider the target clause

  $z\>(b\>(y\>a)) \not\approx \ldots$

  If we don't have FluidSup, we need not only DupSup to rewrite at $z\>(b\>(y\>a))$ or "half inside" $z$ but also an extended "yellow" Sup that deals with $b\>(y\>a)$. So far, all of this was predicted by the conjecture. What wasn't is that we also need to apply DupSup on $y\>a$ and "yellow" Sup on $a$.

  Then, maybe, we're complete. So my question to @Petar Vukmirovic @Alexander Bentkamp and everybody else who cares: Should we make DupSup use a yellow context (i.e. like orange << >>, but without bound variables)? Or have two separate rules?

• Jasmin Blanchette

  2020-05-25 14:10:44 (GMT)

  Or should I give up this idea of achieving completeness via DupSup?

• Alexander Bentkamp

  2020-05-25 14:14:49 (GMT)

  I think it should be just one DupSup rule.

• Alexander Bentkamp

  2020-05-25 14:15:39 (GMT)

  And it doesn't look like a reason to give up the approach. It's not that bad.

• Jasmin Blanchette

  2020-05-25 14:23:54 (GMT)

  What I have right now in my draft is indeed a single rule, and in the "Implementation" section I wrote that we implemented a restriction to green subterms (or contexts, as you like). It is not that bad indeed.

• Jasmin Blanchette

  2020-05-25 14:24:18 (GMT)

  And I think the proof will be fine. We're in almost first order territory here. ;)

• Jasmin Blanchette

  2020-05-25 15:14:43 (GMT)

  @Alexander Bentkamp there's something I don't get. How do you deal in Lemma 27 with cases like the following?

  Left premise: $b \approx a$
  Right premise: $Y\> b \not\approx \cdots$
  Right premise, ground level: $f\>b\>b \not\approx \cdots$

• Jasmin Blanchette

  2020-05-25 15:15:33 (GMT)

  The ground inference rewrites only one $b$ into an $a$, but the nonground inference transforms $Y\> b$ into $Y\>a$, transforming both $b$'s. Right?

• Jasmin Blanchette

  2020-05-25 15:15:55 (GMT)

  Isn't that enough to make the inference nonliftable?

• Jasmin Blanchette

  2020-05-25 15:31:38 (GMT)

  *** Forget it, I worked it out step by step. ;)

• Jasmin Blanchette

  2020-05-25 15:34:9 (GMT)

  For DupSup, the problem seems to present itself. I guess the solution is to show that when the grounding of the nonground inference performs several superpositions in one step, then the produced clause, together with the left premise, entails the initial ground conclusion and hence makes it redundant.

• Alexander Bentkamp

  2020-05-25 15:47:48 (GMT)

  For DupSup itself it shouldn't be a problem because $Y\>b$ becomes $F\>b\>(G\>b)$ by Dup and then $F\>b\>a$ by Sup. So the $b$ is still around.

• Alexander Bentkamp

  2020-05-25 15:50:1 (GMT)

  But for the arguments-of-variables Sup rule, it's indeed a bit tricky.

• Alexander Bentkamp

  2020-05-25 15:54:21 (GMT)

  What if the ground level right premise is $f\>b\>(\lambda x.\> b) \not\approx\dots$?

• Alexander Bentkamp

  2020-05-25 15:55:55 (GMT)

  $f\>a\>(\lambda x.\> a) \not\approx\dots$ does not entail $f\>b\>(\lambda x.\> b) \not\approx\dots$ on the FOL level.

• Alexander Bentkamp

  2020-05-25 15:56:36 (GMT)

  So I think that maybe the arguments-of-variables Sup rule needs to duplicate the argument before it superposes inside it.

• Jasmin Blanchette

  2020-05-25 15:59:5 (GMT)

  Urgl. Actually, I'm kind of fighting with the proof. I know what I want to write, but I find it hard to express it -- these virtual positions in nonground terms are just tricky. I think I'll just forget it. We already have FluidSup -- no need to reinvent it. Pragmatically, we could always look into the unification problems it gives rise to and see if there's some optimization potential.

• Petar Vukmirovic

  2020-05-25 16:2:24 (GMT)

  Looking into unification examples would be useful anyway + might come in handy for the journal version of the HOsup paper

• Petar Vukmirovic

  2020-05-25 16:2:29 (GMT)

  we have no examples from practice there

• Alexander Bentkamp

  2020-05-25 16:53:6 (GMT)

  This leads back to this thread I guess: https://sneeuwbal.zulipchat.com/#narrow/stream/234988-fboolsup-and.20hosup/topic/Special.20unification.20procedure.20for.20FluidSup.3F

• Alexander Bentkamp

  2020-05-25 16:56:48 (GMT)

  To see some concrete examples, is there an easy way to enter a unification problem and get the list of unifiers from Zipperposition?

• Simon Cruanes

  2020-05-25 17:43:35 (GMT)

  I imagine you could write a TPTP problem with thf(the, conjecture, a != b). and see what the immediate steps are?

• Petar Vukmirovic

  2020-05-25 17:50:50 (GMT)

  @Alexander Bentkamp : Function unify_scoped of UnifFramework.ml is whichever version of full HO unification is used (except for your old algo and Simon's algo)

• Petar Vukmirovic

  2020-05-25 17:51:0 (GMT)

  so you can just add a print there

• Petar Vukmirovic

  2020-05-25 17:52:34 (GMT)

  but I guess you want only FluidSup unifiers which you get by putting prints in infer_fluidsup_active(passive)