Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn algorithmic equivalence of instruction sequences for computing bit string functions
409
0
0.0
(
0
)
Added by
Kees Middelburg
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonable degree the intuitive notion that two instruction sequences express the same algorithm.
rate research
Read More
This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each function from ${0,1}^n$ to ${0,1}$ can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to ${0,1}^n$ of the function from ${0,1}^*$ to ${0,1}$ that models the non-zeroness test function, for $n > 0$, under several restrictions on the arbitrary instruction sequence.
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.
Let X^{(k)}(t) = (X_1(t), ..., X_k(t)) denote a k-vector of i.i.d. random variables, each taking the values 1 or 0 with respective probabilities p and 1-p. As a process indexed by non-negative t, $X^{(k)}(t)$ is constructed--following Benjamini, Haggstrom, Peres, and Steif (2003)--so that it is strong Markov with invariant measure ((1-p)delta_0+pdelta_1)^k. We derive sharp estimates for the probability that ``X_1(t)+...+X_k(t)=k-ell for some t in F, where F subset [0,1] is nonrandom and compact. We do this in two very different settings: (i) Where ell is a constant; and (ii) Where ell=k/2, k is even, and p=q=1/2. We prove that the probability is described by the Kolmogorov capacitance of F for case (i) and Howroyds 1/2-dimensional box-dimension profiles for case (ii). We also present sample-path consequences, and a connection to capacities that answers a question of Benjamini et. al. (2003)
Single-pass instruction sequences under execution are considered to produce behaviours to be controlled by some execution environment. Threads as considered in thread algebra model such behaviours: upon each action performed by a thread, a reply from its execution environment determines how the thread proceeds. Threads in turn can be looked upon as producing processes as considered in process algebra. We show that, by apposite choice of basic instructions, all processes that can only be in a finite number of states can be produced by single-pass instruction sequences.
In this paper, we study the phenomenon that instruction sequences are split into fragments which somehow produce a joint behaviour. In order to bring this phenomenon better into the picture, we formalize a simple mechanism by which several instruction sequence fragments can produce a joint behaviour. We also show that, even in the case of this simple mechanism, it is a non-trivial matter to explain by means of a translation into a single instruction sequence what takes place on execution of a collection of instruction sequence fragments.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
