text:
\section{Introduction}\label{sec:intro}

A book has proper spelling provided that each of its sentences does.
For a book to be captivating and suspenseful --- that is not a property that can be reduced to a property of its individual sentences.  Indeed, few interesting properties of a book are simply a property of all its sentences.
By contrast, many interesting requirements of a program can be specified as so-called \dt{trace properties}: there is some property of traces (i.e., observable behaviors) which must be satisfied by all the program's traces.

The unruly mess of contemporary programming languages, design tools, and approaches to formal specification has been given a scientific basis through unifying theories that abstract commonalities by means of algebraic operators and laws.
Algebra abstracts from computational notions like partiality and nondeterminacy by means of operators that are interpreted as total functions and which enable equational reasoning.
Several practical concerns --- such as improving a program's resource usage while not altering its observable behavior, checking conformance of code with design architecture, checking satisfaction of requirements,
and equivalence of two differently presented designs --- are subsumed by the beautiful notion that programs and designs\footnote{This paper was written with the UTP~\cite{HoareHe} community in mind,
but our use of the term ``design'' is informal and does not refer to the technical notion in UTP.}
are just kinds of specification and their relationships are instances of logical implication between specifications.
Transitivity of implication yields the primary relationship: the traces of a program are included in the traces allowed by its specification.
The mathematical development of this idea has been very successful --- for trace properties.

Not all requirements are trace properties.  A program should be easy to read,
consistent with dictates of style, and amenable to revision for adapting to changed requirements.
Some though not all such requirements may be addressed by mathematics; e.g., parametric polymorphism is a form of modularity that facilitates revision through reuse.  In this paper we are concerned with requirements that are extensional in the sense that they pertain directly to observable behavior.
For a simple example, consider a program acting on variables $hi,lo$ where the initial value of $hi$ is meant to be a secret, on which the final value of $lo$ must not depend.  Consider this simple notion of program behavior:
a state assigns values to variables, and a trace is a pair: the initial and final states.
The requirement cannot be specified as a trace property, but it can be specified as follows:
for any two traces $(\sigma,\sigma')$ and $(\tau,\tau')$, if the initial states $\sigma$ and $\tau$ have the same value for $lo$ then so do the final states.
In symbols: $\sigma(lo)=\tau(lo) \Rightarrow \sigma'(lo)=\tau'(lo)$.

Some requirements involve more than two traces, e.g., ``the average response time is under a millisecond'' can be made precise by averaging the response time of each trace, over all traces, perhaps weighted by a distribution that represents likelihood of different requests.
For a non-quantitative example, consider the requirement that a process in a distributed system should know which process is the leader: something is known in a given execution if it is true in all possible traces that are consistent with what the process can observe of the given execution (such as a subset of the network messages).
In the security literature, some information flow properties are defined by closure conditions on the program's traces, such as: for any two traces, there exists a trace with the high (confidential) events of the first and the low (public) events of the second.

This paper explores the notion that just as a property of books is a set of books, not necessarily defined simply in terms of their sentences,
so too a property of programs is a set of programs, not merely a set of traces.
The goal is to investigate how the algebra of programming can be adapted for reasoning about non-trace properties.
To this end, we focus on the most rudimentary notion of trace, i.e., pre/post pairs, and rudimentary program constructs.
We conjecture that the phenomena and ideas are relevant to a range of models, perhaps even the rich notions of trace abstracted by variations on concurrent Kleene algebra~\cite{HoareMSW11}.

It is unfortunate that the importance of trace properties in programming has led to well established use of the term ``property'' for trace property,
and recent escalation in terminology to ``hyperproperty'' to designate the general notion of program property --- sets of programs rather than sets of traces~\cite{ClarksonS10,ClarksonFKMRS14}.
Some distinction is needed, so for clarity and succinctness we follow the crowd.
The technical contribution of this paper can now be described as follows: we give a lifting of the fixpoint semantics of loops to the ``hyper level'', and show anomalies that occur with other liftings.
This enables reasoning at the hyper level with usual fixpoint laws for loops,
while retaining consistency with standard relational semantics.
Rather than working directly with sets of trace sets, our lifting uses a simpler model,
sets of state sets; this serves to illustrate the issues and make connections with other models that may be familiar.
The conceptual contribution of the paper is to call attention to the challenge of unifying theories of programming that encompass requirements beyond trace properties.

\paragraph{Outline.}
Section~\ref{sec:rel} describes a relational semantics of imperative programs and defines an example program property that is not a trace property.
Relational semantics is connected, in Section~\ref{sec:trans}, with semantics mapping sets to sets, like forward predicate transformers.
Section~\ref{sec:htrans} considers semantics mapping sets of sets to the same, this being the level at which hyperproperties are formulated.  Anomalies with obvious definitions motivate a more nuanced semantics of loops.
The main technical result of the paper is Theorem~\ref{thm:main} in this section, connecting the semantics of
Section~\ref{sec:htrans} with that of Section~\ref{sec:trans}.
Section~\ref{sec:spec} connects the preceding results with the intrinsic notion of satisfaction for hyperproperties,
and sketches challenges in realizing the dream of reasoning about hyperproperties using only refinement chains.
The semantics and theorem are new, but similar to results in prior work discussed in Section~\ref{sec:related}.
Section~\ref{sec:concl} concludes.

\section{Programs and specifications as binary relations}\label{sec:rel}

\paragraph{Preliminaries.}

We review some standard notions, to fix notation and set the stage.
Throughout the paper we assume $\Sigma$ is a nonempty set, which stands for the set of program states, or data values, on which programs act.
For any sets $A$, $B$,
let $A \relto B$ denote the binary relations from $A$ to $B$; that is,
$A \relto B$ is $\pset(A\times B)$ where $\pset$ means powerset.
Unless otherwise mentioned, we consider powersets, including $\Sigma\relto\Sigma$, to be ordered by inclusion ($\subseteq$).

We write $A\to B$ for the set of functions from  $A$ to $B$.
For composition of relations, and in particular composition of functions, we use infix symbol $\c$ in the forward direction.
Thus for relations $R,S$ and elements $x,y$ we have
$x(R\c S)y$ iff $\some{z}{xRz \land zSy}$.
For a function $f: A\to B$ and element $x\in A$ we write application as $f x$ and let it associate to the left.
Composition with $g:B\to C$ is written $f\c g$, as functions are treated as special relations,  so $(f\c g)x = g(f x)$.
The symbol $\c$ binds tighter than $\mathbin{\mbox{\small$\cup$}}$ and other operators.

For a relation $R:A \relto B$, the direct image
 $\dirimg{R}$ is a total function $\pset A \to \pset B$
defined by
$y\in\dirimg{R}p$ iff $\some{x\in p}{xRy}$.
It faithfully reflects ordering of relations:
\[
R\subseteq S \quad\mbox{iff}\quad \dirimg{R}\sqsubseteq\dirimg{S}
\]
where $\sqsubseteq$ means pointwise order
 (i.e.,
$\phi\sqsubseteq\psi$ iff $\all{ p\in\pset A }{ \phi\, p \subseteq \psi\, p}$).
We write $\join$ for pointwise union,
defined by $(\phi\join\psi)\,p = \phi\, p \mathbin{\mbox{\small$\cup$}} \psi\, p$.
The $\sqsubseteq$-least element is the function $\lambda p \:\mbox{\small$\bullet$}\: \emptyset$, abbreviated as $\bot$.
A relation can be recovered from its direct image:
\begin{equation}\label{eq:relRecover}
R = sglt \c \dirimg{R} \c \Ni
\end{equation}
where $sglt : A \to \pset A$ maps element $a$ to singleton set $\{a\}$ and $\Ni: \pset A \relto A$ is the converse of the membership relation.
Note that $\bot$ is the direct image of the empty relation.
Direct image is functorial and distributes over union:
\[
\dirimg{id_\Sigma} = id_{\pset\Sigma}
\qquad
\dirimg{R \c S} = \dirimg{R} \c \dirimg{S}
\qquad
\dirimg{R \mathbin{\mbox{\small$\cup$}} S} = \dirimg{R} \join \dirimg{S}
\]
We write $id$ for identity function on the set indicated.
In fact $\dirimg{-}$ distributes over arbitrary union,
i.e., sends any union of relations to the pointwise join of their images.
Also, $\dirimg{R}$ is universally disjunctive, and (\ref{eq:relRecover}) forms a bijection
between universally disjunctive functions
$\pset A\to\pset B$ and relations $A\relto B$.

In this paper we use the term \dt{transformer} for monotonic functions of type
$\pset A \to\pset B$.
For $\phi:\pset A\to\pset B$ to be monotonic is equivalent to
$(\rsps\c \phi) \subseteq (\phi\c\rsps)$.

We write $\mathsf{lfp}\,$ for the least-fixpoint operator.
For monotonic functions $f:A\to A$ and $g:B\to B$ where $A,B$ are sufficiently complete
posets that $\mathsf{lfp}\, f$ and $\mathsf{lfp}\, g$ exist,
the \dt{fixpoint fusion} rule says that for strict and continuous $h:A\to B$,
\begin{equation}\label{eq:fusion}
f\c h = h\c g \Rightarrow h(\mathsf{lfp}\, f) = \mathsf{lfp}\, g
\end{equation}
Inequational forms, such as $f\c h \leq h\c g \Rightarrow h(\mathsf{lfp}\, f) \leq \mathsf{lfp}\, g$,
are also important.\footnote{Fusion rules, also called fixpoint transfer,
can be found in many sources,
e.g.,~\cite{AartsEtal95,Back:book}.
We need the form in Theorem 3 of~\cite{Cousot02},
for Kleene approximation of fixpoints.
}

\paragraph{Relational semantics.}

The relational model suffices for reasoning about terminating executions.
If we write $x+2\leq x'$ to specify a program that increases $x$ by at least two,
we can write this simple refinement chain:
\[ x+2\leq x' \quad \supseteq \quad x := x+3 \choice x := x+5
\quad \supseteq \quad x := x+3
\]
to express that the nondeterministic choice ($\choice$) between adding 3 or adding 5 refines the specification and is refined in turn by the first alternative.
Relations model a good range of operations including relational converse and intersection which are not implementable in general but are useful for expressing specifications.
Their algebraic laws facilitate reasoning.
For example, choice is modeled as union, so the second step is from a law of set theory: $R\mathbin{\mbox{\small$\cup$}} S\supseteq R$.

Equations and inequations may serve as specifications.
For example, to express that relation $R$ is deterministic we can write $\converse{R}\c R \subseteq id$,
where $\converse{R}$ is the converse of $R$.
Note that this uses two occurrences of $R$.
Returning to the example in the introduction, suppose $R$ relates
states with variables $hi,lo$.
To formulate the \dt{noninterference} property that the final value of $lo$ is independent of the initial value of $hi$,
it is convenient to define a relation on states that says they have the same value for $lo$:
define $\mathring{\sim}$ by $\sigma\mathring{\sim}\tau$ iff $\sigma(lo)=\tau(lo)$.
The property is
\[ \all{\sigma,\sigma',\tau,\tau'}{ \sigma R \sigma' \land \tau R \tau'  \land \sigma\mathring{\sim}\tau  \Rightarrow \sigma'\mathring{\sim}\tau' }\]
This is a form of determinacy. A weaker notion allows multiple outcomes for $lo$ but the set of possibilities should be independent from the initial value of $hi$.
\[ \all{\sigma,\sigma',\tau}{ \sigma R \sigma' \land \sigma\mathring{\sim}\tau  \Rightarrow
     \some{\tau'}{ \tau R \tau' \land \sigma'\mathring{\sim}\tau' }}\]
This is known as \dt{possibilistic noninterference}.
It can be expressed without quantifiers, by the usual simulation inequality:
\begin{equation}\label{eq:sim}
\mathord{\mathring{\sim}}\c R \;\subseteq\; R \c \mathord{\mathring{\sim}}
\end{equation}
Another equivalent form is
\( \mathring{\sim} \c R \c \mathring{\sim} \; = \; R \c \mathring{\sim} \),
which again uses two occurrences of $R$.
The algebraic formulations are attractive, but recall the beautiful idea of correctness proof as a chain of refinements
\[ spec \supseteq design \supseteq \ldots \supseteq prog  \]
This requires the specification to itself be a term in the algebra, rather than an (in)equation between terms.

Before proceeding to investigate this issue, we recall the well known fact that
possibilistic noninterference is not closed under refinement of trace sets~\cite{Jacob88}.
Consider $hi,lo$ ranging over bits, so we can write pairs compactly, and consider the set of traces
\( \{
(00,00), \underline{(00,01)},
(01,00), \underline{(01,01)},
\underline{(10,10)}, (10,11),
\underline{(11,10)}, (11,11)
\} \)
It satisfies possibilistic noninterference, but if we remove the underlined pairs the result does not; in fact
the result copies $hi$ to $lo$.

In the rest of this paper, we focus on deterministic noninterference, $\mathsf{NI}$ for short.
It has been advocated as a good notion for security~\cite{RoscoeWW1994}
and it serves our purposes as an example.

\paragraph{A signature and its relational model.}

To investigate how $\mathsf{NI}$ and other non-trace properties may be expressed and used in refinement chains,
it is convenient to focus on a specific signature, the simple imperative language over given atoms (ranged over by $atm$) and boolean expressions (ranged over by $b$).
\begin{equation}\label{eq:signature}
c ::= atm \mid \keyw{skip} \mid c;c \mid c \choice c \mid \ifc{b}{c}{c} \mid \whilec{b}{c}
\end{equation}
For expository purposes we refrain from decomposing the conditional and iteration constructs in terms of choice ($\choice$) and assertions.
That decomposition would be preferred in a more thorough investigation of algebraic laws, and it is evident in the semantic definitions to follow.

Assume that for each $atm$ is given a relation $\meansR{atm}:\Sigma\relto\Sigma$,
and for each boolean expression $b$ is given a coreflexive relation
$\meansR{b}:\Sigma\relto\Sigma$.  That is, $\meansR{b}$ is a subset of the identity relation $id_\Sigma$ on $\Sigma$.
For non-atom commands $c$ the relational semantics $\meansR{c}$ is defined in Fig.~\ref{fig:relsem}.
The fixpoint for loops\footnote{\label{fn:tailrec}
  It is well known that loops are expressible in terms of recursion:
  $\whilec{b}{c}$ can be expressed as $\mu X . (b;c;X \mathbin{\mbox{\small$\cup$}} \neg b)$
  and this is the form we use in semantics.
  A well known law is $\mu X . (b;c;X \mathbin{\mbox{\small$\cup$}} \neg b) =  \mu X . (b;c;X \mathbin{\mbox{\small$\cup$}} \keyw{skip});\neg b$
  which factors out the termination condition.}
is in $\Sigma\relto\Sigma$, ordered by $\subseteq$ with least element $\emptyset$.

\begin{figure}[t]
\begin{normalsize}
\[
\begin{array}{lcl}
\meansR{\keyw{skip}}          &\; = \;& id_\Sigma \\
\meansR{c\, ; d}           & = & \meansR{c} \c \meansR{d} \\
\meansR{c \choice d}           & = & \meansR{c} \mathbin{\mbox{\small$\cup$}} \meansR{d} \\
\meansR{ \ifc{b}{c}{d} } & = &  \meansR{b} \c \meansR{c} \:\mathbin{\mbox{\small$\cup$}}\: \meansR{\neg b} \c \meansR{d} \\
\meansR{ \whilec{b}{c} } & = & \mathsf{lfp}\, \mathsf{F} \\
               &\multicolumn{2}{l}{
                 \mbox{where } \mathsf{F}: (\Sigma\relto\Sigma)\to(\Sigma\relto\Sigma) \mbox{ is defined }} \\
               &\multicolumn{2}{l}{ \mathsf{F} R = \meansR{b} \c \meansR{c} \c R \:\mathbin{\mbox{\small$\cup$}}\: \meansR{\neg b} }
\end{array}
\]
\end{normalsize}
\caption{Relational semantics $\meansR{c} \in \Sigma\relto\Sigma$,
with $\meansR{atm}$ assumed to be given.
}
\label{fig:relsem}
\end{figure}

The language goes beyond ordinary programs, in the sense that atoms are allowed to be unboundedly nondeterministic.  They are also allowed to be partial; coreflexive atoms serve as assume and assert statements.
Other ingredients are needed for a full calculus of specifications, but here our aim is to sketch ideas that merit elaboration in a more comprehensive theory.

\section{Programs as forward predicate transformers}\label{sec:trans}

Here is yet another way to specify $\mathsf{NI}$ for a relation $R$:
\[ \all{p\in\pset\Sigma}{ \Agrl(p) \Rightarrow \Agrl(\dirimg{R}p) } \]
where $\Agrl$ says that all elements of $p$ agree on $lo$:
\[
\Agrl(p) \quad\mbox{iff}\quad \all{\sigma,\tau}{\sigma\in p \land \tau\in p \Rightarrow \sigma\mathring{\sim}\tau}
\]
As with the preceding (in)equational formulations, like (\ref{eq:sim}), this is not directly applicable as the specification in a refinement chain, but it does hint that escalating to sets of states may be helpful.
Note that $R$ occurs just once in the condition.

Weakest-precondition predicate transformers are a good model for programming algebra:
Monotonic functions $\pset\Sigma\to\pset\Sigma$ can model total correctness specifications with both angelic and demonic nondeterminacy.
In this paper we use transformers to model programs in the forward direction.

For boolean expression $b$ we define
\( \meansT{b} = \dirimg{ \meansR{b} } \)
so that $\meansT{b}$ is a filter:
$x$ is in $\meansT{b} p$ iff $x\in p$ and $b$ is true of $x$.
The transformer semantics is in Fig.~\ref{fig:transem}.
For loops, the fixpoint is for the aforementioned $\bot$ and $\sqsubseteq$.

\begin{figure}[t]
\begin{normalsize}
\[
\begin{array}{lcl}
\meansT{atm}             &\; = \;& \dirimg{\meansR{atm}} \\
\meansT{\keyw{skip}}          & = & id_{\pset\Sigma} \\
\meansT{c\, ; d}           & = & \meansT{c} \c \meansT{d} \\
\meansT{c \choice d}      & = & \meansT{c} \join \meansT{d} \\
\meansT{ \ifc{b}{c}{d} } & = &  \meansT{b} \c \meansT{c} \:\join\: \meansT{\neg b} \c \meansT{d} \\
\meansT{ \whilec{b}{c} } & = & \mathsf{lfp}\, \mathsf{G}  \\
               &\multicolumn{2}{l}{
         \mbox{where } \mathsf{G}: (\pset\Sigma\to\pset\Sigma)\to(\pset\Sigma\to\pset\Sigma) \mbox{ is defined }} \\
               &\multicolumn{2}{l}{
                         \mathsf{G} \phi = \meansT{b}\c\meansT{c}\c\phi \join \meansT{\neg b} }
\end{array}
\]
\end{normalsize}
\caption{Transformer semantics  $\protect\meansT{c} \in \pset\Sigma\to\pset\Sigma$.
}\label{fig:transem}
\end{figure}

\paragraph{Linking transformer with relational.}

The transformer model may support a richer range of operators than the relational one,
but for several reasons it is important to establish their mutual consistency on a common set of operators~\cite{HoareL74,HoareHe}.
A relation can be recovered from its direct image, see (\ref{eq:relRecover}), so the following is a strong link.

\begin{proposition}\label{prop:reltran}
For all $c$ in the signature, $\dirimg{\meansR{c}} = \meansT{c}$.
\end{proposition}
\begin{proof}
By induction on $c$.
\begin{itemize}
\item
$\keyw{skip}$: $\dirimg{\meansR{\keyw{skip}}} = \dirimg{id_{\Sigma}} = id_{\pset\Sigma\to\pset\Sigma} = \meansT{\keyw{skip}} $
by definitions and $\dirimg{-}$ law.

\item
$atm$: $\dirimg{\meansR{atm}} = \meansT{atm}$ by definition.

\item
$c ; d$: $\dirimg{\meansR{c; d}}
= \dirimg{\meansR{c}\c\meansR{d}}
= \dirimg{\meansR{c}}\c\dirimg{\meansR{d}}
= \meansT{c}\c\meansT{d}
= \meansT{c ; d}$
by definitions, $\dirimg{-}$ laws, and induction hypothesis.

\item
$c\choice d$: $\dirimg{\meansR{c\choice d}}
= \dirimg{\meansR{c}\mathbin{\mbox{\small$\cup$}}\meansR{d}}
= \dirimg{\meansR{c}}\join\dirimg{\meansR{d}}
= \meansT{c}\join\meansT{d}
= \meansT{c\choice d}$
by definitions, $\dirimg{-}$ laws, and induction hypothesis.

\item
$\ifc{b}{c}{d}$:
$\dirimg{\meansR{\ifc{b}{c}{d}}}
= \dirimg{\meansR{b}\c\meansR{c}\mathbin{\mbox{\small$\cup$}}\meansR{\neg b}\c\meansR{d}}
= \dirimg{\meansR{b}}\c\dirimg{\meansR{c}}\join\dirimg{\meansR{\neg b}}\c\dirimg{\meansR{d}}
= \meansT{b}\c\dirimg{\meansR{c}}\join\meansT{\neg b}\c\dirimg{\meansR{d}}
= \meansT{b}\c\meansT{c}\join\meansT{\neg b}\c\meansT{d}
= \meansT{\ifc{b}{c}{d}}
$
by definitions, $\dirimg{-}$ laws, and induction hypothesis.
\item
$\whilec{b}{c}$:  To prove
$\dirimg{\meansR{\whilec{b}{c}}} = \meansT{\whilec{b}{c}}$,
unfold the definitions to
$\dirimg{\mathsf{lfp}\, \mathsf{F}} = \mathsf{lfp}\, \mathsf{G}$, where $\mathsf{F},\mathsf{G}$ are defined in Figs~\ref{fig:relsem} and~\ref{fig:transem}.
This follows by fixpoint fusion, taking $h$ in  (\ref{eq:fusion}) to be $\dirimg{-}$
so the antecedent to be proved is
$\all{R}{ \dirimg{ \mathsf{F} R } = \mathsf{G}\dirimg{R} }$.
Observe for any $R$:
\begin{calcushort}
\flns{    \dirimg{\mathsf{F} R} }
\plns{=}{ \dirimg{ \meansR{b} \c \meansR{c} \c R \mathbin{\mbox{\small$\cup$}} \meansR{\neg b}} }{def $\mathsf{F}$}

\plns{=}{ \dirimg{ \meansR{b}} \c \dirimg{\meansR{c}} \c \dirimg{R } \join \dirimg{\meansR{\neg b}} }{$\dirimg{-}$ distributes over $\c$ and $\mathbin{\mbox{\small$\cup$}}$}

\plns{=}{ \meansT{b} \c \dirimg{\meansR{c}} \c \dirimg{R } \join \meansT{\neg b} }{def $\meansT{b}$}

\plns{=}{ \meansT{b} \c \meansT{c} \c \dirimg{R} \join \meansT{\neg b} }{induction hypothesis}

\plns{=}{ \mathsf{G}\dirimg{R} }{def $\mathsf{G}$}
\end{calcushort}
\end{itemize}
\qed
\end{proof}
Subsets of $\pset \Sigma \to \pset \Sigma$, such as transformers satisfying  Dijkstra's healthiness conditions,
validate stronger laws than the full set of (monotonic) transformers.
Healthiness conditions can be expressed by inequations,
such as the determinacy inequation $\converse{R}\c R \subseteq id$,
and used as antecedents in algebraic laws.
Care must be taken with joins: not all subsets are closed under pointwise union.
Pointwise union does provide joins in the set of all transformers and also in the set of all universally disjunctive transformers.

In addition to transformers as weakest preconditions~\cite{Back:book},
another similar model is multirelations which are attractive in maintaining a pre-to-post direction~\cite{MartinCR07}.
These are all limited to trace properties, though, so we proceed in a different direction.

\section{Programs as h-transformers}\label{sec:htrans}

Given $R:A\relto B$, the image $\dirimg{R}$ is a function and functions are relations, so the direct image can be taken:
\( \dirimg{\dirimg{R}} : \ppset A \to \ppset B \)
where $\ppset A$ abbreviates $\pset(\pset A)$.
In this paper, monotonic functions of this type are called \dt{h-transformers}, in a nod to hyper terminology.

The underlying relation can be recovered by two applications of (\ref{eq:relRecover}):
\[ R = sglt \c sglt \c \dirimg{\dirimg{R}} \c \Ni \c \Ni \]
More to the point, a quantifier-free  formulation of $\mathsf{NI}$ is now in reach.
Recall that we have $R \in \mathsf{NI}$ iff
$\all{p\in\pset\Sigma}{ \Agrl(p) \Rightarrow \Agrl(\dirimg{R} p) }$.
This is equivalent to
\begin{equation}\label{eq:NI}
\dirimg{\dirimg{R}} \A \subseteq \A
\end{equation}
where the set of sets $\A$ is defined by $\A = \{ p \mid \Agrl(p) \}$.
This is one motivation to investigate $\ppset \Sigma \to \ppset \Sigma$ as a model, rather than
$\pset(\Sigma\relto\Sigma)$ which is the obvious way to embody the idea that a program is a trace set and a property is a set of programs.

In the following we continue to write $\join$ and $\sqsubseteq$ for the pointwise join and pointwise  order on $\ppset\Sigma\to\ppset\Sigma$. Please note the order is defined in terms of set inclusion at the outer layer of sets and is independent of the order on $\pset\Sigma$.
Define $\pbot = \dirimg{\bot}$ and note that
$\pbot\emptyset = \emptyset$ and $\pbot\Q=\{\emptyset\}$ for $\Q\neq\emptyset$.

\paragraph{Surprises.}

For semantics using h-transformers, some obvious guesses work fine but others do not.
The semantics in Fig.~\ref{fig:powtransem}
uses operators $\ijoin$, $\hycond{b}$ and $\Dpset$ which will be explained in due course.
For boolean expressions we simply lift by direct image, defining
\( \meansH{b} = \dirimg{\meansT{b}} \).
The same for command atoms, so the semantics of $atm$ is derived from the given $\meansR{atm}$.

\begin{figure}[t]
\begin{normalsize}
\[
\begin{array}{lcl}
\meansH{atm}             &\; = \;& \dirimg{\meansT{atm}} \\
\meansH{\keyw{skip}}          & = & id \\
\meansH{c\, ; d}           & = & \meansH{c} \c \meansH{d} \\
\meansH{c \choice d}      & = & \meansH{c} \ijoin \meansH{d} \\
\meansH{ \ifc{b}{c}{d} } & = &  \meansH{c} \hycond{b} \meansH{d} \\
\meansH{ \whilec{b}{c} } & = & \mathsf{lfp}\, \H \\
               &\multicolumn{2}{l}{
         \mbox{where } \H: (\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma))\to (\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma))
                           \mbox{ is defined } } \\
               &\multicolumn{2}{l}{ \H \Phi = \meansH{c}\c\Phi \hycond{b} \meansH{\keyw{skip}} }
\end{array}
\]
\end{normalsize}
\caption{H-transformer semantics  $\protect\meansH{c} \in \Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$.
}\label{fig:powtransem}
\end{figure}

The analog of Proposition~\ref{prop:reltran} is that
for all $c$ in the signature, $\dirimg{\meansT{c}} = \meansH{c}$,
allowing laws valid in relational semantics to be lifted to h-transformers.
Considering some cases suggests that this could be proved by induction on $c$:

\begin{itemize}
\item $\keyw{skip}$: $\dirimg{\meansT{\keyw{skip}}} = \dirimg{id_{\pset\Sigma}} = \meansH{\keyw{skip}} $
by definitions and using that $\dirimg{-}$ preserves identity.

\item $atm$: $\dirimg{\meansT{atm}} = \meansH{atm}$ by definition.

\item $c ; d$: $\dirimg{\meansT{c\c d}}
= \dirimg{\meansT{c}\c\meansT{d}}
= \dirimg{\meansT{c}}\c\dirimg{\meansT{d}}
= \meansH{c}\c\meansH{d}
= \meansH{c ; d}$
by definitions, distribution of $\dirimg{-}$ over $\c$, and putative induction hypothesis.

\end{itemize}
These calculations suggest we may succeed with this obvious guess:
\begin{equation}\label{eq:badcond}
\meansH{ \ifc{b}{c}{d} }  =   \meansH{b} \c \meansH{c} \:\join\: \meansH{\neg b} \c \meansH{d}
\end{equation}
The induction hypothesis would give
\( \meansH{ \ifc{b}{c}{d} }  =   \dirimg{\meansT{b} \c \meansT{c}} \join \dirimg{\meansT{\neg b} \c \meansT{d}} \).
On the other hand,
\( \dirimg{\meansT{ \ifc{b}{c}{d} }} = \dirimg{\meansT{b} \c \meansT{c} \join \meansT{\neg b} \c \meansT{d}} \).
Unfortunately these are quite different because the joins are at different levels.
In general, for $\phi$ and $\psi$ of type $\pset\Sigma\to\pset\Sigma$ and $\Q\in\ppset\Sigma$ we have
$\dirimg{\phi \join \psi}\Q = \{ \phi\, p \mathbin{\mbox{\small$\cup$}} \psi\, p \mid p\in \Q \}$
whereas
\( (\dirimg{\phi}\join\dirimg{\psi})\Q = \{ \phi\, p \mid p\in \Q \} \mathbin{\mbox{\small$\cup$}} \{ \psi\, p \mid p \in \Q \} \).
Indeed, the same discrepancy would arise if we define
$\meansH{c \choice d} = \meansH{c} \join \meansH{d}$.

At this point one may investigate notions of ``inner join'', but for expository purposes we proceed to consider a putative definition for loops.
Following the pattern for relational and transformer semantics, an obvious guess is
\begin{equation}\label{eq:badloop}
\meansH{\whilec{b}{c}} = \mathsf{lfp}\, \mathsf{K}
\mbox{ where }
\mathsf{K} \Phi = \meansH{b}\c\meansH{c}\c\Phi \join \meansH{\neg b}
\end{equation}
Consider this program: $\whilec{x<4}{x:=x+1}$. We can safely assume
$\meansH{x<4}$ is $\dirimg{\meansT{x<4}}$ and
$\meansH{x:=x+1}$ is $\dirimg{\meansT{x:=x+1}}$.
As there is a single variable, we can represent a state by its value, for example $\{2,5\}$ is a set of two states.
Let us work out $\meansH{\whilec{x<4}{x:=x+1}} \{\{2,5\}\}$.
Now $\meansH{\whilec{x<4}{x:=x+1}}$ is the limit of the chain $\mathsf{K}^i\pbot$ where $\mathsf{K}^i$ means $i$ applications of $\mathsf{K}$.
Note that for any $\Phi$ and $i>0$,
\[ \mathsf{K}^i \Phi =
   \begin{array}[t]{l}
       (\meansH{x<4}\c\meansH{x:=x+1})^i \c \Phi
         \; \join \\
       (\join j :: 0\leq j < i \:\mbox{\small$\bullet$}\:
                  (\meansH{x<4}\c\meansH{x:=x+1})^j \c\meansH{\neg x<4} )
   \end{array}\]
Writing $\Q_i$ for $\mathsf{K}^i\pbot \{\{2,5\}\}$ one can derive
\[\begin{array}{l}
\Q_0 = \{\emptyset\} \\
\Q_1 = \{\emptyset\} \mathbin{\mbox{\small$\cup$}} \{\{5\}\} = \{ \emptyset,\{5\}\} \\
\Q_2 = \{\emptyset\} \mathbin{\mbox{\small$\cup$}} \{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\{5\}\} = \{ \emptyset,\{5\}\} \\
\Q_3 = \{\emptyset\} \mathbin{\mbox{\small$\cup$}} \{\emptyset\}\mathbin{\mbox{\small$\cup$}}\{\{4\}\}\mathbin{\mbox{\small$\cup$}}\{\{5\}\} = \{ \emptyset,\{4\},\{5\}\}
\end{array}
\]
at which point the sequence remains fixed.
As in the case of conditional (\ref{eq:badcond}), the result is not consistent with the underlying semantics:
\[ \meansT{\whilec{x<4}{x:=x+1}} \{2,5\} = \{4,5\} \]
The result should be $\{\{4,5\}\}$ if we are to have the analog of
Proposition~\ref{prop:reltran}.

A plausible inner join is $\otimes$ defined
by $(\Phi\otimes\Psi)\Q = \{ r\mathbin{\mbox{\small$\cup$}} s \mid \some{q\in\Q}{r\in\Phi\{q\}\land s\in\Psi\{q\}} \}$.
This can be used to define a semantics of $\choice$
as well as semantics of conditional and loop;
the resulting constructs are $\sqsubseteq$-monotonic and enjoy other nice properties.

Indeed, using $\otimes$ in place of $\join$ in (\ref{eq:badloop}),
we get $\mathsf{K}^3\pbot\{\{2,5\}\} = \{\{4,5\}\}$, which is exactly the lift of the transformer semantics.
There is one serious problem: $\mathsf{K}$ fails to be increasing.
In particular, $\pbot\not\sqsubseteq\mathsf{K}\pbot$; for example $\pbot\{\{2,5\}\} = \{\emptyset\}$ but
$\H\pbot\{\{2,5\}\} = \{\{5\}\}$.
While this semantics merits further study, we leave it aside because we aim to use fixpoint fusion results that rely on Kleene approximation: This requires $\pbot\sqsubseteq\mathsf{K}\pbot$ in order to have an ascending chain, and the use of $\pbot$ so that $\dirimg{-}$ is strict.

\paragraph{A viable solution.}

Replacing singleton by powerset in the definition of $\otimes$, for
any h-transformers $\Phi,\Psi : \ppset\Sigma \to \ppset\Sigma$ we define the inner join $\ijoin$ by
\[
(\Phi\ijoin\Psi)\Q
= \{ r\mathbin{\mbox{\small$\cup$}} s \mid \some{p\in\Q}{r\in\Phi(\pset{\,p})\land s\in\Psi(\pset{\,p})} \}
\]
For semantics of conditionals, it is convenient to define, for boolean expression $b$,
this operator on h-transformers:
$\Phi\hycond{b}\Psi = \meansH{b}\c\Phi \ijoin \meansH{\neg b}\c\Psi$.
It satisfies
\begin{equation}\label{eq:defhycond}
 (\Phi\hycond{b}\Psi)\Q =
\{ r \mathbin{\mbox{\small$\cup$}} s \mid \some{p\in \Q}{
   r \in \Phi(\pset(\meansT{b}p)) \land
   s \in \Psi(\pset(\meansT{\neg b}p)) } \}
\end{equation}
because $\meansH{b}(\pset\,p) = \dirimg{\meansT{b}}(\pset\,p) = \pset(\meansT{b} p)$).
These operators are used in Fig.~\ref{fig:powtransem} for semantics of conditional and loop.

It is straightforward to prove $\ijoin$ is monotonic:
$\Phi\sqsubseteq\Phi'$ and $\Psi\sqsubseteq\Psi'$ imply $\Phi\ijoin\Psi \sqsubseteq \Phi'\ijoin\Psi'$.
It is also straightforward to prove
\begin{equation}\label{eq:joinijoin}
\dirimg{\phi\join\psi} \sqsubseteq \dirimg{\phi}\ijoin\dirimg{\psi}
\end{equation}
but in general equality does not hold, so we focus on $\hycond{\args}$.

\begin{lemma}
For any $b$, $\hycond{b}$ is monotonic:
$\Phi\sqsubseteq\Phi'$ and $\Psi\sqsubseteq\Psi'$ imply
$\Phi\hycond{b}\Psi \sqsubseteq \Phi'\hycond{b}\Psi'$.
\end{lemma}
\begin{proof}
Keep in mind this is $\sqsubseteq$ at the outer level:
$\Phi\sqsubseteq\Phi'$ means $\all{\Q}{\Phi\Q \subseteq \Phi'\Q}$ (more sets, not bigger sets, if you will).
This follows by monotonicity of $\ijoin$, or using characterization (\ref{eq:defhycond})
we have
\[ r\mathbin{\mbox{\small$\cup$}} s \in (\Phi\hycond{b}\Psi)\Q
\quad\mbox{ iff }\quad
\some{q\in\Q}{ r\in\Phi(\pset(\meansT{b}q)) \land
                    s\in\Psi(\pset(\meansT{\neg b}q)) }
\]
which implies
$\some{q\in\Q}{ r\in\Phi'(\pset(\meansT{b}q)) \land
                    s\in\Psi'(\pset(\meansT{\neg b}q)) }$
by $\Phi\sqsubseteq\Phi'$ and $\Psi\sqsubseteq\Psi'$.
\qed
\end{proof}

With $\meansH{ \ifc{b}{c}{d} }$ defined as in Fig.~\ref{fig:powtransem} we have the following refinement.

\begin{lemma}\label{lem:hcond}
$\dirimg{\meansT{ \ifc{b}{c}{d} }} \sqsubseteq \meansH{ \ifc{b}{c}{d}}$
provided that
$\dirimg{\meansT{c}} \sqsubseteq \meansH{c}$ and $\dirimg{\meansT{d}} \sqsubseteq \meansH{d}$.
\end{lemma}
\begin{proof}

  {\  } \vspace*{-2ex}

\begin{calcushort}
\flns{ \dirimg{\meansT{ \ifc{b}{c}{d} }} }
\plns{=}{ \dirimg{ \meansT{b}\c\meansT{c}\join\meansT{\neg b}\c\meansT{d} }}{semantics}
\plns{\sqsubseteq}{ \dirimg{\meansT{b}\c\meansT{c}}\ijoin\dirimg{\meansT{\neg b}\c\meansT{d} }
    }{by (\ref{eq:joinijoin})}
\plns{=}{ \meansH{b}\c\dirimg{\meansT{c}}\ijoin\meansH{\neg b}\c\dirimg{\meansT{d} }
    }{distribute $\dirimg{-}$ over $\c$, semantics}
\plns{\sqsubseteq}{ \meansH{b}\c\meansH{c}\ijoin\meansH{\neg b}\c\meansH{d}}{assumption, monotonicity}
\plns{=}{ \meansH{ \ifc{b}{c}{d} }}{semantics, def of $\hycond{b}$ from $\ijoin$}
\end{calcushort}
\qed
\end{proof}

This result suggests that we might be able to prove $\dirimg{\meansT{c}}\sqsubseteq\meansH{c}$ for all $c$, but that would be a weak link between the transformer and h-transformer semantics.  A stronger link can be forged as follows.

We say $\Q\in\ppset\Sigma$ is \dt{subset closed} iff $\Q = \mathsf{ssc}\,\Q$
where the subset closure operator $\mathsf{ssc}\,$ is defined by $p\in\mathsf{ssc}\,\Q$ iff $\some{q\in\Q}{p\subseteq q}$.
For example, the set $\A$ used in (\ref{eq:NI}) is subset closed.
Observe that $\mathsf{ssc}\, = \dirimg{\rsps}$.

\begin{lemma}\label{lem:imghycond}
For transformers $\phi,\psi:\pset\Sigma\to\pset\Sigma$ and condition $b$,
if $\Q=\mathsf{ssc}\, \Q$ then
\( \dirimg{ \meansT{b}\c \phi \join \meansT{\neg b}\c \psi }\Q \;=\; (\dirimg{\phi} \hycond{b} \dirimg{\psi})\Q \).
\end{lemma}
\begin{proof}
For the LHS, by definitions:
\begin{calcushort}
\flns{    \dirimg{ \meansT{b}\c \phi \join \meansT{\neg b}\c \psi }\Q }
\plns{=}{ \{ r\mathbin{\mbox{\small$\cup$}} s \mid \some{q\in\Q}{ r = \phi(\meansT{b}q) \land s = \psi(\meansT{\neg b}q) } \}
    \hspace*{3em} (*)}{}
\end{calcushort}
For the RHS, again by definitions:
\begin{calcushort}
\flns{     (\dirimg{\phi} \hycond{b} \dirimg{\psi})\Q }
\plns{=}{ \{ r\mathbin{\mbox{\small$\cup$}} s \mid \some{q\in\Q}{ r \in \dirimg{\phi}(\pset(\meansT{b}q)) \land
                                          s \in \dirimg{\psi}(\pset(\meansT{\neg b}q)) } \} }{}
\plns{=}{ \{ r\mathbin{\mbox{\small$\cup$}} s \mid \some{q\in\Q}{ \some{t,u}{
                                             t\subseteq \meansT{b}q \land
                                             u\subseteq \meansT{\neg b}q \land
                                             r = \phi t \land
                                             s = \psi u }} \}
    \hspace*{3em} (\dagger) }{}
\end{calcushort}
Now $(*)\subseteq (\dagger)$ by instantiating $t := \meansT{b}q$ and $u := \meansT{\neg b}q$, so LHS $\subseteq$ RHS is proved---as expected, given (\ref{eq:joinijoin}).
If $\Q$ is subset closed, we get $(\dagger)\subseteq(*)$ as follows.
Given $q,t,u$ in $(\dagger)$, let $q' := t\mathbin{\mbox{\small$\cup$}} u$.
Then $t=\meansT{b}q'$ and  $u=\meansT{\neg b}q$ because $\meansT{b}$ and $\meansT{\neg b}$ are filters.
And $q'\in\Q$ by subset closure.
Taking $q:=q'$ in $(*)$ completes the proof of RHS $\subseteq$ LHS.
\qed
\end{proof}

\paragraph{Preservation of subset closure.}

In light of Lemma~\ref{lem:imghycond}, we aim to restrict attention to h-transformers on subset closed sets.
To this end we introduce a few notations.
The subset-closed powerset operator $\Dpset$ is defined on powersets $\pset A$,
by
\begin{equation}\label{eq:Dpset}
\Q\in\Dpset(\pset A) \quad\mbox{iff}\quad \Q\subseteq \pset A \mbox{ and } \Q=\mathsf{ssc}\,\Q \mbox{ and } \Q\neq\emptyset
\end{equation}
To restrict attention to h-transformers of type $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$ we must show that subset closure is preserved by the semantic constructs.

For any transformer $\phi$,
define $\mathsf{PSC}\, \phi$ iff $(\rsps\c \phi) = (\phi\c\rsps)$.
The acronym is explained by the lemma to follow.
By definitions, the inclusion $(\rsps\c \phi) \supseteq (\phi\c\rsps)$ is equivalent to
\begin{equation}\label{eq:psc}
\all{q,r}{ \phi\, q \supseteq r \Rightarrow \some{s}{q\supseteq s \land \phi\, s = r}}
\end{equation}
Recall from Section~\ref{sec:rel} that the reverse,
$(\rsps\c \phi) \subseteq (\phi\c\rsps)$, is monotonicity of $\phi$.

\begin{lemma}\label{lem:psc}
$\mathsf{PSC}\,\phi$ implies $\dirimg{\phi}$ preserves subset closure.
\end{lemma}
\begin{proof}
For any subset closed $\Q$, $\dirimg{\phi}\Q$ is subset closed because
$\dirimg{\rsps}(\dirimg{\phi}\Q)
= \dirimg{\phi\c\rsps} \Q
= \dirimg{\rsps\c\phi} \Q
= \dirimg{\phi}(\dirimg{\rsps}\Q)
= \dirimg{\phi}\Q
$
using functoriality of $\dirimg{-}$, $\mathsf{PSC}\, \phi$, and $\mathsf{ssc}\,\Q = \Q$.
\qed
\end{proof}
It is straightforward to show $\mathsf{PSC}\,\bot$.
The following is a key fact, but also a disappointment that leads us
away from nondeterminacy.

\begin{lemma}\label{lem:pscR}
If $R$ is a partial function (i.e., $\converse{R}\c R\subseteq id$)
then $\mathsf{PSC}\,\dirimg{R}$.
\end{lemma}
\begin{proof}
In accord with (\ref{eq:psc}) we show for any $q,r$ that
$ r \subseteq \dirimg{R} q \Rightarrow \some{s\subseteq q}{\phi s = r}$.
Suppose $r \subseteq \dirimg{R} q$.
Let $s=(\dirimg{\converse{R}} r)\mathbin{\mbox{\small$\cap$}} q$, so for any $x$ we have
$x\in s$ iff $x\in q$ and $\some{y\in r}{x R y}$.
We have $s\subseteq q$ and it remains to show $\dirimg{R} s = r$, which holds because for any $y$
\begin{calcushort}
\flns{ y\in\dirimg{R} s }
\plns{\equiv}{ \some{x}{x \in s \land xRy} }{def $\dirimg{-}$}
\plns{\equiv}{ \some{x}{x\in q \land (\some{z}{z\in r \land xRz}) \land xRy }}{def $s$}
\plns{\equiv}{ \some{x}{x\in q \land y \in r \land xRy} }{$R$ partial function}
\plns{\equiv}{ y \in r}{$\Leftarrow$ by $r\subseteq \dirimg{R}q$ and def $\dirimg{-}$}
\end{calcushort}
\end{proof}

Using dots to show domain and range elements, the diagram on the left
is an example $R$ such that $\mathsf{PSC}\,\dirimg{R}$ but $R$ is not a partial function.
The diagram on the right is a relation, the image of which does not satisfy $\mathsf{PSC}\,$.
\begin{footnotesize}
\begin{center}
      \begin{tikzcd}
         \point \arrow[r,"",dash]
& \point\\
         \point \arrow[r,"",dash]
\arrow[ru,"",dash]
& \point\\
         \point \arrow[ru,"",dash]
& \point
      \end{tikzcd}
\qquad\qquad\qquad\qquad
      \begin{tikzcd}
         \point \arrow[r,"",dash] \arrow[rd,"",dash] & \point\\
         \point \arrow[r,"",dash] \arrow[ru,"",dash] & \point\\
         \point & \point
      \end{tikzcd}
\end{center}
\end{footnotesize}

As a consequence of Lemmas~\ref{lem:psc} and~\ref{lem:pscR} we have the following.
\begin{lemma}\label{lem:imgssc}
If $R$ is a partial function then $\dirimg{\dirimg{R}}:\ppset{A}\to\ppset{B}$ preserves subset closure.
\end{lemma}

\paragraph{The theorem.}

To prove $\meansH{c} = \dirimg{\meansT{c}}$,
we want to identify a subset of $\pset\Sigma\to\pset\Sigma$
satisfying two criteria.
First, $\meansT{\args}$ can be defined within it, so in particular it is closed under $\mathsf{G}$ in Figure~\ref{fig:transem}.
Second, on the subset, $\dirimg{-}$ is strict and continuous
into $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$, to enable the use of fixpoint fusion.
Strictness is the reason\footnote{In~\cite{ClarksonS10},
other reasons are given for using
$\{\emptyset\}$ rather than $\emptyset$ as the false hyperproperty.}
to disallow the empty set in (\ref{eq:Dpset});
it makes $\pbot$ (which equals $\dirimg{\bot}$) the least element, whereas otherwise the least element
would be $\lambda \Q \:\mbox{\small$\bullet$}\: \emptyset$.
We need the subset to be closed under pointwise union, at least for chains, so that $\dirimg{-}$ is continuous.

Given that $\dirimg{R}$ is universally disjunctive for any $R$,
Proposition~\ref{prop:reltran} suggests restricting to universally disjunctive transformers.
Lemma~\ref{lem:psc} suggests restricting to transformers satisfying $\mathsf{PSC}\,$.
But we were not able to show the universally disjunctive transformers satisfying $\mathsf{PSC}\,$ are closed under limits.
We proceed as follows.

Define $\Dom\, \phi = \{ x \mid \phi\{x\} \neq \emptyset \}$ and note that $\Dom\dirimg{R}=\rdom R$ where $\rdom R$ is the usual domain of a relation.
By a straightforward proof we have:

\begin{lemma}\label{lem:domInter}
For universally disjunctive $\phi$ and any $r$ we have $\phi\, r = \phi(r\mathbin{\mbox{\small$\cap$}} \Dom\, \phi)$.
\end{lemma}

\begin{lemma}\label{lem:domDisj}
For universally disjunctive $\phi,\psi$ with $\Dom\,\phi\mathbin{\mbox{\small$\cap$}}\Dom\,\psi = \emptyset$,
if $\mathsf{PSC}\, \phi$ and $\mathsf{PSC}\, \psi$ then $\mathsf{PSC}\,(\phi\join\psi)$.
\end{lemma}
\begin{proof}
For any $q,r$ with $r \subseteq (\phi\join\psi)q$ we need to show
$\some{s\subseteq q}{(\phi\join\psi)s = r}$.
First observe
\begin{calcu}
\fln{ r \subseteq (\phi\join\psi)q }
\pln{\equiv}{ r \subseteq \phi\, q \mathbin{\mbox{\small$\cup$}} \psi\, q }{def $\join$}
\pln{\equiv}{ r \subseteq \phi (q\mathbin{\mbox{\small$\cap$}} \Dom\,\phi) \mathbin{\mbox{\small$\cup$}} \psi(q\mathbin{\mbox{\small$\cap$}} \Dom\,\psi)}{Lemma \ref{lem:domInter}}
\pln{\Rightarrow}{ r = s \mathbin{\mbox{\small$\cup$}} s' \land s \subseteq \phi(q\mathbin{\mbox{\small$\cap$}} \Dom\,\phi)
                            \land s' \subseteq \psi(q\mathbin{\mbox{\small$\cap$}} \Dom\,\psi)}{set theory,
   letting  $s = r\mathbin{\mbox{\small$\cap$}} \phi (q\mathbin{\mbox{\small$\cap$}} \Dom\,\phi)$
   and $s' = r\mathbin{\mbox{\small$\cap$}} \psi(q\mathbin{\mbox{\small$\cap$}} \Dom\,\psi)$}
\pln{\Rightarrow}{ \some{t,t'}{t\subseteq q\mathbin{\mbox{\small$\cap$}}\Dom\,\phi \land t'\subseteq q\mathbin{\mbox{\small$\cap$}}\Dom\,\psi \land
               \phi\, t = s \land \psi\, t' = s' \land s\mathbin{\mbox{\small$\cup$}} s' = r } \quad (*)}{using $\mathsf{PSC}\,\phi$ and $\mathsf{PSC}\,\psi$}
\end{calcu}
We use $(*)$ to show that $t\mathbin{\mbox{\small$\cup$}} t'$ witnesses $\mathsf{PSC}\,(\phi\join\psi)$, as follows:
$ (\phi\join\psi)(t\mathbin{\mbox{\small$\cup$}} t')
= \phi(t\mathbin{\mbox{\small$\cup$}} t') \mathbin{\mbox{\small$\cup$}} \psi(t\mathbin{\mbox{\small$\cup$}} t')
= \phi t \mathbin{\mbox{\small$\cup$}} \psi t'
= s \mathbin{\mbox{\small$\cup$}} s'
= r
$
using also the definition of $\join$, and
$\phi(t\mathbin{\mbox{\small$\cup$}} t')=\phi\,t$ and
$\psi(t\mathbin{\mbox{\small$\cup$}} t')=\psi\,t'$ from Lemma~\ref{lem:domInter} and $(*)$.
\qed
\end{proof}

\begin{lemma}\label{lem:hycondSSC}
If $\Phi$ and $\Psi$ preserve subset closure then
$(\Phi\hycond{b}\Psi)\Q$ is subset closed (regardless of whether $\Q$ is).
\end{lemma}
\begin{proof}
Suppose
$q$ is in $(\Phi\hycond{b}\Psi)\Q$ and
$q' \subseteq q$.
So according to (\ref{eq:defhycond})
there are $r,s,p$ with
$p\in \Q$,
$q=r\mathbin{\mbox{\small$\cup$}} s$,
$r \in \Phi(\pset(\meansT{b}p))$, and
$s \in \Psi(\pset(\meansT{\neg b}p))$.
Let $r'=r\mathbin{\mbox{\small$\cap$}} q'$ and
    $s'=s\mathbin{\mbox{\small$\cap$}} q'$, so $r'\subseteq r$ and $s'\subseteq s$.
Because powersets are subset closed,
$\Phi(\pset(\meansT{b}p))$ and
$\Psi(\pset(\meansT{\neg b}p))$ are subset closed, hence
$r'\in\Phi(\pset(\meansT{b}p))$ and
$s'\in\Psi(\pset(\meansT{\neg b}p))$.
As $q'=r'\mathbin{\mbox{\small$\cup$}} s'$,
we have $q' \in (\Phi\hycond{b}\Psi)\Q$.
\qed
\end{proof}

It is straightforward to prove that $\Phi\ijoin\Psi$ preserves subset closure if $\Phi,\Psi$ do, similar to the proof of Lemma~\ref{lem:hycondSSC}.
By contrast, $\Phi\otimes\Psi$ does not preserve subset closure even if $\Phi$ and $\Psi$ do.

Next, we confirm that $\meansH{\args}$ can be defined within the monotonic functions
$\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$.

\begin{lemma}\label{lem:meansHpsc}
For all $c,\Q$, if $\Q$ is subset closed then so is $\meansH{c}\Q$, provided that
$\mathsf{PSC}\,\dirimg{\meansR{atm}}$ for every $atm$.
\end{lemma}
\begin{proof}
By induction on $c$.
\begin{itemize}
\item
$atm$:
$\meansH{atm}$ is $\dirimg{\dirimg{\meansR{atm}}}$ so by assumption
$\mathsf{PSC}\,\dirimg{\meansR{atm}}$ and Lemma~\ref{lem:psc}.

\item
$\keyw{skip}$: immediate.

\item
$c ; d$: by definitions and induction hypothesis.

\item
  $c\choice d$: by induction hypothesis and observation above about $\ijoin$.

\item
$\ifc{b}{c}{d}$: by Lemma~\ref{lem:hycondSSC} and induction hypothesis.

\item
$\whilec{b}{c}$:
Because $\pbot$ is least in $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$, we have $\pbot\sqsubseteq\H\pbot$,
so using monotonicity of $\H$ we have Kleene iterates.
Suppose $\Q$ is subset closed.
To show $\mathsf{lfp}\, \H \, \Q$ is subset closed, note that $\mathsf{lfp}\, \H = \H^\gamma \, \Q$ where $\gamma$ is some ordinal. We show that $\H^\alpha \, \Q$ is subset closed, for every $\alpha$ up to $\gamma$,
by ordinal induction.
\begin{itemize}
\item $\H^0 \, \Q = \Q$ which is subset closed.

\item $\H^{\alpha+1} \, \Q = (\meansH{c}\c \H^\alpha \hycond{b} \meansH{\keyw{skip}})\Q$ by definition of $\H$.
Now $\H^\alpha$ preserves subset closure by the ordinal induction hypothesis,
and $\meansH{c}$ preserves subset closure by the main induction hypothesis.
So $\meansH{c}\c \H^\alpha$ preserves subset closure, as does $\meansH{\keyw{skip}}$.
Hence $\meansH{c}\c \H^\alpha \hycond{b} \meansH{\keyw{skip}}$ preserves subset closure
by Lemma~\ref{lem:hycondSSC}.

\item $\H^\beta \, \Q = (\join_{\alpha<\beta} H^\alpha)\Q$ (for non-0 limit ordinal $\beta$),
which in turn equals
$\mathbin{\mbox{\small$\cup$}}_{\alpha<\beta} (H^\alpha \, \Q)$ because $\join$ is pointwise.
By induction, each $H^\alpha \, \Q$ is subset closed, and closure is preserved by union,
so we are done.
\qed
\end{itemize}
\end{itemize}
\end{proof}

Returning to the two criteria for a subset of $\pset\Sigma\to\pset\Sigma$,
suppose $\meansR{atm}$ is a partial function, for all $atm$ --- in short,
\dt{atoms are deterministic}.
If in addition $c$ is $\choice$-free, then $\meansR{c}$ is a partial function.
Under these conditions, by Proposition~\ref{prop:reltran}, $\meansT{c}$ is the direct image of a partial function.

Let $\mathsf{IPF}$ be the subset of $\pset\Sigma\to\pset\Sigma$ that are direct images of partial functions,
i.e.,
$\mathsf{IPF} = \{ \phi\in \pset\Sigma\to\pset\Sigma \mid
         \some{R}{\phi=\dirimg{R} \mbox{ and } \converse{R}\c R\subseteq id }  \}$.
Observe that $\mathsf{IPF}$ is closed under $\mathsf{G}$,
because for $\phi\in \mathsf{IPF}$ with $\phi=\dirimg{R}$ we have $\mathsf{G}\dirimg{R}
= \dirimg{\meansR{b}}\c\dirimg{\meansR{c}}\c\dirimg{R} \join
                        \dirimg{\meansR{\neg b}}
= \dirimg{\meansR{b}\c\meansR{c}\c R} \join
                        \dirimg{\meansR{\neg b}}
= \dirimg{\meansR{b}\c\meansR{c}\c R \mathbin{\mbox{\small$\cup$}} \meansR{\neg b}}$
and the union is of partial functions with disjoint domains
so it is a partial function.
We have $\bot\sqsubseteq \mathsf{G}\bot$ because $\bot$ is the least element
in $\pset\Sigma\to\pset\Sigma$.
By Lemma~\ref{lem:imgssc}, when $\dirimg{-}$ is restricted to $\mathsf{IPF}$, its range is included in
$\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$.
In $\mathsf{IPF}$, lubs of chains are given by pointwise union,
so $\dirimg{-}$ is a strict and continuous function
from $\mathsf{IPF}$ to $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$.

To state the theorem,
we write $\dot{=}$ for extensional equality
on h-transformers of type  $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$,
i.e., equal results on all subset closed $\Q$.

\begin{theorem}\label{thm:main}
$\dirimg{\meansT{c}} \; \dot{=} \; \meansH{c}$, provided atoms are deterministic and $c$ is $\choice$-free.
\end{theorem}
\begin{proof}
By induction on $c$.
For the cases of $\keyw{skip}$, atoms, and $\c$ the arguments preceding (\ref{eq:badcond}) are still valid.
For conditional, observe
\begin{calcushort}
\flns{ \dirimg{ \meansT{\ifc{b}{c}{d}}}}
\plns{\dot{=}}{ \dirimg{ \meansT{b}\c\meansT{c} \join \meansT{\neg b}\c\meansT{d} }}{semantics}
\plns{\dot{=}}{ \dirimg{\meansT{c}} \hycond{b} \dirimg{\meansT{d}} }{Lemma~\ref{lem:imghycond}}
\plns{\dot{=}}{ \meansH{c} \hycond{b} \meansH{d} }{induction hypothesis}
\plns{\dot{=}}{ \meansH{\ifc{b}{c}{d}} }{semantics}
\end{calcushort}
Finally, the loop:
\begin{calcushort}
\flns{ \dirimg{ \meansT{\whilec{b}{c}} }}
\plns{\dot{=}}{ \dirimg{ \mathsf{lfp}\, \mathsf{G} }}{semantics}
\plns{\dot{=}}{ \mathsf{lfp}\, \H }{fixpoint fusion, see below}
\plns{\dot{=}}{ \meansH{\whilec{b}{c}} }{semantics}
\end{calcushort}
The antecedent for fusion is
\( \all{\phi}{ \dirimg{\mathsf{G} \phi} = \H\dirimg{\phi} } \)
and it holds because for any $\phi$:
\begin{calcushort}
\flns{ \dirimg{ \mathsf{G} \phi } }
\plns{\dot{=}}{ \dirimg{ \meansT{b}\c\meansT{c}\c\phi \join \meansT{\neg b} }}{def $\mathsf{G}$}
\plns{\dot{=}}{ \dirimg{ \meansT{b}\c\meansT{c}\c\phi \join \meansT{\neg b}\c\meansT{\keyw{skip}} }}{skip law}
\plns{\dot{=}}{ \dirimg{ \meansT{c}\c\phi } \hycond{b} \dirimg{ \meansT{\keyw{skip}} } }{Lemma~\ref{lem:imghycond}}
\plns{\dot{=}}{ \dirimg{ \meansT{c} }\c\dirimg{ \phi } \hycond{b} \dirimg{\meansT{\keyw{skip}}} }{$\dirimg{-}$ distributes over  $\c$}
\plns{\dot{=}}{ \meansH{c}\c\dirimg{ \phi } \hycond{b} \meansH{\keyw{skip}} }{induction hypothesis}
\plns{\dot{=}}{ \H\dirimg{\phi} }{def $\H$}
\end{calcushort}
\end{proof}

\section{Specifications and refinement}\label{sec:spec}

We wish to conceive of specifications as miraculous programs that can
achieve by refusing to do, can choose the best angelically, and can compute the uncomputable.
We wish to establish rigorous connections between programs and specifications,
perhaps by deriving a program that can be automatically compiled for execution,
perhaps by deriving a specification that can be inspected to determine the usefulness or trustworthiness of the program.
A good theory may enable automatic derivation in one direction or the other,
but should also account for ad hoc construction of proofs.
Simple reasons should be expressed simply, so algebraic laws and transitive refinement chains are important.
In this inconclusive section, we return to the general notion of hyperproperty and consider how the h-transformer semantics sheds light on refinement for hyperproperties.  Initially we leave aside the signature/semantics notations.

Let $R:\Sigma\relto\Sigma$ be considered as a program, and $\mathbb{H}$ be a hyperproperty, that is, $\mathbb{H}$ is a set of programs.  Formally: $\mathbb{H}\in\pset(\Sigma\relto\Sigma)$.  For $R$ to satisfy $\mathbb{H}$ means, by definition, that $R\in\mathbb{H}$.
The example of possibilistic noninterference shows that in general trace refinement is unsound: $R\in \mathbb{H}$ does not follow from
$S\in \mathbb{H}$ and $S\supseteq R$.
It does follow in the case that $\mathbb{H}$ is subset closed.  Given that $\pset(\Sigma\relto\Sigma)$ is a huge space, one may hope that specifications of practice interest may lie in relatively tame subsets.  Let us focus on subset closed hyperproperties,
for which one form of chain looks like
\begin{equation}\label{eq:firstChain}
\mathbb{H} \;\Ni\;  S \supseteq \ldots \supseteq T \supseteq R
\end{equation}
Although this is a sound way to prove $R\in\mathbb{H}$, it does not seem sufficient, at least for examples like $\mathsf{NI}$ which require some degree of determinacy.  The problem is that for
intermediate steps of trace refinement it is helpful to use nondeterminacy for the sake of abstraction and underspecification, so finding suitable $S$ and $T$ may be difficult.
One approach to this problem is to use a more nuanced notion of refinement, that preserves a hyperproperty of interest.
For confidentiality, Banks and Jacob explore this approach in the setting of UTP~\cite{BanksJ10a}.

Another form of chain looks like
\begin{equation}\label{eq:secondChain}
 \mathbb{H} \supseteq \mathbb{S} \supseteq \ldots \supseteq \mathbb{T} \;\Ni\; R
\end{equation}
where most intermediate terms are at the hyper level, i.e., $\mathbb{S}$ and $\mathbb{T}$ are, like $\mathbb{H}$, elements of
$\pset(\Sigma\relto\Sigma)$.
The chain is a sound way to prove $R\in \mathbb{H}$, even if $\mathbb{H}$ is not subset closed.
But in what way are the intermediates $\mathbb{S},\mathbb{T},\ldots$ expressed, and by what reasoning are the containments established?  What is the relevant algebra, beyond elementary set theory?

The development in Section~\ref{sec:htrans} is meant to suggest a third form of chain:
\begin{equation}\label{eq:thirdChain}
  \ldots \sqsupseteq \mathbb{S} \sqsupseteq \ldots \sqsupseteq \mathbb{T} \sqsupseteq \dirimg{\dirimg{R}}
\end{equation}
Here the intermediate terms are of type $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$ and $\sqsubseteq$ is the pointwise ordering (used already in Section~\ref{sec:htrans}).
The good news is that if the intermediate terms are expressed using program notations, they may be amenable to familiar laws such as those of Kleene algebra with
tests~\cite{Kozen00,Struth16}, for which relations are a standard model.
A corollary of Theorem~\ref{thm:main} is that the laws hold for deterministic terms expressed in the signature (\ref{eq:signature}).
To make this claim precise one might spell out the healthiness conditions of elements in the range of $\meansH{\args}$,
but more interesting would be to extend the language with specification constructs, using (in)equational conditions like
$\converse{R}\c R \subseteq id$ as antecedents in conditional laws of healthy fragments.
We leave this aside in order to focus on a gap in our story so far.

The third form of chain is displayed with elipses on the left because we lack an account of specifications!
Our leading example, $\mathsf{NI}$, is defined as a set of relations, whereas
in (\ref{eq:thirdChain})
the displayed chain needs the specification, say $\Psi$, to have type $\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$.
The closest we have come is the characterization  $R\in\mathsf{NI}$ iff $\dirimg{\dirimg{R}}\A \subseteq \A$, see (\ref{eq:NI}).
But this is a set containment, whereas we seek $\Psi$ with
$R\in\mathsf{NI}$ iff $\Psi\sqsupseteq\dirimg{\dirimg{R}}$.
In the rest of this section we sketch two ways to proceed.

On the face of it, $\Psi\sqsupseteq\dirimg{\dirimg{R}}$ seems problematic because $\sqsupseteq$ is an ordering on functions.
Given a particular set $p\in\pset\Sigma$ with $\Agrl p$, a noninterfering  $R$ makes specific choice of value for $lo$ whereas specification $\Psi$ should allow any value for $lo$ provided that the choice does not depend on the initial value for $hi$.
One possibility is to escalate further and allow the specification to be a relation $\Dpset(\pset\Sigma)\relto\Dpset(\pset\Sigma)$.
To define such a relation, first lift the predicate $\Agrl$ on sets to the filter
$\widehat{\Agrl}: \pset(\pset\Sigma)\relto\pset(\pset\Sigma)$ defined by
\[ \widehat{\Agrl}\,\Q = \{ p\in \Q \mid \Agrl\, p \} \]
Note that  $\A = \widehat{\Agrl}(\pset\Sigma)$.
More to the point, $\widehat{\Agrl}\,\Q = \Q$ just if each $p\in\Q$ satisfies $\Agrl$.
Now define $\mathbf{NI}$,
as a relation
$\mathbf{NI} : \Dpset(\pset\Sigma)\relto\Dpset(\pset\Sigma)$,
by
\[ \P \:\mathbf{NI}\: \Q \quad\mbox{iff}\quad  \widehat{\Agrl}\,\P = \P \Rightarrow \widehat{\Agrl}\,\Q = \Q \]
This achieves the following: $R\in\mathsf{NI}$ iff $\mathbf{NI}\supseteq \dirimg{\dirimg{R}}$.
But this inclusion does not compose transitively with $\sqsupseteq$ in the third form of chain,
so we proceed no further in this direction.

The second way to proceed can be described using a variation on the h-transformer semantics
of Section~\ref{sec:htrans}.
It will lead us back to
the second form of chain, (\ref{eq:secondChain}), in particular for $\mathsf{NI}$ as $\mathbb{H}$.
The idea resembles UTP models of reactive processes~\cite[Chapt.~8]{HoareHe},
in which an event history is related to its possible extension.
Here we use just pre-post traces, as follows.
Let $\mathsf{Trc} = \Sigma\times\Sigma$.
Consider a semantics $\meansT{\args}'$ such that
$\meansT{c}'$ has type $\pset\mathsf{Trc}\to\pset\mathsf{Trc}$.
Instead of transforming an initial state to a final one
(or rather, state set as in $\meansT{\args}$),
an initial trace $(\sigma,\tau)$ is mapped to traces $(\sigma,\upsilon)$ for $\upsilon$ with $\tau \meansR{c} \upsilon$.
The semantics $\meansT{\args}'$ is not difficult to define (or see~\cite[sec.~2]{AssafNSTT17}).
The upshot is that for $S\in\pset\mathsf{Trc}$,
the trace set $\meansT{c}' S$ is the relation $S\c\meansR{c}$.
In particular, let $init$ be $id_{\Sigma}$, viewed as an element of $\pset\mathsf{Trc}$.
We get $\meansT{c}'init = \meansR{c}$, the relation denoted by $c$.
Lifting, we obtain a semantics $\meansH{\args}'$,
at the level $\ppset\mathsf{Trc}\to\ppset\mathsf{Trc}$,
such that
$\meansH{c}'\{init\}$ contains $\meansR{c}$.
(In light of Theorem~\ref{thm:main} and the discussion preceding it, we do not expect
$\meansH{c}'\{init\}$ to be just the singleton $\{ \meansR{c} \}$, as $\{init\}$ is not subset closed.)
This suggests a chain of the form
$\mathsf{NI} \supseteq \ldots \supseteq \Psi(\mathsf{ssc}\,\{init\}) \supseteq \meansH{c}'(\mathsf{ssc}\,\{init\}) \,\Ni\, \meansR{c} $
which proves that $\meansR{c}$ satisfies $\mathsf{NI}$ --- and which may be derived from a subsidiary chain of refinements
like $\Psi \sqsupseteq \meansH{c}'$ as in the third form of chain, independent of the argument $\mathsf{ssc}\,\{init\}$.

This approach has been explored in the setting of abstract interpretation, where the intermediate terms are obtained as a computable approximation of a given program's semantics.  To sketch the the idea we first review abstract interpretation for trace properties.
Mathematically, abstract interpretation is very close to data refinement, where intermediate steps involve changes of data representation.
For example, the state space $\Sigma$ of $R:\Sigma\relto\Sigma$ would be connected with another, say $\Delta$,
by a coupling relation $\rho:\Delta\relto\Sigma$ subject to a simulation condition such as
$S\c\rho \supseteq \rho\c R$, recall (\ref{eq:sim}).
With a functional coupling, the connection could be $\rho(\dirimg{S}\Delta) \sqsupseteq \dirimg{R}(\rho\Delta)$.

Let $T\in \Sigma\relto\Sigma$ be a trace set intended as a trace property specification.
In terms of the trace-computing semantics $\meansT{\args}'$ above, $c$ satisfies $T$ provided that
$T \supseteq \meansT{c}' init$.
It can be proved by the following chain, ingredients of which are to be explained.
\[
T \;\supseteq\; \gamma(\meansT{c}^\sharp \, a)
  \;\supseteq\; \meansT{c}'(\gamma\, a)
  \;\supseteq\; \meansT{c}' init
\]
Here $\gamma:A\to\pset\mathsf{Trc}$ is like $\rho$ above, mapping some convenient domain $A$ to traces.
The element $a\in A$ is supposed to be an approximation of the initial traces, i.e.,
$\gamma\,a \supseteq init$.
Thus the containment $\meansT{c}'(\gamma\,a) \supseteq \meansT{c}' init$ is by monotonicity of
semantics.
The next containment, $\gamma(\meansT{c}^\sharp a) \supseteq \meansT{c}'(\gamma a)$, involves
an ``abstract'' semantics $\meansT{c}^\sharp : A \to A$.
Indeed, the containment is the soundness requirement for such semantics.
What remains is the containment
$T \supseteq \gamma(\meansT{c}^\sharp \, a)$ which needs to be checked somehow.
Typically, $\gamma$ is part of a Galois connection, i.e., it has a lower adjoint $\alpha:\pset\mathsf{Trc}\to A$
and the latter check is equivalent to
$\alpha T \geq \meansT{c}^\sharp \, a$ where $\geq$ is the order on $A$.
Ideally it is amenable to automation, but that is beside the point.

The point is to escalate this story to the hyper level, in a chain of this form:
\[
\mathbb{H} \;\supseteq\; \gamma(\meansH{c}^\sharp \, a)
  \;\supseteq\; \meansH{c}'(\gamma\, a)
  \;\supseteq\; \meansH{c}'(\mathsf{ssc}\,\{init\})
  \;\,\Ni\;\,  \meansT{c}' init
\]
Now $\gamma$ has type $A\to\ppset\mathsf{Trc}$.
Again, the abstract semantics should be sound --- condition $\gamma(\meansH{c}^\sharp \, a) \supseteq \meansH{c}'(\gamma\, a)$ --- now with respect to a set-of-trace-set semantics $\meansH{\args}'$ that corresponds to our Fig.~\ref{fig:powtransem}.
The element $a\in A$ now approximates the set $\mathsf{ssc}\,\{init\}$
and $\meansH{c}'(\gamma\, a) \supseteq \meansH{c}'(\mathsf{ssc}\,\{init\})$ is by monotonicity.
The step $\mathbb{H} \supseteq \gamma(\meansH{c}^\sharp \, a)$ may again be checked at the abstract level
as $\alpha \mathbb{H} \geq \meansH{c}^\sharp \, a$.
Of course $\mathbb{H}$ is a hyperproperty so the goal is to prove the program is an element of $\mathbb{H}$.
This follows provided that
$\meansH{c}'(\mathsf{ssc}\,\{init\}) \; \Ni \;  \meansT{c}' init$,
a connection like our Theorem~\ref{thm:main} except for moving from $\pset\Sigma$ to $\pset\mathsf{Trc}$.

\section{Related work}\label{sec:related}

The use of algebra in unifying theories of programming has been explored in many works including the book that led to the UTP meetings~\cite{HoareHe,Sampaio97,HoareMSW11}.
Methodologically oriented works include the books by Morgan~\cite{Morgan:book} and by Bird and de
Moor~\cite{BirdDeM}.

The term hyperproperty was introduced by Clarkson and Schneider who among other things mention that refinement at the level of trace properties is admissible for proving subset closed hyperproperties~\cite{ClarksonS10}.
They point out that the topological classification of trace properties, i.e., safety and liveness, corresponds to similar notions dubbed hypersafety and hyperliveness.  Subset closed hyperproperties strictly subsume hypersafety.
As it happens, $\mathsf{NI}$ is in the class called 2-safety that specifies a property as holding for every pair of traces.
For fixed $k$, one can encode $k$-safety by a product program, each trace of which represents $k$ traces of the original.
Some interesting requirements, such as quantitative information flow, are not in $k$-safety for any $k$.

Epistemic logic is the topic of a textbook~\cite{HalpernEtalKnowl95}
and has been explored in the security literature~\cite{BalliuDG11}.
Mantel considers a range of security properties via closure operators~\cite{Mantel02}.
The limited usefulness of trace refinement for proving $\mathsf{NI}$ even for deterministic programs, as in the chain (\ref{eq:firstChain}), is discussed by Assaf and Pasqua~\cite{AssafNSTT17,MastroeniP18}.
The formulation of possibilistic noninterference as
$\mathring{\sim} \c R \c \mathring{\sim} \; = \; R\c\mathring{\sim}$ is due to Joshi and Leino~\cite{Joshi:Leino:SCP00}
and resembles the formulation of Roscoe et al.~\cite{RoscoeWW1994}.

The textbook of Back and von Wright~\cite{Back:book} explores predicate transformer semantics and refinement calculus.
The use of $sglt$ and $\Ni$ in (\ref{eq:relRecover}) is part of the extensive algebra connecting predicate transformers and relations using categorical notions~\cite{MartinSCP}.
Upward closed sets of predicates play an important role in that algebra~\cite{Naumann98},
which should be explored in connection with the present investigation and its potential application to higher order programs.
The extension of functional programming calculus to imperative refinement is one setting in which strong laws (Cartesian closure) for a well-behaved subset are expressed
as implications with inequational antecedents~\cite{Naumann95a,Naumann15}.
These works use backward predicate transformers in order to model general specifications and in particular the combination of angelic and demonic nondeterminacy.
Alternative models with similar aims can be found in
Martin \emph{et al}~\cite{MartinCR07} and Morris \emph{et al}~\cite{MorrisBT09}.

A primary precursor to this paper is the dissertion work of Assaf, which targets refinement chains in the style of abstract interpretation~\cite{CousotCousot79,Cou99}.
Assaf's work~\cite{AssafNSTT17}
introduced a set-of-sets lifted semantics
from which our h-transformer semantics is adapted.
In keeping with the focus on static analysis, Assaf shows the lifted semantics is an approximation of the underlying one.\footnote{Assaf \emph{et al} use fixpoint fusion in the inequational form mentioned following (\ref{eq:fusion}),
to prove soundness of the derived abstract semantics.
Their inequational result corresponding to our Theorem is proved, in the loop case, using explicit induction on approximation chains.
See the proof of Theorem~1 in~\cite{AssafNSTT17}.}
Assaf derives an abstraction $\meansH{c}^\sharp$ for dependency from $\meansH{c}$ (for every $c$), by calculation, following Cousot~\cite{Cou99} and similar to data refinement by calculation~\cite{HeHoareSanders86,Morgan:dr}.
For this purpose and others, it is essential that loops be interpreted by fixpoint at the level of sets-of-sets, so standard fixpoint reasoning is applicable,
as opposed to using $\dirimg{\meansT{\whilec{b}{c}}}$ which is not a fixed point per se.
In fact Assaf derives two abstract semantics $\meansH{c}^\sharp$:
one for dependency ($\mathsf{NI}$) and one that computes cardinality of low-variation, for quantitative information flow properties.  The cardinality abstraction is not in $k$-safety for any $k$.

Pasqua and Mastroeni have aims similar to Assaf \emph{et al}, and investigate several variations on set-of-set semantics of loops~\cite{MastroeniP18}.
Our example in Section~\ref{sec:htrans} is adapted from their work,
which uses examples to suggest that Assaf's definition (called ``mixed'' in~\cite{MastroeniP18}) is preferable.
They also point out that, for subset closed hyperproperties,
these variations are precise in the sense of our Theorem~\ref{thm:main},
strengthening the inequation in Assaf \emph{et al}.\footnote{Displayed formula  $\{ \meansT{c}T \mid T \in \mathbb{T} \} \subseteq \meansH{c}\mathbb{T}$
   following Theorem 1 of~\cite{AssafNSTT17}.}

A peculiarity of these works is the treatment of conditionals.
Assaf \emph{et al} take the equation $\meansH{\ifc{b}{c}{d}} = \dirimg{\meansT{\ifc{b}{c}{d}}}$ as the definition of $\meansH{\ifc{b}{c}{d}}$, but this makes the definition of $\meansH{\args}$ non-compositional and thus the inductive proofs a little sketchy.
We do not discern an explicit definition in~\cite{MastroeniP18},
but do find remarks like this: ``The definition of the collecting hypersemantics is just the additive lift\ldots for every statement, except for the while case.''
As a description of fact, it is true for subset closed hyperproperties (see our Theorem~\ref{thm:main}).
But it is unsuitable as a definition.
We show that a proper definition is possible.

Non-compositionality for sequence and conditional seems difficult to reconcile with proofs by induction on program structure.
It also results in anomalies, e.g., the formulation in Assaf \emph{et al} means that in case $c$ is a loop, the semantics of $c$
is different from the semantics of $\ifc{true}{c}{\keyw{skip}}$.
The obscurity is rectified when the semantics is restricted to subset closed sets,
as spelled out in detail in an unpublished note~\cite{GotliboymNaumann},
confirming remarks by Pasqua and Mastroeni~\cite{MastroeniP17}
elaborated in~\cite{MastroeniP18} and in the thesis of Pasqua.

Although similar to results in the preceding work, our results are novel in a couple of ways.
Our semantics is for a language with nondeterminacy, unlike theirs.
Of course, nondeterministic programs typically fail to satisfy $\mathsf{NI}$ and related properties,
and our theorem is restricted to deterministic programs.
A minor difference is that they formulate loop semantics in a standard form mentioned in Footnote~\ref{fn:tailrec} that asserts the negated guard following the fixpoint rather than as part of it.
Those works use semantics mapping traces to traces (or sets of sets thereof),
like our $\meansT{\args}'$ and $\meansH{\args}'$,
said to be needed in order to express dependency.
We have shown that states-to-states is sufficient to exhibit both the anomaly and its resolution.
It suffices for specifications of the form (\ref{eq:NI})
and may facilitate further investigation owing to its similarity to many variations on relational and transformer semantics.

Apropos $\mathsf{NI}$, the formulation (\ref{eq:NI}) is robust in the sense that it generalizes to more nuanced notions of dependency:
$\dirimg{\dirimg{R}} \P \subseteq \Q$ where $\P$ expresses agreement on some projections of the input (e.g., agreement on whether a password guess is correct, or agreement on some aggregate value derived from a sensitive database)
and $\Q$ expresses agreement on the observable output values.
Such policies are the subject of ~\cite{SabelfeldSandsDeclassJ}.

Banks and Jacob~\cite{BanksJ10a} formalize general confidentiality policies in UTP
and introduce a family of confidentiality preserving refinement relations.
The ideas are developed further in subsequent work
where confidentiality-violating refinements are represented as miracles~\cite{BanksJ14}
and knowledge is explicitly represented by sets encoding alternate executions,
an idea that has appeared in other guises~\cite{Morgan09,AssafN16}.

\section{Conclusion}\label{sec:concl}

We have given what, to the best of our knowledge, is the first
compositional definition of semantics at the hyper level.
Moreover, we proved that it is the lift of a standard semantics when restricted to subset closed hyperproperties.  The latter is a ``forward collecting semantics''
in the terminology of abstract interpretation.
The new semantics includes nondeterministic constructs, although the lifting equivalence is only proved for the deterministic fragment.

Although deterministic noninterference is a motivating example, there are other interesting hyperproperties such as quantitative information flow that can be expressed in subset closed form
and which are meaningful for nondeterministic programs.
This is one motivation for further investigation including the following questions.
$\bullet$
Restricting to subset closed hyperproperties is sufficient to make possible a compositional fixpoint semantics at the hyper level that accurately represents the underlying semantics --- is it necessary?
$\bullet$ The h-transformer semantics allows nondeterministic choice and nondeterministic atoms that satisfy $\mathsf{PSC}\,$ (in light of Lemma~\ref{lem:meansHpsc}), and in fact the definitions
can be used for a semantics in $\pset(\pset\Sigma)\to\pset(\pset\Sigma)$, into which
$\Dpset(\pset\Sigma)\to\Dpset(\pset\Sigma)$ embeds nicely owing to joins being pointwise ---
but what exactly is the significance of determinacy?
$\bullet$ Are disjunctive transformers satisfying $\mathsf{PSC}\,$ closed under join?
What is a good characterization of transformers that are images of relations?

A person not familiar with unifying theories of programming may wonder whether programs are specifications.
Indeed, the author was once criticized by a famous computer scientist who objected to refinement calculi on the grounds that underspecification and nondeterminacy are distinct notions that ought not be confused --- though years later he published a soundness proof for a program logic, in which that confusion is exploited to good effect.
A positive answer to the question can be justified by embedding programs in a larger space of specifications, in a way that faithfully reflects a given semantics of programs.
Our theorem is a result of this kind.  The larger space makes it possible to express important requirements such as noninterference.
However, we do not put forward a compelling notion of specification that encompasses hyperproperties and supports a notion of refinement analogous to existing notions for trace properties.  Rather, we hope the paper inspires or annoys the reader enough to provoke further research.

\medskip

\textbf{Acknowledgements.}
Anonymous reviewers offered helpful suggestions
and pointed out errors, omissions, and infelicities in an earlier version.

The authors were partially supported by NSF award 1718713.

\bibliographystyle{splncs04}

redpajama_set_name: RedPajamaArXiv


text:
package com.amazonaws.services.codecommit.model;

import java.io.Serializable;
import javax.annotation.Generated;

/**
 *
 * @see AWS API
 *      Documentation
 */
@Generated("com.amazonaws:aws-java-sdk-code-generator")
public class ListPullRequestsResult extends com.amazonaws.AmazonWebServiceResult<com.amazonaws.ResponseMetadata> implements Serializable, Cloneable {

    /**
     *

     * The system-generated IDs of the pull requests.
     *

     */
    private java.util.List<String> pullRequestIds;
    /**
     *

     * An enumeration token that allows the operation to batch the next results of the operation.
     *

     */
    private String nextToken;

    /**
     *

     * The system-generated IDs of the pull requests.
     *

     *
     * @return The system-generated IDs of the pull requests.
     */

    public java.util.List<String> getPullRequestIds() {
        return pullRequestIds;
    }

    /**
     *

     * The system-generated IDs of the pull requests.
     *

     *
     * @param pullRequestIds
     *        The system-generated IDs of the pull requests.
     */

    public void setPullRequestIds(java.util.Collection<String> pullRequestIds) {
        if (pullRequestIds == null) {
            this.pullRequestIds = null;
            return;
        }

        this.pullRequestIds = new java.util.ArrayList<String>(pullRequestIds);
    }

    /**
     *

     * The system-generated IDs of the pull requests.
     *

     *

     * NOTE: This method appends the values to the existing list (if any). Use
     * {@link #setPullRequestIds(java.util.Collection)} or {@link #withPullRequestIds(java.util.Collection)} if you want
     * to override the existing values.
     *

     *
     * @param pullRequestIds
     *        The system-generated IDs of the pull requests.
     * @return Returns a reference to this object so that method calls can be chained together.
     */

    public ListPullRequestsResult withPullRequestIds(String... pullRequestIds) {
        if (this.pullRequestIds == null) {
            setPullRequestIds(new java.util.ArrayList<String>(pullRequestIds.length));
        }
        for (String ele : pullRequestIds) {
            this.pullRequestIds.add(ele);
        }
        return this;
    }

    /**
     *

     * The system-generated IDs of the pull requests.
     *

     *
     * @param pullRequestIds
     *        The system-generated IDs of the pull requests.
     * @return Returns a reference to this object so that method calls can be chained together.
     */

    public ListPullRequestsResult withPullRequestIds(java.util.Collection<String> pullRequestIds) {
        setPullRequestIds(pullRequestIds);
        return this;
    }

    /**
     *

     * An enumeration token that allows the operation to batch the next results of the operation.
     *

     *
     * @param nextToken
     *        An enumeration token that allows the operation to batch the next results of the operation.
     */

    public void setNextToken(String nextToken) {
        this.nextToken = nextToken;
    }

    /**
     *

     * An enumeration token that allows the operation to batch the next results of the operation.
     *

     *
     * @return An enumeration token that allows the operation to batch the next results of the operation.
     */

    public String getNextToken() {
        return this.nextToken;
    }

    /**
     *

     * An enumeration token that allows the operation to batch the next results of the operation.
     *

     *
     * @param nextToken
     *        An enumeration token that allows the operation to batch the next results of the operation.
     * @return Returns a reference to this object so that method calls can be chained together.
     */

    public ListPullRequestsResult withNextToken(String nextToken) {
        setNextToken(nextToken);
        return this;
    }

    /**
     * Returns a string representation of this object. This is useful for testing and debugging. Sensitive data will be
     * redacted from this string using a placeholder value.
     *
     * @return A string representation of this object.
     *
     * @see java.lang.Object#toString()
     */
    @Override
    public String toString() {
        StringBuilder sb = new StringBuilder();
        sb.append("{");
        if (getPullRequestIds() != null)
            sb.append("PullRequestIds: ").append(getPullRequestIds()).append(",");
        if (getNextToken() != null)
            sb.append("NextToken: ").append(getNextToken());
        sb.append("}");
        return sb.toString();
    }

    @Override
    public boolean equals(Object obj) {
        if (this == obj)
            return true;
        if (obj == null)
            return false;

        if (obj instanceof ListPullRequestsResult == false)
            return false;
        ListPullRequestsResult other = (ListPullRequestsResult) obj;
        if (other.getPullRequestIds() == null ^ this.getPullRequestIds() == null)
            return false;
        if (other.getPullRequestIds() != null && other.getPullRequestIds().equals(this.getPullRequestIds()) == false)
            return false;
        if (other.getNextToken() == null ^ this.getNextToken() == null)
            return false;
        if (other.getNextToken() != null && other.getNextToken().equals(this.getNextToken()) == false)
            return false;
        return true;
    }

    @Override
    public int hashCode() {
        final int prime = 31;
        int hashCode = 1;

        hashCode = prime * hashCode + ((getPullRequestIds() == null) ? 0 : getPullRequestIds().hashCode());
        hashCode = prime * hashCode + ((getNextToken() == null) ? 0 : getNextToken().hashCode());
        return hashCode;
    }

    @Override
    public ListPullRequestsResult clone() {
        try {
            return (ListPullRequestsResult) super.clone();
        } catch (CloneNotSupportedException e) {
            throw new IllegalStateException("Got a CloneNotSupportedException from Object.clone() " + "even though we're Cloneable!", e);
        }
    }

}

redpajama_set_name: RedPajamaGithub


FB SEO Org ("FB SEO Org") operates fairbairnpb.com and may operate other websites. It is FB SEO Org's policy to respect your privacy regarding any information we may collect while operating our websites.
Like most website operators, FB SEO Org collects non-personally-identifying information of the sort that web browsers and servers typically make available, such as the browser type, language preference, referring site, and the date and time of each visitor request. FB SEO Org's purpose in collecting non-personally identifying information is to better understand how FB SEO Org's visitors use its website. From time to time, FB SEO Org may release non-personally-identifying information in the aggregate, e.g., by publishing a report on trends in the usage of its website.
FB SEO Org also collects potentially personally-identifying information like Internet Protocol (IP) addresses for logged in users and for users leaving comments on fairbairnpb.com blogs/sites. FB SEO Org only discloses logged in user and commenter IP addresses under the same circumstances that it uses and discloses personally-identifying information as described below, except that commenter IP addresses and email addresses are visible and disclosed to the administrators of the blog/site where the comment was left.
Certain visitors to FB SEO Org's websites choose to interact with FB SEO Org in ways that require FB SEO Org to gather personally-identifying information. The amount and type of information that FB SEO Org gathers depends on the nature of the interaction. For example, we ask visitors who sign up at fairbairnpb.com to provide a username and email address. Those who engage in transactions with FB SEO Org are asked to provide additional information, including as necessary the personal and financial information required to process those transactions. In each case, FB SEO Org collects such information only insofar as is necessary or appropriate to fulfill the purpose of the visitor's interaction with FB SEO Org. FB SEO Org does not disclose personally-identifying information other than as described below. And visitors can always refuse to supply personally-identifying information, with the caveat that it may prevent them from engaging in certain website-related activities.
FB SEO Org may collect statistics about the behavior of visitors to its websites. FB SEO Org may display this information publicly or provide it to others. However, FB SEO Org does not disclose personally-identifying information other than as described below.
FB SEO Org discloses potentially personally-identifying and personally-identifying information only to those of its employees, contractors and affiliated organizations that (i) need to know that information in order to process it on FB SEO Org's behalf or to provide services available at FB SEO Org's websites, and (ii) that have agreed not to disclose it to others. Some of those employees, contractors and affiliated organizations may be located outside of your home country; by using FB SEO Org's websites, you consent to the transfer of such information to them. FB SEO Org will not rent or sell potentially personally-identifying and personally-identifying information to anyone. Other than to its employees, contractors and affiliated organizations, as described above, FB SEO Org discloses potentially personally-identifying and personally-identifying information only in response to a subpoena, court order or other governmental request, or when FB SEO Org believes in good faith that disclosure is reasonably necessary to protect the property or rights of FB SEO Org, third parties or the public at large. If you are a registered user of an FB SEO Org website and have supplied your email address, FB SEO Org may occasionally send you an email to tell you about new features, solicit your feedback, or just keep you up to date with what's going on with FB SEO Org and our products. If you send us a request (for example via email or via one of our feedback mechanisms), we reserve the right to publish it in order to help us clarify or respond to your request or to help us support other users. FB SEO Org takes all measures reasonably necessary to protect against the unauthorized access, use, alteration or destruction of potentially personally-identifying and personally-identifying information.
If FB SEO Org, or substantially all of its assets, were acquired, or in the unlikely event that FB SEO Org goes out of business or enters bankruptcy, user information would be one of the assets that is transferred or acquired by a third party. You acknowledge that such transfers may occur, and that any acquirer of FB SEO Org may continue to use your personal information as set forth in this policy.


text:
Please Stop Demonizing Christmas
During a recent trip to El Salvador, a pastor and I were talking about how much we both love Christmas music. We shared some of the songs on our personal playlists, and then he told me that his wife is especially fond of songs like "It's the Most Wonderful Time of the Year" and "Let It Snow" because the church she grew up in discouraged members from celebrating Christmas or hanging any type of holiday decorations.
By J. Lee Grady
Her story reminded me that several Charisma readers jumped on me a few years ago after I wrote a column about Christmas. They were angry because they consider Christmas a pagan holiday that is luring gift-giving revelers into hell itself. One person who identified himself as "Albert" wrote in our online forum that he "isn't comfortable celebrating Christmas" because of its "demonic origins."
You probably know there are many Christians who boycott Christmas for various reasons—some factual and some quite debatable. These people insist:
o The holiday has become too commercialized and promotes greed. (I can't really argue with that.)
o No one knows when Jesus was born. (True—and the Bible is silent about the date.) However, "Albert" and other anti-Christmas purists insist Jesus was born on Sept. 11, in 3 B.C., during Rosh Hoshana.
o The Dec. 25 date was chosen to "Christianize" the pagan celebration of Saturnalia, an ancient winter solstice festival. (Probably true—but is there anything wrong with Christianizing something? I'm glad a pagan celebration was replaced.)
o Christmas trees are a pagan tradition, since druids believed evergreen boughs were magical and had the power to scare away demons. ("Thursday" is also named for the Norse god Thor, but that doesn't mean I worship him when I use the word.)
o Dec. 25 is the birthday of Nimrod, who later became known as the pagan god Baal, who later became known as Nicolas, who later became known as Santa Claus. For this reason, we can be sure that demons lurk behind all wreaths, candles, ornaments, fruitcakes, sleighs or anyone dressed in red and green.
o "Santa" is just a jumbled misspelling of "Satan"! (Seriously?)
In all fairness to these Christmas critics, I will admit I never encouraged my children to believe in Santa Claus. This was not because I was afraid he was Baal, Nimrod or an ancient Turkish bishop in disguise, but because 1) I felt I would be lying to my kids if I told them Santa brought them gifts; 2) I hate standing in lines at department stores; and 3) the prospect of inviting a strange old man into my house so he can "check" on my sleeping daughters is downright creepy.
But I unashamedly love Christmas. I love the trees, the ornaments, the lights, the smells, the eggnog, the music, the gifts and the family and friends who share the celebration with me. All the decorations point me to Jesus—from the bells on the front porch to the angel on top of the tree to the plastic manger scene that shows some wear (mainly because our dachshund, Flapjack, chewed a shepherd's head off in 1996.)
For me, Christmas is a wondrous time of year when I ponder the miracle of Christ's birth and, hopefully, get lots of chances to share his generous love with people who are less fortunate than I am.
People have been fighting about Christmas for a long time. Christmas gift-giving was condemned by the Catholic Church during the Middle Ages because of the "pagan origins" of the holiday. Then, anti-Catholic Puritans declared war on Christmas in England and banned it from 1647 to 1660, calling it "a popish festival with no justification." In the United States, Puritans outlawed Christmas in Massachusetts from 1659 to 1681, and it was an unpopular holiday after the Revolutionary War because Americans associated it with England.
Christmas became a federal holiday in 1870. Yet today, in spite of the fact that Christmas has morphed into a meaningless mush of secularized snowflakes, reindeer, penguins, gift cards and year-end sales, the Scrooges of our day want to suck all the remaining Christian spirituality out of it.
I expect atheists to hate Christmas. I know they will try to ban nativity scenes from public parks or remove Christmas carols from classrooms. But it is downright tragic when Christians—who should welcome every opportunity to bring the miracle of Jesus' incarnation into public life—start bah-humbugging (or even demonizing) the holiday.
Keep Christmas in your own way, by all means. If it's offensive to you to hang mistletoe from your mantle or to send a Christmas card to friends, then don't. I won't judge you for that. But please don't judge other believers simply because they want to celebrate all that is pure and decent and meaningful this special time of year.
P.S. Merry Christmas!
J. Lee Grady was editor of Charisma for 11 years before he launched into full-time ministry in 2010. Today he directs The Mordecai Project, a Christian charitable organization that is taking the healing of Jesus to women and girls who suffer abuse and cultural oppression.

redpajama_set_name: RedPajamaCommonCrawl


text:
Q: How do I remove leading text from this string How do I remove all the chars up to the number 41 in this line
all the way to the number 41
##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin

A: It's unclear to me whether or not you want the 41 included in your output. Accordingly here are two sets of options
1. Removing text upto and including 41
If you are running bash you can use built-in variable processing
line='##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin'
printf "%s\n" "${line#*41}"

If you can guarantee that there is no other 41 on the line you could use sed
line='##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin'
printf "%s\n" "$line" | sed 's/^.*41//'

If you have GNU grep you can pick off everything following the 41
line='##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin'
printf "%s\n" "$line" | grep -Po '(?<=41).*'

2. Removing text upto but excluding 41, using the ## as a marker
If you are running bash you can use built-in variable processing
line='##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin'
printf "%s\n" "${line#*?##}"

If you can guarantee that there is no other ## on the line you could use sed
line='##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin'
printf "%s\n" "$line" | sed 's/^..*##//'

If you have GNU grep you can pick off everything following the ##
line='##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin'
printf "%s\n" "$line" | grep -Po '(?<=.##).*'

A: You could use sed to remove everything until the first digit
echo '##SHUTDOWN_MAINT##41 * * * * /vend/oracle/util/bin' | sed 's/[^0-9]*//'
If you want change it in a file use
sed -i 's/[^0-9]*//' filename
Hope that helps
Cheers

redpajama_set_name: RedPajamaStackExchange


text:
Welcome to Cyberia
Arturo Escobar, (1994) Current Anthropology
In "Welcome to Cyberia, Arturo Escobar provides details how anthropological research methods can be used to explore and better understand cyberculture. The fact that "technologies are bringing about a fundamental transformation in the structure and meaning of modern society" (211) warrants an anthropological approach to research. According to Escobar, to articulate an "anthropology of cyberculture" (211) we need to move away from the idea that technology is value-neutral and independent of socioeconomic and political contexts. Taking a constructivist approach, we could recognize the situated-ness of tech and its relationship to social processes in order to reveal the inter-relatedness of technology, society, and nature. Research from this perspective would result in "a multipath and multilevel evolutionary model of technological change" (212) that identifies socially relevant groups and their interpretations of the technologies they encounter to provide insight into the common uses of technologies and their adoption.
An inquiry into cyberculture necessitates reflection upon the notion of modernity, where we situate ourselves in relation to it , and the arrangement of life within this period. (Post? Escobar: perhaps we have not left it since capital and science still dominate) Drawing on Foucault, if modernity is characterized by certain arrangements life, labor, language, and related practices, it would be important to investigate whether or not (and how) cyberculture reproduces these arrangements. Acknowledging these arrangements is important because modernity "constitutes the 'background of understanding' – the taken for granted tradition and way of being…that inevitably shapes the discourses and practices generated by and around the new technologies." (214) For example, modernity has supplied us with the idea of technology as a neutral tool that draws on natural energy to transform everyday life. {While likely the creation and use of tech relies on resources and assumptions such as: building these technologies via labor and resources provides greater good to the world than protecting the welfare of the individuals and environments that is required to create it.}
To study technology anthropologically, one could investigate the rituals it initiates, the social relations it creates, the practices users develop, and values the users/technologies foster. Though Escobar focuses on AI and Biotech, the anthropological inquiries he outlines could be applied more broadly:
*"What new forms of social construction of reality ('technoscapes') and of negotiation of such construction(s) are introduced by new technology? How do people routinely engage technoscapes, and what are the consequences of doing so in terms of the adoption of new ways of thinking and being?"*
"What established anthropological concepts and methods would be appropriate to the study of cyberculture?" How will notions of community/fieldwork/the body/nature/writing/etc. Be transformed by tech? (some answers starting to emerge on this already)
Which modern practices (life, labor, language) shape our relations to tech?
What is the political economy of tech? How does the local reflect the flows of global capital?
Reflecting that "only with modern science and technology studies has the possibility arisen of seeing science and technology in relation to complex techno social systems" (215), Escobar highlights several past attempts to articulate an anthropological investigation of science and tech. He mentions Margaret Mead's work in cybernetics as an important precursor to 3 projects:
David Thomas' work on cyberspace and the cyborg and the social productions of certain technologies and virtual worlds
"Cyborg Anthropology – ethnographic study of the boundaries between humans and machines" displacing "Anthropos" as the main unit of study coming to the understanding that "human and social reality is as much a product of machines as of human activity, that we should grant agency to machines…to examine ethnographically how technology serves as an agent of social and cultural production." (216)
"'Anthropology of, and in, cyberspace' [in which] anthropologists would study technologies in the cultural contexts from which they originate and in which they operate…[in order to] describe, in the manner of an initial cultural diagnosis, what is happening in terms of the emerging practices and transformations associated with rising techno-scientific developments." (216)
Regardless of which approach is taken, "all of these analyses need to take into account the social and cultural relations of science and technology as central mechanism for the production of life and culture in the 21st century" keeping in mind that capital will continue to play a dominant role in shaping life and society and reinventing nature for its own exploitation. Some anthropological investigations of tech that Escobar suggests include:
Production and use of new technologies – following scientists and experts through development etc.
The production of subjectivities, computer as "an evocative object", "technologies of the self"
Reconstruction of space and the body
Computer-mediated communities and "interface anthropology" that investigates human/computer interfaces
Effect of science and tech development on popular imaginaries and the "aesthetic and practical incorporation of technology into daily life"
Techno-literacy and practices that help people use and relate to new tech
Computer-mediated communication, human interaction via computers, changes in communicative and linguistic practices, and relationship between machines and subjects to produce discourse(s)
Political economy of cyberculture, tech and changes in capital accumulation, the relationship between information and capital, possible "mode of information" much like "mode of production", and how information, science and tech have become crucial to capital accumulation, etc.
Escobar's "Welcome to Cyberia" provides simulating ideas for jumping off points and methodological possibilities for exploring use of technology in higher education. More on that HERE.
Cite: Escobar, A. (1994) "Welcome to Cyberia: Notes on the Anthropology of Cyberculture". Current Anthropology 35(3), 211-231.
constructivist, cyberculture, escobar, Summary, technospaces
Anthropology, methods
The Writing Thing (AKA: Why Writing is Important)
Learning Spaces, learning environments and the 'dis'placement of learning
Posts by Laurie
OpenCUNY is Hiring!
Event Recap & Resources: Managing your Digital Footprint
Managing Your Digital Footprint
Join Us: March 28 @6:30pm to Discuss Using OpenCUNY to Support Your Student Group
Comments by Laurie


text:
«Omplim Madrid» fou una iniciativa ciutadana promoguda a les xarxes socials per entitats sobiranistes, com l'Assemblea Nacional Catalana i Òmnium Cultural, consistent en una manifestació el 16 de març de 2019 a les 18:00 de la tarda a Madrid per reclamar el dret a decidir de Catalunya i l'alliberament dels presos polítics catalans que havien defensat la creació de la República Catalana, en el context del judici al procés independentista català. Els lemes de la manifestació van ser: «L'autodeterminació no és delicte» i «Democràcia és decidir». El recorregut de la manifestació, encapçalada pel president de la Generalitat de Catalunya, Quim Torra, el president del Parlament de Catalunya, Roger Torrent, i altres representants dels partits independentistes (Junts, ERC i CUP), va tenir lloc al llarg del passeig del Prado, entre les places d'Atocha i de Cibeles. La Policia Nacional Espanyola informà que la manifestació concentrà 18.000 persones, mentre que l'organització xifrà en 120.000 els assistents. Altres fonts, com el diari El País, parlaren de 55.000 persones.

Referències

Vegeu també
 Independentisme català
 Omplim Brussel·les
 Omplim Estrasburg

Enllaços externs

Manifestacions del procés independentista català
Esdeveniments a Madrid
Manifestacions del segle XXI
2019 a Espanya

redpajama_set_name: RedPajamaWikipedia