Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
9ba4ad2b
Commit
9ba4ad2b
authored
Aug 04, 2016
by
Ralf Jung
Browse files
fix some typos in the docs
parent
ef669d81
Changes
2
Hide whitespace changes
Inline
Side-by-side
docs/algebra.tex
View file @
9ba4ad2b
...
...
@@ -35,7 +35,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e
A function
$
f :
\cofe
\to
\cofeB
$
between two COFEs is
\emph
{
non-expansive
}
(written
$
f :
\cofe
\nfn
\cofeB
$
) if
\[
\All
n, x
\in
\cofe
, y
\in
\cofe
. x
\nequiv
{
n
}
y
\Ra
f
(
x
)
\nequiv
{
n
}
f
(
y
)
\]
It is
\emph
{
contractive
}
if
\[
\All
n, x
\in
\cofe
, y
\in
\cofe
.
(
\All
m < n. x
\nequiv
{
m
}
y
)
\Ra
f
(
x
)
\nequiv
{
n
}
f
(
x
)
\]
\[
\All
n, x
\in
\cofe
, y
\in
\cofe
.
(
\All
m < n. x
\nequiv
{
m
}
y
)
\Ra
f
(
x
)
\nequiv
{
n
}
f
(
y
)
\]
\end{defn}
Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within
$
n
$
steps remain indistinguishable after applying
$
f
$
.
...
...
@@ -211,7 +211,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\end{defn}
Note that every object/arrow in
$
\CMRAs
$
is also an object/arrow of
$
\COFEs
$
.
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
\ralf
{
Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
}
%TODO:
Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
%%% Local Variables:
%%% mode: latex
...
...
docs/logic.tex
View file @
9ba4ad2b
...
...
@@ -135,7 +135,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
Note that
$
\always
$
and
$
\later
$
bind more tightly than
$
*
$
,
$
\wand
$
,
$
\land
$
,
$
\lor
$
, and
$
\Ra
$
.
We will write
$
\pvs
[
\term
]
\prop
$
for
$
\pvs
[
\term
][
\term
]
\prop
$
.
If we omit the mask, then it is
$
\top
$
for weakest precondition
$
\wpre\expr
{
\Ret\var
.
\prop
}$
and
$
\emptyset
$
for primitive view shifts
$
\pvs
\prop
$
.
\ralf
{
$
\top
$
is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
}
%FIXME
$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
Some propositions are
\emph
{
timeless
}
, which intuitively means that step-indexing does not affect them.
This is a
\emph
{
meta-level
}
assertion about propositions, defined as follows:
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment