ترغب بنشر مسار تعليمي؟ اضغط هنا

Counting and Generating Terms in the Binary Lambda Calculus (Extended version)

101   0   0.0 ( 0 )
 نشر من قبل Pierre Lescanne
 تاريخ النشر 2015
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English
 تأليف Katarzyna Grygiel




اسأل ChatGPT حول البحث

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.



قيم البحث

اقرأ أيضاً

79 - Yann Hamdaoui 2021
In this paper, we show how to interpret a language featuring concurrency, references and replication into proof nets, which correspond to a fragment of differential linear logic. We prove a simulation and adequacy theorem. A key element in our transl ation are routing areas, a family of nets used to implement communication primitives which we define and study in detail.
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.
We consider multi-agent systems where agents actions and beliefs are determined aleatorically, or by the throw of dice. This system consists of possible worlds that assign distributions to independent random variables, and agents who assign probabili ties to these possible worlds. We present a novel syntax and semantics for such system, and show that they generalise Modal Logic. We also give a sound and complete calculus for reasoning in the base semantics, and a sound calculus for the full modal semantics, that we conjecture to be complete. Finally we discuss some application to reasoning about game playing agents.
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.
211 - Giulio Manzonetto 2009
In this paper we briefly summarize the contents of Manzonettos PhD thesis which concerns denotational semantics and equational/order theories of the pure untyped lambda-calculus. The main research achievements include: (i) a general construction of l ambda-models from reflexive objects in (possibly non-well-pointed) categories; (ii) a Stone-style representation theorem for combinatory algebras; (iii) a proof that no effective lambda-model can have lambda-beta or lambda-beta-eta as its equational theory (this can be seen as a partial answer to an open problem introduced by Honsell-Ronchi Della Rocca in 1984).
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

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