اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدSimulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq
92
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
This paper shows equivalence of sever
قيم البحث
اقرأ أيضاً
We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is e
quipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a call-by-name language whereas the latter is call-by-value; the former considers algebraic equalities whereas the latter approaches them through rewrite rules. In this paper, we analyse how these different approaches relate to one another. To this end, we propose four canonical languages based on each of the possible choices: call-by-name versus call-by-value, algebraic equality versus algebraic rewriting. We show that the various languages simulate one another. Due to subtle interaction between beta-reduction and algebraic rewriting, to make the languages consistent some additional hypotheses such as confluence or normalisation might be required. We carefully devise the required properties for each proof, making them general enough to be valid for any sub-language satisfying the corresponding properties.
In this paper we prove that any lambda-term that is strongly normalising for beta-reduction is also strongly normalising for beta,assoc-reduction. assoc is a call-by-value rule that has been used in works by Moggi, Joachimsky, Espirito Santo and othe
rs. The result has often been justified with incomplete or incorrect proofs. Here we give one in full details.
This paper studies useful sharing, which is a sophisticated optimization for lambda-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing turns out to be harder to manipulate in call-by-need than in call-by-name
or call-by-value, because call-by-need evaluates inside environments, making it harder to specify when a substitution step is useful. We isolate the key involved concepts and prove the correctness of useful sharing in this setting.
We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is i
ts linear type system, which includes a duplicability operator ! as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements. The ! operator gives rise to a comonad, as in the linear logic models of Seely, Bierman, and Benton. The side-effects give rise to a monad, as in Moggis computational lambda calculus. It is this combination of a monad and a comonad that makes the present paper interesting. We show that our categorical semantics is sound and complete.
We introduce two extensions of the $lambda$-calculus with a probabilistic choice operator, $Lambda_oplus^{cbv}$ and $Lambda_oplus^{cbn}$, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys conflu
ence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, $Lambda_oplus^!$, which allows for a fine control of the interaction between choice and copying, and which allows us to develop a unified, modular approach.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
