اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدProperties of Input-Consuming Derivations
63
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. We consider the class of nicely-moded programs and queries. We show that for these programs a weak version of the well-known switching lemma holds also for input-consuming derivations. Furthermore, we show that, under suitable conditions, there exists an algebraic characterization of termination of input-consuming derivations.
قيم البحث
اقرأ أيضاً
Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric compositionality propert
y. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between processes when they are combined by that operator. The compositionality property of an operator is computed by recursively counting how many times the combined processes are copied along their evolution. The compositionality properties allow to derive an upper bound on the distance between processes by purely inspecting the operators used to specify those processes.
We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Separation logic with abstract predicates enforces a resource discipline
that constrains when and how calls may be made between a client and a library. Intuitively, this can enforce a protocol on the interaction trace. This intuition is broadly used in the separation logic community but has not previously been formalised. We provide just such a formalisation. Our approach is based on using wrappers which instrument library code to induce execution traces for the properties under examination. By considering a separation logic extended with trace resources, we prove that when a library satisfies its separation logic specification then its wrapped version satisfies the same specification and, moreover, maintains the trace properties as an invariant. Consequently, any client and library implementation that are correct with respect to the separation logic specification will satisfy the trace properties.
This paper is concerned with the form of typed name binding used by the FreshML family of languages. Its characteristic feature is that a name binding is represented by an abstract (name,value)-pair that may only be deconstructed via the generation o
f fresh bound names. The paper proves a new result about what operations on names can co-exist with this construct. In FreshML the only observation one can make of names is to test whether or not they are equal. This restricted amount of observation was thought necessary to ensure that there is no observable difference between alpha-equivalent name binders. Yet from an algorithmic point of view it would be desirable to allow other operations and relations on names, such as a total ordering. This paper shows that, contrary to expectations, one may add not just ordering, but almost any relation or numerical function on names without disturbing the fundamental correctness result about this form of typed name binding (that object-level alpha-equivalence precisely corresponds to contextual equivalence at the programming meta-level), so long as one takes the state of dynamically created names into account.
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $textit{space}$ efficiencies, the price being $textit{time}$ performances often poorer than those obtainable with tra
ditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how emph{general} this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.
Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in particular processing due to jump instructions. We mo
del mechanistic processing preceding some further behavior as a delay of that behavior; we borrow a unary delay operator from discrete time process algebra. We define a mechanistic improvement ordering on threads and observe that some threads do not have an optimal implementation.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
