refactor(LTS): refactor LTS/Relation properties

[SamuelSchlesinger]

The current definition requires a global bound, which seems wrong. At least it is misleading as a reader of the documentation, perhaps it is intended and the documentation simply confused me.

[ctchou]

I don't know @fmontesi's original intention when he made this definition. But, prima facie, shouldn't Acyclic be defined by something like this?

class Acyclic (lts : LTS State Label) where
  acyclic : ¬ ∃ s μs, lts.MTr s μs s ∧ 0 < μs.length

It seems to me that the current definition should be called "Bounded" (perhaps with n as an explicit parameter) and the new definition that @SamuelSchlesinger proposes should be called "WellFounded".

[SamuelSchlesinger]

Yes, your proposal makes the most semantic sense to me.

[SamuelSchlesinger]

I think the bounded definition also can choose to order the quantifiers differently and those are different types of Bounded. GloballyBounded vs LocallyBounded or something.

[thomaskwaring]

i agree both that the name is confusing (it should be more like @ctchou's suggestion) and that the docs don't match the code — fwiw in Sangiorgi's book "acyclic" is only ever applied to finite-state lts's for which all of these notions agree

also given the swapping of arguments, perhaps WellFounded could be replaced by cslib's Terminating?

[ctchou]

Indeed, since transition labels don't really matter in these definitions, perhaps they should be defined on Relation rather than LTS?

[fmontesi]

i agree both that the name is confusing (it should be more like @ctchou's suggestion) and that the docs don't match the code — fwiw in Sangiorgi's book "acyclic" is only ever applied to finite-state lts's for which all of these notions agree

Formalising that book is where the def came from, but indeed we should improve this.

Summarising the thoughts expressed so far and my own, I'd suggest:

• Rename the current Acyclic to Bounded (we can later separate globally from locally, but I think Bounded would make sense as interim since it is the obvious global one that says 'the lts has a bound to the length of all possible executions').
• Rename @SamuelSchlesinger's proposal into WellFounded.
• Make a new Acyclic that actually checks that there are no loops (as in graphs). We can do this in another PR, if you prefer.

[SamuelSchlesinger]

I think that makes sense. I'll reform this PR into what I believe is the synthesis of this discussion, and we can do another round of discussion.

[ctchou]

BTW, the title of this PR should change, too.

[SamuelSchlesinger]

@ctchou addressed your comments and deleted a noisy theorem with no use sites.

[ctchou]

LGTM.

[SamuelSchlesinger]

@fmontesi can you re-review and/or merge?

[fmontesi]

The entire PR looks good to me now but I have a minor annoyance here:

This has exactly the same name as LTS.Tr.toRelation and LTS.MTr.toRelation, which have the 'expected' meaning from the literature -- fixing the (multi)transition relation on a label. This new LTS.toRelation should probably go in Relation.lean, be namespaced under LTS.Tr, and have a different name to distinguish it from the other ones.

[SamuelSchlesinger]

Good catch. Busy today but when I get online I'll patch this.

[SamuelSchlesinger]

If anyone else wants this merged, feel free to push this last commit and merge it.