search

informalsystems / vdd

Verification-Driven Development
21 stars 0 forks source link

Introduce support for tag synonymy #21

Closed shonfeder closed 3 years ago

shonfeder commented 3 years ago

Without this feature, we have no way of indicating when a single logical unit implements multiple ancestors.

Note that this generalizes the graph structure from a tree to a DAG, but I think it must be supported.

shonfeder commented 3 years ago

Should synonym not mean that one unit has more than one names that can be used "synonymously"?

I'd hoped to explain that here:

A logical unit may bear multiple tags, as a result of implementing multiple ancestor logical units. This gives rise to "synonyms tags"

If a single unit has multiple tags, then in terms of reference, those two tags (which are the names of the unit) are synonymous. However, the sense of these two tags (which relate to the implementation ancestry) is different.

In the units added here, each bears two tags that are synonymous in terms of reference. The tags |TRC-TAG.1::SYNTAX.1::SYNONYMY.1| and |TRC-IMPL.1::SYNONYMY.1| are synonymous in just the same way that Hesperus and Phosphorus are: they both refer to the same, singular object (here, a logical unit) but through different senses.

That said, I'm happy to use a term for this that you'd find clearer or more helpful. Any suggestions?

josef-widder commented 3 years ago

In the units added here, each bears two tags that are synonymous in terms of reference. The tags |TRC-TAG.1::SYNTAX.1::SYNONYMY.1| and |TRC-IMPL.1::SYNONYMY.1| are synonymous in just the same way that Hesperus and Phosphorus are: they both refer to the same, singular object (here, a logical unit) but through different senses.

That said, I'm happy to use a term for this that you'd find clearer or more helpful. Any suggestions?

Now, I had to google "Hesperus" ;-).

I guess my confusion came from the fact that in my mind not all synonyms were necessarily the result of ancestry relationships. So when I think about synonyms, ancestry is not the first point to come up in my mind. So if the primary use is capturing ancestry, synonyms might be a misleading term. But perhaps I am just overthinking words.

shonfeder commented 3 years ago

True that the primary use is to record multiple ancestry and that the only way in which synonymous tags can arise, according to this proposal, is via multiple ancestry. If you find it confusing, I'm happy to use a name you prefer. (For my part, it is not at all confusing that we give syntax for synonymous tags, but that this only has application in the case of multiple ancestry. The entire naming scheme is inseparable from the ancestry relationships, so almost any aspect of the tagging syntax will be focused narrowly on ancestry. But I wrote this, and I think clarity for readers is more important than self-understanding of writers :))

Keeping in mind that this is a specification of the syntax, what kind of name would you find less confusing?

shonfeder commented 3 years ago

In particular, if you could consider the places where I use the therm "synonymous tags" to refer to the set of tags which are all tagging the same unit, and ensure that your counter suggestion would work for this purpose. I cannot think of a more clear, and still succinct way of referring to this collection of tags (which all refer to the same unit).

shonfeder commented 3 years ago

As an alternative (in case no better name occurs to you), I could expand the description a bit to give more explanation of why these tags are synonymous, and why this synonymy of tags can only serve to indicate multiple ancestry. (I think this latter part is just do the semantics of the tags themselves: they only serve to communicate versions and ancestry.)

josef-widder commented 3 years ago

I guess just adding one or two sentences may help. Perhaps we can say that there are "ancestry tags", and that an entry can have multiple "ancestry tags", and that requires us to consider synonyms. I guess all of that was already in your initial write-up, just a bit too quick for me.

shonfeder commented 3 years ago

I've expanded the introduction of the concept a bit. Let me know if you think this helps!

josef-widder commented 3 years ago

I've expanded the introduction of the concept a bit. Let me know if you think this helps!

Perfect! Thanks a lot!!

shonfeder commented 3 years ago

Thank you for the review and for helping push this to be clearer :pray: