اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدTermination of lambda-calculus with the extra Call-By-Value rule known as assoc
173
0
0.0
(
0
)
تأليف
Stephane Lengrand
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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 others. The result has often been justified with incomplete or incorrect proofs. Here we give one in full details.
قيم البحث
اقرأ أيضاً
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.
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.
95 -
Manfred Schmidt-Schau{ss} (Dept. Informatik und Mathematik
, Inst.n Informatik
, J.W. Goethe-University
2015
This paper shows equivalence of sever
Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate problem, which depends on the notion of evaluation strategy. Since the ni
neties, it is known that weak (that is, out of abstractions) call-by-value evaluation is a reasonable strategy while Levys optimal parallel strategy, which is strong (that is, it reduces everywhere), is not. The strong case turned out to be subtler than the weak one. In 2014 Accattoli and Dal Lago have shown that strong call-by-name is reasonable, by introducing a new form of useful sharing and, later, an abstract machine with an overhead quadratic in the number of beta-steps. Here we show that also strong call-by-value evaluation is reasonable for time, via a new abstract machine realizing useful sharing and having a linear overhead. Moreover, our machine uses a new mix of sharing techniques, adding on top of useful sharing a form of implosive sharing, which on some terms brings an exponential speed-up. We give examples of families that the machine executes in time logarithmic in the number of beta-steps.
In this paper we introduce a typed, concurrent $lambda$-calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we recover strong normalization. The proof is based on a reducibility t
echnique and an original interactive property reminiscent of the Game Semantics approach.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
