back to root

back to Matryoshka

Superposition with lambdas

• Jasmin Blanchette

  2020-04-09 15:15:52 (GMT)

  That metaquasiorder is quite a bitch!

• Jasmin Blanchette

  2020-04-09 15:15:55 (GMT)

  But I'm getting there.

• Jasmin Blanchette

  2020-04-09 15:26:16 (GMT)

  BTW the "Term Order" section is now starting to get quite long.

• Jasmin Blanchette

  2020-04-09 15:26:23 (GMT)

  I'm thinking we could split it into two.

• Jasmin Blanchette

  2020-04-09 15:26:58 (GMT)

  We keep the first few paras more or less where they are, but as part of "The Inference Rules".

• Jasmin Blanchette

  2020-04-09 15:27:32 (GMT)

  And then we move the "metaorders" to their own section, called "Term Order" or something, at the end of Section 3.

• Jasmin Blanchette

  2020-04-09 15:28:15 (GMT)

  The metaorders are fully optional but quite technical and will have four lemmas once I'm done + proofs.

• Jasmin Blanchette

  2020-04-09 15:48:33 (GMT)

  OK, I moved them. I'm much happier with where they are now.

• Jasmin Blanchette

  2020-04-09 15:49:28 (GMT)

  I called the subsection "A Term Order". @Sophie, we could even call it "A Generic Term Order". "Term Metaorder" probably sounds weird.

• Alexander Bentkamp

  2020-04-09 16:7:53 (GMT)

  I like Generic Term Order. I think it's more self-explanatory than meta order.

• Jasmin Blanchette

  2020-04-09 16:19:17 (GMT)

  I was bitching today about "generic" being almost meaningless (any order is generic in the sense that it's parameterized by a precedence, weights, etc.).

• Jasmin Blanchette

  2020-04-09 16:19:38 (GMT)

  A metaprover is a prover that builds on other provers.

• Jasmin Blanchette

  2020-04-09 16:19:45 (GMT)

  In that sence, metaorder is the best.

• Sophie

  2020-04-09 16:19:53 (GMT)

  cryptic humor... ^^

• Jasmin Blanchette

  2020-04-09 16:20:6 (GMT)

  It's the best, but only to me in my head. ;)

• Jasmin Blanchette

  2020-04-09 16:20:17 (GMT)

  Where's the humor?

• Jasmin Blanchette

  2020-04-09 16:20:41 (GMT)

  And a "meta-term-order", there's just no way to put the spaces and the hyphens at the right place.

• Jasmin Blanchette

  2020-04-09 16:21:1 (GMT)

  I think some US publications would write "meta--term order".

• Jasmin Blanchette

  2020-04-09 16:21:7 (GMT)

  Like "pre--World War II".

• Jasmin Blanchette

  2020-04-09 16:21:24 (GMT)

  But that looks weird.

• Jasmin Blanchette

  2020-04-09 16:22:1 (GMT)

  Anyway, I'm open to other suggestions that make it clear perhaps that the parameter is a KBO or LPO or EPO, not just some precedence or weights.

• Jasmin Blanchette

  2020-04-09 16:22:16 (GMT)

  Like "An Encoding-Based Term Order"

• Jasmin Blanchette

  2020-04-09 16:24:14 (GMT)

  (I'm procrastinating -- I'm really not good at paper proofs. :S)

• Jasmin Blanchette

  2020-04-09 16:27:57 (GMT)

  (Maybe if I can extend Alex's contract by one day, he could help me out? ;))

• Jasmin Blanchette

  2020-04-09 16:28:33 (GMT)

  Yeah, I like "encoding-based".

• Jasmin Blanchette

  2020-04-09 16:28:42 (GMT)

  It's a fitting heading for 2-3 pages of heavy encodings.

• Jasmin Blanchette

  2020-04-09 16:32:26 (GMT)

  @Alexander Bentkamp : I think the proof of what is now Lemma 12 (lem:lsucc-preserves-lfsucc-stability-under-ground-subst) could be improved.

• Jasmin Blanchette

  2020-04-09 16:32:43 (GMT)

  The $\rho$ construction only takes into account some term $t$.

• Jasmin Blanchette

  2020-04-09 16:33:9 (GMT)

  But later you invoke $\rho$ in the presence of two terms, called $t, s$, and it's not clear who is $t$ and why $s$ is ignored.

• Jasmin Blanchette

  2020-04-09 16:34:7 (GMT)

  In practice, I know $s$ wouldn't contain variables $t$ doesn't have, but we still need to be (1) more explicit about the $\rho$ construction (which term is passed as $t$) and (2) argue "axiomaticaly" about any such property.

• Jasmin Blanchette

  2020-04-09 16:34:32 (GMT)

  Or, probably better, change the $\rho$ construction to take both $s$ and $t$ into consideration.

• Jasmin Blanchette

  2020-04-09 16:34:42 (GMT)

  Or eliminate the dependency on $t$ altogether.

• Jasmin Blanchette

  2020-04-09 16:34:59 (GMT)

  The reason why I'm looking is that I need to do something similar for Lemma 14.

• Jasmin Blanchette

  2020-04-09 16:35:31 (GMT)

  I'll try to eliminate the dependency.

• Jasmin Blanchette

  2020-04-09 16:36:16 (GMT)

  Hm, now I see why that doesn't work.

• Alexander Bentkamp

  2020-04-09 17:23:39 (GMT)

  It's all because substitutions only map only finitely many variables and are the identity on all others. Why does it have to like this?

• Alexander Bentkamp

  2020-04-09 17:23:58 (GMT)

  But your current solution looks ok.

• Jasmin Blanchette

  2020-04-09 17:26:11 (GMT)

  There's no deep reason.

• Jasmin Blanchette

  2020-04-09 17:26:13 (GMT)

  Tradition.

• Jasmin Blanchette

  2020-04-09 17:26:33 (GMT)

  In fact, in some papers I say "screw everybody; our substitutions may have infnite domain".

• Jasmin Blanchette

  2020-04-09 17:26:38 (GMT)

  In other words.

• Jasmin Blanchette

  2020-04-09 17:27:25 (GMT)

  Being able to write any substitution out as $\{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\}$ isn't something we really use...

• Jasmin Blanchette

  2020-04-09 17:27:46 (GMT)

  We could change that.

• Jasmin Blanchette

  2020-04-09 17:30:26 (GMT)

  Actually, wait a sec.

• Jasmin Blanchette

  2020-04-09 17:30:39 (GMT)

  There is one good reason to keep substitutions finite.

• Jasmin Blanchette

  2020-04-09 17:30:49 (GMT)

  I think.

• Jasmin Blanchette

  2020-04-09 17:30:59 (GMT)

  We need to generate fresh variable names sometimes.

• Jasmin Blanchette

  2020-04-09 17:31:4 (GMT)

  E.g. in the CSU business.

• Jasmin Blanchette

  2020-04-09 17:31:12 (GMT)

  Much of it is implicit.

• Jasmin Blanchette

  2020-04-09 17:31:32 (GMT)

  But if substitutions are infinite, this gives us no leway.

• Jasmin Blanchette

  2020-04-09 17:31:54 (GMT)

  That's why also nominal logic (for binders) requires binding syntax to be finitary, but the set of variables to be infinite.

• Jasmin Blanchette

  2020-04-09 17:32:24 (GMT)

  (I don't think we mention that \mathcal{V} must be infinite because that's a very boring detail but in fact it probably needs to. Maybe I'll add it.)

• Jasmin Blanchette

  2020-04-09 17:32:39 (GMT)

  So it's all about finite vs. infinite, which gives us an infinite set of fresh names.

• Jasmin Blanchette

  2020-04-09 17:33:17 (GMT)

  But as Andrei Popescu observed, it doesn't need to stop there. One could have countably infinite vs. uncountably infinite. And that's useful sometimes.

• Jasmin Blanchette

  2020-04-09 17:33:32 (GMT)

  Anyway, all of this to say: Let's keep the current def of substitution.

• Jasmin Blanchette

  2020-04-10 17:10:32 (GMT)

  I'm done with the derived quasiorder (formerly known as "meta-quasiorder"). See second half of Section 3.5.

  @Alexander Bentkamp: I'd feel safer if you could go over the definition and proof.

• Jasmin Blanchette

  2020-04-10 18:11:27 (GMT)

  @Petar Vukmirovic let me know once you're ready to discuss the implementation.

• Alexander Bentkamp

  2020-04-10 19:6:57 (GMT)

  Looks good! Condition (*) could be misread as applying the typing condition to both (1) and (2). Maybe swap (1) and (2)?

• Jasmin Blanchette

  2020-04-10 19:32:2 (GMT)

  I'd done that already. ;)

• Jasmin Blanchette

  2020-04-10 19:32:56 (GMT)

  Just pull.

• Alexander Bentkamp

  2020-04-10 21:50:37 (GMT)

  Couldn't this quasi order be defined in a simpler way, roughly like this:

  $t \succsim_\lambda s$ iff

  • $t \succeq_\lambda s$ or
  • $t = x \bar u$ and $s = x \bar v$ and $u_i \succsim_\lambda \bar v_i$ and $u_i$ and $v_i$ are non-functional for all $i$
  • $t = \mathsf{f} \bar u$ and $s = \mathsf{f} \bar v$ and $u_i \succsim_\lambda \bar v_i$ for all $i$
  • [Insert case for lambdas here]

  I don't know exactly this could be made to work, but it would be much more intuitive. Have you tried something like this?

• Jasmin Blanchette

  2020-04-11 5:29:35 (GMT)

  That's true. What I like about the current approach is the symmetry with non-quasi.

• Jasmin Blanchette

  2020-04-11 5:30:0 (GMT)

  E.g. I can (if necessary) say things like $O_t(s) = O(s)$ if $s$ contains no applied var.

• Jasmin Blanchette

  2020-04-11 5:30:8 (GMT)

  And exploit this in the proof.

• Jasmin Blanchette

  2020-04-11 5:30:25 (GMT)

  But it turns out now that I'm done with the proofs, I didn't need that.

• Jasmin Blanchette

  2020-04-11 5:34:30 (GMT)

  But still, if you look at the proof of the one lemma about the quasi order, that would need to change to rule induction.

• Jasmin Blanchette

  2020-04-11 5:34:46 (GMT)

  I guess that would work nicely.

• Jasmin Blanchette

  2020-04-11 5:35:14 (GMT)

  Today I work with all mismatches emerging from all applied variables in one swoop, "flattened".

• Jasmin Blanchette

  2020-04-11 5:35:34 (GMT)

  With rule induction, one would have only one variable at a time.

• Jasmin Blanchette

  2020-04-11 5:35:53 (GMT)

  I can do it on Tuesday.

• Jasmin Blanchette

  2020-04-11 5:37:3 (GMT)

  Actually, you forgot the B encoding above.

• Jasmin Blanchette

  2020-04-11 5:37:35 (GMT)

  The second case shouldn't kick in if x is bound.

• Jasmin Blanchette

  2020-04-11 6:33:30 (GMT)

  ---

  I think I know what to do about the bound variables.

• Jasmin Blanchette

  2020-04-11 6:34:11 (GMT)

  We replace $\mathcal{B}(t)$ by $\mathcal{B}_x(t)$, which renames only one var $x$ at a time.

• Jasmin Blanchette

  2020-04-11 6:34:45 (GMT)

  When we see $\lambda x. t$ we call it.

• Jasmin Blanchette

  2020-04-11 6:34:56 (GMT)

  That works both for the order and the quasiorder.

• Jasmin Blanchette

  2020-04-11 6:35:29 (GMT)

  For the order, it gets rid of one translation ($\mathcal{O}$ and $\mathcal{Z}$ get merged).

• Jasmin Blanchette

  2020-04-11 6:35:58 (GMT)

  And no more $\mathcal{B}^{-1}(y)$ to find out if it was fluid.

• Jasmin Blanchette

  2020-04-11 6:36:9 (GMT)

  (Which I avoid today by "abusing notation".)

• Jasmin Blanchette

  2020-04-11 6:36:33 (GMT)

  For the quasiorder, it makes your definition above work.

• Jasmin Blanchette

  2020-04-11 6:37:14 (GMT)

  We should have done that all along. The idea of "freezing" bound variables as you enter $\lambda$'s is quite standard.

• Jasmin Blanchette

  2020-04-11 7:22:2 (GMT)

  ACTUALLY, Alex, your def is weaker than mine.

• Jasmin Blanchette

  2020-04-11 7:23:14 (GMT)

  Cex: $g \> (Y \> b) \> d \> c$ vs. $g \> (Y \> a) \> c \> d$.

• Jasmin Blanchette

  2020-04-11 7:23:40 (GMT)

  With, say KBO.

• Jasmin Blanchette

  2020-04-11 7:24:27 (GMT)

  You couldn't apply your third rule, because either $c \geq d$ or $d \geq c$, but not both.

• Alexander Bentkamp

  2020-04-11 10:4:29 (GMT)

  I think there are other examples where mine is stronger than yours:
  $g\>d\>(Y\>b)\>(Y\>a)$ vs. $g\>c\>(Y\>a)\>(Y\>b)$ with KBO, all weights 1, left-to-right length-lex
  Mine would handle this by the first rule because $g\>d\>(Z_{Y\>b})\>(Z_{Y\>a}) \succeq_{\lambda f} g\>c\>(Z_{Y\>a})\>(Z_{Y\>b})$
  But yours would attempt $g\>d\>(Z_{Y\>b})\>(Z_{Y\>a}) \not\succeq_{\lambda f} g\>c\>(Z_{Y\>b})\>(Z_{Y\>b})$

• Alexander Bentkamp

  2020-04-11 10:44:12 (GMT)

  Maybe we should let @Petar Vukmirovic decide which one can be implemented more efficiently...

• Jasmin Blanchette

  2020-04-11 13:18:28 (GMT)

  Yep, I thought about the same one while cleaning.

• Jasmin Blanchette

  2020-04-11 13:19:12 (GMT)

  And a big bug

• Jasmin Blanchette

  2020-04-11 13:19:17 (GMT)

  green -> orange!

• Jasmin Blanchette

  2020-04-11 13:19:55 (GMT)

  for the impl, no metaorder

• Jasmin Blanchette

  2020-04-11 13:20:2 (GMT)

  I know what to do for KBO and RPO.

• Jasmin Blanchette

  2020-04-11 13:20:13 (GMT)

  Maybe the metaquasi was a bad idea.

• Jasmin Blanchette

  2020-04-11 13:21:0 (GMT)

  the problem with mine is that it's just a heuristic

• Jasmin Blanchette

  2020-04-11 13:21:9 (GMT)

  which vars to change which not to change.

• Jasmin Blanchette

  2020-04-11 13:21:36 (GMT)

  i'll explain on tuesday how to do KBO

• Jasmin Blanchette

  2020-04-11 15:56:22 (GMT)

  Jasmin Blanchette said:

  And a big bug

  Actually no bug. Got confused. ;)

• Jasmin Blanchette

  2020-04-11 15:56:41 (GMT)

  I think we should go with your solution in JAR paper.

• Jasmin Blanchette

  2020-04-11 15:57:11 (GMT)

  And perhaps write a workshop/conf paper "Term Orders for Lambda-Superposition", maybe Petar et al.

• Jasmin Blanchette

  2020-04-11 15:57:30 (GMT)

  With the quasiorders for KBO etc. spelled out and proved correct.

• Jasmin Blanchette

  2020-04-11 15:58:21 (GMT)

  And also the currently impl. orders (which combine encoding and KBO etc.).

• Petar Vukmirovic

  2020-04-11 17:40:26 (GMT)

  I will carefully read what Jasmin wrote this week (unfortunately, have some other stuff to work on at the beginning of the week) and get back to you

• Alexander Bentkamp

  2020-04-11 17:56:57 (GMT)

  There is no hurry I think. The JAR reviewer's need to get back to us first before we have to deliver anything.

• Petar Vukmirovic

  2020-04-11 18:1:6 (GMT)

  I am also interested in making the order tighter :slight_smile:

• Petar Vukmirovic

  2020-04-11 18:1:19 (GMT)

  Today I implemented new precedence generation schemes for RPO and selection functions

• Jasmin Blanchette

  2020-04-11 19:13:43 (GMT)

  Actually, Petar, don't read anything yet.

• Jasmin Blanchette

  2020-04-11 19:13:50 (GMT)

  It's going to change.

• Jasmin Blanchette

  2020-04-11 19:42:57 (GMT)

  BTW the reason I write "quasiorder" is because for a type $\kappa$ with only one ground term $c$, we can have $x \succsim c$ and $c \succsim x$.

• Jasmin Blanchette

  2020-04-11 19:44:40 (GMT)

  But we don't need reflexivity and transitivity any more than we need antisymmetry, so I'm going to rename it a "relation" instead.

• Petar Vukmirovic

  2020-04-13 8:30:49 (GMT)

  Ok Let me know when I can read it :slight_smile:

• Jasmin Blanchette

  2020-04-14 10:33:35 (GMT)

  I talked with Alex this morning and we discussed a few options regarding $\succsim$.

• Jasmin Blanchette

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

  None of the two options we discussed was fully satisfactory, and I had come to the conclusion that the best way to implement $\succsim$ is in an ad hoc fashion for each term order. Any generic approach is bound to have some undesirable imprecisions or be unpractical and not suggest an implementation. So I took out what I did on Friday.

• Jasmin Blanchette

  2020-04-14 10:38:16 (GMT)

  Instead, I propose to collect our ideas in a separate document, which might evolve and become a workshop or conference paper of its own, and/or a section or chapter in Petar's thesis: "Term Orders for Lambda-Superposition" or something like that.

• Jasmin Blanchette

  2020-04-14 10:46:46 (GMT)

  This should include the lambda KBO (and LPO and EPO?) as implemented in Zipperposition and the future nonstrict counterparts (formerly known as "quasiorders"). Also, we could prove once and for all compatibility with orange contexts, which could be used in the JAR submission to optimize $\lambda$-DemodExt to remove one of the $\succ$ checks.

• Jasmin Blanchette

  2020-04-14 10:47:11 (GMT)

  And Petar is working on heuristics to generate orders, some of which behave interestingly w.r.t. lambdas and bound variables.

• Jasmin Blanchette

  2020-04-14 10:58:18 (GMT)

  I have tentatively created a document in "papers/lam_orders" in the Matryoshka repository, tentatively with Petar, Alex, and me as authors. The topic isn't hypersexy, but it would be nice to have these things written down and (for the nonstrict orders and heuristics) implemented.

• Jasmin Blanchette

  2020-04-14 10:58:44 (GMT)

  If you're interested to contribute, just let me know.

• Jasmin Blanchette

  2020-04-17 10:34:10 (GMT)

  @Alexander Bentkamp Concerning the intersection of subsumption and formula size, Uwe pointed out that this can in general be problematic for infinite signatures.

• Jasmin Blanchette

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

  But the only counterexample he has is with constraint superposition.

• Jasmin Blanchette

  2020-04-17 10:35:9 (GMT)

  I think we're safe but ideally we should convince ourselves that the intersection of these two non-wf relations is actually wf.

• Jasmin Blanchette

  2020-04-17 10:35:35 (GMT)

  Or we just state that our signature is finite (which is not so nice, e.g. once you have rules that introduce skolems).

• Alexander Bentkamp

  2020-04-17 11:12:12 (GMT)

  So why is it problematic with infinite signatures?

• Jasmin Blanchette

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

  There's no concrete counterexample, but with an infinite signature $\leq$ is no longer well founded.

• Jasmin Blanchette

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

  OK, well, it never is.

• Jasmin Blanchette

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

  Let me rephrase: There's a counterexample for our order using constraints.

• Jasmin Blanchette

  2020-04-17 11:30:18 (GMT)

  But we don't have constraints. Yet, our order is not obviously well founded just by looking at it.

• Jasmin Blanchette

  2020-04-17 11:30:24 (GMT)

  Hence we must prove it well founded.

• Jasmin Blanchette

  2020-04-17 11:30:58 (GMT)

  One easy way, I think: We say that variables have size 0 and all constants have size 1.

• Jasmin Blanchette

  2020-04-17 11:31:14 (GMT)

  Then p(x) is smaller than p(a), syntactically.

• Jasmin Blanchette

  2020-04-17 11:32:4 (GMT)

  And we can define $\sqsupset$ as the intersection of subsumption and syntactic size (with size of var = 0).

• Jasmin Blanchette

  2020-04-17 11:32:44 (GMT)

  Strict subsumption and strict syntactic size.

• Alexander Bentkamp

  2020-04-17 11:33:26 (GMT)

  So you want to redefine $\sqsupset$?

• Jasmin Blanchette

  2020-04-17 11:33:52 (GMT)

  Yes. It would have no impact in practice -- I think it's the same order mathematically, just a different characterization.

• Jasmin Blanchette

  2020-04-17 11:34:26 (GMT)

  Or maybe there are some odd formulas where it would make a difference.

• Jasmin Blanchette

  2020-04-17 11:34:49 (GMT)

  E.g. one that combines applied variables and the $p(x)$ kind of stuff.

• Jasmin Blanchette

  2020-04-17 11:35:6 (GMT)

  Alternative, we keep the current definition but we prove it well founded.

• Alexander Bentkamp

  2020-04-17 11:35:25 (GMT)

  Yeah, I think it's not too hard. Here is how I would start:

• Jasmin Blanchette

  2020-04-17 11:35:37 (GMT)

  Here's Uwe's counterexample, for reference:

  The construction of the tiebreaker ordering \sqsupset using
  subsumption and size is not guaranteed to give a well-founded ordering.
  For finite signatures, it works, but for infinite signatures, say,
  with constants a0 < a1 < a2 < ..., each of the constrained clauses
  
   p(x) [[ x > a0 ]]
   p(x) [[ x > a1 ]]
   p(x) [[ x > a2 ]]
   ...
  
  is properly subsumed by the next one, and the size is the same.
  

• Alexander Bentkamp

  2020-04-17 11:35:37 (GMT)

  Let's assume there is an infinite $\sqsupset$-chain. The size of the clauses is equal or decreases with each step in the chain. Clearly, there can be only finitely many decreasing steps. So at some point the size stays the same forever. Similarly, the number of literals can not increase because that would contradict subsumption. It can also not decrease forever. So at some point, the number of literals must be constant. From this point on, each clause must be a proper instance of the previous one, while the size is constant.

• Jasmin Blanchette

  2020-04-17 11:37:7 (GMT)

  Sounds reasonable. :)

• Alexander Bentkamp

  2020-04-17 11:37:35 (GMT)

  The last sentence sounds like it can't be true, but I can't quite argue why

• Jasmin Blanchette

  2020-04-17 11:38:7 (GMT)

  Well the rest from there is like in FOL. I've proved something like this in Isabelle before.

• Alexander Bentkamp

  2020-04-17 11:38:28 (GMT)

  I am worried about the applied vars though

• Jasmin Blanchette

  2020-04-17 11:38:55 (GMT)

  I realize now that my proposal would handle some weird cases better, on paper.

• Jasmin Blanchette

  2020-04-17 11:39:55 (GMT)

  E.g. X a is bigger but more general than X, but it would be compensated elsewhere by an X which is smaller but more general than a.

• Jasmin Blanchette

  2020-04-17 11:40:31 (GMT)

  Of course we wouldn't bother implementing this, but this speaks in favor of defining $\sqsupset$ the way I'm now proposing (which is, really, the way Uwe suggested all along).

• Jasmin Blanchette

  2020-04-17 11:42:12 (GMT)

  Uwe now proposes this:

  There's one size-based ordering that handles most of the relevant cases,
  namely
  
   C \sqsupset C'
  
   if   C \issubsumedtilde C'
        and (size(C) > size(C')
             or (size(C) = size(C')
                 and C contains fewer distinct variables than C'))
  

• Alexander Bentkamp

  2020-04-17 11:44:2 (GMT)

  Okay, that's different from what you said earlier.

• Jasmin Blanchette

  2020-04-17 11:44:18 (GMT)

  Well Uwe sent the email 1 minute ago!

• Alexander Bentkamp

  2020-04-17 11:44:27 (GMT)

  Ok, I see :-)

• Jasmin Blanchette

  2020-04-17 11:44:50 (GMT)

  The previous proposal is a combination of Uwe's general approach (take the intersection of subsumption and some other well-founded size-based order)

• Jasmin Blanchette

  2020-04-17 11:45:0 (GMT)

  and my idea of giving weight 0 to vars.

• Jasmin Blanchette

  2020-04-17 11:45:27 (GMT)

  The current Uwe proposal is to be less hackish (and perhaps slightly less precise in weird hybrid cases).

• Jasmin Blanchette

  2020-04-17 11:45:45 (GMT)

  We'll probably put it in the report of the saturation paper.

• Alexander Bentkamp

  2020-04-17 11:46:30 (GMT)

  This can also handle f (X F F) ≈ c ⊐ f (Y G) ≈ c, which the vars=0-idea cannot.

• Jasmin Blanchette

  2020-04-17 11:46:32 (GMT)

  (This whole discussion started because Uwe found a cex to "your" order which I had moved to the saturation paper where it was perceived as the ultimate solution to everybody's problems, including people who care about constraints.)

• Jasmin Blanchette

  2020-04-17 11:46:43 (GMT)

  Even better then. ;)

• Jasmin Blanchette

  2020-04-17 11:47:18 (GMT)

  But then I would strike back by shifting everything by $\omega$.

• Jasmin Blanchette

  2020-04-17 11:47:39 (GMT)

  I.e. constants have size $\omega$, variables have size 1. ;)

• Alexander Bentkamp

  2020-04-17 11:47:47 (GMT)

  Hehe, ok :-)

• Jasmin Blanchette

  2020-04-17 11:47:52 (GMT)

  Ordinals are wf. :)

• Jasmin Blanchette

  2020-04-17 11:48:14 (GMT)

  Shall we go for Uwe's last proposal?

• Alexander Bentkamp

  2020-04-17 11:48:47 (GMT)

  Yes, please no ordinals!

• Jasmin Blanchette

  2020-04-17 11:49:13 (GMT)

  The ordinals were just a strawman to get you to accept Uwe's proposal. ;)

• Jasmin Blanchette

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

  You see, that's how I manipulate people. ;)

• Jasmin Blanchette

  2020-04-17 11:49:45 (GMT)

  Now go forth and do likewise!

• Alexander Bentkamp

  2020-04-17 11:50:10 (GMT)

  You shouldn't always give away your tricks. I will not fall for this again...

• Jasmin Blanchette

  2020-04-17 11:50:34 (GMT)

  I'll implement it.

• Jasmin Blanchette

  2020-04-17 11:50:44 (GMT)

  Feel free to keep an eye on my commit.

• Jasmin Blanchette

  2020-04-17 12:0:3 (GMT)

  Done. But the diff looks messy -- my editor decided it didn't like Windows-style CRLF and changed these to Unix-style LF.