اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدQuantitative aspects of linear and affine closed lambda terms
260
0
0.0
(
0
)
تأليف
Pierre Lescanne
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Affine $lambda$-terms are $lambda$-terms in which each bound variable occurs at most once and linear $lambda$-terms are $lambda$-terms in which each bound variables occurs once. and only once. In this paper we count the number of closed affine $lambda$-terms of size $n$, closed linear $lambda$-terms of size $n$, affine $beta$-normal forms of size $n$ and linear $beta$-normal forms of ise $n$, for different ways of measuring the size of $lambda$-terms. From these formulas, we show how we can derive programs for generating all the terms of size $n$ for each class. For this we use a specific data structure, which are contexts taking into account all the holes at levels of abstractions.
قيم البحث
اقرأ أيضاً
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.
This volume of the EPTCS contains the proceedings of the 15th international workshop on Qualitative Aspects of Programming Languages and Systems, QAPL 2017, held at April 23, 2017 in Uppsala, Sweden as a satellite event of ETAPS 2017, the 20th Europe
an Joint Conferencec on Theory and Practice of Software. The volume contains two invited contributions by Erika Abraham and by Andrea Vandin as well as six technical papers selected by the QAPL 2017 program committee.
This volume contains the proceedings of the Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL 2010), held in Paphos, Cyprus, on March 27-28, 2010. QAPL 2010 is a satellite event of the European Joint Conferences on Theory and Pra
ctice of Software (ETAPS 2010). The workshop theme is on quantitative aspects of computation. These aspects are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust), and play an important (sometimes essential) role in characterising the behavior and determining the properties of systems. Such quantities are central to the definition of both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of the systems properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems.
We study the existence of automatic presentations for various algebraic structures. An automatic presentation of a structure is a description of the universe of the structure by a regular set of words, and the interpretation of the relations by synch
ronised automata. Our first topic concerns characterising classes of automatic structures. We supply a characterisation of the automatic Boolean algebras, and it is proven that the free Abelian group of infinite rank, as well as certain Fraisse limits, do not have automatic presentations. In particular, the countably infinite random graph and the random partial order do not have automatic presentations. Furthermore, no infinite integral domain is automatic. Our second topic is the isomorphism problem. We prove that the complexity of the isomorphism problem for the class of all automatic structures is Sigma_1^1-complete.
We study the (hereditary) discrepancy of definable set systems, which is a natural measure for their inherent complexity and approximability. We establish a strong connection between the hereditary discrepancy and quantifier elimination over signatur
es with only unary relation and function symbols. We prove that set systems definable in theories (over such signatures) with quantifier elimination have constant hereditary discrepancy. We derive that set systems definable in bounded expansion classes, which are very general classes of uniformly sparse graphs, have bounded hereditary discrepancy. We also derive that nowhere dense classes, which are more general than bounded expansion classes, in general do not admit quantifier elimination over a signature extended by an arbitrary number of unary function symbols. We show that the set systems on a ground set $U$ definable on a monotone nowhere dense class of graphs $mathscr C$ have hereditary discrepancy at most $|U|^{c}$ (for some~$c<1/2$) and that, on the contrary, for every monotone somewhere dense class $mathscr C$ and for every positive integer $d$ there is a set system of $d$-tuples definable in $mathscr C$ with discrepancy $Omega(|U|^{1/2})$. We further prove that if $mathscr C$ is a class of graphs with bounded expansion and $phi(bar x;bar y)$ is a first-order formula, then we can compute in polynomial time, for an input graph $Ginmathscr C$, a mapping $chi:V(G)^{|bar x|}rightarrow{-1,1}$ witnessing the boundedness of the discrepancy of the set-system defined by~$phi$, an $varepsilon$-net of size $mathcal{O}(1/varepsilon)$, and an $varepsilon$-approximation of size $mathcal{O}(1/varepsilon)$.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
