Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 20
    • Merge requests 20
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #82
Closed
Open
Issue created Mar 20, 2017 by Ralf Jung@jungOwner

Consider adding a "strong" always modality

The idea of a stronger always modality keeps coming up, so let's collect the arguments somewhere.

IMHO the main argument against it is that it would increase the number of modalities of the base logic by 33%. In other words, the default should be not to add anything unless we really need it -- and we got pretty far without the strong always.

So what do we have that this would enable? (I am writing "SB" for the strong box below.)

  • Propositional extensionality. Not sure how useful that would be though.
  • (|=> SB P) -> SB P, i.e. basic updates can be removed around the strong box. That seems pretty powerful, but the only application we have so far is to make the adequacy lemma nicer to state (no more "nested laters and basic updates", but just "nested laters").
  • It would be possible to have the "core of a proposition" in a clean way, defined as ∀ Q, SB (Q -> □Q) -> SB (P -> Q) → □ Q. This works because SB P -> □ Q is persistent.

@robbertkrebbers I seem to remember you saying that one of the Iris-based papers added the strong box. Why again did they need it?

I am not convinced that the above is enough of a reason to add the box to the core. In particular, I feel like it would be non-trivial to explain to people why we have two box-like modalities.

Assignee
Assign to
Time tracking