Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCharacterisation of Strongly Normalising lambda-mu-Terms
242
0
0.0
(
0
)
Added by
EPTCS
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Authors
Steffen van Bakel
Ask ChatGPT about the research
No Arabic abstract
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.
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.
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.
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)}$.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
