Add symmetry and definition to `simultaneous with`

anitacaron commented 2 years ago

balhoff commented 2 years ago

Discussion at RO meeting 2022-06-28: we should have definitions for 'simultaneous with', 'ends' and 'starts' in order to decide how they are related. Some definition may be produced via the definitions of the inverses, but some translation may be needed to make this clear.

dosumis commented 2 years ago

The comment on simultaneous_with has a proposed def:

t1 simultaneous_with t2 iff:= t1 before_or_simultaneous_with t2 and not (t1 before t2).

This is certainly not ideal, but I think it indicates that this is not meant to be used between processes/intervals but between points in time - where the points in time we are interested in our those that define the start and end points of an occurrent. Defined in this way, the term should not be used in Uberon (where this request originates). I think what's needed for Uberon is probably the Allen 'equals' relation:

http://www.thomasalspaugh.org/pub/fnd/allen.html.

We don't seem to have that at present.

To be consistent with other defs, this should be something like this:

x {name_TBD} y iff ω(x) = ω(y) and ω(α ) = ω(α), where α is a function that maps a process to a start point, and ω is a function that maps a process to an end point and '=' indicates the same instance in time.

(Note - the = above is the same as the intent of the current 'simultaneous_with relation)

TBD:

do we repurpose simultaneous_with for this? If we do we should drop the grouping term and the 'before' objectProperty as both of these are also apply between instance in time? Perhaps the strictly correct thing to do would be to obsolete this term and create a new simultaneous_with using the above def.
Re - where this should be in the property hierarchy - to be a subproperty of starts and ends, starts and ends should be defined as α(y) = α(x) and ω(y) = ω(x) respectively. This is not currently that case. starts is inverse_of starts_with and has def "α(y) = α(x) ∧ ω(y) < ω(x), where α is a function that maps a process to a start point, and ω is a function that maps a process to an end point" (where < indicates before). Defining starts as 'α(y) = α(x)' only - leaving the end point open, would make it a parent to e, S & s.

More generally - it would be really awesome if we could find a decent logician to review this whole branch. We decided years ago to not directly re-use Allen relations, but to use derivable relations that (we believe(d)) are more intuitive for biologists. For example our 'precedes' is a subproperty of Allen 'meets'. The general work required is to derive property heirarchy & chains (or rules) and standardise definitions - using Allen as a starting point. Here's a rather ancient attempt: https://docs.google.com/document/d/1kBv1ep_9g3sTR-SD3jqzFqhuwo9TPNF-l-9fUDbO6rM/edit?pli=1

shawntanzk commented 2 years ago

From tech call

Minimum:

[ ] obsolete this term and create a new simultaneous_with using the above def. @cmungall is this definition acceptable, and shall we create a new relation?

Other parts of https://github.com/oborel/obo-relations/pull/611#issuecomment-1173714948 should be opened as a new ticket for longer term modelling solutions

balhoff commented 1 year ago

I'm not sure if this is ready to be merged; @cmungall approved but @shawntanzk's comment suggests some changes?

wdduncan commented 1 year ago

@dosumis @shawntanzk Can you attend the next RO call so that we can discuss this.

github-actions[bot] commented 1 year ago

This PR has not seen any activity in 90 days and has been marked as stale. If it is no longer needed, please close the PR. Otherwise, please update the PR with a status update.

cmungall commented 1 year ago

Here is what I think needs to be done right now with this relation in RO:

back out the two subproperties in this PR, on reflection these are not correct
- the corresponding injections should also be removed from uberon
make the relation symmetric
add the textual definition @dosumis proposes

This will be sufficient to have a PR we can merge

I also completely agree with @dosumis that we should have a separate review where we encode all these relations in a stronger formalism than OWL and validate them. Note the temporal relations mirror genome ones so we can piggy back off of this: https://www.biorxiv.org/content/10.1101/006650v1 (without the complexities of reverse complementation)

anitacaron commented 1 year ago

I did the changes. Just to make it clear that this relation is already transitive. This type is in the temporal-intervals.owl

oborel / obo-relations

Add symmetry and definition to `simultaneous with` #611