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 to mean just entailment w.r.t. 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.
2020-06-02 15:45:47 (GMT)
For the moment, I'll write or something.
2020-06-02 15:50:25 (GMT)
Yes, Booleans will be built into all consequence relations. is ok with me.
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.
2020-06-02 16:12:57 (GMT)
Makes sense. Right now I'm writing .
2020-06-02 16:13:13 (GMT)
would be yet another option.
2020-06-02 16:45:35 (GMT)
euf au plat?
2020-06-02 16:45:52 (GMT)
maybe I'm too hungry...
2020-06-02 19:14:23 (GMT)
Equality with uninterpreted functions.
2020-06-02 19:14:39 (GMT)
Never read EUF as OEUF before. ;)
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 for "with Booleans" too confusing. Traditionally, one puts theories as a subscript to . Maybe or something. ( = Booleans, kind of standard.)
2020-06-02 19:18:27 (GMT)
"Obviously, Equality with Uninterpreted Functions"
2020-06-02 19:19:33 (GMT)
Omogeneous Equality with UF. As opposed to heterogeneous equality (e.g., == in Lean).
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.
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 for "with Booleans" too confusing. Traditionally, one puts theories as a subscript to . Maybe or something. ( = Booleans, kind of standard.)
That's true. We should distinguish two different kinds of entailment I think. @Sophie @Visa
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.
2020-06-02 19:39:1 (GMT)
Right -- I presume the 's interpret Booleans correctly only in terms smaller than or something.
2020-06-02 19:42:24 (GMT)
, do not interpret Booleans correctly at all. only for terms smaller than . Only and interpret all Boolean terms correctly.
2020-06-02 19:43:58 (GMT)
I see. ;)
2020-06-02 19:44:0 (GMT)
But your intuition is right. roughly corresponds to what is in the standard completeness proof.
2020-06-02 19:44:47 (GMT)
My intuition is always right. It's just the execution that's often wrong... like last week. ;)
2020-06-02 19:46:34 (GMT)
But to go back to my initial question: Is it so that (the ultimate) falsifies, using only rewrite rules, all the subclauses of productive clauses, or is the construction more complicated?
2020-06-02 19:47:6 (GMT)
In the latter case, I guess a Skype call might be useful tomorrow (Wed).
2020-06-02 19:50:51 (GMT)
Yes, that's what Lemma 12 says.
2020-06-02 19:51:52 (GMT)
Thanks. I already have 5 calls scheduled for tomorrow; no need for a 6th one. ;)
2020-06-02 19:52:7 (GMT)
(Maybe 6 actually...)
2020-06-02 19:53:27 (GMT)
I realize now that the symbol in Lemma 12 is not entailment, but rather "This interpretation is a model of that clause". So there is no difference between and .
2020-06-03 6:13:28 (GMT)
There's still a subtle difference. It is reasonable to read as meaning what you said plus is a Boolean-standard interpretation. Just like somewhat implicitly implies that interprets equality as a congruence (otherwise the expression is "ill-typed"). I would be very grateful if you could reserve the plain symbols, whether for entailment or for the models relation, for the plain EUF concepts.
2020-06-03 10:50:9 (GMT)
Regardless of notations, am I guessing right that won't hold?
2020-06-03 10:53:24 (GMT)
I presume you are talking about the FOL layer? Then it would rather be . And indeed it does not hold.
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 or , and the answer is the same.
2020-06-03 11:12:34 (GMT)
Coming back to the notation, I don't think I need 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 , just like , is not argument-congruent.
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 and .)
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 or , and the answer is the same.
Now I am confused. In the redundancy criterion, there is only one reference to , which is the one on the FOL layer.
The consequence relation 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.
2020-06-03 11:22:34 (GMT)
Jasmin Blanchette said:
Coming back to the notation, I don't think I need after all.
That's great. We have enough entailments relations already :-)
2020-06-03 11:28:37 (GMT)
By I meant the lifting one gets by the saturation framework. iff . The redundancy criterion might not textually use the symbol , but it's still the same lifting. Do you use the same symbol () for something else? How can it do HO reasoning if it's obtained by a grounding (as suggested by the notation?).
2020-06-03 11:30:59 (GMT)
It's just grounding and not flooring.
2020-06-03 11:31:18 (GMT)
Ah.
2020-06-03 11:31:59 (GMT)
But I still don't understand your sentence that it has nothing to do with redundancy. Anyway.
2020-06-03 11:32:45 (GMT)
Ok, you're right, it's all connected to redundancy.
2020-06-03 11:32:49 (GMT)
You can explain it to me next time.
2020-06-03 11:32:52 (GMT)
OK. ;)
2020-06-03 15:0:39 (GMT)
Looks like I need after all. Ah well. Maybe you need it too (for those intermediate models) and then we can use the same symbol, whichever it is.
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.