Commit e1f4aaad authored by Robbert Krebbers's avatar Robbert Krebbers

Docs: remark about name "Camera".

parent 46313843
Pipeline #5838 passed with stages
in 8 minutes and 33 seconds
...@@ -173,7 +173,11 @@ Since Iris ensures that the global ghost state is valid, this means that we can ...@@ -173,7 +173,11 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\end{align*} \end{align*}
\end{defn} \end{defn}
This is a natural generalization of RAs over OFEs. This is a natural generalization of RAs over OFEs\footnote{The reader may wonder why on earth we call them ``cameras''.
The reason, which may not be entirely convincing, is that ``camera'' was originally just used as a comfortable pronunciation of ``CMRA'', the name used in earlier Iris papers.
CMRA was originally supposed to be an acronym for ``complete metric resource algebras'' (or something like that), but we were never very satisfied with it and thus ended up never spelling it out.
To make matters worse, the ``complete'' part of CMRA is now downright misleading, for whereas previously the carrier of a CMRA was required to be a COFE (complete OFE), we have relaxed that restriction and permit it to be an (incomplete) OFE.
For these reasons, we have decided to stick with the name ``camera'', for purposes of continuity, but to drop any pretense that it stands for something.}.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index. All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation: We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation:
\[ \mvalFull(\melt) \eqdef \All n. n \in \mval(\melt) \] \[ \mvalFull(\melt) \eqdef \All n. n \in \mval(\melt) \]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment