Do you want to publish a course? Click here

Characterisation of Strongly Normalising lambda-mu-Terms

237   0   0.0 ( 0 )
 Added by EPTCS
 Publication date 2013
and research's language is English




Ask ChatGPT about the research

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.



rate research

Read More

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 corresponds 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.
384 - Steffen van Bakel 2011
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 implies that this notion of intersection-union type assignment is suitable to define a semantics.
100 - Katarzyna Grygiel 2015
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 terms 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.
221 - Steffen van Bakel 2014
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 bisimilarity. 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, corresponding 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)}$.
comments
Fetching comments Fetching comments
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا