back to root

back to Matryoshka

HOSup (and BoolSup)

• Jasmin Blanchette

  2020-06-02 15:45:32 (GMT)

  I just want to make sure I get it right: In the forthcoming HOSup paper, we will never (or almost never) need $\models$ to mean just entailment w.r.t. $\approx$ and not the bold symbols, is that right? In particular, the redundancy criterion will support Booleans, e.g. p(a) will make p(a \/ false) redundant. That sounds reasonable but I want to be sure. Also, I'll need a symbol for the raw kind of entailment I just mentioned to deal with ArgCong efficiently.

• Jasmin Blanchette

  2020-06-02 15:45:47 (GMT)

  For the moment, I'll write $\models_0$ or something.

• Alexander Bentkamp

  2020-06-02 15:50:25 (GMT)

  Yes, Booleans will be built into all consequence relations. $\models_0$ is ok with me.

• Alexander Bentkamp

  2020-06-02 15:56:4 (GMT)

  Of course, the redundancy criterion can only do first-order boolean reasoning. So it does indeed know that a and a \/ false are the same, but it doesn't know that p ≈ (λx. ⊤) and ∀ x. p x are the same.

• Jasmin Blanchette

  2020-06-02 16:12:57 (GMT)

  Makes sense. Right now I'm writing $\models_\approx$.

• Jasmin Blanchette

  2020-06-02 16:13:13 (GMT)

  $\models_\mathrm{euf}$ would be yet another option.

• Alexander Bentkamp

  2020-06-02 16:45:35 (GMT)

  euf au plat?

• Alexander Bentkamp

  2020-06-02 16:45:52 (GMT)

  maybe I'm too hungry...

• Jasmin Blanchette

  2020-06-02 19:14:23 (GMT)

  Equality with uninterpreted functions.

• Jasmin Blanchette

  2020-06-02 19:14:39 (GMT)

  Never read EUF as OEUF before. ;)

• Jasmin Blanchette

  2020-06-02 19:18:18 (GMT)

  Quick question: at the GF layer, the lemma that says that if C' \/ t = s is productive, then "not R |= C'". For this one, entailment is plain entailment without Booleans, right? It just performs rewriting with R, right?

  If so, I'm starting to find the notation $\models$ for "with Booleans" too confusing. Traditionally, one puts theories as a subscript to $\models$. Maybe $\models_{\mathbb{B}}$ or something. ($\mathbb{B}$ = Booleans, kind of standard.)

• Simon Cruanes

  2020-06-02 19:18:27 (GMT)

  "Obviously, Equality with Uninterpreted Functions"

• Jasmin Blanchette

  2020-06-02 19:19:33 (GMT)

  Omogeneous Equality with UF. As opposed to heterogeneous equality (e.g., == in Lean).

• Simon Cruanes

  2020-06-02 19:20:5 (GMT)

  Ominous Equality with Unsecure Functions. Anything could be equal to anything if you don't pay close enough attention.

• Alexander Bentkamp

  2020-06-02 19:23:1 (GMT)

  Jasmin Blanchette said:

  Quick question: at the GF layer, the lemma that says that if C' \/ t = s is productive, then "not R |= C'". For this one, entailment is plain entailment without Booleans, right? It just performs rewriting with R, right?

  If so, I'm starting to find the notation $\models$ for "with Booleans" too confusing. Traditionally, one puts theories as a subscript to $\models$. Maybe $\models_{\mathbb{B}}$ or something. ($\mathbb{B}$ = Booleans, kind of standard.)

  That's true. We should distinguish two different kinds of entailment I think. @Sophie @Visa

• Alexander Bentkamp

  2020-06-02 19:28:47 (GMT)

  We've spoken about this in last week's meeting. Some of the rewrite systems in the proof do not interpret Booleans correctly. So we probably need a weaker notion of interpretation, which comes with a weaker notion of entailment.

• Jasmin Blanchette

  2020-06-02 19:39:1 (GMT)

  Right -- I presume the $R_C$'s interpret Booleans correctly only in terms smaller than $C$ or something.

• Alexander Bentkamp

  2020-06-02 19:42:24 (GMT)

  $R_C$, $R_N$ do not interpret Booleans correctly at all. $R_C^s$ only for terms smaller than $s$. Only $R_C^*$ and $R_N^*$ interpret all Boolean terms correctly.

• Jasmin Blanchette

  2020-06-02 19:43:58 (GMT)

  I see. ;)

• Alexander Bentkamp

  2020-06-02 19:44:0 (GMT)

  But your intuition is right. $R_C^s$ roughly corresponds to what $R_C$ is in the standard completeness proof.

• Jasmin Blanchette

  2020-06-02 19:44:47 (GMT)

  My intuition is always right. It's just the execution that's often wrong... like last week. ;)

• Jasmin Blanchette

  2020-06-02 19:46:34 (GMT)

  But to go back to my initial question: Is it so that $R$ (the ultimate) falsifies, using only rewrite rules, all the subclauses $C'$ of productive clauses, or is the construction more complicated?

• Jasmin Blanchette

  2020-06-02 19:47:6 (GMT)

  In the latter case, I guess a Skype call might be useful tomorrow (Wed).

• Alexander Bentkamp

  2020-06-02 19:50:51 (GMT)

  Yes, that's what Lemma 12 says.

• Jasmin Blanchette

  2020-06-02 19:51:52 (GMT)

  Thanks. I already have 5 calls scheduled for tomorrow; no need for a 6th one. ;)

• Jasmin Blanchette

  2020-06-02 19:52:7 (GMT)

  (Maybe 6 actually...)

• Alexander Bentkamp

  2020-06-02 19:53:27 (GMT)

  I realize now that the $\models$ symbol in Lemma 12 is not entailment, but rather "This interpretation is a model of that clause". So there is no difference between $\models$ and $\models_{\mathbb{B}}$.

• Jasmin Blanchette

  2020-06-03 6:13:28 (GMT)

  There's still a subtle difference. It is reasonable to read $R \models_\mathbb{B} C$ as meaning what you said plus $R$ is a Boolean-standard interpretation. Just like $R \models C$ somewhat implicitly implies that $R$ interprets equality as a congruence (otherwise the expression is "ill-typed"). I would be very grateful if you could reserve the plain $\models$ symbols, whether for entailment or for the models relation, for the plain EUF concepts.

• Jasmin Blanchette

  2020-06-03 10:50:9 (GMT)

  Regardless of notations, am I guessing right that $h\>(g\>\pmb{\approx}\>f) \approx a \models_{\mathbb{B}} h\>(g\>a\>\pmb{\approx}\>f\>a) \approx a$ won't hold?

• Alexander Bentkamp

  2020-06-03 10:53:24 (GMT)

  I presume you are talking about the FOL layer? Then it would rather be $h(g_0\>\pmb{\approx}\>f_0) \approx a \models_{\mathbb{B}} h(g_1(a)\>\pmb{\approx}\>f_1(a)) \approx a$. And indeed it does not hold.

• Jasmin Blanchette

  2020-06-03 11:7:38 (GMT)

  Sorry, I wasn't clear. I meant at the HO layer (i.e. the HO syntax wasn't accidental), as in the redundancy criterion, but there I should have written $\models_\mathcal{G}$ or $\models_{\mathbb{B}\mathcal{G}}$, and the answer is the same.

• Jasmin Blanchette

  2020-06-03 11:12:34 (GMT)

  Coming back to the notation, I don't think I need $\models_0$ after all. Yesterday, when we talk or chatted about ArgCong, we discovered a snag with Booleans, which I quickly fixed by using "nonstandard" models of the Booleans. But the problem is not the Booleans (which can be characterized easily as an equational theory). The difficulty is that $\pmb{\approx}$, just like $\approx$, is not argument-congruent.

• Jasmin Blanchette

  2020-06-03 11:13:54 (GMT)

  Which is perfect. I think things will plug nicely together. (Whereas until now, I've been fighting unsuccessfully various mismatches between $\models_0$ and $\models_\mathbb{B}$.)

• Alexander Bentkamp

  2020-06-03 11:20:35 (GMT)

  Jasmin Blanchette said:

  Sorry, I wasn't clear. I meant at the HO layer (i.e. the HO syntax wasn't accidental), as in the redundancy criterion, but there I should have written $\models_\mathcal{G}$ or $\models_{\mathbb{B}\mathcal{G}}$, and the answer is the same.

  Now I am confused. In the redundancy criterion, there is only one reference to $\models$, which is the one on the FOL layer.

  The consequence relation $\models_\mathcal{G}$ has nothing to do with the redundancy criterion. That consequence relation can do higher-order reasoning and the answer would not be the same here.

• Alexander Bentkamp

  2020-06-03 11:22:34 (GMT)

  Jasmin Blanchette said:

  Coming back to the notation, I don't think I need $\models_0$ after all.

  That's great. We have enough entailments relations already :-)

• Jasmin Blanchette

  2020-06-03 11:28:37 (GMT)

  By $\models_\mathcal{G}$ I meant the lifting one gets by the saturation framework. $N \models_\mathcal{G} C$ iff $\mathcal{G}(N) \models \mathcal{G}(C)$. The redundancy criterion might not textually use the symbol $\models_\mathcal{G}$, but it's still the same lifting. Do you use the same symbol ($\models_\mathcal{G}$) for something else? How can it do HO reasoning if it's obtained by a grounding (as suggested by the notation?).

• Alexander Bentkamp

  2020-06-03 11:30:59 (GMT)

  It's just grounding and not flooring.

• Jasmin Blanchette

  2020-06-03 11:31:18 (GMT)

  Ah.

• Jasmin Blanchette

  2020-06-03 11:31:59 (GMT)

  But I still don't understand your sentence that it has nothing to do with redundancy. Anyway.

• Alexander Bentkamp

  2020-06-03 11:32:45 (GMT)

  Ok, you're right, it's all connected to redundancy.

• Jasmin Blanchette

  2020-06-03 11:32:49 (GMT)

  You can explain it to me next time.

• Jasmin Blanchette

  2020-06-03 11:32:52 (GMT)

  OK. ;)

• Jasmin Blanchette

  2020-06-03 15:0:39 (GMT)

  Looks like I need $\models_0$ after all. Ah well. Maybe you need it too (for those intermediate models) and then we can use the same symbol, whichever it is.

• Alexander Bentkamp

  2020-06-03 15:4:15 (GMT)

  For the intermediate models, I would have been comfortable with using one symbol for both. But if you need it, it might be worth making the distinction throughout.