اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn algorithmic equivalence of instruction sequences for computing bit string functions
412
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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 ver
y 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 concerne
d. 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, Hagg
strom, 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 instructio
n 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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
