Email Gateway (Aug 22 2022 at 15:31): Email Gateway (Aug 22 2022 at 15:31):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I'm currently in the process of reorganising the library w.r.t. things
related to sublists.
We have a "prefix" and "suffix" predicate with the obvious definitions,
and we have something called "sublisteq" for "non-continuous sublists"
(i.e. sublisteq ''bd'' ''abcde'' holds).
I would now like to introduce a predicate for continuous sublists, i.e.
where ''bcd'' is a sublist of ''abcde'', but ''bd'' is not.
I struggled to find a good and concise name for this. Possible solutions
are:
– substring (reason: seems to be more or less standard name for this;
disadvantage: sounds like "string" as in "text string")
– infix (reason: Haskell has "isPrefixOf", "isSuffixOf", "isInfixOf";
disadvantage: seems to be very non-standard and not the usual meaning of
the word "infix")
Any opinions/other suggestions on this? I would also be open to call
this "sublist" and rename the current "sublist" to something else.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:31):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Manuel,
Any opinions/other suggestions on this? I would also be open to call
this "sublist" and rename the current "sublist" to something else.
I believe "sublist" and "substring" are implicitly contiguous in most people's mind (unless otherwise specified), whereas "subsequence" is possibly noncontiguous. I'm not saying there's anything very logical about any of this.
This would mean renaming "sublist" to "subseq" or "subsequence" and using "sublist" for what you describe would be the most standard terminology.
If people are somehow attached to the old "sublist" name, I would propose "contig_sublist" or, why not, "infix". Both are better than "substring", which sounds like the specialization of "sublist" to "char list", i.e. "string".
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 15:31):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
How about "segment"?
Email Gateway (Aug 22 2022 at 15:31):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think that sublist, subsequence and substring really have much of a bias
in either direction, except possibly substring, but the latter does indeed sound
too specialized. This does not mean we have to avoid sublist/seq, but just that
I don't believe there is a natural choice. But we could make one.
On 25/05/2017 14:03, Eugene W. Stark wrote:
How about "segment"?
I like it. It is unambiguous. Same as contig_sublist, but shorter.
In conversation Manuel actually suggested "fragment" as a possible name for the
current sublisteq. It would go nicely with "segment". Of course neither have
"list" in the name...
Tobias
On 05/25/2017 07:38 AM, Jasmin Blanchette wrote:
Hi Manuel,
Any opinions/other suggestions on this? I would also be open to call
this "sublist" and rename the current "sublist" to something else.I believe "sublist" and "substring" are implicitly contiguous in most people's mind (unless otherwise specified), whereas "subsequence" is possibly noncontiguous. I'm not saying there's anything very logical about any of this.
This would mean renaming "sublist" to "subseq" or "subsequence" and using "sublist" for what you describe would be the most standard terminology.
If people are somehow attached to the old "sublist" name, I would propose "contig_sublist" or, why not, "infix". Both are better than "substring", which sounds like the specialization of "sublist" to "char list", i.e. "string".
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 15:31):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Wikipedia has a clear bias (and I did not edit it, nor did I look it up before writing my previous email):
https://en.wikipedia.org/wiki/Subsequence
https://en.wikipedia.org/wiki/Substring
Popular algorithm sbooks like Cormen et al. follow the same definition of subsequence. Standard expressions like "longest increasing subsequence" depend on this semantics.
As for sublist, all the examples I see by Googling either "sublist", "is_sublist", "isSublist", or "indexOfSubList" in Java, Python, Scala, etc., have the contiguous semantics. Including this page:
http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html
I'm not saying we should rename the Isabelle concepts, just that Isabelle is the odd (wo)man out.
Jasmin
Email Gateway (Aug 22 2022 at 15:31):From: Manuel Eberl <eberlm@in.tum.de>
Personally, what Jasmin suggested resonated most with me: rename
"sublisteq" to "subseq" (for non-contiguous sub-sequences) and introduce
"sublist" (for contiguous sub-sequences).
For this, one would also have to rename the existing function sublist,
which is of type "'a list ⇒ nat set ⇒ 'a list", but frankly, I was never
quite happy with that name to begin with.
Perhaps one could call this "select_indices" or "nths" (in analogy to
List.nth) or something like that?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I have no strong opinion on that matter, but would suggest the following:
Contiguous sub-sequences: »infix« (following Jasmin)
Given that prefix, suffix are already there, the name is
unambiguously and does not need yet another terminology.
Non-continuous sub-sequences: »selection«
Indeed the most difficult candidate to come up with a convincing
name. »sublist« indeed suggests contiguous sub-sequence analogously
to »substring«.
sublist :: "'a list ⇒ nat set ⇒ 'a list"
=> nths :: "'a list ⇒ nat set ⇒ 'a list"
100 % for Manuel. The »s« suffix is quite established in such cases
(cf. maps in Isabelle/ML).
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 15:32):From: Tobias Nipkow <nipkow@in.tum.de>
Thank you for your research. I am perfectly happy with "sublist" (for the
contiguous case) and "subseq" (for the general case) and think we should adopt it.
[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒ nat set ⇒ 'a
list" (in List) to something else, eg sublist_index)
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC