2020-11-06 8:19:57 (GMT)
Jasmin Blanchette said:
I'd propose to vote and suggest the winner to the broader community, first informally asking the people who use the word the most (e.g. Konstantin, Uwe), then perhaps in the AAR newsletter?
The next AAR newsletter should appear sometime in December (likely after mid-december), and I am pretty sure such a column would be welcome in it. :wink:
2020-11-06 9:28:53 (GMT)
Well you suggested "stray", so I think it would be most appropriate if you wrote a short column about it, don't you think? ;)
2020-11-06 9:29:9 (GMT)
(I'm also teaching this period and trying to avoid taking on any further commitments.)
2020-11-10 8:34:8 (GMT)
I don't buy into the "you suggested "stray"" argument, (after all, if we want to play that game, there are other metrics, e.g., @Alexander Bentkamp was the one who started the whole thing with the comment
Alexander Bentkamp said:
Maybe our chance to give it a new name?
).
That being said, there has not been an editor's column in a while, so I can try to do it (I can't promise it will be ready for the next newsletter but there is no rush anyway, it's not like real orphans are being deleted when we use this terminology), but I would need a bit of help regarding the groundwork of identifying the main users of orphan deletion and getting their opinions on the topic. The ones already mentioned are:
2020-11-10 10:52:12 (GMT)
I'm not sure if Vampire does any orphan deletion, but you could ask Giles & Ahmed. A quick search on Google Scholar also reveals Guillaume Burel among the users of the phrase "orphan elimination".
2020-11-12 12:17:9 (GMT)
I had a short discussion with Uwe today where I mentioned the idea of replacing orphans with strays. He is not overly enthusiastic about the proposal (@Uwe Waldmann and now you know which thread to look at if you want to discuss this topic further).
2020-11-12 12:30:32 (GMT)
@Stephan Schulz: This zulip thread of discussion is mostly about how we could rename "orphan deletion" into something with a less negative connotation. Since you are one of the people most concerned by this technique, don't hesitate to share your opinion about it.
In particular, it would be great to know if you would be willing to adopt a new terminology in your future work, and if yes, under what requirements.
2020-11-12 12:34:19 (GMT)
@Uwe Waldmann : I believe it would be nice to also have your answers on the same question I asked Stephan. From our earlier discussion, I understood that you would prefer to keep the term "orphan" rather than something like "stray" because the latter doesn't fit with the parent-child terminology used for inferences. Is that correct?
2020-11-12 12:41:17 (GMT)
The parent-child terminology is completely broken. A parentless clause (resulting from a nullary inference) is not an orphan, but a clause from a binary inference with a single parent is. This confuses people and leads them to want to add sentences saying that orphan deletion doesn't apply to nullary inferences.
2020-11-12 12:41:56 (GMT)
Plus, it's completely non-PC.
2020-11-12 12:42:8 (GMT)
PC?
2020-11-12 12:42:16 (GMT)
politically correct
2020-11-12 12:42:46 (GMT)
2020-11-12 12:43:56 (GMT)
Thanks!
2020-11-12 12:57:43 (GMT)
Well, IIRC, historically this came from Waldmeister, in the much less PC "Waisenmord", or "orphan murder". In German, "Waise" (Orphan) can refer to both "Halbwaise" (half-orphan) and "Vollweise" (full orphan). That usage is, indeed, not unknown in English, but it's not the most common usage.
I don't see a PC problem, though. Parent-child relations are extremely common in computer science. I can see a point in avoiding master-slave terminology, but I see none in avoiding parent-child.
2020-11-12 12:59:21 (GMT)
An orphan is someone who has lost one or more parents. Adam was not an orphan. And that is exactly what the orphan notion in saturation reflects - if one parent is gone, the child can (modulo some thinking) go as well.
2020-11-12 13:3:58 (GMT)
Stephan: "Orphan deletion" is my problem.
2020-11-12 13:4:10 (GMT)
Or, more common, "orphan elimination".
2020-11-12 13:4:10 (GMT)
2020-11-12 13:6:38 (GMT)
Also, Stephan, see my argument about "orphan" != "half-orphan" upstairs.
2020-11-12 13:14:16 (GMT)
Yes, I saw that. "However, the United Nations Children's Fund (UNICEF), Joint United Nations Programme on HIV and AIDS (UNAIDS), and other groups label any child who has lost one parent as an orphan." (https://en.wikipedia.org/wiki/Orphan). It's not the most common usage, but it's not unheard of, either.
2020-11-12 13:15:8 (GMT)
If you want to avoid the "orphan=children" connotation, why not go for "orphan clause elimination" - that makes it into an adjective, and makes clear that we are talking about clauses.
2020-11-12 13:23:51 (GMT)
"Orphan clause" solves the PC problem, which is the most immediate one.
2020-11-12 13:24:7 (GMT)
It doesn't solve the half-orphan but maybe that's too late for that.
2020-11-12 15:3:27 (GMT)
Note that "stray" also doesn't solve the half-orphan problem. I would even say that it makes it worse.
2020-11-12 15:5:52 (GMT)
The metaphor could be cats:
2020-11-12 15:25:9 (GMT)
@Sophie Tourret Why does it make it worse? These clauses are kind of "lost".
2020-11-12 15:25:28 (GMT)
but they have not lost all of their premises.
2020-11-12 15:25:43 (GMT)
Nothing in "stray" talks about parents or premises.
2020-11-12 15:26:6 (GMT)
"not in the right place; separated from the group or target"
2020-11-12 15:26:27 (GMT)
(about animals) "having no home or having wandered away from home"
2020-11-12 15:26:50 (GMT)
So "stray" would simply refer to the fact that the inference that produced them is no longer valid.
2020-11-12 15:28:45 (GMT)
By the way, I also contacted Konstantin (he said he would take a look) and (just now) Guillaume.
2020-11-12 17:46:51 (GMT)
In general, I think there is quite some value in stare decisis with respect to terminology, or, if you feel you have to address the PC problem, to keep the change as small and gradual as possible. There is more than one possible cause for confusion, and changing terminology is definitely one of them. Just consider "subsumption resolution" vs. "clause simplification" vs. "contextual literal cutting".
2020-11-12 17:51:56 (GMT)
Stephan Schulz said:
In general, I think there is quite some value in stare decisis with respect to terminology, or, if you feel you have to address the PC problem, to keep the change as small and gradual as possible. There is more than one possible cause for confusion, and changing terminology is definitely one of them. Just consider "subsumption resolution" vs. "clause simplification" vs. "contextual literal cutting".
If I may interfere I both agree and disagree on this very good example. Just today I had discussion with someone from SAT world in which I discussed CLC which is called SR in their world.
I do agree that having 3 names is horrible, but changing the name in one of the communities to unify is probably good.
This brings me to the question: Do other communities have "orphan deletion" concept? If so, if we unify with them this will probably reduce confusion introduced with the new name
2020-11-12 19:1:54 (GMT)
@Stephan Schulz Sure, the multiplication of terminology hs to be combatted, but there are ample precedents for swift renamings, e.g. from the unfortunate GRID (gay-related immune deficiency) in the early 1980s to AIDS.
2020-11-12 19:2:35 (GMT)
I think "subsumption resolution" is actually nicer, we should all move to it :p
2020-11-12 20:29:19 (GMT)
Sophie notified me that killing orphans is considered to be not very nice any more...
Personally I'm ok with the current terminology, brings some attention from outside ;) children are quite standard, why not orphans. I guess, term comes from "orphan process" but usually processes have a single parent.
Might be we should call it zombie clause ;) at least killing zombies should be still be PC ;) although the connotation with zombie processes will be skewed.
If you are really looking for a change to a neutral (aka boring) term, as a suggestion: "detached clause".
2020-11-13 17:7:30 (GMT)
I am following Konstantin's terminology in my papers, so I can change and use whatever the consensus will make emerge.
That being said, I am not sure that being PC is a good reason for a change in that case. But the fact that such clauses are only half-orphans is a good one.
I am not sure about stray. I suggest "amputated clause", but it would not be PC to "eliminate amputees" neither.
2020-11-16 13:42:27 (GMT)
I am quite generally opposed to the idea of changing notations. (I have written too many footnotes explaining that "redundancy was called compositeness in BG-JLC-1994, and that redundancy meant something else in BG-JLC-1994"). I'm even more opposed to changing established notations. It's just annoying for future generations of scientists, who find a term in paper A, google it, and don't find paper B because the authors of paper B decided to call the concept differently. If the name was "orphan killing" or "orphan murder", yes, I'd call that offensive, but I don't have any problems with "orphan deletion". If you're really unhappy with it, I'd suggest "orphan(ed) clause deletion".
2020-11-16 15:12:9 (GMT)
I'm also siding with "orphan(ed) clause deletion". The background for all of this is when Sophie and I wrote
https://matryoshka-project.github.io/pubs/satur_isa_paper.pdf
for an ITP audience. I'd be happy to change "a technique with the unfortunate name of 'orphan deletion' " to "a technique called 'orphaned formula deletion' ".
2020-11-16 17:55:11 (GMT)
Or even better, kill "a technique called". ;)