Bounded Reversibility in HO \(\pi \)
摘要
The higher-order causally-consistent reversible \(\pi \) -calculus, known as \({\mathbf {roll{-}}\pi }\) , enables the rollback of arbitrary past actions while preserving causal consistency – ensuring that effects are undone before their causes. This prevents the occurrence of actions without justifications, even after a rollback. However, in practical scenarios, not all events can be reversed; for example, once a document is printed, it cannot be unprinted. To better model real-world constraints, we introduce \({\mathbf {broll{-}}\pi }\) (bounded \({\mathbf {roll{-}}\pi }\) ), an extension of \({\mathbf {roll{-}}\pi }\) that limits reversibility. Our approach imposes two key restrictions: spatial bounds, which prevent certain processes from being affected by rollbacks, and temporal bounds, which restrict how far back in time a rollback can go. Bounded reversibility allows for more realistic and controlled rollbacks in computational systems. In this paper, we provide an informal introduction to \({\mathbf {broll{-}}\pi }\) and discuss its implications for modeling reversible processes in practical applications.