---
abstract: |
    In cyber-physical systems, software may control safety-significant operations. This report discusses a method to structure software testing to measure the statistical confidence that algorithms are true to their intended design. The subject matter appears in two main parts: theory, which shows the relationship between discrete systems theory, software, and the actuated automaton; and application, which discusses safety demonstration and indemnification, a safety assurance metric.

    The recommended form of statistical testing involves sampling algorithmic behavior in a specific area of safety risk known as a hazard. When this sample is random, it is known as a safety demonstration. It provides evidence for indemnification, a statistic expressing an assured upper bound for accident probability. The method obtains results efficiently from practical sample sizes.

    Keywords: software, safety, hazard, demonstration, operational profile, automata, confidence, statistics
author:
- '\'
title: Software Safety Demonstration and Indemnification
---

\[section\] \[theorem\][Lemma]{} \[theorem\][Corollary]{} \[theorem\][Conjecture]{} \[theorem\][Fact]{}

\[theorem\][Definition]{}

Prologue
========

Copyright {#S:COPYRIGHT}
---------

This document may be freely copied or modified in accordance with the Creative Commons Attribution license[^1].

Executive summary {#S:EXECUTIVE_SUMMARY}
-----------------

In systems of integrated hardware and software, the intangible nature of software raises the question of fitness in roles bearing safety risk. Such a safety risk in software, known as a hazard, is a region of code involving safety constraints (requirements) necessitating some degree of verification. Hazards are identified and monitored by safety engineers, and possess hypothetical (threatened) frequency and severity ratings. During its development, potentially hazardous software merits not only rigorously controlled general engineering process, but also quantitative assurance of hazards within particular products.

### Approach {#S:APPROACH}

The topic of this essay is assuring the interplay between safety constraints (requirements) and software control. Software is appreciated as a branching process whose permutations are intractably numerous to test exhaustively. Barring exhaustive testing, statistical verification remains an option.

The degree of statistical verification will be expressed as residual risk, a contravariant quantity. A software item’s total risk has many constituents. For instance, any software communicating with an operator runs human factors risk. Statistical safety risk, one constituent of total risk, focuses on hazardous code. Code is potentially hazardous if its statistical risk (numerical product of frequency of execution, probability of error, and expected safety loss per error) is sufficiently high.

The subject matter results from applying standard mathematics to a well-known (but cloudy) problem. It is organized according to a mathematized version of the Joint Software Systems Safety Engineering Handbook[@DD10] of the United States Department of Defense (2010). This mathematization affords a deeper structural view of safety engineering. This view inspires a unification of that document’s risk management goals, and exerts commonality against its disparate hardware and software risk disciplines.

### Synopsis {#S:SYNOPSIS}

A hazard in software is a region of code involving safety requirements, whose logical correctness is essential to *safe* operation (hazards do not embrace all forms of software error). This condition motivates some degree of formal verification of correctness. Hazards are measured according to their statistical risk, which is the numeric product of three factors associated with a software point. First is the point’s frequency of execution. Second is the probability of encountering error during execution of a code trajectory that reaches the point. Third is the point’s severity, its safety consequence (loss) per error.

Software safety assurance may be accomplished via management of statistical risk. It is organized into two phases. First is guestimation, which uses expert opinion to yield a rough ranking of hazard risks, based on the three constituents. The subject of this essay is the approximation phase which follows, producing refined post-development risk for each hazard. This refinement, following hardware practice, is known as a residual risk.

Data for calculation of each residual risk is drawn from a collection of specially constructed tests called a demonstration. Because error is associated with software sequences rather than points, demonstrations exercise a variety of approaching trajectories. Each demonstration does produce a maximum-likelihood estimate of the probability of walking into error, but this figure isn’t useful because it is usually zero. Define the indifference upper bound as the upper bound at 50% confidence, so the odds of underestimation balance those of overestimation. The indifference upper bound yields unbiased assurance.

Indemnification is the risk level assured by the indifference upper bound on proportion failing some test of a demonstration. The indifference upper bound, which is non-zero, functionally replaces the maximum-likelihood estimate. Owing to its definition as a confidence upper bound, indemnification is also a quality assurance metric on completeness of safety testing relative to risk level. This essay proposes a re-unification of hardware and software risk, prescribing that statistical risk become the common standard bearer.

### Significance {#S:SIGNIFICANCE}

Profound difference exists between this essay’s proposal and current standards such as MIL-STD-882E and its companion Joint Software Systems Safety Engineering Handbook. Present adherents of MIL-STD-882E must break new procedural ground if they intend to evaluate statistical risk. The protocol confuses statistical assurance with other techniques for design vetting. Perhaps in an effort to encompass both, the standard’s analysis describes a hierarchy for software based on safety impact: potential human intervention, redundancy, or level of safety responsibility. This protocol’s measure is a hierarchy of discrete categories rather than a continuum variable. It may enable some types of analysis, but it renders statistical risk assessment impossible.

These standards modify the definition of risk, preferring to introduce separate risk concepts for hardware and software. According to the military standard, statistical risk exists only for hardware, and is consequently lost for software. This essay proposes a re-introduction of statistical risk to software, with the result that hardware and software risks become interchangeable in meaning.

Apologies {#S:APOLOGY}
---------

This essay is not rendered to academic standards of quality; it benefits from no formal literature search and was written in isolation. The experienced reader may find terms in nonstandard context. The author has strived to maintain consistency, but admits deficiency in standardization of terminology. The author apologizes for resulting inconvenience.

The author also apologizes that the concepts discussed here are nascent. Difficult engineering must be accomplished before a mature technology is available for commercialization.

The author features mathematics centrally,[^2] presuming undergraduate background and providing necessary computer science. This approach risks estranging many worthy engineering readers; however, a mathematical foundation is necessary. This essay serves that need.

Informal introduction
---------------------

### Hall’s definitions {#S:SYSTEMS}

The concept of *system* is intuitively obvious but describing its analytical properties is tricky. A famous example appeared in Hall’s 1962 treatise on systems engineering methodology [@aH62 p. 60ff]. Hall proposes succinct definitions of the terms *system* and *environment*:

-   A system is a set of objects with relationships between the objects and between their attributes.

-   For a given system, the environment is the set of all objects outside the system: (1) a change in whose attributes affect the system and (2) whose attributes are changed by the behavior of the system.

These definitions allow a component to belong either to the system or the environment, because Hall’s definitions are ambiguous (different phraseology is used that is actually equivalent). Our regimen modifies Hall’s historical definitions to remove ambiguity; systems will be regarded as all-inclusive. From the standpoint of relevant influences, there simply is no “outside” influence. We clarify that a system is characterized as a sequence of stimulus and response. Below “component” is a synonym for “object.” These descriptions still suffer some circularity:

-   A system is the set of *all* components having attributes, changes to which affect the system’s response.

-   The environment is the set of all components *inside* the system whose attributes are *not* affected by the system’s response.

In summary, the environment affects the system’s response, but the system response does not affect the environment’s attributes. Factors outside the system may influence the environment’s attributes.

### Classification {#S:INTRO_CLASSIFICATION}

In a system, the terms mechanism, construct, and model have specially differentiated meaning.

-   *Mechanisms* are abstractions, not necessarily separable, whose structure emulates all behaviors of a given phenomenon.

-   *Constructs* are isolatable substructures of a mechanism, for examining particular behaviors.

-   *Models* interpret a behavior of a construct in terms of alternate infrastructure.

*Exempli gratia*, hardware and software are mechanisms and operational profiles are constructs, while safety risk is a model. A description of major mechanisms, constructs, and models follows.

#### Hardware mechanism {#S:INTRO_HARDWARE}

The dynamics of hardware components is portrayed as constrained real time trajectories over a state space. A trajectory is a mapping from time into state space. A constraint relation is an alternative expression for what is familiar as an equation or inequality of state; it is merely a substitute for an equivalent equation. It is characteristic of systems that at any time, intersecting constraints delimit apparently independent choices so that just one is valid. Interacting constraints endow hardware with capabilities. Constraints can be classified according to their engineering significance. A violated safety constraint jeopardizes life, health, equipment, or surroundings.

#### Software mechanism {#S:INTRO_SOFTWARE}

Theoretical investigations of discrete reactive systems[^3] (or software) can be accomplished using a simple substitute for programming languages: the automaton. Automata are purely mechanistic structures positioned in the machine/language spectrum somewhere between the Turing machine and the Gurevich abstract state language (ASM). Beside its adequacy for examining theory, automata avoid selection of a preferred programming language, which would unnecessarily particularize concepts intended to be general.

Automata perform work in discrete units called steps. A sequence of steps is further known as a walk. This essay presents the actuated automaton, a variant form whose work is deterministic conditional sequencing and application of instructions. Instructions are represented by mathematical morphisms, collectively known as functionalities. The order of these functionalities is governed by the actuated automaton through its state. Iteration of an actuated automaton emulates an operating program.

#### Reactive mechanism {#S:INTRO_REACTIVE}

Reactive systems characteristically need some means to transfer external stimuli. The reactive mechanism contains structures enabling the hardware and software mechanisms to inter-operate cohesively. The nature of time differs between the two; time is a continuum in hardware while it is discrete in software. The clock synchronization permits integration by specifying an ordered cross-reference between discrete and real time.

Remaining is need for inter-mechanism communication. Two forms exist:

-   Sensors convey information about the hardware environment to the software mechanism. Using the clock synchronization, a real-time trajectory is sampled into a sequence of events.

-   Transducers map a point of the software state into a trajectory in hardware. This trajectory is called a control.

#### Cone construct {#S:INTRO_CONE}

The actuated automaton has a generalized inverse called the converse. Through reiteration, the converse constructs a partially ordered set (poset) of effects and potential causes. This poset is not linear because an effect may have more than one preceding cause.

A cone is the result of decomposing the poset into constituent chains called reverse walks. Viewed as forward walks (reversing the reverse walks), these chains are ordinary sequences of causes and consequent effects. The collection of forward chains converges to a point known as the crux, while the cone diverges from the same point. One subcomponent of a cone is its edge, which is the collection of steps radially opposite the crux.

#### Operational profile construct {#S:INTRO_OP_PROFILE}

As previously mentioned, automata accomplish work in units called steps. An operational profile is a measure of a step’s excitation probability relative to a reference set of steps.

The [reference set of steps]{} itself historically represented a software usage pattern, so it sought to resemble the natural mix of functionalities in deployed software. This idea is abstracted to a potentially purposeless reference set, but the software usage pattern remains important. From the usage pattern, along with the automaton’s static logic, arises the very notion of probability.

An operational profile may be applied to the edge of a cone.

#### Safety risk model {#S:INTRO_RISK}

Accidents occur haphazardly with varying frequency and severity. In the context of software, risk expresses the potential impact of algorithmic design errors. Since its true extent is unknown, software safety risk is expressed as a statistical hypothesis. The compound Poisson process is a model simulating discrete event-based losses that accumulate with passing time. It offers the advantage of independent parameterization of the loss’ intensity (frequency) and severity. Indemnification is statistical assurance of software safety.

### Principle of emergence {#S:PRINCIPLE_OF_EMERGENCE}

Emergence [@wW14e] is a broad principle of physics describing a process whereby larger entities possessing a property arise through interactions between simpler entities that themselves do not exhibit the property. Particularized to software testing, the [principle of (weak) emergence]{} is that erroneous software can do no actual harm until certain of its values emerge from the realm of digital logic into a physical subsystem. This principle inquires both into mechanics of transduction, and how transducible values come into being. The automaton of the software mechanism answers the latter question. If software hazard is to be evaluated starting at points of transduction and proceeding backwards through internal logic, then the automaton must support reverse inference – meaning reversed in computational order, from final conclusion to possible premise (see §\[S:INTRO\_CONE\]).

CHOICE FORK {#S:CHOICE_FORK}
-----------

Chapter 2 (Discrete Systems Theory) details relationships between systems theory and automata. From a mathematical standpoint the material is necessary, but there are readers for whom this chapter would duplicate existing knowledge. After verifying their understanding of operational profiles, section \[S:OPERATIONAL\_PROFILE\_SECTION\], they are invited to skip forward to Chapter 3.

Chapter 2 is summarized here to decide whether to skip it. Software is described using a triad of structures: the process, the procedure, and the path; not all are independent. Rudiments underlying these structures consist of ensembles and Cartesian products. Walks, the actuated automaton, converse automata, reverse walks, and cones follow.

Those desiring detailed introduction to fundamentals may access Appendix \[Ch:GROUNDWORK\], which reviews groundwork and notation used here. Its highlights include that an ensemble is a mapping from a set of stimuli into a set of responses. Ensembles are denoted by uppercase Greek letters such as $\Psi$. The general Cartesian product of an ensemble, called a choice space, is denoted ${\prod{\Psi}}$.

Discrete systems theory
=======================

Discrete systems theory (software) is identified with the actuated automaton.

Process
-------

Chains of stimulus and response characterize reactive discrete systems. In this chain, successive links are not independent: the response effected in one link feeds forward into the stimulus of the following link. For instance, in a system of cog-wheels and escapements, gear train movement accomplished in one stage of operation becomes input to the next. A formalism called a process captures this notion of sequential inheritance. We assemble processes from a simple unit called the frame, which is two-part structure consisting of starting and ending conditions. A process is a sequence of frames such that the starting condition of each frame subsumes the ending condition of its predecessor frame. Interpreted in systems language, a frame’s starting condition is a stimulus and its ending condition is a response. Current response re-appears as part of future stimulus.

Definitions of *ensemble* and related basic concepts appear in Groundwork, Appendix \[S:ENSEMBLE\] ff.

\[D:BASIS\] The pair of ensembles $\langle \Psi, \Phi \rangle$ is a *basis* if $\Phi \subseteq \Psi$.

It is necessary to represent states (variables) which are used but not set – so-called [volatile]{} variables. For example, such variables can hold the transient values of sensors. The remainder $\Psi \setminus \Phi$ is the generating ensemble of volatile variables (see terminology following definition \[D:CHOICE\_SPACE\]).

\[D:FRAME\_SPACE\] The *frame space* ${\mathbf{F}}$ of basis $\langle \Psi, \Phi \rangle$ is the set ${\prod{\Psi}} \times {\prod{\Phi}}$. A member ${\mathbf{f}} \in {\mathbf{F}}$ is a *frame*.

Let ${\mathbf{f}} = (\psi, \phi) \in {\prod{\Psi}} \times {\prod{\Phi}}$ be a frame. The choice $\psi \in {\prod{\Psi}}$ is the frame’s starting condition (abscissa) and $\phi \in {\prod{\Phi}}$ is the frame’s ending condition (ordinate).

Two frames may be related such that the ending condition of one frame is embedded within the next frame’s starting condition. This stipulation is conveniently expressed as a mapping restriction:

\[D:CONJOINT\] Let $\langle \Psi, \Phi \rangle$ be a basis with frames ${\mathbf{f}} = (\psi, \phi)$, ${\mathbf{f}}\,' = (\psi', \phi') \in {\prod{\Psi}} \times {\prod{\Phi}}$. Frame ${\mathbf{f}}$ *conjoins* frame ${\mathbf{f}}\,'$ if ${{\psi'}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}} = \phi$.

\[N:SEQUENCE\_NOTATION\] A sequence in a set $S$ is some mapping $\sigma \colon {\mathbb{N}}\to S$ – that is, $\sigma \in S^{\mathbb{N}}$. The anonymous sequence convention allows reference to a sequence using the compound symbol $\lbrace s_n \rbrace$, understanding $s \in S$. Formally, the symbol $s_i$ denotes that term $(i, s_i) \in \lbrace s_n \rbrace$. The convention is clumsy expressing functional notation; for instance $s_i = \lbrace s_n \rbrace(i)$ means $i \stackrel{\lbrace s_n\!\rbrace}{\mapsto} s_i$.

\[D:SUCCESIVELY\_CONJOINT\] Let $\langle \Psi, \Phi \rangle$ be a basis with sequence of frames $\lbrace {\mathbf{f}}_n \rbrace \colon {\mathbb{N}}\to {\prod{\Psi}} \times {\prod{\Phi}}$. The sequence is *successively conjoint* if ${\mathbf{f}}_i$ conjoins ${\mathbf{f}}_{i+1}$ for each $i \geq 1$.

\[D:PROCESS\] With $\langle \Psi, \Phi \rangle$ a basis, a *process* is a successively conjoint sequence of frames ${\mathbb{N}}\to {\prod{\Psi}} \times {\prod{\Phi}}$.

\[D:ABSCISSA\_PROJECTION\] Let $\langle \Psi, \Phi \rangle$ be a basis with frame space ${\mathbf{F}} = {\prod{\Psi}} \times {\prod{\Phi}}$. Define the *abscissa* projection ${{\operatorname{absc}{}}}: {\mathbf{F}} \to {\prod{\Psi}}$ by $(\psi, \phi) \stackrel{{{\operatorname{absc}{}}}}{\mapsto} \psi$. Define the *ordinate* projection ${{\operatorname{ord}{}}}: {\mathbf{F}} \to {\prod{\Phi}}$ by $(\psi, \phi) \stackrel{{{\operatorname{ord}{}}}}{\mapsto} \phi$.

\[D:PERSISTENT\_VOLATILE\_COMPONENTS\] Let $\langle \Psi, \Phi \rangle$ be a basis with persistent-volatile partition $\Psi = \Phi\Xi$ (see appendix §\[S:STATE\_EVENT\_PRTN\]). Suppose ${\mathbf{f}}$ is a frame in ${\prod{\Psi}} \times {\prod{\Phi}}$. The *reactive* state of frame ${\mathbf{f}}$ is $\psi = \phi \xi = {{\operatorname{absc}{{\mathbf{f}}}}}$. The *event* or *volatile* excitation state of frame ${\mathbf{f}}$ is $\xi = {{({{\operatorname{absc}{{\mathbf{f}})}}}}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Xi}}}}}$. Similarly, the *persistent* state of frame ${\mathbf{f}}$ is $\phi = {{({{\operatorname{absc}{{\mathbf{f}})}}}}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}}$.

Process concepts interpret into systems language. The reactive space ${\prod{\Psi}}$ contains the system stimulus. Sequential conjointness allows circumstantial interpretation of the choice space ${\prod{\Phi}}$. It is the system’s response in the context of the frame ending condition. To place ${\prod{\Phi}}$ in context of the frame’s reactive state, the Cartesian product ${\prod{\Phi}}  = \prod ({{\Psi}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}}) = (\thinspace\prod\Psi) \mid {{\operatorname{dom}{\Phi}}}$ \[by theorem \[T:CHC\_RSTR\_EQ\_RSTR\_CHC\]\] is the persistent state space. Using this nomenclature, sequential conjointness is summarized that each frame’s response becomes the next frame’s persistent state, symbolically ${{\operatorname{ord}{{\mathbf{f}}_{\,i}}}} = {{{{\operatorname{absc}{{\mathbf{f}}_{\,i+1}}}}}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}}$.

Procedure
---------

The procedure is useful to portray a process frame as a transformation from the stimulus space to the response space. To distinguish such transformations from other mappings, we use the special term [functionality]{} and stipulate that the collection of functionalities is a finite set called a catalog. The term [catalog]{} will later be applied to resource sets identified with an automaton.

### Functionality {#S:FUNCTIONALITY}

The functionality generalizes the frame. If ${\mathbf{f}}_i = (\psi_i, \phi_i)$ is the $i^{\text{th}}$ process frame, this concept permits writing $\phi_i = {{\mathit{f}}}_i(\psi_i)$, where ${\mathit{f}}_i$ is some functionality belonging to catalog ${\mathscr{F}}$.

\[D:FUNCTIONALITY\] A *functionality* is a mapping whose domain and codomain are choice spaces (definition \[D:CHOICE\_SPACE\]), with the codomain a subspace (definition \[D:SUBSPACE\]) of the domain.

\[L:BASIS\_FUNCTIONALITY\] Let $\langle \Psi, \Phi \rangle$ be a basis. Any mapping ${\mathit{f}} \colon {\prod{\Psi}} \to {\prod{\Phi}}$ is a functionality.

As a basis, definition \[D:BASIS\] establishes that $\Psi$ and $\Phi$ are ensembles with $\Phi \subseteq \Psi$. Since $\Psi$ and $\Phi$ are ensembles, definition \[D:CHOICE\_SPACE\] asserts that ${\prod{\Psi}}$ and ${\prod{\Phi}}$ are choice spaces. Theorem \[T:SUBSET\_IFF\_SUBSPACE\] provides that ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$ because $\Phi \subseteq \Psi$. By virtue of ${\mathit{f}} \in {{\prod{\Phi}}}^{{\prod{\Psi}}}$, then ${\mathit{f}} \colon {\prod{\Psi}} \to {\prod{\Phi}}$ is a mapping from one choice space to another, which is a subspace of the first. These conditions satisfy the premises of definition \[D:FUNCTIONALITY\].

In its programming sense, the term [function]{} will not be used here. A mathematical functionality differs from a software function; functionalities lack arguments. By virtue of its calling protocol, a programming function is effectively a class of functionalities.

### Procedure {#S:PROCEDURE}

Procedures are sequences in a finite set of functionalities:

\[D:CATALOG\_OF\_FUNCTIONALITY\] Let $\langle \Psi, \Phi \rangle$ be a basis. A finite subset ${\mathscr{F}} \subseteq {{\prod{\Phi}}}^{{\prod{\Psi}}}$ is a *catalog* of functionality.

\[D:PROCEDURE\] Let $\langle \Psi, \Phi \rangle$ be a basis and ${\mathscr{F}} \subseteq {{\prod{\Phi}}}^{{\prod{\Psi}}}$ be a catalog of functionality. A *procedure* is a sequence $\lbrace {\mathit{f}}_n \rbrace \colon {\mathbb{N}}\to {\mathscr{F}}$.

After noting the functionality’s successful generalization of the frame, the next question is whether the procedure correspondingly abstracts the process. We find that not all processes are [computable]{} as procedures based on a finite number of functionalities.

### Covering {#S:COVERING}

The relation holding between frame ${\mathbf{f}} \in {\prod{\Psi}} \times {\prod{\Phi}}$ and functionality ${\mathit{f}} \colon {\prod{\Psi}} \to {\prod{\Phi}}$ is membership: either ${\mathbf{f}} \in {\mathit{f}}$ or ${\mathbf{f}} \notin {\mathit{f}}$.

\[D:BASIC\_COVERING\] Let ${\mathbf{f}}$ be a frame and ${\mathit{f}}$ be a functionality. The functionality *covers* the frame if ${\mathbf{f}} \in {\mathit{f}}$ (that is, ${\mathbf{f}} = (\psi, \phi) = (\psi, {\mathit{f}}(\psi))$).

\[D:COVERING\_PROCEDURE\] Let $\lbrace {\mathbf{f}}_n \rbrace$ be a sequence of frames and $\lbrace {\mathit{f}}_n \rbrace$ be a procedure. The procedure *covers* the sequence of frames if ${\mathbf{f}}_i \in {\mathit{f}}_i$ for each $i \geq 1$ (that is, ${\mathbf{f}}_i = (\psi_i, \phi_i) = (\psi_i, {\mathit{f}}_i(\psi_i))$).

Any procedure covers some process.

\[T:PROCEDURE\_COVER\_PROCESS\] Let $\langle \Psi, \Phi \rangle$ be a basis with persistent-volatile partition $\Psi = \Phi\Xi$ and catalog of functionality ${\mathscr{F}}$. Suppose $\lbrace {\mathit{f}}_n \rbrace \colon {\mathbb{N}}\to {\mathscr{F}}$ is a procedure. For each choice of persistent state $\varphi \in {\prod{\Phi}}$ and volatile excitation sequence $\lbrace \xi_n \rbrace \in {(\,{\prod{\Xi}})}^{{\mathbb{N}}}$ there is a process $\lbrace {\mathbf{f}}_n \rbrace \colon {\mathbb{N}}\to {\prod{\Psi}} \times {\prod{\Phi}}$ such that the procedure covers the process.

The persistent state $\varphi$ and volatile excitation $\lbrace \xi_n \rbrace$ are given. Inductively define sequence $\lbrace \phi_n \rbrace$ using base clause $\phi_1 = \varphi$ and recursive clause $\phi_{i+1} = {\mathit{f}}_i(\phi_i\xi_i)$ for $i \ge 1$ (dyadic notation, definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\] ff).

We first show that the sequence $\lbrace \phi_n \rbrace$ lies in ${\prod{\Phi}}$. Through $\varphi$, definition \[D:PERSISTENT\_VOLATILE\_COMPONENTS\] provides that $\phi_1 \in {\prod{\Phi}}$. For the iterative part, the hypothesis $\phi_i \in {\prod{\Phi}}$ implies that $\phi_i\xi_i \in {\prod{\Psi}}$ by Theorem \[T:DYADIC\_CHOICE\_PROD\]. Since ${\mathit{f}}_i$ maps ${\prod{\Psi}}$ to ${\prod{\Phi}}$, then ${\mathit{f}}_i(\phi_i\xi_i) = \phi_{i+1} \in {\prod{\Phi}}$. This chain of implication concludes that $(\phi_i \in {\prod{\Phi}}) \Rightarrow (\phi_{i+1} \in {\prod{\Phi}})$.

Use $\lbrace \phi_n \rbrace$ and $\lbrace \xi_n \rbrace$ to define another sequence $\lbrace {\mathbf{f}}_n \rbrace$ by setting ${\mathbf{f}}_i = (\phi_i\xi_i, \phi_{i+1})$. Since $\phi_i\xi_i \in {\prod{\Psi}}$ and $\phi_{i+1} \in {\prod{\Phi}}$, then $(\phi_i\xi_i, \phi_{i+1}) \in {\prod{\Psi}} \times {\prod{\Phi}}$ so $\lbrace {\mathbf{f}}_n \rbrace$ is a sequence of frames. Note that ${\mathbf{f}}_i = (\phi_i\xi_i, \phi_{i+1})$ and ${\mathbf{f}}_{i+1} = (\phi_{i+1}\xi_{i+1}, \phi_{i+2})$. In this case, the sequence is successively conjoint (definitions \[D:CONJOINT\] and \[D:SUCCESIVELY\_CONJOINT\]) because ${{\phi_{i+1}\xi_{i+1}}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}} = \phi_{i+1}$. As a successively conjoint sequence of frames, $\lbrace {\mathbf{f}}_n \rbrace$ is a process (definition \[D:PROCESS\]).

Since ${\mathbf{f}}_i = (\phi_i\xi_i, \phi_{i+1})$, and by construction $\phi_{i+1} = {\mathit{f}}_i(\phi_i\xi_i)$, then ${\mathbf{f}}_i = (\phi_i\xi_i, {\mathit{f}}_i(\phi_i\xi_i))$ and ${\mathbf{f}}_i \in {\mathit{f}}_i$. By definition \[D:COVERING\_PROCEDURE\], procedure $\lbrace {\mathit{f}}_n \rbrace$ covers process $\lbrace {\mathbf{f}}_n \rbrace$.

### Uncoverable process {#S:UNCOVERABLE_PROCESS}

Although any procedure does cover some process, some processes have no covering procedure. See §\[S:UNCOVERABLE\_PROCESS\_APPENDIX\].

Automata
--------

The algorithm is conceived as a method to solve problems using a network of mechanistic steps consisting of decisions and contingent actions. An automaton is a formal machine whose architecture of states and transitions concretizes some aspects of the algorithm. The deterministic finite automaton (DFA, see example in §\[S:DFA\]) is a simple structure describing transit-based behavior. However, the DFA leaves unexplained the working mechanism underlying transitions. The DFA’s definition can be modified to effect closer alignment with our notion of software algorithm. The result is the actuated automaton, which mechanizes logic using structure analogous to programming language. An informal analogy between an automaton and a programming language will be proposed at the end of this section.

### Locus {#S:LOCUS}

A formalization of the algorithm’s stepwise network of decisions and actions requires some means of indicating one’s place in the overall method, to track what is current and what is next. We provide this in the form of a set of loci, which serve as labels for the [locations]{} implicit in a program or algorithm.

\[D:CATALOG\_OF\_LOCI\] A catalog of *loci* is a finite non-empty set $\Lambda$, each member $\lambda$ of which is called a locus.

Let $\Lambda$ be a catalog of loci. A *path* is a sequence $\lbrace \lambda_n \rbrace \colon {\mathbb{N}}\to \Lambda$.

### Summary {#S:THREE_P}

We now identify the components of a walk, the three fundamental P’s:

-   A path is a sequence in the catalog of loci $\Lambda$.

-   A process is a conjoint sequence in the frame space ${\mathbf{F}} = {\prod{\Psi}} \times {\prod{\Phi}}$.

-   A procedure is a covering sequence in the catalog of functionality ${\mathscr{F}}$.

### Auxiliary mechanisms {#S:AUXILIARY_MECHANISMS}

\[D:LOCUS\_ACTUATOR\] Let ${\mathscr{F}}$ be a catalog of functionality on basis $\langle \Psi, \Phi\rangle$. An *actuator* ${\mathsf{a}}$ is a mapping ${\mathsf{a}} \colon {\prod{\Psi}} \to {\mathscr{F}}$ from the process stimulus space to the catalog of functionality.

In other words, any ${\mathsf{a}} \in {\mathscr{F}}^{{\prod{\Psi}}}$ is an actuator.

\[D:LOCUS\_CATALOG\_OF\_ACTUATION\] A catalog of *actuation* is a non-empty finite set ${\mathsf{A}} \subseteq {\mathscr{F}}^{{\prod{\Psi}}}$ of actuators.

With each locus is associated exactly one designated actuator:

\[D:LOCUS\_ACTUATOR\_DESIGNATION\] Let the *locator* be a surjective mapping $\ell \colon \Lambda \to {\mathsf{A}}$.

To permit each actuator to be located, it is prerequisite that ${\lvert{{\mathsf{A}}}\rvert} \leq {\lvert{\Lambda}\rvert}$ (the number of actuators is less than or equal to the number of loci).

\[D:JUMP\_FUNCTION\] Let $\Lambda$ be a catalog of loci. The *jump* function is a mapping $\Delta \colon \Lambda \times {\prod{\Psi}} \to \Lambda$.

### Actuated automaton {#S:ACTUATED_AUTOMATON}

\[D:ACTUATED\_AUTOMATON\] The structure ${\mathfrak{A}} = \langle \Psi, \Phi, {\mathscr{F}}\!, {\mathsf{A}}, \Lambda, \ell, \Delta \rangle$ of an *actuated* automaton consists of seven synchronized catalogs: a basis $\langle \Psi, \Phi \rangle$ with catalog of functionality ${\mathscr{F}}$, catalog of actuation ${\mathsf{A}}$, catalog of loci $\Lambda$, locator function $\ell$, and jump function $\Delta$.

Automata exist in many varieties. Since the actuated automaton occupies the entire present scope of interest, we forgo mandatory use of the qualifier [actuated.]{}

### Programming language analogy {#S:LANGUAGE_ANALOGY}

The automaton $\langle \Psi, \Phi, {\mathscr{F}}\!, {\mathsf{A}}, \Lambda, \ell, \Delta \rangle$ of definition \[D:ACTUATED\_AUTOMATON\] resembles an algorithm written in an elementary programming language. The following comprise the analogy:

-   the generating ensemble $\Phi$ of the persistent state space represents ordinary program variables;

-   the remainder ensemble $\Psi \setminus \Phi$ represents volatile external inputs, such as sensors;

-   functionalities of the catalog ${\mathscr{F}}$ represent blocks of program assignment statements;

-   actuators in ${\mathsf{A}}$ implement if-then-elsif-else decisions,

-   the jump function $\Delta$ is a [goto]{} indicating the next point of execution, and

-   loci in $\Lambda$ are labels serving as [goto-able]{} points of execution.

Iteration
---------

While leaving undefined the notion of a step in an algorithm, we do formalize it for the automaton. Identifying a step space leads to defining iterative operators, and hence to iteration.

### Step space {#S:STEP_SPACE}

The step space underlies automata. It is formed by augmenting a catalog of loci to the building blocks of processes and procedures, namely frames and functionalities.

\[D:STEP\_SPACE\] Suppose $\Lambda$ is a catalog of loci. Let basis $\langle \Psi, \Phi\rangle$ underly frame space ${\mathbf{F}} = {\prod{\Psi}} \times {\prod{\Phi}}$ and catalog of functionality ${\mathscr{F}} \subseteq {{\prod{\Phi}}}^{{\prod{\Psi}}}$. A *step space* ${\mathbb{S}}$ is the Cartesian product ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$.

The volatile excitation, whose generating ensemble is $\Psi \setminus \Phi$, is intrinsically part of the definition of step space. Lest this implicit fact be forgotten, we shall adopt explicit but redundant notation as reminders.

\[D:STEP\_SPACE\_PROJECTION\] Let ${\mathit{s}} = (\lambda,{\mathit{f}},{\mathbf{f}})$ be a member of step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$. Define the *locus* projection $\mho_\Lambda \colon {\mathbb{S}} \to \Lambda$ by setting $\mho_\Lambda(\lambda,{\mathit{f}},{\mathbf{f}}) = \lambda$. Similarly define the *frame* and *functionality* projections by $\mho_{\mathbf{F}}(\lambda,{\mathit{f}},{\mathbf{f}}) = {\mathbf{f}}$ and $\mho_{\mathscr{F}}(\lambda,{\mathit{f}},{\mathbf{f}}) = {\mathit{f}}$ respectively.

Definition \[D:CONJOINT\] considers the covering relation between a frame and a functionality. *Consistency* is the same principle applied to the context of a step:

\[D:CONSISTENT\_STEP\] Let ${\mathit{s}} = (\lambda,{\mathit{f}},{\mathbf{f}})$ be a member of step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$. The step ${\mathit{s}}$ is *consistent* if $\mho_{\mathbf{F}}({\mathit{s}}) = {\mathbf{f}} \in {\mathit{f}} = \mho_{\mathscr{F}}({\mathit{s}})$ (that is, its frame is a member of its functionality).

#### Sequence projection {#S:SEQUENCE_PROJECTION}

\[D:STEP\_SPACE\_WALK\] Let ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$ be a step space and ${\mathscr{I}}$ be a denumerable index set. A *walk* is a sequence ${\mathscr{I}} \to {\mathbb{S}}$ of steps (usually ${\mathscr{I}}$ will be the natural numbers ${\mathbb{N}}$).

We revisit the three fundamental P’s (path, procedure, and process – §\[S:THREE\_P\]). A walk in step space decomposes into these three sequences: $\textrm{walk}_{\,i} = (\textrm{path}_{\,i}, \textrm{process}_{\,i}, \textrm{procedure}_{\,i})$. This triple is not logically independent; being so, shorter characterizations of step space exist. However we retain the present representation, favoring its three-element formulation, which covers all possibilities in simple fashion.

[\[Extended projection\]]{} \[D:EXTENDED\_PROJECTION\] Let $\lbrace {\mathit{s}}_n \rbrace$ be a walk in step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$ and let ${\mathscr{I}}$ be a denumerable index set (usually ${\mathbb{N}}$). Use the locus projection $\mho_\Lambda \colon {\mathbb{S}} \to \Lambda$ of definition \[D:STEP\_SPACE\_PROJECTION\] to construct the sequential *path* projection $\overline{\mho}_\Lambda \colon {\mathbb{S}}^{\mathscr{I}} \to \Lambda^{\mathscr{I}}$ via setting $\overline{\mho}_\Lambda(\lbrace {\mathit{s}}_n \rbrace) = \lbrace (i,\mho_\Lambda({\mathit{s}})) \colon
    (i,{\mathit{s}}) \in \lbrace {\mathit{s}}_n \rbrace \rbrace$. Similarly define the sequential *process* and *procedure* projections $\overline{\mho}_{\mathbf{F}} \colon {\mathbb{S}}^{\mathscr{I}} \to {\mathbf{F}}^{\mathscr{I}}$ and $\overline{\mho}_{\mathscr{F}} \colon {\mathbb{S}}^{\mathscr{I}} \to {\mathscr{F}}^{\mathscr{I}}$.

With $\lbrace x_n \rbrace \colon {\mathscr{I}} \to X$ a sequence in some set $X$, we alternatively denote the sequence’s ${{i}^{\text{th}}}$ term by $x_i = \lbrace x_n \rbrace(i)$.

\[L:RELATED\_PROJECTION\] Let $\langle \Psi, \Phi \rangle$ and locus set $\Lambda$ be the bases for step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$. Let $\lbrace {\mathit{s}}_n \rbrace$ be a walk ${\mathscr{I}} \to {\mathbb{S}}$. For each $i \in {\mathscr{I}}$, $(\overline{\mho}_\Lambda(\lbrace {\mathit{s}}_n \rbrace))(i) = \mho_\Lambda(\lbrace {\mathit{s}}_n \rbrace(i))$; that is, the ${{i}^{\text{th}}}$ term of the sequential path projection equals the locus projection of the ${{i}^{\text{th}}}$ step.

Analogous assertions are true of the remaining sequential projections: $(\overline{\mho}_{\mathbf{F}}(\lbrace {\mathit{s}}_n \rbrace))(i) = \mho_{\mathbf{F}}(\lbrace {\mathit{s}}_n \rbrace(i))$ and $(\overline{\mho}_{\mathscr{F}}(\lbrace {\mathit{s}}_n \rbrace))(i) = \mho_{\mathscr{F}}(\lbrace {\mathit{s}}_n \rbrace(i))$.

By definition \[D:EXTENDED\_PROJECTION\], the sequential path projection $\overline{\mho}_\Lambda \colon {\mathbb{S}}^{\mathscr{I}} \to \Lambda^{\mathscr{I}}$ is $\overline{\mho}_\Lambda(\lbrace {\mathit{s}}_n \rbrace) = \lbrace (i,\mho_\Lambda({\mathit{s}})) \colon
    (i,{\mathit{s}}) \in \lbrace {\mathit{s}}_n \rbrace \rbrace$. The $i^\text{th}$ term of $\overline{\mho}_\Lambda(\lbrace {\mathit{s}}_n \rbrace)$ is $(\overline{\mho}_\Lambda(\lbrace {\mathit{s}}_n \rbrace))(i)$. From set builder notation we observe that the $i^\text{th}$ term of the expression $\lbrace (i,\mho_\Lambda({\mathit{s}})) \colon (i,{\mathit{s}}) \in \lbrace {\mathit{s}}_n \rbrace \rbrace$ is $\mho_\Lambda({\mathit{s}}_i) = \mho_\Lambda(\lbrace {\mathit{s}}_n \rbrace(i))$. Since the sequences are equal, then each of their corresponding terms are equal: $(\overline{\mho}_\Lambda(\lbrace {\mathit{s}}_n \rbrace))(i) = \mho_\Lambda(\lbrace {\mathit{s}}_n \rbrace(i))$. Demonstration is similar for the other two sequential projections.

### Iterative operators {#S:ITERATIVE_OPERATOR}

\[D:ITERATIVE\_OPERATOR\] Let ${\mathbb{S}}$ be a step space with basis $\langle \Psi, \Phi \rangle$. Suppose the volatile excitation space $\Psi \setminus \Phi$ is non-empty. A *iterative* operator is a mapping $V \colon {\mathbb{S}} \to {\mathbb{S}}$.

#### Disambiguation

An iterative operator maps a step space into itself. One element of a step space is a reactive state space, having persistent and volatile components. A functionality maps a reactive state space into the persistent subset of itself.

#### Walk of iterative operator {#S:ITERATIVE_OPERATOR_WALK}

\[D:ITERATIVE\_OPERATOR\_WALK\] Let $\langle \Psi, \Phi \rangle$ be a basis with step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times (\,{\prod{\Psi}} \times {\prod{\Phi}})$. Suppose $V \colon {\mathbb{S}} \to {\mathbb{S}}$ is an iterative operator, step ${\mathit{s}} \in {\mathbb{S}}$, and $\lbrace \xi_n \rbrace \in (\,{\prod{\Xi}})^{\mathbb{N}}$ is an volatile excitation sequence. Define inductively a sequence of steps by setting ${\mathit{s}}_1 = {\mathit{s}}$ and ${\mathit{s}}_{i+1} = V({\mathit{s}}_i)$ for each $i \ge 1$. The walk of ${\mathit{s}} \in {\mathbb{S}}$ under $V$, assuming sequence of volatile excitation $\lbrace \xi_n \rbrace$, is the walk $\lbrace {\mathit{s}}_n \rbrace$.

An iterative operator’s $i^\text{th}$ *iteration* is its walk’s ${(i+1)}^\text{th}$ term.

### Automaton-induced iterative operators {#S:INDUCED_ITERATIVE_OPERATOR}

Iteration of automata guarantees properties not necessarily enjoyed by other classes of iterative operators: automata generate consistent steps having conjoint processes.

#### Automaton as transformation

\[D:ITERATIVE\_TRANSFORM\] Let $\langle \Psi, \Phi \rangle$ be a basis with persistent-volatile partition $\Psi = \Phi\Xi$ and step space ${\mathbb{S}} = \Lambda  \times {\mathscr{F}} \times (\,{\prod{\Psi}} \times {\prod{\Phi}})$. Let ${\mathfrak{A}} = \langle \Psi, \Phi, {\mathscr{F}}\!, {\mathsf{A}}, \Lambda, \ell, \Delta \rangle$ be an actuated automaton. Let $\xi \in {\prod{\Xi}}$ be an event stimulus and $(\lambda, {\mathit{f}}, {\mathbf{f}}) = (\lambda, {\mathit{f}}, (\psi, \phi)) \in {\mathbb{S}}$ be a step. The transform $T_{{\mathfrak{A}}}$ induced by ${\mathfrak{A}}$ is $$(\lambda, {\mathit{f}}, (\psi, \phi)) \stackrel{{\mathfrak{A}}}{\mapsto} (\lambda', {\mathit{f}}', (\psi', \phi')),$$ where $$\begin{aligned}
  \lambda' &= \Delta(\lambda, \psi).&\quad\text{[next locus]}\\
  {\mathit{f}}' &= (\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi')&\quad\text{[next functionality]} \\
  {\mathbf{f}}\,' &= (\psi', \phi') = 
            ([{\mathit{f}}(\psi) \xi'], [(\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi')]([{\mathit{f}}(\psi) \xi']))&\quad\text{[next frame]}\end{aligned}$$

A partial unfolding of these expressions’ generators clarifies the roles of components in overall mechanism:

1.  Current reactive state is $\psi = \phi \xi$.

2.  Current locus is $\lambda$.

3.  Current actuator is ${\mathsf{a}} = \ell(\lambda)$.

4.  Current functionality is ${\mathit{f}} = {\mathsf{a}}(\psi) = (\ell(\lambda))(\psi)$.

5.  Current frame is ${\mathbf{f}} = (\psi, {\mathit{f}}(\psi))$.

6.  Current step is ${\mathit{s}} = (\lambda, (\psi, (\ell(\lambda))(\psi), {\mathit{f}}(\psi)))$.

7.  Next reactive state is $\psi' = \phi' \xi' = {\mathit{f}}(\psi) \xi'$ (by conjointness).

8.  Next locus is found through the jump function: $\lambda' = \Delta(\lambda, \psi)$.

9.  Next actuator is ${\mathsf{a}}' = \ell(\lambda')$,

10. ${\mathsf{a}}' = \ell(\Delta(\lambda, \psi))$.

11. Next functionality is ${\mathit{f}}\,' = {\mathsf{a}}'(\psi')$,

12. ${\mathit{f}}' = [\ell(\Delta(\lambda, \psi))](\psi')$,

13. ${\mathit{f}}' = (\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi')$.

14. Next frame is ${\mathbf{f}}\,' = (\psi', {\mathit{f'}}(\psi'))$,

15. ${\mathbf{f}}\,' = ([{\mathit{f}}(\psi) \xi'], {\mathit{f'}}([{\mathit{f}}(\psi) \xi']))$,

16. ${\mathbf{f}}\,' = ([{\mathit{f}}(\psi) \xi'], [(\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi')]([{\mathit{f}}(\psi) \xi']))$.

17. Next step is ${\mathit{s}}' = (\Delta(\lambda, \psi), {\mathsf{a}}'(\psi'), (\psi', {\mathit{f'}}(\psi')))$.

#### Automaton as iterative operator

\[T:AUTOMATON\_OPERATOR\] Let $\langle \Psi, \Phi \rangle$ be a basis with persistent-volatile partition $\Psi = \Phi\Xi$ and step space ${\mathbb{S}}$. Let ${\mathfrak{A}}$ be an automaton. The transform $T_{\mathfrak{A}} \colon {\mathbb{S}} \to {\mathbb{S}}$ induced by ${\mathfrak{A}}$ is an iterative operator (that is, if ${\mathit{s}} \in {\mathbb{S}}$, then $T_{{\mathfrak{A}}}({\mathit{s}}) \in {\mathbb{S}}$).

By definition \[D:ACTUATED\_AUTOMATON\], automaton ${\mathfrak{A}}$ consists of components $\langle \Psi, \Phi, {\mathscr{F}}\!, {\mathsf{A}}, \Lambda, \ell, \Delta \rangle$. Other premises are that the iterative operator’s domain is ${\mathbb{S}}$, the persistent-volatile partition $\Psi = \Phi\Xi$, and that $\xi \in {\prod{\Xi}}$.

Suppose $\xi \in {\prod{\Xi}}$ and ${\mathit{s}} \in {\mathbb{S}}$. By definition \[D:STEP\_SPACE\] of step space, there exist locus $\lambda \in \Lambda$, functionality ${\mathit{f}} \in {\mathscr{F}} \subseteq {{\prod{\Phi}}}^{{\prod{\Psi}}}$, and frame ${\mathbf{f}} = (\psi, \phi) \in {\prod{\Psi}} \times {\prod{\Phi}}$ such that ${\mathit{s}} = (\lambda,(\psi, \phi), {\mathit{f}})$.

Definition \[D:ITERATIVE\_TRANSFORM\] calls for application $(\ell(\lambda))(\phi)$ to define succeeding functionality ${\mathit{f}}'$. Definition \[D:LOCUS\_ACTUATOR\_DESIGNATION\] specifies $\ell \colon \Lambda \to {\mathsf{A}}$, so ${\mathsf{a}} = \ell(\lambda) \in {\mathsf{A}}$ is an actuator. Definition \[D:LOCUS\_ACTUATOR\] specifies ${\mathsf{a}} \colon {\prod{\Phi}} \to {\mathscr{F}}$, so application ${\mathit{f}}' = (\ell(\lambda))(\phi) = {\mathsf{a}}(\phi)$ is a functionality in ${\mathscr{F}}$.

Definition \[D:ITERATIVE\_TRANSFORM\] next calls for evaluating $(\psi', \phi') = (\phi\xi, {\mathit{f}}'(\phi\xi))$ as the succeeding frame ${\mathbf{f}}\,'$. By premise $\xi \in {\prod{\Xi}}$. By virtue of its origin as a frame ordinate, $\phi \in {\prod{\Phi}}$. Since $\Psi = \Phi\Xi$, then $\phi\xi$ is a valid dyadic product and $\psi' = \phi\xi \in {\prod{\Psi}}$. Since definition \[D:CATALOG\_OF\_FUNCTIONALITY\] asserts ${\mathscr{F}} \subseteq {{\prod{\Phi}}}^{{\prod{\Psi}}}$ and ${\mathit{f}}' \in {\mathscr{F}}$, then ${\mathit{f}}' \colon {\prod{\Psi}} \to {\prod{\Phi}}$. With $\phi\xi \in {\prod{\Psi}}$, then $\phi' = {\mathit{f}}'(\phi\xi) \in {\prod{\Phi}}$. Hence ${\mathbf{f}}\,' = (\psi', \phi') \in {\prod{\Psi}} \times {\prod{\Phi}}$, and ${\mathbf{f}}\,'$ is a frame.

Finally, definition \[D:ITERATIVE\_TRANSFORM\] calls for the succeeding locus as $\lambda' = \Delta(\lambda, \psi)$. Definition \[D:JUMP\_FUNCTION\] specifies the jump function as a mapping $\Delta \colon \Lambda \times {\prod{\Psi}} \to \Lambda$. It is established above that $\lambda \in \Lambda$ and $\psi \in {\prod{\Psi}}$, so $\lambda' = \Delta(\lambda, \psi) \in \Lambda$ is a locus.

With locus $\lambda' \in \Lambda$, functionality ${\mathit{f}}' \in {\mathscr{F}}$, and frame ${\mathbf{f}}\,' = (\psi', \phi') \in {\prod{\Psi}} \times {\prod{\Phi}}$, we then summarize that ${\mathit{s}}' = (\lambda', {\mathit{f}}', (\psi', \phi')) \in {\mathbb{S}}$ is a step, and conclude that transform $T_{{\mathfrak{A}}}$ is an iterative operator ${\mathbb{S}} \to {\mathbb{S}}$.

Application of the iterative operator $T_{{\mathfrak{A}}}$ induced by automaton ${\mathfrak{A}}$ is denoted ${\mathit{s}}' = {\mathfrak{A}}({\mathit{s}})$.

Let ${\mathbb{S}}$ be a step space with automaton ${\mathfrak{A}}$ inducing iterative operator $T_{{\mathfrak{A}}}$. The walk of ${\mathit{s}} \in {\mathbb{S}}$ under $T_{{\mathfrak{A}}}$ assuming sequence of volatile excitation $\lbrace \xi_n \rbrace$ is denoted ${\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}})$.

The notation ${\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}})$ is a reminder of the important role of the sequence of volatile excitations $\lbrace \xi_n \rbrace$. While each $\xi$ is entirely determined by initial frame $\psi$ within step ${\mathit{s}}$, this notation emphasizes that the volatile excitations are essentially free variables. Persistent variables are bound.

#### Automaton iterative properties

\[T:AUTOMATON\_ITERATE\_CONJOINT\] Let ${\mathfrak{A}}$ be an automaton and ${\mathbb{S}}$ be a step space with persistent-volatile partition $\Psi = \Phi\Xi$. Suppose step ${\mathit{s}} \in {\mathbb{S}}$ and event $\xi \in \Xi$. Frame $\mho_{\mathbf{F}}({\mathit{s}})$ conjoins frame $\mho_{\mathbf{F}}({\mathfrak{A}}_\xi({\mathit{s}}))$.

By hypothesis $\xi \in {\prod{\Xi}}$ and ${\mathit{s}} \in {\mathbb{S}}$. By definition \[D:STEP\_SPACE\] of step space, there exist locus $\lambda \in \Lambda$, frame ${\mathbf{f}} = (\psi, \phi) \in {\prod{\Psi}} \times {\prod{\Phi}}$, and functionality ${\mathit{f}} \in {\mathscr{F}}$ such that ${\mathit{s}} = (\lambda, {\mathit{f}}, (\psi, \phi))$. Definition \[D:STEP\_SPACE\_PROJECTION\] establishes that $\mho_{\mathbf{F}}({\mathit{s}}) = (\psi, \phi)$.

By Theorem \[T:AUTOMATON\_OPERATOR\] the automaton induces an iterative operator, so there exists ${\mathfrak{A}}_\xi( {\mathit{s}}) = (\lambda', {\mathit{f}}',(\psi', \phi')) \in {\mathbb{S}}$. Again by definition \[D:STEP\_SPACE\_PROJECTION\], $\mho_{\mathbf{F}}({\mathfrak{A}}_\xi( {\mathit{s}})) = (\psi', \phi')$.

Definition \[D:ITERATIVE\_TRANSFORM\] evaluates ${\mathbf{f}}\,' = (\psi', \phi') = (\phi\xi, {\mathit{f}}'(\phi\xi))$ as the succeeding frame. Definition \[D:CONJOINT\] asserts that frame $(\psi, \phi)$ conjoins frame $(\psi', \phi')$ if ${{\psi'}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}} = \phi$. Here $\psi' = \phi\xi$, so ${{\phi\xi}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}} = \phi$ by virtue of persistent-volatile partition $\Psi = \Phi\Xi$. Thus we conclude $(\psi, \phi)$ conjoins $(\psi', \phi')$.

Since $\mho_{\mathbf{F}}({\mathit{s}}) = (\psi, \phi)$, $(\psi, \phi)$ conjoins $(\psi', \phi')$, and $(\psi', \phi') = \mho_{\mathbf{F}}({\mathfrak{A}}_\xi( {\mathit{s}}))$, then by transitivity $\mho_{\mathbf{F}}({\mathit{s}})$ conjoins $\mho_{\mathbf{F}}({\mathfrak{A}}_\xi( {\mathit{s}}))$.

\[T:AUTOMATON\_WALK\_PROCESS\] Let ${\mathfrak{A}}$ be an automaton and ${\mathbb{S}}$ be a step space with step ${\mathit{s}} \in {\mathbb{S}}$ and volatile excitation $\lbrace \xi_n \rbrace$. Sequential process projection $\overline{\mho}_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}}))$ is indeed a process per definition \[D:PROCESS\].

Definition \[D:PROCESS\] asserts that a process is a successively conjoint sequence of frames. To show contradiction, hypothesize that the frame sequence $\overline{\mho}_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}}))$ is *not* a process. Then there is some index $i$ such that frame $\mho_{\mathbf{F}}({\mathit{s}}_i)$ does not conjoin frame $\mho_{\mathbf{F}}({\mathit{s}}_{i+1})$.

Let ${\mathit{s}}_i$ be the $i^\text{th}$ step of walk ${\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}})$. From definition \[D:ITERATIVE\_OPERATOR\_WALK\], the succeeding step is ${\mathit{s}}_{i+1} = {\mathfrak{A}}_{\xi_i}({\mathit{s}}_i)$. By Theorem \[T:AUTOMATON\_ITERATE\_CONJOINT\], frame $\mho_{\mathbf{F}}({\mathit{s}}_i)$ conjoins frame $\mho_{\mathbf{F}}({\mathfrak{A}}_{\xi_i}({\mathit{s}}_i))$. This contradicts the conclusion drawn from the hypothesis that the frame sequence is not a process, so $\overline{\mho}_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}}))$ *is* a process.

Be a step consistent or not, in automaton-based iteration that step’s successor is consistent.

\[T:AUTOMATON\_ITERATE\_CONSISTENT\] Let ${\mathfrak{A}}$ be an automaton and ${\mathbb{S}}$ be a step space with persistent-volatile partition $\Psi = \Phi\Xi$. Suppose step ${\mathit{s}} \in {\mathbb{S}}$ and event $\xi \in \Xi$. Step ${\mathfrak{A}}_\xi({\mathit{s}})$ is consistent.

By hypothesis $\xi \in {\prod{\Xi}}$ and ${\mathit{s}} \in {\mathbb{S}}$. By definition \[D:STEP\_SPACE\] of step space, there exist locus $\lambda \in \Lambda$, frame ${\mathbf{f}} = (\psi, \phi) \in {\prod{\Psi}} \times {\prod{\Phi}}$, and functionality ${\mathit{f}} \in {\mathscr{F}}$ such that ${\mathit{s}} = (\lambda, (\psi, \phi), {\mathit{f}})$.

By Theorem \[T:AUTOMATON\_OPERATOR\] the automaton induces an iterative operator, so there exists ${\mathfrak{A}}_\xi({\mathit{s}}) = (\lambda', (\psi', \phi'), {\mathit{f}}') \in {\mathbb{S}}$. By definition \[D:STEP\_SPACE\_PROJECTION\], $\mho_{\mathbf{F}}({\mathfrak{A}}_\xi({\mathit{s}})) = {\mathbf{f}}\,' = (\psi', \phi')$ and $\mho_{\mathscr{F}}({\mathfrak{A}}_\xi({\mathit{s}})) = {\mathit{f}}'$

Definition \[D:ITERATIVE\_TRANSFORM\] evaluates ${\mathbf{f}}\,' = (\psi', \phi') = (\phi\xi, {\mathit{f}}'(\phi\xi))$ as the succeeding frame. This complex relation separates into simple conditions $\psi' = \phi\xi$ and $\phi' = {\mathit{f}}'(\phi\xi) = {\mathit{f}}'(\psi')$. The assertion ${\mathbf{f}}\,' = (\psi', \phi') = (\psi', {\mathit{f}}'(\psi'))$ bears the same meaning as ${\mathbf{f}}\,' = (\psi', \phi') \in {\mathit{f}}'$.

Definition \[D:CONSISTENT\_STEP\] states that step ${\mathfrak{A}}_\xi({\mathit{s}})$ is *consistent* if $\mho_{\mathbf{F}}({\mathfrak{A}}_\xi({\mathit{s}})) = {\mathbf{f}}\,' \in {\mathit{f}}' = \mho_{\mathscr{F}}({\mathfrak{A}}_\xi({\mathit{s}}))$, which is here satisfied.

\[T:AUTOMATON\_WALK\_PROCEDURE\] Let ${\mathfrak{A}}$ be an automaton and ${\mathbb{S}}$ be a step space with consistent step ${\mathit{s}} \in {\mathbb{S}}$ and volatile excitation $\lbrace \xi_n \rbrace$. Suppose $\lbrace {\mathit{s}}_n \rbrace$ is the walk ${\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}})$. Sequential procedure projection $\overline{\mho}_{\mathscr{F}}(\lbrace {\mathit{s}}_n \rbrace)$ covers sequential process projection $\overline{\mho}_{\mathbf{F}}(\lbrace {\mathit{s}}_n \rbrace)$.

We have the premises that step ${\mathit{s}} \in {\mathbb{S}}$ is consistent, that $\lbrace \xi_n \rbrace$ is an excitation, that ${\mathfrak{A}}$ is an automaton, and that $\lbrace {\mathit{s}}_n \rbrace$ is the walk ${\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}})$. We temporarily suppress the repetitive lengthy expression ${\mathfrak{A}}^{\mathbb{N}}_{\lbrace \xi_n \rbrace}({\mathit{s}})$ through the abbreviation ${\mathfrak{A}}^{\mathbb{N}}$.

Induction demonstrates that each step of walk ${\mathfrak{A}}^{\mathbb{N}}$ is consistent. For the base clause, the case $i = 1$ is true by hypothesis, since the initial step ${\mathfrak{A}}^{\mathbb{N}}(1) = {\mathit{s}}$ is presumed consistent. For the recursive clause, definition \[D:ITERATIVE\_OPERATOR\_WALK\] provides that ${\mathit{s}}_{i+1} = {\mathfrak{A}}(\xi_{i}, {\mathit{s}}_i)$ for each $i \ge 1$. By theorem \[T:AUTOMATON\_ITERATE\_CONSISTENT\], step ${\mathfrak{A}}(\xi_{i}, {\mathit{s}}_i) = {\mathfrak{A}}^{\mathbb{N}}(i+1)$ is consistent. By the axiom of induction, step ${\mathfrak{A}}^{\mathbb{N}}(i)$ is consistent for each $i \ge 1$.

By definition \[D:CONSISTENT\_STEP\] and the conclusion that step ${\mathfrak{A}}^{\mathbb{N}}(i)$ is consistent for each $i \ge 1$, it follows that $\mho_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}(i)) \in \mho_{\mathscr{F}}({\mathfrak{A}}^{\mathbb{N}}(i))$, also for each $i \ge 1$.

Substituting ${\mathfrak{A}}^{\mathbb{N}}= \lbrace {\mathit{s}}_n \rbrace$ into lemma \[L:RELATED\_PROJECTION\] yields frame $(\overline{\mho}_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}))(i) = \mho_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}(i))$ and functionality $(\overline{\mho}_{\mathscr{F}}({\mathfrak{A}}^{\mathbb{N}}))(i) = \mho_{\mathscr{F}}({\mathfrak{A}}^{\mathbb{N}}(i))$. From equality it then follows that $(\overline{\mho}_{\mathbf{F}}({\mathfrak{A}}^{\mathbb{N}}))(i) \in (\overline{\mho}_{\mathscr{F}}({\mathfrak{A}}^{\mathbb{N}}))(i)$ for each $i \ge 1$. In simple language, the $i^\text{th}$ term of the process projection is a member of the $i^\text{th}$ term of the procedure projection. This satisfies the requirement of definition \[D:COVERING\_PROCEDURE\] that the procedure covers the sequence of frames: ${\mathbf{f}}_i \in {\mathit{f}}_i$ for each $i \geq 1$.

Reverse inference
-----------------

The construction of automata provides that steps unfold in sequential fashion – that is, the next step becomes known after completing the current step. Consequently automata inherit an intrinsic [forward]{} orientation. It is also reasonable to inquire what may have occurred in previous steps. This question is the motivation for reverse inference, which considers automata operating backwards.

### Iterative converse {#S:ITERATIVE_CONVERSE}

Let $\langle \Psi, \Phi \rangle$ be a basis with persistent-volatile partition $\Psi = \Phi\Xi$ and step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times ({\prod{\Psi}} \times {\prod{\Phi}})$. Suppose step ${\mathit{s}}  = (\lambda, {\mathit{f}}, (\psi, \phi)) \in {\mathbb{S}}$, whence the volatile excitation of ${\mathit{s}}$ is $\xi = {{\psi}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Xi}}}}}$.

\[D:VOLATILE\_CONVERSE\] Let $\langle \Psi, \Phi \rangle$ be a basis with step space ${\mathbb{S}}$ and iterative operator $V \colon {\mathbb{S}} \to {\mathbb{S}}$. The *iterative* converse of $V$ is the mapping $\tilde{V} \colon {\mathbb{S}} \to {\mathscr{P}({{\mathbb{S}}})}$ defined by $$\tilde{V}({\mathit{s}}) = \lbrace \tilde{{\mathit{s}}} \in {\mathbb{S}} \colon V(\tilde{{\mathit{s}}}) = {\mathit{s}} \rbrace,$$ where ${\mathscr{P}({{\mathbb{S}}})}$ denotes the power set of ${\mathbb{S}}$ (in other words, the iterative converse is a mapping from a step to a set of steps).

### Converse actuated automaton {#S:CONVERSE_AUTOMATON}

An actuated automaton ${\mathfrak{A}} = \langle \Psi, \Phi, {\mathscr{F}}\!, {\mathsf{A}}, \Lambda, \ell, \Delta \rangle$ induces an iterative operator on step space. Reverse inference is identifying all immediate predecessor steps ${{\mathit{s}}_{n-1}}$ such that ${\mathit{s}}_n = {\mathfrak{A}}({\mathit{s}}_{n-1})$. We have obviously $$\tilde{{\mathfrak{A}}}({\mathit{s}}) = \lbrace \tilde{{\mathit{s}}} \in {\mathbb{S}} \;\colon\; {\mathfrak{A}}(\tilde{{\mathit{s}}}) = {\mathit{s}} \rbrace.$$

Although referring informally to the converse $\tilde{{\mathfrak{A}}}$ of an automaton ${\mathfrak{A}}$, speaking precisely we have defined the converse $\tilde{{\mathit{s}}}$ of a *step* ${\mathit{s}} \in {\mathbb{S}}$ within the step space associated with that automaton.

A system of equations ensues with subscripted variables known and held constant, and unsubscripted variables free. Roots of the system represent discrete solutions. Let us look carefully at the further case that ${\mathit{s}} = (\lambda, {\mathit{f}}, {\mathbf{f}}) = (\lambda, {\mathit{f}}, (\psi, \phi)) \in \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$. $$\begin{aligned}
\tilde{{\mathfrak{A}}}(\lambda_0, {\mathit{f}}_0, {\mathbf{f}}_0) &= \lbrace (\lambda, {\mathit{f}}, {\mathbf{f}}) \in {\mathbb{S}} \;\colon\; 
    {\mathfrak{A}}(\lambda, {\mathit{f}}, {\mathbf{f}}) = (\lambda_0, {\mathit{f}}_0, {\mathbf{f}}_0) \rbrace \\
\tilde{{\mathfrak{A}}}(\lambda_0, {\mathit{f}}_0, (\psi_0, \phi_0)) &= \lbrace (\lambda, {\mathit{f}}, (\psi, \phi)) 
    \in {\mathbb{S}} \;\colon\; {\mathfrak{A}}(\lambda, {\mathit{f}}, (\psi, \phi)) = (\lambda_0, {\mathit{f}}_0, (\psi_0, \phi_0)) \rbrace.\end{aligned}$$

### Constraining equations {#S:CONSTRAINING_EQUATIONS}

State transition in an actuated automaton is built in three successive phases: locus state, functionality state, and frame state.

Definition \[D:ITERATIVE\_TRANSFORM\] presents rules governing forward state transition in the form of three equations, portraying current state as known and unknown future state as uniquely determined by formulas. This sense can be reversed, with current state known and feasible past states represented as unknowns.

The automaton-induced *forward* transformation ${\mathfrak{A}} \colon {\mathbb{S}} \to {\mathbb{S}}$ has been set (definition \[D:ITERATIVE\_TRANSFORM\]) as $$\begin{aligned}
  \lambda' &= \Delta(\lambda, \psi),\\
  {\mathit{f}}' &= (\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi'),\\
  {\mathbf{f}}\,' &= (\psi', \phi') = 
            ([{\mathit{f}}(\psi) \xi'], [(\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi')]([{\mathit{f}}(\psi) \xi'])).\end{aligned}$$

The respective governing *backwards* transformations are $$\begin{aligned}
  \lambda_0 &= \Delta(\lambda, \psi),\\
  {\mathit{f}}_0 &= (\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi_0),\\
  {\mathbf{f}}_0 &= (\psi_0, \phi_0) = 
            ([{\mathit{f}}(\psi) \xi_0], [(\ell(\Delta(\lambda, \psi)))({\mathit{f}}(\psi) \xi_0)]([{\mathit{f}}(\psi) \xi_0])).\end{aligned}$$

Due to conjointness, $\psi_0 = {\mathit{f}}(\psi) \xi_0 = \phi_0 \xi_0$ throughout: $$\begin{aligned}
  \lambda_0 &= \Delta(\lambda, \psi),\\
  {\mathit{f}}_0 &= (\ell(\Delta(\lambda, \psi)))(\psi_0),\\
  {\mathbf{f}}_0 &= (\psi_0, \phi_0) = (\psi_0, [(\ell(\Delta(\lambda, \psi)))(\psi_0)](\psi_0)])).\end{aligned}$$

Substituting $\lambda_0 = \Delta(\lambda, \psi)$ and ${\mathsf{a}}_0 = \ell(\lambda_0)$ into the last two formulas, $$\begin{aligned}
  \lambda_0 &= \Delta(\lambda, \psi),\\
  {\mathit{f}}_0 &= (\ell(\lambda_0)(\psi_0) = {\mathsf{a}}_0(\psi_0),\\
  {\mathbf{f}}_0 &= (\psi_0, \phi_0) = (\psi_0, [(\ell(\lambda_0))(\psi_0)](\psi_0)])) = (\psi_0, [{\mathsf{a}}_0(\psi_0)](\psi_0)])).\end{aligned}$$

Finally, substituting ${\mathit{f}}_0 = {\mathsf{a}}_0(\psi_0)$ into the last two formulas, $$\begin{aligned}
  \lambda_0 &= \Delta(\lambda, \psi),\\
  {\mathit{f}}_0 &= {\mathit{f}}_0,\\
  {\mathbf{f}}_0 &= (\psi_0, {\mathit{f}}_0(\psi_0)) = {\mathbf{f}}_0.\end{aligned}$$

Only the first of these is a [real]{} constraint; the others are identities.

### Solution set {#S:SOLUTION_SET}

A feasible set for an equation is the collection of values that satisfy the equation. Producing the solution for a system of constraining equations involves intersecting the individual feasible sets $Q_i$. The general solution set for the system of equations is $Q = \bigcap_i Q_i$.

The case of the converse automaton $\tilde{{\mathfrak{A}}}$ consists of three constraining equations (§\[S:CONSTRAINING\_EQUATIONS\]). First of these is $\lambda_0 = \Delta(\lambda, \psi)$. Let ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times (\;{\prod{\Psi}} \times {\prod{\Phi}})$ be a fully elaborated step space. In set-builder notation the feasible set is $Q_1 = \lbrace (\lambda, {\mathit{f}}, (\psi, \phi)) \in {\mathbb{S}} \colon \lambda_0 = \Delta(\lambda, \psi) \rbrace$. The other constraints are identities, which all members of ${\mathbb{S}}$ satisfy – in other words, $Q_2 = Q_3 = {\mathbb{S}}$. The general solution is $Q = Q_1 \cap Q_2 \cap Q_3 = Q_1 \cap {\mathbb{S}} \cap {\mathbb{S}} = Q_1$, or $Q = \lbrace (\lambda, {\mathit{f}}, (\psi, \phi)) \in {\mathbb{S}} \colon \lambda_0 = \Delta(\lambda, \psi) \rbrace$. An understandable abuse of terminology says that the solution set is $\lambda_0 = \Delta(\lambda, \psi)$, which is technically a constraining equation.

Cone {#S:CONE_SECTION}
----

A cone is a construct prepared with the iterative converse of an actuated automaton. It consists of all finite backwards walks converging to a given point. The term [cone]{} is more ideologic than geometric.

### Description {#S:CONE_DESCRIPTION}

The actuated automaton possesses a non-deterministic[^4] converse relation. See §\[S:ITERATIVE\_CONVERSE\].

A collection of reverse walks is realized through repetitive re-application of the converse, converging to a designated *crux* step. These iterative chains may be localized (trimmed to finite length) by enforcing some stopping criterion. This construction results in the cone, a structured set of possible localized walks eventually leading to the crux step. The starting points of such walks are known as *precursor* steps of the crux step.

### Inductive generation {#S:CONE_GENERATION}

Let ${\mathbb{S}}$ be a step space containing crux step ${\mathit{s}}_{\text{crux}}$. Suppose $V \colon {\mathbb{S}} \to {\mathbb{S}}$ is an iterative operator with converse $\tilde{V} \colon {\mathbb{S}} \to {\mathscr{P}({{\mathbb{S}}})}$.

(base clause) Let base protoset $G_\heartsuit^{(0)} = \lbrace {\mathit{s}}_\text{crux} \rbrace$ be the $0^{\text{th}}$ predecessor generation of ${\mathit{s}}_{\text{crux}}$.

(inductive clause) The ${(n+1)}^{\text{st}}$ generation predecessors are defined in terms of the $n^{\text{th}}$ generation: $$G_\heartsuit^{(n+1)} = 
    \bigcup_{{\mathit{s}} \in G_\heartsuit^{(n)}} \tilde{V}({\mathit{s}}).$$

This definition places protoset $G_\heartsuit^{(1)} = \tilde{V}({\mathit{s}}_{\text{crux}})$.

For a discussion of protoset $G_\heartsuit^{(n)}$ in context of the Cartesian product, see Appendix §\[D:PROTOSET\].

### Partial order {#S:CONE_ORDER}

Membership in a converse iterative operator induces a partial ordering:

Let ${\mathbb{S}}$ be a step space with converse iterative operator $\tilde{V} \colon {\mathbb{S}} \to {\mathscr{P}({{\mathbb{S}}})}$. If ${\mathit{s}}' \in \tilde{V}({\mathit{s}})$, then ${\mathit{s}}'$ *precedes* ${\mathit{s}}$, written ${\mathit{s}}' \prec {\mathit{s}}$.

### Predecessor walk {#S:CONE_WALK}

A predecessor walk begins at step ${\mathit{s}}_0 = {\mathit{s}}_{\text{crux}}$ and proceeds backwards, indexing through the negative integers. In this case we abuse the proper sense of the term [sequence]{} by permitting an indexing not being the natural numbers.

Let ${\mathbb{S}}$ be a step space. A localized predecessor walk starting with step ${\mathit{s}}_0 = {\mathit{s}}_{\text{crux}}$ is a *finite* sequence in step space such that ${\mathit{s}}_{i-1} \prec {\mathit{s}}_i$ for every $i \leq 0$.

For example in the case $i = -2$, we have ${\mathit{s}}_{-3} \prec {\mathit{s}}_{-2}$.

Since a localized predecessor walk ${\mathit{w}}$ is a *finite* sequence of steps, then it has a finite number of terms which run in index $i$ from $-(n-1) \leq i \leq 0$, where $n = {\lvert{{\mathit{w}}}\rvert} < \infty$ is the number of steps in ${\mathit{w}}$.

\[S:COMPLETE\_CONE\_WALK\] A set ${\mathbb{W}}$ of localized predecessor walks, all starting at ${\mathit{w}}_0 = {\mathit{s}}_{\text{crux}}$, is *complete* if\
$$\forall({\mathit{w}} \in {\mathbb{W}}) 
\forall(-({\lvert{{\mathit{w}}}\rvert}-2) \leq i \leq 0) 
\forall({\mathit{s}} \in \tilde{V}({\mathit{w}}_{i}))
\exists({\mathit{e}} \in {\mathbb{W}})
     : {\mathit{w}}_{i} = {\mathit{e}}_{i} \wedge {\mathit{s}} = {\mathit{e}}_{i-1}.$$

Completeness assures combinatorial diversity. An algorithm equivalent to the above one-liner is:\
\
$
\text{for each }{\mathit{w}} \text{ in }{\mathbb{W}} \text{ begin}\\
\text{\quad\quad \# number of steps in localized walk is } {\lvert{{\mathit{w}}}\rvert}\\
\text{\quad\quad \# abused index runs between 0 [for start step } {\mathit{w}}_{\text{crux}} \text{] and } 
    -({\lvert{{\mathit{w}}}\rvert}-1) \text{ [last predecessor step]}\\
\text{\quad\quad \# no iteration through } i = -({\lvert{{\mathit{w}}}\rvert}-1) \text{ because then } 
    {\mathit{s}} \text{ == } {\mathit{e}}_{i-1} \text{ below would be undefined}\\
\text{\quad\quad for }i = 0 \text{ downto } -({\lvert{{\mathit{w}}}\rvert}-2)  \text{ begin}\\
\text{\quad\quad\quad\quad for each }{\mathit{s}} \text{ in } \tilde{V}({\mathit{w}}_{i}) \text{ begin}\\
\text{\quad\quad\quad\quad\quad\quad if there is a member }{\mathit{e}} \in {\mathbb{W}} \text{ such that }
    {\mathit{w}}_{i} \text{ == } {\mathit{e}}_{i} \text{ and }{\mathit{s}} \text{ == } {\mathit{e}}_{i-1} \text{ then}\\
\text{\quad\quad\quad\quad\quad\quad\quad\quad answer = TRUE}\\
\text{\quad\quad\quad\quad\quad\quad else}\\
\text{\quad\quad\quad\quad\quad\quad\quad\quad answer = FALSE}\\
\text{\quad\quad\quad\quad\quad\quad if answer == FALSE then return FALSE}\\
\text{\quad\quad\quad\quad end}\\
\text{\quad\quad end}\\
\text{end}\\
\text{return TRUE}\\
$

\[S:DEPENDENT\_CONE\_WALK\] Let ${\mathit{w}}$ and ${\mathit{w}}'$ be localized predecessor walks starting at ${\mathit{w}}_0 = {\mathit{w}}_0' = {\mathit{s}}_{\text{crux}}$. Suppose the length of ${\mathit{w}}$ is ${\lvert{{\mathit{w}}}\rvert} = n$ and the length of ${\mathit{w}}'$ is ${\lvert{{\mathit{w}}'}\rvert} = m$, with $m \leq n$. If ${\mathit{w}}'(i) = {\mathit{w}}(i)$ for every $-(m-1) \leq i \leq 0$, then ${\mathit{w}}$ and ${\mathit{w}}'$ are *dependent* with ${\mathit{w}}'$ *dispensable*.

\[S:INDEPENDENT\_CONE\_WALK\] Let ${\mathbb{W}}$ be a set of localized predecessor walks starting at ${\mathit{s}}_0 = {\mathit{s}}_{\text{crux}}$. The set is *independent* if it contains no dispensable member.

### Cone {#S:CONE_CONE_WALK}

\[S:CONE\_DEFINITION\] A *cone* ${\mathcal{C}}$ is a complete independent set of localized predecessor walks starting at ${\mathit{s}}_{\text{crux}}$.

[\[Stopping rule\]]{} We avoid the specificity of various stopping criteria (§\[S:CONE\_DESCRIPTION\]) by introducing the equivalent but arbitrary notion of localization.

\[S:CONE\_EDGE\_STEP\] Let ${\mathcal{C}}$ be a cone with ${\mathit{w}} \in {\mathcal{C}}$ a member localized predecessor walk. Suppose $n = {\lvert{{\mathit{w}}}\rvert}$ is the number of steps in ${\mathit{w}}$. The terminus ${\mathit{w}}(-(n-1)) = {\mathit{w}}_{-(n-1)}$ is the *edge step* of walk ${\mathit{w}}$.

\[S:CONE\_EDGE\] Let ${\mathcal{C}}$ be a cone. Its *edge*, written ${{\operatorname{edge}{{\mathcal{C}}}}}$, is the collection of edge steps of all member localized predecessor walks.

\[S:ACYLIC\_CONE\] An *acyclic* cone has no cycle (loop) in its path projection $\overline{\mho}_\Lambda$ (see §\[D:EXTENDED\_PROJECTION\]).

\[T:ACYLIC\_CONE\_CORRESPONDENCE\] The acyclic cone ${\mathcal{C}}$ and ${{\operatorname{edge}{{\mathcal{C}}}}}$ are in one-to-one correspondence via the edge step relation of a localized predecessor walk.

Assume the opposite: there are different localized predecessor walks with the same edge step. Let ${\mathit{u}}$ and ${\mathit{v}}$ be two different walks with common edge step ${\mathit{s}}_\text{common}$.

Suppose ${\lvert{{\mathit{u}}}\rvert} = m$ and ${\lvert{{\mathit{v}}}\rvert} = n$, so the indexes of ${\mathit{s}}_\text{common}$ are $-(m-1)$ and $-(n-1)$ respectively.

We assert that if ${\mathit{u}}_{-(m-1)+i} = {\mathit{v}}_{-(n-1)+i}$ for some $0 \leq i$, then ${\mathit{u}}_{-(m-1)+(i+1)} = {\mathit{v}}_{-(n-1)+(i+1)}$.

Suppose sequencing is governed by an actuated automaton ${\mathfrak{A}}$. So sequenced, the next step in predecessor walk ${\mathit{u}}$ is ${\mathit{u}}_{-(m-1)+(i+1)} = {\mathfrak{A}}({\mathit{u}}_{-(m-1)+i})$. Similarly, the next step in ${\mathit{v}}$ is ${\mathit{v}}_{-(n-1)+(i+1)} = {\mathfrak{A}}({\mathit{v}}_{-(n-1)+i})$. But if ${\mathit{u}}_{-(m-1)+i} = {\mathit{v}}_{-(n-1)+i}$, then ${\mathfrak{A}}({\mathit{u}}_{-(m-1)+i}) = {\mathfrak{A}}({\mathit{v}}_{-(n-1)+i}) = {\mathfrak{A}}({\mathit{s}})$. By transitivity of equality, ${\mathit{u}}_{-(m-1)+(i+1)} = {\mathfrak{A}}({\mathit{s}}) = {\mathit{v}}_{-(n-1)+(i+1)}$.

Without loss of generality suppose $m \leq n$. Then ${\mathit{u}}_{-(m-1)+i} = {\mathit{v}}_{-(n-1)+i}$ is true for $i = 0, 1, \;...\; m-1$. At $i = m - 1$ we have ${\mathit{s}}_{\text{crux}} = {\mathit{u}}_0 = {\mathit{v}}_{-(n-1)+(m-1)} = {\mathit{v}}_{-(n-m)}$. Since ${\mathit{v}}$ is a localized predecessor walk of a cone, then ${\mathit{v}}_0 = {\mathit{s}}_{\text{crux}}$. But ${\mathit{v}}_0 = {\mathit{s}}_{\text{crux}} = {\mathit{v}}_{-(n-m)}$. Because the cone is assumed acyclic, ${\mathit{v}}_0$ and ${\mathit{v}}_{-(n-m)}$ must then be the same identical step – that is, $m = n$.

Here the assumption of two different local predecessor walks with the same edge step leads to the contradiction that both are indeed the same identical walk. This means local predecessor walks within an acyclic cone ${\mathcal{C}}$ are in one-to-one correspondence with ${{\operatorname{edge}{{\mathcal{C}}}}}$ via the edge step relation.

Operational profile {#S:OPERATIONAL_PROFILE_SECTION}
-------------------

An operational profile is a limit of the cumulative history of software execution ratios under normal operations (which is troublesome to define).

This section frequently uses the compound idiom that $\{x_n\}$ represents an anonymous sequence of objects of the same type as $x$. That is, if $X$ is the set of all $x_i$, then $\{x_n\} \colon {\mathbb{N}}\to X$.

### Musa’s operational profile {#S:MUSA_OP_PROFILE}

Musa et al intended operational profiles as a tool for analysis of software reliability. A notion of the operational profile appeared in their pioneering exposition [@jM87]. This reference gives a definition in terms of the program’s higher purpose, as reflected in run types. Consequently an operational profile is the set of run types that the program can execute along with the probabilities they will occur. One can easily envision its extension to smaller program units.

### Extended operational profile {#S:EXTENDED_OP_PROFILE}

We shall extend run types into steps, the elementary quantum of automata. This detaches the operational profile concept from notions such as run types which are part of human understanding rather than algorithmic structure (however, the idea pops up elsewhere). Despite appearances, this extension is not so large – the only addition is a method for counting step events.

### Counting {#S:COUNTING}

Let $\{{\mathit{s}}_n\}$ be a walk (infinite sequence of steps) and let $Z$ be an arbitrary reference set of steps (members of step space ${\mathbb{S}} = \Lambda \times {\mathscr{F}} \times {\mathbf{F}}$). Simply summarized, $N_Z(\{{\mathit{s}}_n\},k)$ denotes the number of occurrences of any member of $Z$ before or at the ${{k}^{\text{th}}}$ automaton step.

Details follow for those interested. When the ${{i}^{\text{th}}}$ step of the walk is a member of $Z$ (${{\mathit{s}}_i} \in Z$), then $\{{\mathit{s}}_n\}$ is said to *arrive* at $i$.

\[D:ARRIVAL\] An *arrival* function is a sequence $\varphi \colon \{1,2,\cdots\} \to \{n_1,n_2,\cdots\}$ mapping each arrival, as identified by its ordinal occurrence number $i$, into its frame sequence number $n_i$.

The arrival function assumes the natural order, that is, $i < j$ implies $n_i < n_j$.

A related function counts *how many* arrivals occur within a given interval:

\[D:COUNTING\] Suppose $\{{\mathit{s}}_n\}$ is a walk and $Z$ is a set of steps. Let $\varphi$ be an arrival function. The *counting* function $N_Z \colon {\mathbb{S}}^{{\mathbb{N}}} \times {\mathbb{Z}^+}\to {\mathbb{Z}^+}$ induced by $\varphi$ is $$N_Z(\{{\mathit{s}}_n\}, k) = \max_{\varphi(i) \leq k} \: i ,$$ and for completeness set $\max(\varnothing) = 0$.

### Normal operations {#S:NORMAL_OPERATIONS}

The idea behind [normal operations]{} is a long program run following a software usage pattern. Interaction with the environment affects software behavior, which is ultimately transmitted through response to changing volatile variables. Normal operations calls for a run of figuratively unbounded duration during which software experiences the usage pattern’s variation of volatile stimulus, in response to which possibly unbalanced service is demanded from its inventory of functions.

Systems engineering often augments what is here the automaton’s step poset with a transition network of modes. These modes symbolically encapsulate enabled or disabled capabilities. However, even though this augmentation facilitates visualization of behaviors, it fails to be mathematically definitive[^5].

#### Orbit {#S:ORBIT}

We have not defined normal operations, but every example would certainly constitute a walk (sequence of steps). A special walk illustrating normal operations (as described above) will be termed here an *orbit*. Without formal definition, use of this term sacrifices rigor.

The actuated automaton governs pure step transition logic, but an orbit also reflects a usage pattern.

#### Limit conjecture {#S:LIMIT_CONJECTURE}

Orbits may differ in specific sequence and content, but they have the same limit ratios. We consider a case drawn with the counting procedure of §\[S:COUNTING\].

\[T:LIMIT\_RATIO\] For different orbits ${\mathit{o}} = \{{\mathit{s}}_n\}$ and ${\mathit{o}}' = \{{\mathit{s}}'_n\}$ having the same usage pattern, $$\lim_{\;k \to \infty} \frac{N_U(\{{\mathit{s}}_n\}, k)}{N_Z(\{{\mathit{s}}_n\}, k)} = 
\lim_{\;k \to \infty} \frac{N_U(\{{\mathit{s}}'_n\}, k)}{N_Z(\{{\mathit{s}}'_n\}, k)}$$ for sets of steps $\varnothing \neq U \subseteq Z \subseteq {\mathbb{S}}$.

### Types of operational profile {#S:TYPES_OP_PROFILE}

A relative operational profile is the conditional probability that a step in an actuated automaton’s orbit coincides with a particular member of the reference set, given that it agrees with the reference set. We consider one other: an absolute operational profile is the time rate at which a particular step of an orbit coincides with any member of the reference set.

### Relative operational profile {#S:RELATIVE_OP_PROFILE}

Let ${\mathit{o}} = \{{\mathit{s}}_n\}$ be an orbit. Suppose $z \in Z \subset {\mathbb{S}}$ is a step of the reference set. Software encounters $N_{\{z\}}(\{{\mathit{s}}_n\}, k)$ instances of steps satisfying $\lbrace {\mathit{s}}_n \rbrace(i) = {\mathit{s}}_i = z$ during the first $k$ automaton steps. In the same execution there are $N_Z(\{{\mathit{s}}_n\}, k)$ instances of ${\mathit{s}}_i \in Z$. In the frequentist [@wW14fp] school of interpreting probability, $$P(z \mid Z) = \lim_{\;k \to \infty} \frac{N_{\{z\}}(\{{\mathit{s}}_n\}, k)}{N_Z(\{{\mathit{s}}_n\}, k)}$$ represents the conditional probability of occurrence of $z$, given that $Z$ occurs. By Conjecture \[T:LIMIT\_RATIO\], every orbit (of the same usage pattern) yields the same relative operational profile.

A relative operational profile is an arbitrary set $Z$ of steps, along with each step’s conditional probability of execution. In other words, a relative operational profile is a mapping $\mathcal{O} \colon Z \to [0,1]$ having total measure 1.

### Absolute operational profile {#S:ABSOLUTE_OP_PROFILE}

Let ${\mathit{o}} = \{{\mathit{s}}_n\}$ be an orbit. An absolute operational profile is the probability $P(Z)$ with which an orbit (of some usage pattern) coincides with any step of the reference set $Z$. As before, this probability is the limiting ratio of two counting functions. Its numerator contains $N_Z(\{{\mathit{s}}_n\}, k)$, the same count as appears in the denominator of the relative operational profile. In its denominator is the counting function of all possible steps, namely $N_{{\mathbb{S}}}(\{{\mathit{s}}_n\}, k)$, where ${\mathbb{S}}$ is the space of all steps. Thus the ratio of counting functions of reference set $Z$ to the entire space ${\mathbb{S}}$ is $\frac{N_Z(\{{\mathit{s}}_n\}, k)}{N_{{\mathbb{S}}}(\{{\mathit{s}}_n\}, k)} = \frac{N_Z(\{{\mathit{s}}_n\}, k)}{k}$, and the absolute operational profile (of collection $Z$) is $$P(Z) = \lim_{\;k \to \infty} \frac{N_Z(\{{\mathit{s}}_n\}, k)}{k}.$$

### Conversion into a rate {#S:ABSOLUTE_OP_PROFILE_RATE}

Section \[S:INTRO\_REACTIVE\] mentions the synchronization function, a cross-reference between discrete and real time. During each step, an amount of real time appropriate for a software system emulating the automaton’s step is added to the time consumption budget. Let $Z$ be the usual arbitrary reference collection of steps and ${\mathit{o}} = \{{\mathit{s}}_n\}$ be an orbit. These two provide a set of events and a sequence of steps in which to count the events’ arrivals. The synchronization records discrete pairs $(i, t_i)$, where $i$ is the index of the automaton step and $t_k$ is the total elapsed time after $k$ steps. Call this mapping the synchronization function, having the formalism $\sync \colon {\mathbb{S}}^{\mathbb{N}}\times {\mathbb{N}}\to {\mathbb{R}^+}$, along with assumed starting point $\sync(\{{\mathit{s}}_n\}, 0) = 0$.

Let the sequence index of each step be the discrete analog of time. Of course, this has the effect that discrete software time will not hold proportional to hardware real time. The approximate real time required by execution of step ${\mathit{s}} = (\lambda, {\mathit{f}}, {\mathbf{f}})$ is $\tau({\mathit{f}})$ – that is, elapsed real time is taken as a function of the executing functionality.

\[D:SYNC\_APPOX\] For orbit ${\mathit{o}} = \{{\mathit{s}}_n\}$, approximate time elapsed during the first $k$ steps accumulates to $$\sync(\{{\mathit{s}}_n\}, k) = \sum_{i=1}^k \tau({\mathit{f}}_i)) = \sum_{i=1}^k \tau(\mho_{{\mathscr{F}}}({\mathit{s}}_i)) = t_k.$$

A theorem to avoid creating dependency on specific orbits is in order. Inability to define normal operations leads instead to conjecture, expressing such need:

\[T:TIME\_RATIO\] For different orbits ${\mathit{o}} = \{{\mathit{s}}_n\}$ and ${\mathit{o}}' = \{{\mathit{s}}'_n\}$ having the same usage pattern, $$\lim_{\;k \to \infty} \frac{N_Z(\{{\mathit{s}}_n\}, k)}{{\sync}(\{{\mathit{s}}_n\}, k)} = 
\lim_{\;k \to \infty} \frac{N_Z(\{{\mathit{s}}'_n\}, k)}{{\sync}(\{{\mathit{s}}'_n\}, k))}$$ for a reference set of steps $\varnothing \neq Z \subseteq {\mathbb{S}}$.

The synchronization function allows expression of the absolute operational profile as an intensity (rate or quasi-frequency).

The *counting norm* is written using the double bar notation ${\Vert{\cdot}\Vert}$: $${\Vert{Z}\Vert} = \lim_{\;k \to \infty} \frac{N_Z(\{{\mathit{s}}_n\}, k)}{\sync(\{{\mathit{s}}_n\}, k)}.$$

The absolute operational profile is properly a subadditive seminorm on sets of steps. As the limiting ratio of two counts in the natural numbers, the norm is positive. The norm is a seminorm because for some nonempty set $Z$ it may be true that ${\Vert{Z}\Vert} = 0$ (if the usage pattern does not activate any member of the reference set). This norm is subadditive because for any other set $S$, $N_{Z \cup S}(\{{\mathit{s}}_n\}, k) \leq N_Z(\{{\mathit{s}}_n\}, k) + N_S(\{{\mathit{s}}_n\}, k)$. It follows that ${\Vert{Z \cup S}\Vert} \leq {\Vert{Z}\Vert} + {\Vert{S}\Vert}$.

Application
===========

The safety demonstration furnishes data for the indemnification statistic, which originates in the compound Poisson random process.

Reliability demonstration
-------------------------

A reliability demonstration is a structured random experiment carrying controlled statistical uncertainty and providing [hard]{} evidence against potential liability.

### Safety demonstration {#S:SAFETY_DEMONSRATION}

In software safety analysis, a hazard is a region of code bearing potential harmful side effects if incorrectly implemented. A safety demonstration is a special type of reliability demonstration posed to exercise a hazard. Here the region is presumed to be an acyclic cone, with the hazard located at its crux. The crux is a point of software/hardware transduction, illustrating the principle of emergence[^6] (see §\[S:PRINCIPLE\_OF\_EMERGENCE\]).

To oversimplify, a safety demonstration is a random sample from such a region (acyclic cone). The complete story is not so simple, because the cone is not a probabilistic structure; it possesses no probability to support randomness.

As a probabilistic structure, the operational profile (§\[S:RELATIVE\_OP\_PROFILE\]) permits random sampling from its reference set, regardless of its higher level meaning. As the edge of a cone is a set, it can become a relative operational profile’s reference set. Thus we tie an operational profile to a cone’s edge. Let $\mathcal{O} \colon {{\operatorname{edge}{{\mathcal{C}}}}} \to [0,1]$ be a relative operational profile on the edge of cone ${\mathcal{C}}$. At this stage we have the ability to draw a random sample from ${{\operatorname{edge}{{\mathcal{C}}}}}$.

Theorem \[T:ACYLIC\_CONE\_CORRESPONDENCE\] asserts that an acyclic cone ${\mathcal{C}}$ and ${{\operatorname{edge}{{\mathcal{C}}}}}$ are in one-to-one correspondence via the edge step relation of a localized predecessor walk. Equivalent to the one-to-one correspondence is the bijection $\mathbf{b} = \{({{\operatorname{edge}{{\mathit{w}}}}},{\mathit{w}}) \colon {\mathit{w}} \in {\mathcal{C}}\}$. For ${\mathit{e}} \in {{\operatorname{edge}{{\mathcal{C}}}}}$, $\mathbf{b}({\mathit{e}})$ is the bijectively corresponding localized predecessor walk.

We now bijectively associate the random edge event ${\mathit{e}} = \mathbf{b}^{-1}({\mathit{w}})$ with the localized predecessor walk ${\mathit{w}}$: $\mathcal{O}' = \{ (\mathcal{O}(\mathbf{b}^{-1}({\mathit{w}})), {\mathit{w}}) \colon {\mathit{w}} \in {\mathcal{C}} \}$. With probability inherited from an operational profile, we can speak validly of a random sample from a cone.

### Tests {#S:TESTS}

The last piece of the safety demonstration story is converting local predecessor walks into tests. Localized predecessor walks are finite walks existing in confusion-prone backwards time. One may skip this section unless he wishes the detail of converting backward to forward walks.

The *test* function reverses and re-indexes localized predecessor walks into conventional sequences.

\[D:TEST\] Let ${\mathit{w}}$ be a localized predecessor walk of $n = {\lvert{{\mathit{w}}}\rvert}$ steps, indexed from $0$ down to $-(n-1)$. Define the *test* function $\test({\mathit{w}})  = \widetilde{{\mathit{w}}}$ according to formula $\widetilde{{\mathit{w}}}_i = {\mathit{w}}_{i - n}$ for $i = 1, 2, \cdots , n$.

Assuming that a localized predecessor walk is indexed from $0$ down to $-(n-1)$, its corresponding test will be indexed from $1$ to $n$. In sense of direction, the localized predecessor walk traverses steps from ${\mathit{s}}_{\text{crux}}$ to ${\mathit{s}}_{\text{edge}}$, while the corresponding test traverses steps from ${\mathit{s}}_{\text{edge}}$ to ${\mathit{s}}_{\text{crux}}$.

Suppose ${\mathcal{C}}$ is an acyclic cone and ${\mathbb{W}} \subset {\mathcal{C}}$ is a (unique) set of localized predecessor walks. If $\widetilde{{\mathbb{W}}} = \test({\mathbb{W}})$ is its converted set of reversed and re-indexed tests, then ${\mathbb{W}}$ and $\widetilde{{\mathbb{W}}}$ are in one-to-one correspondence.

By virtue of construction, $\test$ is already a mapping. Remaining to show is that $\test$ is additionally a bijection. Let ${\mathit{u}}$ and ${\mathit{v}}$ be localized predecessor walks and ${\mathit{x}}$ be a finite walk. As hypothesis set ${\mathit{x}} = \test({\mathit{u}})  = \test({\mathit{v}})$. These sequences cannot be equal unless they possess the same number of terms, $n = {\lvert{{\mathit{x}}}\rvert} = {\lvert{\test({\mathit{u}})}\rvert} = {\lvert{\test({\mathit{v}})}\rvert}$. Since transformation $\test$ preserves the number of steps (from Definition \[D:TEST\] ${\lvert{{\mathit{w}}}\rvert} = {\lvert{\test({\mathit{w}})}\rvert}$), then $n = {\lvert{{\mathit{x}}}\rvert} = {\lvert{{\mathit{u}}}\rvert} = {\lvert{{\mathit{v}}}\rvert}$.

Again invoking Definition \[D:TEST\] on the first part of the hypothesis, we write ${\mathit{x}}_i = {\mathit{u}}_{i - n}$. The second part similarly yields ${\mathit{x}}_i = {\mathit{v}}_{i - n}$. By equating the two parts, we now have ${\mathit{u}}_{i - n} = {\mathit{v}}_{i - n}$ for each $i$. In other words, the two localized predecessor walks are actually the same walk: ${\mathit{u}} = {\mathit{v}}$. Thus $\test$ is a bijection.

#### Volatile variables preservation {#S:VOLATILE_VARIABLES}

The danger in reversed thinking about tests is inadvertently conceptualizing volatile variables as free. This is untrue, as the volatile variables at any stage of a predecessor chain are fixed, and the [next]{} stage considers the set of what previous conditions may have led to the current stage. Thus, predecessor walks are chains of a poset of steps, which include the settings of volatile variables. One must be mindful to reproduce all volatile stimuli of the localized predecessor walk in its analogous test.

### Outcome {#S:OUTCOME}

The outcome of a test, pass or fail, will be regarded as a Bernoulli random event, $P_\rho = \rho^n {(1 - \rho)}^{1 - n}$, for $n = 1$ (pass) or $n = 0$ (fail). These probabilities are statistically independent of the bias involved with drawing the sample from the operational profile. This bias affects the origin of discovered failures, but not how many failures are found. In other words, the total statistical power of the sampling plan is not affected by sampling bias.

Sums of independent Bernoulli random variables are binomial. That is, the probability of finding $n$ failures collectively among $N$ sample items is binomial, $\binom{N}{n} \rho^n {(1 - \rho)}^{N - n}$.

### Physics {#S:PHYSICS}

In the real world, tests pass or fail depending on whether the information transduced at step ${\mathit{s}}_\text{crux}$ meets all safety constraints. Such engineering requirements are varied, ultimately involving position, timing, voltage, insulation, dimensional tolerance, toxicity, temperature, mechanical shielding, luminosity, and hydrostatic pressure – just to name a few areas. Review of a test offers a last chance to discover a missed constraint (requirement). Another possibility is that the chain of precursor events should actually lead to a different conclusion.

Transduced values potentially control the status of any safety concern. Tests simply pass or fail, but evaluation of why a test passes or fails can become nontrivial, requiring collaboration between mechanical, software, and system safety engineers.

### Statistics {#S:STATISTICS}

Some statistical error originates in inference from random sample to [unknown]{} population (parametric family of probability distributions on a measurable space). Just one distribution is true, while the others are false. An assertion separating the parameterization into two decision units is called a hypothesis. One decision unit is traditionally designated null, while the other is called alternate. The true distribution belongs either to the null or alternative decision units.

Each sample item either passes or fails its associated test (see §\[S:PHYSICS\]). Within the entire cone ${\mathcal{C}}$, suppose the proportion of tests that fail is $\rho$. This proportion is subsequently realized approximately through a random sample. Regardless of the sample size, since the application is to safety, the only cases of interest will be when the number of failures is zero. Other cases, implying need for reliability growth, are treated in the literature, particularly [@jM87].

We now examine the case defined by drawing a random sample of size $N$ from ${{\operatorname{edge}{{\mathcal{C}}}}}$ and allowing $n = 0$ failures in the associated tests from cone ${\mathcal{C}}$. The null decision unit contains the probability distribution $P_0(\text{pass}) = 1$ and $P_0(\text{fail}) = 0$. The alternate decision unit is the set of probability distributions $P_\rho$ having $0 < \rho \leq 1$. Hypothesis evaluation entails two types of error, known as $\alpha$ and $\beta$ error.

#### False rejection ($\alpha$ error) {#S:FALSE_REJECTION}

The first is false rejection of the null decision unit, with associated measurement error $\alpha$. The sampling plan can reject only if finds an error, so this sampling plan is incapable of false rejection. Thus $\alpha \equiv 0$.

#### False acceptance ($\beta$ error) {#S:FALSE_ACCEPTANCE}

The second is false acceptance of the null decision unit, with associated measurement error $\beta$. We experience false acceptance when $0 < \rho$ but the sample contains no failures.

Under the binomial model, the probability of observing a random sample of size $N$ with $n$ failures collectively is $\binom{N}{n} \rho^n {(1 - \rho)}^{N - n}$. Proceeding to our case of interest, $n = 0$, we have $\binom{N}{n} \rho^n {(1 - \rho)}^{N - n} \bigm|_{n=0} = {(1 - \rho)}^{N}$. This expression is the probability that random samples of size $N$ from a source of characteristic failure proportion $\rho$ will be accepted.

#### Power function {#S:POWER_FUNCTION}

It is confusing to reason in terms of contravariant[^7] attributes. In our case we formulate probability of rejection as an increasing function of $\rho$, a measure of the population’s undesirability. The probability that random samples will be properly rejected is the previous expression’s complement: $$K_{N,0}(\rho) = 1 - {(1 - \rho)}^{N} = 1 - \beta.$$

This non-contravariant result is known as the power function of sample size $N$, tolerating zero $(0)$ failures. The graph of the power function always increases, starting at $0$ for $\rho = 0$ and ending at $1$ for $\rho = 1$. Just how fast this function increases in its midrange is determined by the sample size $N$. With sample size one $(N = 1)$, $K_{1,0}(\rho) = \rho$.

      $N$  $K_{N,0}(.001)$   $K_{N,0}(.01)$   $K_{N,0}(.05)$   $K_{N,0}(.10)$   $K_{N,0}(.50)$   $K_{N,0}(.90)$
  ------- ----------------- ---------------- ---------------- ---------------- ---------------- ----------------
        1       .0010            .0100            .0500            .1000            .5000            .9000
        5       .0050            .0490            .2262            .4095            .9688            1.0000
       10       .0100            .0956            .4013            .6513            .9990            1.0000
       15       .0149            .1399            .5367            .7941            1.0000           1.0000
       20       .0198            .1821            .6415            .8784            1.0000           1.0000
       30       .0296            .2603            .7854            .9576            1.0000           1.0000
       50       .0488            .3950            .9231            .9948            1.0000           1.0000
      100       .0952            .6340            .9941            1.0000           1.0000           1.0000
      200       .1814            .8660            1.0000           1.0000           1.0000           1.0000
      500       .3936            .9934            1.0000           1.0000           1.0000           1.0000
     1000       .6323            1.0000           1.0000           1.0000           1.0000           1.0000
     2000       .8648            1.0000           1.0000           1.0000           1.0000           1.0000
     5000       .9933            1.0000           1.0000           1.0000           1.0000           1.0000
    10000      1.0000            1.0000           1.0000           1.0000           1.0000           1.0000

  : Family of power functions (probability of rejection)[]{data-label="Ta:POWER_FUNCTION"}

Within this family $\beta = {(1 - \rho)}^{N} = 1 - K_{N,0}(\rho)$.

One is initially dismayed by this sketch of the family of power functions; it suggests that high degrees of assurance are unobtainable through random sampling using practical sample sizes. However, reasonable performance useful for coarser screening is very possible. Detecting a defective population of 10 percent with a probability of approximately 90% requires only 20 sample items.

### Sampling philosophy {#S:SAMPLING_PHILOSOPHY}

Our safety demonstration sampling technique contrasts two assurance philosophies – software reliability versus software correctness. The software reliability perspective involves a separate operational profile on ${{\operatorname{edge}{{\mathcal{C}}}}}$, whereas software correctness examines only the structure within cone ${\mathcal{C}}$. The operational profile asserts the importance of relative excitational intensity to safety analysis. An accident that occurs more frequently is worse than an accident that happens less frequently, given that they are of comparable severity. This safety factor is ignored under software correctness alone.

Modeling accidents
------------------

Accidents are diverse in effect and mechanism, including injury, death, or damage either to equipment or environment. Since the causality of accidents is temporarily unknown, they manifest an apparent nature of unpredictability or randomness. However, under emulation as a stochastic process, the exact timing of accidents *is* truly a random phenomenon rather than causal. Nevertheless, it has proven useful to compare well-understood summary statistics of stochastic processes with those of deterministic but unknown physical processes.

### Compound Poisson process {#S:CPP}

Today’s prevalent safety model for the occurrence of accidents is the compound Poisson[^8] process. This model captures accidents’ two dominant attributes: rate of occurrence (intensity) and scalar measure of loss (severity). With some exceptions, neither the timing nor severity of one software accident affects another. The compound Poisson process (CPP) is appropriate to model accidents of this nature.

As stochastic processes are models rather than mechanisms, deriving their properties involves somewhat out-of-scope mathematics. The interested reader can immediately find greater detail in Wikipedia online articles: [@wW_Poisson_distribution], [@wW_Poisson_process], [@wW_total_expectation], [@wW_Compound_Poisson_process], and [@wW_Cumulant]. Relevant theorems will be documented here simply as facts.

### Poisson processes {#S:POISSON_PROCESSES}

We will consider three variants of basic stochastic process: the ordinary Poisson process, the compound Poisson process, and the intermittent compound Poisson process.

#### Ordinary Poisson process {#S:INTERMITTENT_POISSON}

(Ordinary) Poisson processes are characterized simply by their rate or intensity:

-   its fundamental rate $\lambda$, which is the expected number of arrivals per unit time.

Let $\lambda$ be the rate of a Poisson process. The probability of experiencing $k$ arrivals in a time interval $t$ units long is $$P_\lambda(k) = e^{-\lambda t}\frac{{(\lambda t)}^k}{k!}.$$

#### Compound Poisson process {#S:INTERMITTENT_POISSON}

A compound Poisson process is characterized by two rates:

-   its fundamental rate $\lambda$ as before, and

-   its rate of loss $L$, which is a random variable invoked once for each arrival.

Let $\lambda$ be the rate and $L$ be the loss random variable of a compound Poisson process. The expectation of the compound process for a time interval $t$ units long is $$\begin{aligned}
{1}
\E (\text{compound Poisson}) &= \lambda t \cdot \E (L)\\
                             &= \lambda t \cdot \mu_L.\end{aligned}$$

\[D:STATISTICAL\_RISK\] The statistical *risk*, written $h$, of a compound Poisson process is the time derivative of its expectation in a duration of length $t$; that is $$h = \frac{d}{dt} \E(\text{compound Poisson}) =  \frac{d}{dt} (\lambda t \cdot \mu_L) = \lambda \mu_L,$$ which is the product of its rate $\lambda$ and its expected loss $\mu_L$.

#### Intermittent compound Poisson process {#S:INTERMITTENT_POISSON}

A variation of the CPP is the intermittent compound Poisson process, which is intermittently on or off with expected durations $\E(\text{on}) = \mu_\text{on}$ and $\E(\text{off}) = \mu_\text{off}$. An intermittent compound Poisson process (ICPP) is characterized by three rates:

-   its fundamental rate $\lambda$ as before, and

-   its rate of loss $L$, also as before,

-   alternating durations of random lengths $\tau_\text{on}$ and $\tau_\text{off}$.

Random variables $\tau_\text{on}$ and $\tau_\text{off}$ converge to $\mu_\text{on}$ and $\mu_\text{off}$ in the limit. The *idle* ratio of a intermittent compound Poisson process is $\iota = \frac{\mu_\text{off}}{\mu_\text{on} + \mu_\text{off}}$.

Let $\lambda$ be the rate, $L$ be the loss random variable, and $\iota$ be the idle ratio of an intermittent compound Poisson process. The expectation of the ICPP for a time interval $t$ units long is $$\begin{aligned}
{1}
\E (\text{intermittent compound Poisson}) &= (1 - \iota) \cdot \lambda t \cdot \E(L) \\
                                          &= (1 - \iota) \cdot \lambda t \cdot \mu_L.\end{aligned}$$

The statistical risk of an ICPP is $$\begin{aligned}
{1}
h &= \frac{d}{dt} \E(\text{intermittent compound Poisson}) \\
  &= \frac{d}{dt} ((1 - \iota) \cdot \lambda t \cdot \mu_L + \iota \cdot 0 t  \cdot 0) \\
  &= (1 - \iota) \lambda \mu_L.\end{aligned}$$

Indemnification {#S:INDEMNIFICATION_FORMULA}
---------------

Hypothesize that a software hazard is emulated by a compound Poisson process (CPP) having intensity $\lambda$ and expected loss $\mu_L$. Suppose further that the actual control mechanism is a cone convergent to the software point of exhibition of the hazard. We wish to consider statistical evidence that the hazard’s hypothetical description via the stochastic process is consistent with its mechanism as revealed by safety demonstration.

### Unification {#S:UNIFICATION}

Before undertaking the question of whether test data supports a hypothetical stochastic process, we must establish the theoretical conditions under which equality is expected.

#### Fundaments of the model

The compound Poisson process is a model stochastic process for occurrence of accidents. This model is used in safety analysis to quantify the occurrence and losses of accidents without considering their causes. MIL-STD-882 (see Appendix \[S:MIL-STD-882\]) is an important example. In a time interval of duration $t$, accidents converge stochastically in rate to expectation $\lambda t$ and in mean loss to $\mu_L$. This means an intensity of $\lambda$ accidents per time unit.

#### Fundaments of the mechanism

The actuated automaton is a mechanism representing software. When extended by the principle of emergence (§\[S:PRINCIPLE\_OF\_EMERGENCE\]) and the constructs of the operational profiles (§\[S:OPERATIONAL\_PROFILE\_SECTION\]) and cones (§\[S:CONE\_SECTION\]), it becomes capable of representing precursor conditions for software accidents. Let ${\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert}$ (see §\[S:ABSOLUTE\_OP\_PROFILE\_RATE\]) be the rate-based absolute operational profile of the edge of an acyclic cone ${\mathcal{C}}$. Since a member of ${{\operatorname{edge}{{\mathcal{C}}}}}$ is executed at the average intensity of ${{\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert}}$, then so is the cone’s step of convergence ${\mathit{s}}_\text{crux}$. Let $\rho$ be the proportion of failing tests (localized predecessor walks). Under that supposition, failures occur at the intensity of $\rho \cdot {\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert}$. The definition of ${\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert}$, through the internal function $\text{sync}(\cdot)$, allows for the passage of time in the proper duration.

#### Uniting mechanism and model

We presume that one failing test equals one accident. The cone’s step of convergence is considered to be the point of exhibition of a hazard whenever safety constraints are not met. This mechanism may be separately equated to the intensity (not the rate of loss) of the compound Poisson process: $$\lambda = \rho \cdot {\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert}.$$

This equation places a property of the model on the left and properties of the mechanism on the right.

The execution rate of the edge of an acyclic cone numerically equals the execution rate of the (set containing the) cone’s crux. The cone’s definitional status (as a complete independent set of localized predecessor walks ending at ${\mathit{s}}_{\text{crux}}$) causes this. Symbolically, $${\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert} = {\Vert{\lbrace{\mathit{s}}_{\text{crux}}\rbrace}\Vert}.$$

### Evidence {#S:EVIDENCE}

We propose that the same data used earlier for indemnification testing be re-used in a slightly different statistical context. Recall that an indemnification test has $N$ items among which are zero failures, where each item is a localized predecessor walk, and a cone is a structured collection of localized predecessor walks of an automaton.

We wish to measure the amount of information in an indemnification sample to explain the phenomenon that larger samples justify more precise estimates than smaller samples. We refer to this information as measuring the *weight of evidence*. This situation differs from the familiar problem of finding the maximum likelihood estimator.

#### Method of indifference {#S:INDIFFERENCE_POWER_FUNCTION}

The power function of sample size $N$, tolerating zero $(0)$ failures, is $K_{N,0}(\rho) = 1 - {(1 - \rho)}^{N}$ (see §\[S:POWER\_FUNCTION\]). It measures the probability of rejection as a function of $\rho$.

Each power function $K_{N,0}(\rho) = 1 - {(1 - \rho)}^{N}$ is characterized by its indifference proportion, which is defined as the proportion at which rejection and acceptance become equally likely (that is, $K_{N,0}(\hat{\rho}_\text{\,I}) = {^1\!\!/\!_2} = 1 - K_{N,0}(\hat{\rho}_\text{\,I})$). With only modest algebra, the analytic expression for the indifference proportion may be derived from the power function $K_{N,0}(\rho)$; it is $$\hat{\rho}_\text{\,I} = 1 - \sqrt[N]{{^1\!\!/\!_2}}. $$

Below is a numerical tabulation of the previous formula:

      $N$  $\hat{\rho}_{\,\text{indifference}}$
  ------- --------------------------------------
        1                 .50000
        5                 .12945
       10                 .06697
       15                 .04516
       20                 .03406
       30                 .02284
       50                 .01377
      100                 .00691
      200                 .00346
      500                 .00139
     1000                 .00069
     2000                 .00035
     5000                 .00014
    10000                 .00007

  : Indifference proportion[]{data-label="Ta:INDIFFERENCE_PROPORTION"}

#### Indemnification formula {#S:UPPER_BOUND}

The indemnification formula provides a statistical upper bound on hazard intensity. Indemnification data may be expressed as an equivalent statistical upper bound on hazard intensity. This differs fundamentally from estimating the intensity of a hazard. By a statistically [guaranteed]{} hazard intensity, we mean an upper bound such that the true hazard intensity is likely to fall beneath this level with known confidence (probability).

Suppose we choose ${^1\!\!/\!_2}$ as the known confidence. The indifference proportion $\hat{\rho}_\text{\,I} = 1 - \sqrt[N]{{^1\!\!/\!_2}}$ then has a second interpretation as an upper bound with confidence ${^1\!\!/\!_2}$. For any $\rho \leq \hat{\rho}_\text{\,I}$, it is true that power function $P_{N,0}(\rho) \leq {^1\!\!/\!_2}$, so $\hat{\rho}_\text{\,I}$ is an upper bound of confidence ${^1\!\!/\!_2}$.

To convert from the size of the indemnification sample into its equivalent upper bound hazard intensity, find the indifference proportion $\hat{\rho}_{\,\text{I}} = 1 - \sqrt[N]{{^1\!\!/\!_2}}$.

Check the sample physics. This amounts to analysis of the originating cone ${\mathcal{C}}$, which is the point of exhibition of a hazard whenever safety constraints are not met. The cone’s edge has an absolute operational profile expressed as a rate. This quantity is the counting norm of the cone’s edge.

We have shown that the probable upper bound of the hazard intensity is proportional to the indifference proportion, with constant of proportionality furnished by the counting norm of the cone’s edge. The indemnification formula is: $$\hat{\lambda}_{\,\text{I}} = \hat{\rho}_{\,\text{I}} \cdot {\Vert{{{\operatorname{edge}{{\mathcal{C}}}}}}\Vert} 
= \hat{\rho}_{\,\text{I}} \cdot {\Vert{\lbrace{\mathit{s}}_{\text{crux}}\rbrace}\Vert}.$$

Epilogue
========

From previous discussion two structures of system safety emerge: the safety demonstration and indemnification, its measure of assurance. Opinion follows.

Programmatic fit {#S:PROGRAMMATIC_FIT}
----------------

Safety demonstration and indemnification merge smoothly into today’s programmatic picture. Early in the development cycle, safety engineers provide [ballpark]{} quantifications of the threat of hazards[@DD12], expressed as intensity and severity. These numbers are often educated guesses: a mixture of circumstance, intuition, similar design, and history. At that stage, the process is without supporting evidence. Later in the development cycle, assuming a program of structured testing has been followed, statistical evidence is available in the form of a safety demonstration. These data are expressed as a statistical upper bound on each software hazard’s intensity – that is, an indemnification – and used as evidence of correct operation. This additional step frees the safety engineer from having to re-asses his original estimate using the same shallow method as the original guesstimate.

Increasingly, automatic static syntax analyzers satisfy need for overall code robustness. However, exclusive reliance on these analyzers would result in a software safety engineering shortcoming, because they do not always detect code defects that have valid syntax (that is, syntactically valid but wrong algorithm).

Commercialization {#S:COMMERCIALIZATION}
-----------------

Difficult work remains before safety demonstration and indemnification can be supported as mature commercial technology. The role of the actuated automaton must be replaced by a real-world programming language. Present theory restricting tests (predecessor walks) to acyclic cones may require generalization to cyclic cones to achieve broader range. Safety demonstration demands the ability to produce approximate operational profiles from which can be drawn pseudo-random samples. Spin-offs from similar technologies may be possible; static analyzers are one example.

Criticism of MIL-STD-882 {#S:CRITICISM}
------------------------

Statistical risk is a model (see §\[S:INTRO\_RISK\]) emulating the threat of accidents. Users of MIL-STD-882 are familiar with statistical risk as an accident model for hardware. Software is properly deterministic and therefore non-stochastic, but it’s successfully approximated with the same Poisson stochastic process as hardware. The rationale for this approximation is to apply a useful Poisson mathematical assurance property; thus assurance depends on the validity of the Poisson process as an approximation to the actuated automaton.

The Standard introduces a risk-like scale replacing statistical risk for software. For purpose of this chapter, we call this replacement scale the *design* risk. The discussion of chapters 2 and 3 conclude that, from the standpoint of statistical assurance, there is no justification for the presently differing versions of the term *risk* between hardware and software.

The state of software engineering is mixed science and sophisticated art. In the current Standard, art has somewhat overtaken science; for software, the concept of statistical risk has been abandoned. One subsequently loses the ability to measure and assure risk uniformly.

Design risk and statistical risk do share a severity axis, but the similarity ends there. Statistical risk has another axis composed of a numerical product, the frequency of execution times the probability of error. What we have called design risk also possesses another axis, but it is a categorical scale arranged in decreasing order of the design safety importance of the software’s functionality.

This results in an error of omission in MIL-STD-882 with serious consequence. Because the frequency of execution of a software point is not well-correlated with its functionality’s design safety importance, statistical risk does not correlate well with design risk. Because the Standard assigns statistical risk to hardware and design risk to software, and due to lack of correlation between the two, there is no way to rank the relative importance of hazards of mixed type. Loss of the ability to compare risks of all hazards is a flagrant omission. Under correct physics, risks of multiple hazards are additive. This is not the case under MIL-STD-882.

The formal sense of *assurance* is lost by these definitional variants. Being quantitatively assured requires a limit value on proportion or mean deviation and a statement of statistical confidence for this limit; the Standard clearly lacks this characteristic. Properly assurance is a numeric quantity associated with statistical control of risk, not an engineering activity to further psychological confidence. Despite that its developers may express great confidence in the methodology, software built under the Standard is not quantitatively assured.

Repair of MIL-STD-882 {#S:REPAIR}
---------------------

Rehabilitation of MIL-STD-882 is straightforward. It must be amended to contain an engineering introduction to statistical risk for software, including allied procedures. This subject matter is covered here in mathematical language, but should be presented differently for engineers’ consumption. The revised Standard should distinguish between formal assurance and design confidence, and classify what procedures support either. Generally, the concerns associated with design risk align with developmental software engineering, while those of statistical risk align with responsibilities of system safety engineering, part of systems engineering. Software and Systems Engineering should not duplicate each other’s efforts.

Groundwork {#Ch:GROUNDWORK}
==========

This appendix examines ensembles, a fundamental structure in the theory of systems which formalizes the notion of stimulus and response. From this start, discussion proceeds into the Cartesian product, choice spaces and subspaces, and partitions of choice spaces into persistent and volatile components. Dyadic notation is introduced.

Ensemble {#S:ENSEMBLE}
--------

An ensemble is a special form of a more general structure known as a *family*. We employ nomenclature abridged from Halmos [@pH74 p. 34] as follows:

Let $I$ and $X$ be non-empty sets, and $\varphi \colon I \to X$ be a mapping. Each element $i \in I$ is an *index*, while $I$ itself is an *index set*. The mapping $\varphi$ is a *family*; its co-domain $X$ is an *indexed set*. An ordered pair $(i,x)$ belonging to the family is a *term*, whose value $x = \varphi(i)\in X$ is often denoted $\varphi_i$.

The family $\varphi$ itself is routinely but abusively denoted $\{\varphi_n\}$. This notation is a compound idiom.[^9] Especially in the case of sequences over a set $G$, the symbol $\{g_n\}$ signifies the mapping $\{ 1\mapsto g_1, \; 2\mapsto g_2, \; \ldots \;\}$.

\[D:ENSEMBLE\] An *ensemble* is a non-empty family.

\[D:CONSTANT\_VARIABLE\] Let $\Psi$ be an ensemble, with ${{\operatorname{ran}{\Psi}}}$ its range. If ${\lvert{{{\operatorname{ran}{\Psi}}}}\rvert} = 1$, the ensemble is *constant*; otherwise it is *variable*.

Since physical systems possess only a finite number of attributes, the scope of practical interest is limited to ensembles having finite-dimensional index sets.

A constant ensemble (definition \[D:CONSTANT\_VARIABLE\]) is also referenced under the historically colorful name *Hobson’s*[^10] choice. Using the word *choice* in its everyday sense, a Hobson’s choice is oxymoronic: a free choice in which only one option is offered, with gist [Only one choice is no choice.]{}

Let $\Psi$ be an ensemble. For term $(i,P) \in \Psi$, we denote $P = \Psi_i$.

Ensemble arithmetic {#S:ENSEMBLE_ARITHMETIC}
-------------------

\[D:DISJOINT\_ENSEMBLES\] Ensembles $\Psi$ and $\Phi$ are *disjoint* if ${{\operatorname{dom}{\Psi}}}\thickspace\cap\thickspace{{\operatorname{dom}{\Phi}}} = \varnothing$ (that is, if their index sets have no member in common).

\[D:COMPLEMENTARY\_ENSEMBLES\] Ensembles $\Psi$ and $\Phi$ are *complementary* with respect to a third ensemble $\Upsilon$ if they are disjoint and $\Psi \cup \Phi = \Upsilon$.

Regarding ensembles $\Psi$ and $\Phi$, we write $\Phi \subseteq \Psi$ to express that $\Phi$ is contained in $\Psi$, following ordinary set theory that term $(i,P) \in \Phi$ implies $(i,P) \in \Psi$.

\[D:ENSEMBLE\_DIFFERENCE\] Let $\Psi$ and $\Phi$ be ensembles such that $\Phi \subseteq \Psi$. In classification of difference between $\Psi$ and $\Phi$, $\Psi$ is the *minuend*, $\Phi$ is the *subtrahend*, and the set difference[^11] $\Psi \setminus \Phi$ is the *remainder*.

\[L:DISJOINT\_AND\_COMPLEMENTARY\] Let $\Psi$ and $\Phi$ be ensembles such that $\Phi \subseteq \Psi$. The subtrahend $\Phi$ and remainder $\Psi \setminus \Phi$ are disjoint and complementary with respect to $\Psi$.

Since $\Phi \subseteq \Psi$, definition \[D:ENSEMBLE\_DIFFERENCE\] applies. The minuend is $\Psi$, the subtrahend is $\Phi$, and the remainder is $\Psi \setminus \Phi$.

Definition \[D:DISJOINT\_ENSEMBLES\] asserts that two ensembles $\Theta$ and $\Upsilon$ are disjoint if ${{\operatorname{dom}{\Theta}}}\thickspace\cap\thickspace{{\operatorname{dom}{\Upsilon}}} = \varnothing$. As hypothesis presume the lemma’s antithesis, namely that the subtrahend $\Phi$ and the remainder $\Psi \setminus \Phi$ are not disjoint. This implies that there exists some $i$ such that $i \in {{\operatorname{dom}{\Phi}}}\thickspace\cap\thickspace{{\operatorname{dom}{(\Psi \setminus \Phi)}}}$. For this $i$ to exist in the intersection of the domains of two mappings, there must be both a term $(i,P) \in \Phi$ and a term $(i,Q) \in (\Psi \setminus \Phi)$.

Because $(i,P) \in \Phi$ and the lemma’s premise states that $\Phi \subseteq \Psi$, then $(i,P) \in \Psi$. Since term $(i,Q) \in (\Psi \setminus \Phi)$, then $(i,Q) \in \Psi$ and $(i,Q) \notin \Phi$. Since $\Psi$ is a mapping, then $(i,P) \in \Psi$ and $(i,Q) \in \Psi$ together imply $P = Q$. With $P = Q$ and $(i,Q) \notin \Phi$, then also $(i,P) \notin \Phi$.

However, the immediately preceding conclusion that $(i,P) \notin \Phi$ contradicts the earlier inference that term $(i,P) \in \Phi$ must exist if $i$ is a member of the intersection of the domains. Since the presumption that the subtrahend and remainder are not disjoint arrives at a contradiction, then subtrahend $\Phi$ and remainder $\Psi \setminus \Phi$ are indeed disjoint.

The ensembles are complementary with respect to $\Psi$ by definition \[D:COMPLEMENTARY\_ENSEMBLES\] because they are disjoint and $\Phi \cup (\Psi \setminus \Phi) = \Psi$.

Choice space {#S:CHOICE_SPACE}
------------

Informally, a choice space is the totality of all possible combinations of variables’ values within a given ensemble. The general Cartesian product formalizes this notion.

### General Cartesian product {#S:GCP}

\[D:PROTOSET\] Let $\Psi$ be an ensemble. By definition \[D:ENSEMBLE\], each member of ${{\operatorname{ran}{\Psi}}}$ is itself a non-empty set. The *proto-set* $\Psi_\heartsuit$ is the union of all such sets: $$\Psi_\heartsuit = \bigcup_{R \in\: {{\operatorname{ran}{\Psi}}}} R.$$

Definition \[D:PROTOSET\] expresses a relation between the ensemble $\Psi$’s indexed sets and the proto-set, namely that for each $i \in {{\operatorname{dom}{\Psi}}}$, $\Psi(i) \subseteq \Psi_\heartsuit$. An alternative portrayal uses the power set, claiming $\Psi(i) \in {\mathscr{P}({\Psi_\heartsuit})}$.

\[D:PROTOSPACE\] Let $\Psi$ be an ensemble with proto-set $\Psi_\heartsuit$. The *proto-space* of $\Psi$ is the set ${\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$, where ${\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$ is the set of all mappings ${{\operatorname{dom}{\Psi}}} \to \Psi_\heartsuit$.

\[D:CHOICE\] Let $\Psi$ be an ensemble with proto-set $\Psi_\heartsuit$. Let $\chi \colon {{\operatorname{dom}{\Psi}}} \to \Psi_\heartsuit$ be a mapping. If $\chi$ satisfies $\chi(i) \in \Psi(i)$ for each $i \in {{\operatorname{dom}{\Psi}}}$, then $\chi$ is a *choice* mapping of $\Psi$.

\[D:CHOICE\_SPACE\] The set of all choice mappings of ensemble $\Psi$ is the *choice space* (or general Cartesian product) $\prod\Psi$.

Through the general Cartesian product, an ensemble *generates* a choice space. For brevity we refer to a point in a choice space (that is, a choice mapping) simply as a *choice*.

\[T:PROTOSPACE\_INCLUDES\_CHOICESPACE\] The proto-space ${\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$ of ensemble $\Psi$ includes its choice space $\prod\Psi$ (that is, $\prod\Psi \subseteq {\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$).

Suppose $\chi \in \prod\Psi$. By definition \[D:CHOICE\], $\chi$ is a mapping ${{\operatorname{dom}{\Psi}}} \to \Psi_\heartsuit$. Then, by definition \[D:PROTOSPACE\], $\chi \in {\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$. Thus, any member of $\prod\Psi$ is also a member of ${\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$. From this we conclude $\prod\Psi \subseteq {\Psi_\heartsuit}^{{{\operatorname{dom}{\Psi}}}}$.

\[T:ENSEMBLE\_UNIQ\_SPACE\] An ensemble generates one unique choice space: let $\Theta$ and $\Phi$ be two ensembles generating choice spaces $\prod\Theta$ and $\prod\Phi$ respectively. If $\Theta = \Phi$, then $\prod\Theta = \prod\Phi$.

To show the contrapositive, suppose $\prod\Theta \not= \prod\Phi$. This premise can be true if either A: there is a choice $\alpha \in \prod\Theta$ such that $\alpha \notin \prod\Phi$, or if B: there is a choice $\beta \in \prod\Phi$ such that $\beta \notin \prod\Theta$.

In case A, $\alpha$ is a choice of $\Theta$ – that is, for each $k \in {{\operatorname{dom}{\Theta}}}$, $\alpha(k) \in \Theta(k)$. For hypothesis, assume $\Theta = \Phi$, so that ${{\operatorname{dom}{\Theta}}} = {{\operatorname{dom}{\Theta}}}$. Then for each $k \in {{\operatorname{dom}{\Theta}}}$, $\alpha(k) \in \Phi(k)$, since by equality hypothesis $\Theta(k) = \Phi(k)$ and $\alpha(k) \in \Theta(k)$. This means $\alpha$ is a choice of $\Phi$, that is, $\alpha \in \prod\Phi$. However, this conclusion contradicts the second part of the premises for case A, namely that $\alpha \notin \prod\Phi$. Thus the hypothesis $\Theta = \Phi$ is false, so $\Theta \not= \Phi$.

The argument for case B is the same as A, except reversing the roles of $\Theta$ and $\Phi$. Together, cases A and B show that $\prod\Theta \not= \prod\Phi$ implies $\Theta \not= \Phi$. Applying the contrapositive principle[^12] gives $\prod\Theta = \prod\Phi$ if $\Theta = \Phi$.

\[T:SPACE\_UNIQ\_ENSEMBLE\] Any choice space has one unique generating ensemble: let $\Theta$ and $\Phi$ be two ensembles generating choice spaces $\prod\Theta$ and $\prod\Phi$ respectively. If $\prod\Theta = \prod\Phi$, then $\Theta = \Phi$.

To show the contrapositive, suppose $\Theta \not= \Phi$. From this premise there must exist either A: $(i,P) \in \Theta$ such that $(i,P) \notin \Phi$, or B: $(j,Q) \in \Phi$ such that $(j,Q) \notin \Theta$.

The first case A decomposes into two sub-cases: either A1: $i \in S$ and $i \in S'$, or A2: $i \in S$ and $i \notin S'$.

In sub-case A1, we must have $\Theta(i) \not= \Phi(i)$ to support $\Theta \not= \Phi$. For this there must be either A1a: there is $u \in \Theta(i)$ such that $u \notin \Phi(i)$, or A1b: there is $v \in \Phi(i)$ such that $v \notin \Theta(i)$.

In sub-sub-case A1a, there must exist by definitions \[D:CHOICE\_SPACE\] and \[D:CHOICE\], a choice $\alpha \in \prod\Theta$ such that $\alpha(i) = u$. However, there can be no choice $\beta \in \prod\Phi$ such that $\beta(i) = u$, since $u \notin \Phi(i)$. Therefore $\alpha \notin \prod\Phi$, with the consequence that $\prod\Theta \not= \prod\Phi$.

In sub-sub-case A1b there is $v \in \Phi(i)$ such that $v \notin \Theta(i)$. Similarly to A1a, there exists $\beta \in \prod\Phi$ such that $\beta(i) = v$, but no $\alpha \in \prod\Theta$ such that $\alpha(i) = v$, again concluding that $\prod\Theta \not= \prod\Phi$.

In sub-case A2, we have $i \in {{\operatorname{dom}{\Theta}}}$ and $i \notin {{\operatorname{dom}{\Phi}}}$. By definitions \[D:CHOICE\_SPACE\] and \[D:CHOICE\], for any $x \in \Theta(i)$, there exists choice $\alpha_x \in \prod\Theta$ such that $\alpha_x(i) = x$. However, there is no choice $\beta \in \prod\Phi$ such that $\beta(i) = x$ because $i \notin {{\operatorname{dom}{\Phi}}} = {{\operatorname{dom}{\beta}}}$. This concludes $\prod\Theta \not= \prod\Phi$ for sub-case A2.

The proofs for subordinate cases of B are the same as A, reversing the roles of $\Theta$ and $\Phi$. Taken together, these sub-case analyses show that exhaustively $\Theta \not= \Phi$ implies $\prod\Theta \not= \prod\Phi$. By contraposition, $\Theta = \Phi$ if $\prod\Theta = \prod\Phi$.

\[T:SPACE\_BIJECTION\_ENSEMBLE\] Choice spaces and generating ensembles are in one-to-one correspondence via the general Cartesian product.

Theorem \[T:ENSEMBLE\_UNIQ\_SPACE\] asserts that any ensemble generates only one unique choice space, and \[T:SPACE\_UNIQ\_ENSEMBLE\] asserts that any choice space has only one unique generating ensemble.

\[N:CARTESIAN\_PRODUCT\_INVERSE\] By Theorem \[T:SPACE\_BIJECTION\_ENSEMBLE\], the Cartesian product is invertible, providing a mapping from choice spaces to generating ensembles. There is need for a symbol designating this inverse. In preference to $\prod^{-1}$, for present purpose we borrow the coproduct symbol $\coprod$ from another field, since there is no danger of confusion.

\[D:FINITE\_CHOICE\_SPACE\] A *finite* choice space is a choice space (definition \[D:CHOICE\_SPACE\]) whose generating ensemble has a finite index set.

### Dyadic Operators {#S:DYADIC_OPERATORS}

This section presents binary operators on ensembles and choice spaces whose intended usage will value notational compactness. To this end these operators will be displayed through dyadic notation, which indicates an operator application implicitly by simple juxtaposition of the operator’s arguments, forgoing explicit rendering of the operation’s symbol as a prefix, infix, or suffix. For reason of denotational style, these operators will be called products despite that they suggest sums.

\[D:DYADIC\_ENSEMBLE\_PRODUCT\] Let $\Theta$ and $\Phi$ be disjoint (definition \[D:DISJOINT\_ENSEMBLES\]) ensembles. The dyadic product $(\Theta,\Phi) \mapsto \Theta\Phi$ is $$\Theta\Phi = \Theta \cup \Phi.$$

An immediate consequence of this definition is commutativity $\Theta\Phi = \Phi\Theta$, since $\Theta \cup \Phi = \Phi \cup \Theta$.

\[T:DYADIC\_PRODUCT\_IS\_ENSEMBLE\] Let $\Theta$ and $\Phi$ be disjoint ensembles. Their dyadic product $\Upsilon = \Theta\Phi$ is an ensemble with domain $({{\operatorname{dom}{\Theta}}} \cup {{\operatorname{dom}{\Phi}}})$ and range $({{\operatorname{ran}{\Theta}}} \cup {{\operatorname{ran}{\Phi}}})$.

Suppose $i \in {{\operatorname{dom}{\Theta\Phi}}}$. By definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\], $\Theta\Phi = \Theta \cup \Phi$. From this it follows that $i \in {{\operatorname{dom}{\Theta}}} \cup {{\operatorname{dom}{\Phi}}}$. Therefore, $i \in {{\operatorname{dom}{\Theta}}}$, $i \in {{\operatorname{dom}{\Phi}}}$, or both. The stipulation that $\Theta$ and $\Phi$ be disjoint entails ${{\operatorname{dom}{\Theta}}} \cap {{\operatorname{dom}{\Phi}}} = \varnothing$ (definition \[D:DISJOINT\_ENSEMBLES\]). That stipulation eliminates the possibility of both memberships, leaving two feasible cases: either A) $i \in {{\operatorname{dom}{\Theta}}}$ and $i \notin {{\operatorname{dom}{\Phi}}}$, or B) $i \notin {{\operatorname{dom}{\Theta}}}$ and $i \in {{\operatorname{dom}{\Phi}}}$.

In case A, there exists $(i, \Theta_i) \in \Theta$, so $(i, \Theta_i) \in \Upsilon = \Theta \cup \Phi$. Furthermore, since $i \notin {{\operatorname{dom}{\Phi}}}$, $\Upsilon_i = \Theta_i$ is well-defined. Since by definition \[D:ENSEMBLE\] each member of ${{\operatorname{ran}{\Theta}}}$ is a non-empty set, then equivocally $\Upsilon_i = \Theta_i$ is a non-empty set.

Argumentation for case B, supporting that $\Upsilon_i = \Phi_i$ is well-defined and that $\Upsilon_i$ is a non-empty set, is obtained by interchanging the roles of $\Theta$ and $\Phi$ in case A.

Over all possibilities, $\Upsilon = \Theta \cup \Phi$ is well-defined as a mapping (family) and each element of its range is a non-empty set. Therefore the dyadic product of two disjoint ensembles is itself an ensemble.

The sub-case analysis establishes ${{\operatorname{dom}{\Theta\Phi}}} \subseteq ({{\operatorname{dom}{\Theta}}} \cup {{\operatorname{dom}{\Phi}}})$. For the converse, first assume $i \in {{\operatorname{dom}{\Theta}}}$. Then there is some $P$ such that $(i,P) \in \Theta$. From this it follows that $(i,P) \in \Theta \cup \Phi$, so $i \in {{\operatorname{dom}{\Theta\Phi}}}$ and ${{\operatorname{dom}{\Theta}}} \subseteq {{\operatorname{dom}{\Theta\Phi}}}$. Similarly, ${{\operatorname{dom}{\Phi}}} \subseteq {{\operatorname{dom}{\Theta\Phi}}}$. From these two inclusions it follows that $({{\operatorname{dom}{\Theta}}} \cup {{\operatorname{dom}{\Phi}}}) \subseteq {{\operatorname{dom}{\Theta\Phi}}}$. With the previous result that ${{\operatorname{dom}{\Theta\Phi}}} \subseteq ({{\operatorname{dom}{\Theta}}} \cup {{\operatorname{dom}{\Phi}}})$, we conclude ${{\operatorname{dom}{\Theta\Phi}}} = ({{\operatorname{dom}{\Theta}}} \cup {{\operatorname{dom}{\Phi}}})$.

The sub-case analysis shows also that for $(i, P) \in \Theta\Phi$, either $P \in {{\operatorname{ran}{\Theta}}}$ or $P \in {{\operatorname{ran}{\Phi}}}$. This implies that ${{\operatorname{ran}{\Theta\Phi}}} \subseteq {{\operatorname{ran}{\Theta}}} \medspace\cup\medspace {{\operatorname{ran}{\Phi}}}$.

To demonstrate the converse, assume $P \in {{\operatorname{ran}{\Theta}}}$. Then there exists $(i,P) \in \Theta$, and by definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\], $(i,P) \in \Theta\Phi$. From this we conclude that ${{\operatorname{ran}{\Theta}}} \subseteq {{\operatorname{ran}{\Theta\Phi}}}$. With modest changes as above we conclude ${{\operatorname{ran}{\Phi}}} \subseteq {{\operatorname{ran}{\Theta\Phi}}}$. This establishes the converse ${{\operatorname{ran}{\Theta}}} \medspace\cup\medspace {{\operatorname{ran}{\Phi}}} \subseteq {{\operatorname{ran}{\Theta\Phi}}}$.

Finally, with both ${{\operatorname{ran}{\Theta\Phi}}} \subseteq {{\operatorname{ran}{\Theta}}} \medspace\cup\medspace {{\operatorname{ran}{\Phi}}}$ and its converse, ${{\operatorname{ran}{\Theta\Phi}}} = {{\operatorname{ran}{\Theta}}} \medspace\cup\medspace {{\operatorname{ran}{\Phi}}}$.

\[D:DYADIC\_SPACE\_PRODUCT\] Let $\Theta$ and $\Phi$ be disjoint ensembles. The dyadic space product of $\prod\Theta$ and $\prod\Phi$ is $$\prod \Theta \prod \Phi = \prod \Theta\Phi$$ (that is, with $\Upsilon = \Theta\Phi$, the set of all $\Upsilon$-choices).

\[D:DYADIC\_CHOICE\_PROD\] Let $\Theta$ and $\Phi$ be disjoint ensembles generating choice spaces $\prod\Theta$ and $\prod\Phi$. Suppose $\alpha \in \prod\Theta$ and $\beta \in \prod\Phi$ are choices. Their dyadic *choice* product $(\alpha,\beta) \mapsto \alpha\beta$ is $$\alpha\beta = \alpha \cup \beta.$$

\[T:DYADIC\_CHOICE\_PROD\] Let $\Theta$ and $\Phi$ be disjoint ensembles. The dyadic choice product is a bijection $$\prod\Theta \times \prod\Phi \leftrightarrow \prod\Theta\Phi.$$

Suppose $(\theta, \phi) \in \prod\Theta \times \prod\Phi$, whence it follows that choices $\theta \in \prod\Theta$ and $\phi \in \prod\Phi$. Consider the dyadic products $\theta\phi = \theta \cup \phi$ and $\Theta\Phi = \Theta \cup \Phi$. Since ${{\operatorname{dom}{\theta}}} = {{\operatorname{dom}{\Theta}}} = T$ and ${{\operatorname{dom}{\phi}}} = {{\operatorname{dom}{\Phi}}} = P$, then ${{\operatorname{dom}{\theta\phi}}} = T \cup P = {{\operatorname{dom}{\Theta\Phi}}}$. Let $i \in {{\operatorname{dom}{\theta\phi}}} = T \cup P$. Since $\Theta$ and $\Phi$ are disjoint, then exactly one of two cases holds: either $i \in T$ and $i \notin P$, or $i \notin T$ and $i \in P$.

In the first case, $i \in T$, $\theta\phi(i) = \theta(i)$ and $\Theta\Phi(i) = \Theta(i)$. Since $\theta$ is a $\Theta$-choice, then $\theta(i) \in \Theta(i)$. But since $\theta\phi(i) = \theta(i)$ and $\Theta\Phi(i) = \Theta(i)$, then $\theta\phi(i) \in \Theta\Phi(i)$ for any $i \in T$.

The second case is similar and leads to $\theta\phi(i) \in \Theta\Phi(i)$ for any $i \in P$. From these two cases we conclude that $\theta\phi(i) \in \Theta\Phi(i)$ for any $i \in T \cup P = {{\operatorname{dom}{\theta\phi}}}$, and that $\theta\phi \in \prod\Theta\Phi$.

The preceding establishes that the choice product is a relation between $\prod\Theta \times \prod\Phi$ and $\prod\Theta\Phi$. For this relation to be a mapping, it must yet be established that any member of the domain is related to exactly one member of the co-domain.

Again with $(\theta, \phi) \in \prod\Theta \times \prod\Phi$, suppose $\alpha \in \prod\Theta\Phi$ and $\beta \in \prod\Theta\Phi$ are $\Theta\Phi$-choices such that $(\theta, \phi) \mapsto \alpha$ and $(\theta, \phi) \mapsto \beta$. The hypothesis $\alpha \not= \beta$ now leads to the contradiction $\theta \cup \phi \not= \theta \cup \phi$, so the hypothesis is false and $\alpha = \beta$. Therefore the dyadic choice product is a mapping.

To be bijective, this mapping must be injective and surjective.

To assess injection, let $\theta$, $\theta' \in \Theta$ and $\phi$, $\phi' \in \prod\Phi$, and hypothesize $\theta\phi = \theta'\phi'$. With $\theta\phi = \theta'\phi'$, then the restrictions $\theta\phi\mid{{\operatorname{dom}{\Theta}}} = \theta'\phi'\mid{{\operatorname{dom}{\Theta}}}$. By \[D:DYADIC\_CHOICE\_PROD\], $\theta\phi\mid{{\operatorname{dom}{\Theta}}} = \theta$ and $\theta'\phi'\mid{{\operatorname{dom}{\Theta}}} = \theta'$. This establishes $\theta = \theta'$ in $\prod\Theta$. A similar approach, using restriction by ${{\operatorname{dom}{\Phi}}}$, establishes $\phi = \phi'$ in $\prod\Phi$. Since the assumption $\theta\phi = \theta'\phi'$ implies $\theta = \theta'$ and $\phi = \phi'$, then the dyadic choice product is injective.

To assess surjection, consider a general $\gamma \in \prod\Theta\Phi$. Define $\theta = \gamma \mid {{\operatorname{dom}{\Theta}}}$. By definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\], the non-empty sets $\Theta(i) = \Theta\Phi(i)$ for $i \in {{\operatorname{dom}{\Theta}}}$. Since $\theta(i) \in \Theta\Phi(i)$ by construction, and $\Theta(i) = \Theta\Phi(i)$, then $\theta(i) \in \Theta(i)$ for $i \in {{\operatorname{dom}{\Theta}}}$ – that is, $\theta$ is a choice in $\prod\Theta$.

A similar tactic shows the existence of $\phi \in \prod\Phi$. Construct $\phi = \gamma \mid {{\operatorname{dom}{\Phi}}}$. For each $i \in {{\operatorname{dom}{\Phi}}}$, the non-empty sets $\Phi(i) = \Theta\Phi(i)$ by definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\]. Since by construction $\phi(i) \in \Theta\Phi(i)$, and $\Phi(i) = \Theta\Phi(i)$, then $\phi(i) \in \Phi(i)$ for $i \in {{\operatorname{dom}{\Phi}}}$ – that is, $\phi$ is a choice in $\prod\Phi$.

It is thus established that for any $\gamma \in \prod\Theta\Phi$, there exists $\theta \in \prod\Theta$ and $\phi \in \prod\Phi$ such that $\gamma = \theta\phi$. Therefore the dyadic choice product is surjective.

Since the dyadic choice product is both injective and surjective, then it is a bijection $\prod\Theta \times \prod\Phi \leftrightarrow \prod\Theta\Phi$.

### Choice subspaces {#S:CHOICE_SUBSPACE}

Any mapping, including a choice mapping, may be restricted to subsets of its domain.

\[D:SUBCHOICE\] Let $\Psi$ be an ensemble, and let $R \subseteq {{\operatorname{dom}{\Psi}}}$ be a subset of its index set. Suppose $\chi \in \prod\Psi$ is a choice. A *subchoice* $\chi \mid R$ is the ordinary mapping restriction of $\chi$ to its domain subset $R$.

In the above, degenerate case $R = \varnothing$ yields $\chi \mid R = \varnothing$.

\[D:SUBSPACE\] Let $\Psi$ be an ensemble. For each $R \subseteq {{\operatorname{dom}{\Psi}}}$, the *subspace* $(\thinspace\prod\Psi) \mid R$ is the set of subchoices $\lbrace\thinspace\chi \mid R \medspace \colon \chi \in \prod\Psi\thinspace\rbrace$.

\[T:CHC\_RSTR\_EQ\_RSTR\_CHC\] Let ensemble $\Psi$ generate choice space $\prod \Psi$, and let $R \subseteq {{\operatorname{dom}{\Psi}}}$ be a subset of its index set. The restriction of the choice space equals the choice space of the restriction: $$(\thinspace\prod\Psi) \mid R = \prod ({{\Psi}\negmedspace\mid\negmedspace{R}}).$$

Suppose $\xi \in (\thinspace\prod\Psi) \mid R$. By definition \[D:SUBCHOICE\], there exists $\chi \in \prod\Psi$ such that $\xi = \chi \mid R$. By definition of Cartesian product, for each $i \in {{\operatorname{dom}{\Psi}}}$, $\chi(i) \in \Psi(i)$. Since $R \subseteq {{\operatorname{dom}{\Psi}}}$, then for each $r \in R$, $\xi(r) \in \Psi(r)$. Consider ${{\Psi}\negmedspace\mid\negmedspace{R}}$, for which ${{\operatorname{dom}{({{\Psi}\negmedspace\mid\negmedspace{R}})}}} = R$. By definition of restriction, for $r \in R$, $({{\Psi}\negmedspace\mid\negmedspace{R}})(r) = \Psi(r)$. Since $\xi(r) \in \Psi(r)$ and $\Psi(r) = ({{\Psi}\negmedspace\mid\negmedspace{R}})(r)$, then for any $r \in R$, $\xi(r) \in ({{\Psi}\negmedspace\mid\negmedspace{R}})(r)$ – that is, $\xi$ is a choice of ${{\Psi}\negmedspace\mid\negmedspace{R}}$. From the preceding, $\xi \in (\thinspace\prod\Psi) \mid R$ implies $\xi \in \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$, or $(\thinspace\prod\Psi) \mid R \subseteq \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$.

Next suppose $\xi \in \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$. Then, by definitions \[D:CHOICE\] and \[D:CHOICE\_SPACE\] covering Cartesian products, for each $r \in R$, $\xi(r) \in ({{\Psi}\negmedspace\mid\negmedspace{R}})(r)$. The ensemble $\Psi$ coincides with its restriction ${{\Psi}\negmedspace\mid\negmedspace{R}}$ on $R$. A restatement of this is $({{\Psi}\negmedspace\mid\negmedspace{R}})(r) = \Psi(r)$ for $r \in R$. Substituting $\Psi(r)$ for $({{\Psi}\negmedspace\mid\negmedspace{R}})(r)$ yields $\xi(r) \in \Psi(r)$ for each $r \in R$. From this it follows that $\xi \in (\thinspace\prod\Psi) \mid R$, with the further implication that $\prod ({{\Psi}\negmedspace\mid\negmedspace{R}}) \subseteq (\thinspace\prod\Psi) \mid R$.

We conclude equality $(\thinspace\prod\Psi) \mid R = \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$ after establishing that each of these two sets is a subset of the other.

\[L:SUBSPACE\_SUBSET\] Let $\Psi$ and $\Phi$ be ensembles. If ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$, then $\Phi \subseteq \Psi$.

Let ${\prod{\Phi}}$ be a subspace of ${\prod{\Psi}}$. By definition \[D:SUBSPACE\], there exists $R \subseteq {{\operatorname{dom}{\Psi}}}$ such that ${\prod{\Phi}} = (\thinspace{\prod{\Psi}}) \mid R$. By Theorem \[T:CHC\_RSTR\_EQ\_RSTR\_CHC\], the restriction of the choice space equals the choice space of the restriction: $(\thinspace\prod\Psi) \mid R = \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$. Transitivity of equality implies ${\prod{\Phi}} = \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$. Then, by Theorem \[T:SPACE\_UNIQ\_ENSEMBLE\] (invertibility of the Cartesian product), $\Phi = {{\Psi}\negmedspace\mid\negmedspace{R}}$.

Suppose term $(i,P) \in \Phi$. Since $\Phi = {{\Psi}\negmedspace\mid\negmedspace{R}}$, then $(i,P) \in {{\Psi}\negmedspace\mid\negmedspace{R}}$. By the definition of restriction, this implies both $(i,P) \in \Psi$ and $i \in R$. Since $(i,P) \in \Phi$ implies $(i,P) \in \Psi$, we conclude $\Phi \subseteq \Psi$.

\[L:SUBSET\_RESTRICTION\] Let $\Psi$ and $\Phi$ be ensembles. If $\Phi \subseteq \Psi$ and $R = {{\operatorname{dom}{\Phi}}}$, then $\Phi = {{\Psi}\negmedspace\mid\negmedspace{R}}$.

Consider $(i,P) \in {{\Psi}\negmedspace\mid\negmedspace{R}}$. It then follows from the definition of restriction that $(i,P) \in \Psi$ and $i \in R$. But $R = {{\operatorname{dom}{\Phi}}}$, so $i \in {{\operatorname{dom}{\Phi}}}$. This implies there exists $(i,Q) \in \Phi$. Since $\Phi \subseteq \Psi$, then $(i,Q) \in \Psi$. Since $\Psi$ is a mapping, then $(i,P) \in \Psi$ and $(i,Q) \in \Psi$ implies $P = Q$. From $P = Q$ and $(i,Q) \in \Phi$, we infer that $(i,P) \in \Phi$. Thus $(i,P) \in {{\Psi}\negmedspace\mid\negmedspace{R}}$ implies $(i,P) \in \Phi$, so ${{\Psi}\negmedspace\mid\negmedspace{R}} \subseteq \Phi$.

Next suppose $(i,P) \in \Phi$. From this it follows that $i \in R = {{\operatorname{dom}{\Phi}}}$. From the premises $(i,P) \in \Phi$ and $\Phi \subseteq \Psi$ we conclude $(i,P) \in \Psi$. Together $(i,P) \in \Psi$ and $i \in R$ imply that $(i,P) \in {{\Psi}\negmedspace\mid\negmedspace{R}}$. Thus $(i,P) \in \Phi$ implies $(i,P) \in {{\Psi}\negmedspace\mid\negmedspace{R}}$, so $\Phi \subseteq {{\Psi}\negmedspace\mid\negmedspace{R}}$.

From ${{\Psi}\negmedspace\mid\negmedspace{R}} \subseteq \Phi$ and $\Phi \subseteq {{\Psi}\negmedspace\mid\negmedspace{R}}$ we infer $\Phi = {{\Psi}\negmedspace\mid\negmedspace{R}}$.

\[L:SUBSET\_SUBSPACE\] Let $\Psi$ and $\Phi$ be ensembles. If $\Phi \subseteq \Psi$, then ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$.

Set $R = {{\operatorname{dom}{\Phi}}}$. Since $\Phi \subseteq \Psi$ by hypothesis, then by applying lemma \[L:SUBSET\_RESTRICTION\] we infer $\Phi = {{\Psi}\negmedspace\mid\negmedspace{R}}$. With this equality and Theorem \[T:SPACE\_UNIQ\_ENSEMBLE\] (invertibility of the Cartesian product), we have ${\prod{\Phi}} = \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$. Theorem \[T:CHC\_RSTR\_EQ\_RSTR\_CHC\] asserts that the restriction of the choice space equals the choice space of the restriction: $(\thinspace\prod\Psi) \mid R = \prod ({{\Psi}\negmedspace\mid\negmedspace{R}})$. Transitivity of equality implies ${\prod{\Phi}} = (\thinspace\prod\Psi) \mid R$. This last equality is exactly the premise of definition \[D:SUBSPACE\]: ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$.

\[T:SUBSET\_IFF\_SUBSPACE\] Let $\Psi$ and $\Phi$ be ensembles. ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$ if and only if $\Phi \subseteq \Psi$.

Lemma \[L:SUBSPACE\_SUBSET\] asserts that if ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$, then $\Phi \subseteq \Psi$. Lemma \[L:SUBSET\_SUBSPACE\] asserts that if $\Phi \subseteq \Psi$, then ${\prod{\Phi}}$ is a subspace of ${\prod{\Psi}}$. This pair of converse implications establishes the biconditional.

\[L:ENSEMBLE\_PROD\_SUBSETS\] If $\Upsilon$, $\Psi$, and $\Phi$ are ensembles such that $\Upsilon = \Psi\Phi$, then $\Psi \subseteq \Upsilon$ and $\Phi \subseteq \Upsilon$.

Since $\Upsilon$ is the dyadic product of $\Psi$ and $\Phi$, then by definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\], $\Psi$ and $\Phi$ are disjoint ensembles and $\Upsilon = \Psi \cup \Phi$.

Suppose $i \in {{\operatorname{dom}{\Upsilon}}} = {{\operatorname{dom}{(\Psi \cup \Phi)}}}$. Through definition \[D:DISJOINT\_ENSEMBLES\], disjointness entails that ${{\operatorname{dom}{\Psi}}}\thickspace\cap\thickspace{{\operatorname{dom}{\Phi}}} = \varnothing$. Thus, if $i \in {{\operatorname{dom}{\Upsilon}}}$, exactly one of two cases hold: either A: $i \in {{\operatorname{dom}{\Psi}}}$ and $i \notin {{\operatorname{dom}{\Phi}}}$, or B: $i \in {{\operatorname{dom}{\Phi}}}$ and $i \notin {{\operatorname{dom}{\Psi}}}$.

Assume case A, that $i \in {{\operatorname{dom}{\Psi}}}$ and $i \notin {{\operatorname{dom}{\Phi}}}$. With $\Upsilon = \Psi \cup \Phi$, it follows from the definition of set union that for any $i \in {{\operatorname{dom}{\Psi}}}$, $(i,P) \in \Psi$ implies $(i,P) \in \Upsilon$ – that is, $\Psi \subseteq \Upsilon$.

For case B, similar argument leads to $\Phi \subseteq \Upsilon$.

\[C:ENSEMBLE\_PROD\_MEMBERS\] If $\Upsilon$, $\Psi$, and $\Phi$ are ensembles such that $\Upsilon = \Psi\Phi$, then $\Psi(i) = \Upsilon(i)$ for $i \in {{\operatorname{dom}{\Psi}}}$, and $\Phi(j) = \Upsilon(j)$ for $j \in {{\operatorname{dom}{\Phi}}}$.

Under identical premises, lemma \[L:ENSEMBLE\_PROD\_SUBSETS\] provides $\Psi \subseteq \Upsilon$ and $\Phi \subseteq \Upsilon$. Suppose $i \in {{\operatorname{dom}{\Psi}}}$. If $(i,P) \in \Psi$, then $(i,P) \in \Upsilon$ since $\Psi \subseteq \Upsilon$. The notation $\Psi(i) = \Upsilon(i)$ (both equaling $P$) is equivalent. A similar argument demonstrates $\Phi(j) = \Upsilon(j)$ for $j \in {{\operatorname{dom}{\Phi}}}$.

\[T:ENSEMBLE\_PROD\_CHOICE\_PROD\] Let $\Upsilon$, $\Psi$, and $\Phi$ be ensembles such that $\Upsilon = \Psi\Phi$. For each $\upsilon \in {\prod{\Upsilon}}$, there exist unique $\psi \in {\prod{\Psi}}$ and $\phi \in {\prod{\Psi}}$ such that $\upsilon = \psi\phi$.

Suppose $\upsilon \in {\prod{\Upsilon}}$. Since any choice has the same domain as its generating ensemble, ${{\operatorname{dom}{\Upsilon}}} = {{\operatorname{dom}{\upsilon}}}$. Theorem \[T:DYADIC\_PRODUCT\_IS\_ENSEMBLE\] states that ${{\operatorname{dom}{\Upsilon}}} = {{\operatorname{dom}{\Psi}}} \cup {{\operatorname{dom}{\Phi}}}$, from which transitivity of equality provides ${{\operatorname{dom}{\upsilon}}} = {{\operatorname{dom}{\Psi}}} \cup {{\operatorname{dom}{\Phi}}}$.

From lemma \[L:ENSEMBLE\_PROD\_SUBSETS\] we conclude $\Psi \subseteq \Upsilon$ and $\Phi \subseteq \Upsilon$. Since these relations hold for entire ensembles, then the same is true of the ensembles’ domains: ${{\operatorname{dom}{\Psi}}} \subseteq {{\operatorname{dom}{\Upsilon}}}$ and ${{\operatorname{dom}{\Phi}}} \subseteq {{\operatorname{dom}{\Upsilon}}}$. By substitution, the previous result ${{\operatorname{dom}{\Upsilon}}} = {{\operatorname{dom}{\upsilon}}}$ then establishes that ${{\operatorname{dom}{\Psi}}} \subseteq {{\operatorname{dom}{\upsilon}}}$ and ${{\operatorname{dom}{\Phi}}} \subseteq {{\operatorname{dom}{\upsilon}}}$.

The inclusion ${{\operatorname{dom}{\Psi}}} \subseteq {{\operatorname{dom}{\upsilon}}}$ ensures that the restriction $\psi = {{\upsilon}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Psi}}}}}$ is well-defined. Similarly $\phi = {{\upsilon}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}}$ is also well-defined.

We next focus on the restriction $\psi$ constructed above, seeking to demonstrate that it is also a member of the choice space ${\prod{\Psi}}$. Suppose term $(i, p) \in \psi$. Since $\psi = {{\upsilon}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Psi}}}}}$, then both $(i, p) \in \upsilon$ and $i \in {{\operatorname{dom}{\Psi}}}$. Since $\upsilon \in {\prod{\Upsilon}}$ by hypothesis, definition \[D:CHOICE\] demands that $p \in \Upsilon(i)$ whenever $(i, p) \in \upsilon$. Corollary \[C:ENSEMBLE\_PROD\_MEMBERS\] asserts $\Psi(i) = \Upsilon(i)$ for $i \in {{\operatorname{dom}{\Psi}}}$. Since $p \in \Upsilon(i)$ and $\Upsilon(i) = \Psi(i)$ then $p \in \Psi(i)$. Thus for any $(i,p) \in \psi$, it follows that $p \in \Psi(i)$. This means that $\psi$ is a choice of $\Psi$ by definition \[D:CHOICE\] – that is, $\psi \in {\prod{\Psi}}$ by definition \[D:CHOICE\_SPACE\].

Similar reasoning establishes that the other restriction $\phi$ is a member of ${\prod{\Phi}}$. The unique $\psi \in {\prod{\Psi}}$ and $\phi \in {\prod{\Psi}}$ such that $\upsilon = \psi\phi$ are expressed by the restrictions $\psi = {{\upsilon}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Psi}}}}}$ and $\phi = {{\upsilon}\negmedspace\mid\negmedspace{{{\operatorname{dom}{\Phi}}}}}$.

Persistent-volatile partition {#S:STATE_EVENT_PRTN}
-----------------------------

Definition \[D:BASIS\] asserts that basis $\langle \Psi, \Phi \rangle$ is comprised of two ensembles satisfying $\Phi \subseteq \Psi$. This allows partitioning terms of $\Psi$ into two sets: those terms that are members of both $\Psi$ and $\Phi$, and those terms that are members of $\Psi$ but not $\Phi$. The ensemble difference terminology of definition \[D:ENSEMBLE\_DIFFERENCE\] poses the minuend, subtrahend, and remainder of this basis as respectively $\Psi$, $\Phi$, and $\Psi \setminus \Phi$.

This partition is important when interpreted as systems theory. The minuend $\Psi$ generates a choice space ${\prod{\Psi}}$ called the *stimulus* space. The subtrahend $\Phi$ generates the *persistent* (alternatively *response*) space ${\prod{\Phi}}$. The remainder $\Psi \setminus \Phi$ generates the *event* space ${\prod{(\Psi \setminus \Phi)}}$.

\[T:STATE\_EVENT\_SPACES\] Let $\langle \Psi, \Phi \rangle$ be a basis. The persistent $(\Phi)$ and volatile $(\Upsilon = \Psi \setminus \Phi)$ generating ensembles are disjoint and complementary with respect to the generating ensemble $\Psi$ of the stimulus space. Expressed in dyadic product, $$\Psi = \Phi\Upsilon$$

Since $\langle \Psi, \Phi \rangle$ is a basis, then $\Phi \subseteq \Psi$ by definition \[D:BASIS\]. With that result and by lemma \[L:DISJOINT\_AND\_COMPLEMENTARY\], the subtrahend $\Phi$ and remainder $\Psi \setminus \Phi$ are disjoint and complementary with respect to $\Psi$.

The dyadic product recapitulates these results. Since $\Psi \setminus \Phi$ and $\Phi$ are disjoint the dyadic product $[\Psi \setminus \Phi][\Phi]$ is well-defined. By definition \[D:DYADIC\_ENSEMBLE\_PRODUCT\], $[\Psi \setminus \Phi][\Phi] = (\Psi \setminus \Phi) \cup \Phi = \Psi$.

The case $\Phi = \varnothing$ does not occur naturally in systems theory because no proper system is unresponsive to all possible stimuli. When $\Psi = \Phi$, the basis has no event space through which to receive transient external stimuli.

Uncoverable processes {#S:UNCOVERABLE_PROCESS_APPENDIX}
=====================

Although any procedure does cover some process, some processes have no covering procedure. This disparity arises naturally through limiting the quantity of distinct functionalities participating in a procedure. Here the constraining mechanism is the catalog of functionality, whose membership must be finite. This stricture’s rationale is to emulate software, which is presumed to possess finite functionality.

Uncoverability of a process entails more than failure of definition \[D:COVERING\_PROCEDURE\] in the case of a particular procedure; uncoverability implies failure for *any* procedure constructed from a given catalog of functionality. With process $\lbrace {\mathbf{f}}_n \rbrace \colon {\mathbb{N}}\to {\prod{\Psi}} \times {\prod{\Phi}}$ and catalog of functionality ${\mathscr{F}}$, uncoverability requires an $i \in {\mathbb{N}}$ and term ${\mathbf{f}}_i = {\mathbf{f}}$ such that ${\mathbf{f}} \notin {\mathit{f}}$ for each ${\mathit{f}} \in {\mathscr{F}}$.

Pigeonhole principle
--------------------

The pigeonhole principle can verify uncoverability, but not coverability. Suppose two frames have the same abscissa but different ordinates. No single functionality can cover both frames, since functionalities are mappings. In more general analogy, let distinct equi-abscissa frames be pigeons, while functionalities be pigeonholes. If more than $N$ pigeons occupy $N$ pigeonholes, then some pigeonhole contains more than one pigeon, which is not allowed.

Underpigeonholing
-----------------

The *frame set* derived from the initial segment of length $k$ of process $\lbrace {\mathbf{f}}_n \rbrace$ is the set ${\mathbf{F}} = \lbrace {\mathbf{f}} \colon {\mathbf{f}} = {\mathbf{f}}_i \;\text{and}\; i \le k\rbrace$. This set’s $\psi$-homogeneous subset contains only those frames having initial condition (abscissa) $\psi \in {\prod{\Psi}}$. The corresponding end-condition set consists of those frames’ ordinates. Obviously the $\psi$-homogeneous end-condition set must have cardinality $\bigl\lvert\lbrace \phi \colon (\psi, \phi) = {\mathbf{f}}_i \;\text{and}\; i \le k\rbrace\bigr\rvert \le k$. The limit supremum (respecting initial segment length and homogeneity choice) presents the process’ worst case scenario.

\[D:UNDERPIGEONHOLE\] Let $\langle \Psi, \Phi \rangle$ be a basis for process $\lbrace {\mathbf{f}}_n \rbrace \colon {\mathbb{N}}\to {\prod{\Psi}} \times {\prod{\Phi}}$ and catalog of functionality ${\mathscr{F}}$. Catalog ${\mathscr{F}}$ *under-pigeonholes* process $\lbrace {\mathbf{f}}_n \rbrace$ if $${\lvert{{\mathscr{F}}}\rvert} <
\lim_{n \to \infty} \biggl(\sup_{\psi \in {\prod{\Psi}}} 
    \biggl(
        \bigl\lvert
        \lbrace \phi \colon (\psi, \phi) = {\mathbf{f}}_i \;\text{and}\; i \le n\rbrace
        \bigr\rvert
    \biggr)\biggr).$$

Whenever the limit supremum fails to converge, no procedure based on a (finite) catalog can cover the process.

MIL-STD-882 and the CPP {#S:MIL-STD-882}
=======================

MIL-STD-882 is the United States Department of Defense Standard Practice for System Safety. Revision E became effective May 11, 2012. In preference to *accident*, this standard prefers the term *mishap*, which it defines as [an event or series of events resulting in unintentional death, injury, occupational illness, damage to or loss of equipment or property, or damage to the environment.]{}

Its safety risk assessment method uses the compound Poisson process (CPP) to represent the timing and severity of mishaps. MIL-STD-882E partitions compound Poisson processes into a lattice of categories and levels that covers the range of interest. The *category* is a variable which, in an explicit range \[1-4\], expresses the expectation $(\mu_L)$ of the CPP loss random variable $L$. The *level* is a variable which, in an explicit range \[A-F\], expresses the rate or intensity $\lambda$ of the CPP.

The system of categories and levels agrees with the limits of discernibility of human intuition. Two different compound Poisson processes having the same category and level are indeed different but in practice are indistinguishable. This characteristic imposes a logarithmic organization on the categories and levels.

  -------------- ---------- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  Description     Severity  Mishap Result Criteria
                  Category  
  Catastrophic       1      Could result in one or more of the following: death, permanent total disability, irreversible significant environmental impact, or monetary loss equal to or exceeding \$10M.
  Critical           2      Could result in one or more of the following: permanent partial disability, injuries or occupational illness that may result in hospitalization of at least three personnel, reversible significant environmental impact, or monetary loss equal to or exceeding \$1M but less than \$10M.
  Marginal           3      Could result in one or more of the following: injury or occupational illness resulting in one or more lost work day(s), reversible moderate environmental impact, or monetary loss equal to or exceeding \$100K but less than \$1M.
  Negligible         4      Could result in one or more of the following: injury or occupational illness not resulting in a lost work day, minimal environmental impact, or monetary loss less than \$100K.
  -------------- ---------- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

  : MIL-STD-882E Severity Categories[]{data-label="Ta:SEVERITY_CATEGORY"}

  Description    Level  Specific Individual Item                                                                   Fleet or Inventory
  ------------- ------- ------------------------------------------------------------------------------------------ ----------------------------------------------------
  Frequent         A    Likely to occur often in the life of an item.                                              Continuously experienced.
  Probable         B    Likely to occur often in the life of an item.                                              Will occur frequently.
  Occasional       C    Likely to occur sometime in the life of an item.                                           Will occur several times.
  Remote           D    Unlikely, but possible to occur in the life of an item.                                    Unlikely, but can reasonably be expected to occur.
  Improbable       E    So unlikely, it can be assumed occurrence may not be experienced in the life of an item.   Unlikely to occur, but possible.
  Eliminated       F                                                                                               

  : MIL-STD-882E Probability Levels[]{data-label="Ta:PROBABILITY_LEVELS"}

Table 2 above is a qualitative description of levels. Table 3 below, appearing in MIL-STD-882E Appendix A, outlines certain pitfalls in accomplishing the same task quantitatively. Numerical expression of the intensity or rate of occurrence is generally preferable to mere qualitative phrasing. For quantitative description, the intensity is the ratio of mishaps (numerator) to some measure of exposure (denominator).

  Description    Level  Individual Item                                                                           Fleet/Inventory\*                                   Quantitative
  ------------- ------- ----------------------------------------------------------------------------------------- --------------------------------------------------- ---------------------------------------------------------------------------------------
  Frequent         A    Likely to occur often in the life of an item                                              Continuously experienced.                           Probability of occurrence greater than or equal to $10^{-1}$.
  Probable         B    Will occur several times in the life of an item                                           Will occur frequently.                              Probability of occurrence less than $10^{-1}$ but greater than or equal to $10^{-2}$.
  Occasional       C    Likely to occur sometime in the life of an item                                           Will occur several times.                           Probability of occurrence less than $10^{-2}$ but greater than or equal to $10^{-3}$.
  Remote           D    Unlikely, but possible to occur in the life of an item                                    Unlikely but can reasonably be expected to occur.   Probability of occurrence less than $10^{-3}$ but greater than or equal to $10^{-6}$.
  Improbable       E    So unlikely, it can be assumed occurrence may not be experienced in the life of an item   Unlikely to occur, but possible.                    Probability of occurrence less than $10^{-6}$.
  Eliminated       F                                                                                                                                                  

  : MIL-STD-882E Example Probability Levels []{data-label="Ta:EXAMPLE_PROBABILITY_LEVELS"}

The false hegemony of a single intuitively understood measure of exposure will now be examined. We will find that, however well-intended, Table 3 lacks essential explanation. Without that, it is an oversimplification.

[Natural]{} measures of exposure must embrace a variety of units, some examples of which are: the life of one item, number of missile firings, flight hours, miles driven, or years of service. For example, an exposure measure of miles driven is expected silently to exclude substantial periods when the system is out of use. Similar would be any situation-based measure of exposure having a sizable portion of time spent in unused status (time not counted). This topic appeared in §\[S:INTERMITTENT\_POISSON\], the intermittant compound Poisson process. The natural unit of exposure can be tuned to the culture of a particular hazard. However, lacking conversion capability, this freedom of choice leads to the problem of a system composed of a heterogeneous plethora of non-comparable exposure units.

What is behind this incomparability? Natural units are important but incomplete – MIL-STD-882E needs additional factors to paint a full quantitative picture. There is need for conversion of various natural units into a single common standard unit, so that comparison involves only observation of magnitudes, without pondering the meaning of different units. This is particularly important in the cases of many ambiguous references to [life.]{} Suppose we arbitrarily standardize time duration at one year. We then define a conversion factor $p$, which means that $p$ years constitute a life. A measure $\iota$ quantifies what fraction of time the system’s mission is inactive or idle. A conversion factor for remaining units must be established; without specifying what units remain to be converted, we can say that the unit conversion calculus of elementary physics results in some linear coefficient $\kappa$. With $N$ a natural exposure unit and $U$ a standard measure, what we have stated so far is summarized in the following form: $$U = \frac{\kappa \cdot (1 - \iota)}{p} \cdot N .$$

Standard units measure statistical risk as resulting from exposure to an intermittent compound Poisson process. These standard units may not be a proper exposure, but measure the exposure expected in a year’s duration. For this reason we celebrate the importance of the role of pure natural units; it is important to understand risk as proportionate to exposure. To understand this importance, imagine yourself as the one exposed to a transient but intense hazard. But that does not imply the dismissal of statistical risk as a concern; it is also part of the risk analysis picture to consider how much risk exposure occurs within a given duration. This is the role of the standard unit.

Another complicating factor is the use of the term [level]{} itself. A level is a designator for a class of possibly intermittent indistinguishable probability distributions. Rather than being clear about this, MIL-STD-882E equivocates greatly in Table 3, confusing this designator with a literal probability statement. Only after full quantitative analysis is completed ($p$, $\iota$, and $\kappa$ known) can definite statements concerning probability be asserted. It is insufficient to mandate vague documentation of [all numerical definitions of probability used in risk assessments]{} without further guidance.

Table 4 below is a categorical rendering of the hyperbola of statistical risk. Definition \[D:STATISTICAL\_RISK\] asserts $h = \lambda \mu_L$. Excepting the administrative level [Eliminated]{}, this cross-tabulation presents the level $(\lambda)$ on the vertical axis and the category $(\mu_L)$ along the horizontal axis. For each combination of level and category, another categorical variable[^13] represents the statistical risk $h = \lambda \mu_L$ with values: High, Serious, Medium, and Low.

  ---------------- -------------- ---------- ---------- ------------
  SEVERITY /        Catastrophic   Critical   Marginal   Negligible
  PROBABILITY           (1)          (2)        (3)         (4)
  Frequent (A)          High         High     Serious      Medium
  Probable (B)          High         High     Serious      Medium
  Occasional (C)        High       Serious     Medium       Low
  Remote (D)          Serious       Medium     Medium       Low
  Improbable (E)       Medium       Medium     Medium       Low
  Eliminated (F)                                        
  ---------------- -------------- ---------- ---------- ------------

  : MIL-STD-882E Risk Assessment Matrix[]{data-label="Ta:RISK_ASSESSMENT_MATRIX"}

This table suffers the same ambiguity as in Table 3. MIL-STD-882’s definitions are clearly inadequate for quantitative analysis. Through equivocation, exposure to an intermittent compound Poisson process is regarded as not different than exposure to a compound Poisson process, despite that the difference becomes obvious through the linear factor $(1 - \iota)$. MIL-STD-882 is an evolving document in its fifth major revision; let us hope these ambiguities are resolved in the future.

Other approaches to automata
============================

Deterministic finite automaton {#S:DFA}
------------------------------

This depiction of the deterministic finite automaton [@wW11autmaton] appears in Wikipedia:

> An *automaton* is represented formally by the 5-tuple $\langle Q, \Sigma, \delta, q_0, A \rangle$, where:
>
> -   $Q$ is a finite set of *states*.
>
> -   $\Sigma$ is a finite set of *symbols*, called the *alphabet* of the automaton.
>
> -   $\delta$ is the *transition function*, that is, $\delta \colon Q \times \Sigma \to Q$.
>
> -   $q_0$ is the *start state*, that is, the state which the automaton is *in* when no input has been processed yet, where $q_0 \in Q$.
>
> -   $A$ is a set of states of $Q$ (i.e. $A \subseteq Q$) called *accept states*.
>
An approach for engineers is found in [@jH79].

[20]{}

Benjamin S. Blanchard and Wolter J. Fabrycky, Systems Engineering and Analysis, 3rd edition, Prentice Hall, 1998

Arthur D. Hall, A Methodology For Systems Engineering, (New York: Van Nostrand Reinhold Company), 1962

John D. Musa and Anthony Iannino and Kazuhira Okumoto, [*Software reliability - measurement, prediction, application*]{}, McGraw-Hill, 1987

Hopcroft, J. E. and Ullman, J. D., [*Introduction to Automata Theory, Languages and Computation*]{}, Second Edition, Addison-Wesley, 1979

Paul R. Halmos, Naive Set Theory, Springer-Verlag New York, 1974

United States Department of Defense, Joint Software Systems Safety Engineering Handbook, Internet, http://www.acq.osd.mil/se/docs/Joint-SW-Systems-Safety-Engineering-Handbook.pdf, retrieved 2014-09-19

United States Department of Defense, MIL-STD-882E (Standard Practice for System Safety), Internet, http://www.assistdocs.com/search/search\_basic.cfm, retrieved 2012-05-13T18:01Z

Wikipedia, Internet, http://en.wikipedia.org/wiki/Automata\_theory, retrieved July 18, 2011

Wikipedia, Internet, http://en.wikipedia.org/wiki/Emergence, retrieved June 13, 2014

Wikipedia, Internet, http://en.wikipedia.org/wiki/Frequentist\_probability, retrieved March 10, 2014

Wikipedia, Internet, http://en.wikipedia.org/wiki/Poisson\_distribution, retrieved May 20, 2013

Wikipedia, Internet, http://en.wikipedia.org/wiki/Poisson\_process, retrieved May 20, 2013

Wikipedia, Internet, http://en.wikipedia.org/wiki/Law\_of\_total\_expectation, retrieved May 20, 2013

Wikipedia, Internet, http://en.wikipedia.org/wiki/Compound\_Poisson\_process, retrieved May 20, 2013

Wikipedia, Internet, http://en.wikipedia.org/wiki/Cumulant, retrieved May 24, 2013

[^1]: http://creativecommons.org/licenses/by/3.0/

[^2]: The author is a retired software safety engineer, not a mathematician.

[^3]: A reactive system responds to its environment, or external stimuli.

[^4]: That is, the *converse* is not generally a pointwise invertible mapping as suggested by the term *inverse*.

[^5]: The author is unaware of a proper definition.

[^6]: software causes no harm until erroneous values transduce the boundary between software and hardware.

[^7]: One increasing, the other decreasing

[^8]: After Siméon Denis Poisson, mathematician and physicist, 1781 – 1840

[^9]: Its symbol is a composite of other notational devices that have no separate meaning.

[^10]: Hobson was proprietor of a livery. He was noted for offering his customers their choice of any horse, as long as that horse was in the first unoccupied stall.

[^11]: The set difference $A \setminus B$ is not conventionally restricted to $B \subseteq A$, as is stipulated here.

[^12]: one form of which is $(\neg B \Rightarrow \neg A)\Leftrightarrow(A \Rightarrow B)$

[^13]: Not to be confused with the categorical variable named [category]{}
