اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCharacterisation of Strongly Normalising lambda-mu-Terms
209
0
0.0
(
0
)
تأليف
Steffen van Bakel
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter and a restricted use of the type omega enable us to represent the particular notion of continuation used in the literature for the definition of semantics for the lambda-mu-calculus. This makes it possible to lift the well-known characterisation property for strongly-normalising lambda-terms - that uses intersection types - to the lambda-mu-calculus. From this result an alternative proof of strong normalisation for terms typeable in Parigots propositional logical system follows, by means of an interpretation of that system into ours.
قيم البحث
اقرأ أيضاً
We study the sequences of numbers corresponding to lambda terms of given sizes, where the size is this of lambda terms with de Bruijn indices in a very natural model where all the operators have size 1. For plain lambda terms, the sequence correspond
s to two families of binary trees for which we exhibit bijections. We study also the distribution of normal forms, head normal forms and strongly normalizing terms. In particular we show that strongly normalizing terms are of density 0 among plain terms.
In this paper we define intersection and union type assignment for Parigots calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This imp
lies that this notion of intersection-union type assignment is suitable to define a semantics.
In a paper entitled Binary lambda calculus and combinatory logic, John Tromp presents a simple way of encoding lambda calculus terms as binary sequences. In what follows, we study the numbers of binary strings of a given size that represent lambda te
rms and derive results from their generating functions, especially that the number of terms of size n grows roughly like 1.963447954. .. n. In a second part we use this approach to generate random lambda terms using Boltzmann samplers.
We study the lambda-mu-calculus, extended with explicit substitution, and define a compositional output-based interpretation into a variant of the pi-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimi
larity. We define four notions of weak equivalence for lambda-mu -- one based on weak reduction, two modelling weak head-reduction and weak explicit head reduction (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation -- and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes.
The differential branching fraction of the rare decay $Lambda^{0}_{b} rightarrow Lambda mu^+mu^-$ is measured as a function of $q^{2}$, the square of the dimuon invariant mass. The analysis is performed using proton-proton collision data, correspondi
ng to an integrated luminosity of $3.0 mbox{ fb}^{-1}$, collected by the LHCb experiment. Evidence of signal is observed in the $q^2$ region below the square of the $J/psi$ mass. Integrating over $15 < q^{2} < 20 mbox{ GeV}^2/c^4$ the branching fraction is measured as $dmathcal{B}(Lambda^{0}_{b} rightarrow Lambda mu^+mu^-)/dq^2 = (1.18 ^{+ 0.09} _{-0.08} pm 0.03 pm 0.27) times 10^{-7} ( mbox{GeV}^{2}/c^{4})^{-1}$, where the uncertainties are statistical, systematic and due to the normalisation mode, $Lambda^{0}_{b} rightarrow J/psi Lambda$, respectively. In the $q^2$ intervals where the signal is observed, angular distributions are studied and the forward-backward asymmetries in the dimuon ($A^{l}_{rm FB}$) and hadron ($A^{h}_{rm FB}$) systems are measured for the first time. In the range $15 < q^2 < 20 mbox{ GeV}^2/c^4$ they are found to be $A^{l}_{rm FB} = -0.05 pm 0.09 mbox{ (stat)} pm 0.03 mbox{ (syst)}$ and $A^{h}_{rm FB} = -0.29 pm 0.07 mbox{ (stat)} pm 0.03 mbox{ (syst)}$.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
