Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFactorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
96
0
0.0
(
0
)
Added by
Giulio Guerrieri
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
In each variant of the lambda-calculus, factorization and normalization are two key-properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the lambda-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV. The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.
rate research
Read More
We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a call-by-name language whereas the latter is call-by-value; the former considers algebraic equalities whereas the latter approaches them through rewrite rules. In this paper, we analyse how these different approaches relate to one another. To this end, we propose four canonical languages based on each of the possible choices: call-by-name versus call-by-value, algebraic equality versus algebraic rewriting. We show that the various languages simulate one another. Due to subtle interaction between beta-reduction and algebraic rewriting, to make the languages consistent some additional hypotheses such as confluence or normalisation might be required. We carefully devise the required properties for each proof, making them general enough to be valid for any sub-language satisfying the corresponding properties.
Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate problem, which depends on the notion of evaluation strategy. Since the nineties, it is known that weak (that is, out of abstractions) call-by-value evaluation is a reasonable strategy while Levys optimal parallel strategy, which is strong (that is, it reduces everywhere), is not. The strong case turned out to be subtler than the weak one. In 2014 Accattoli and Dal Lago have shown that strong call-by-name is reasonable, by introducing a new form of useful sharing and, later, an abstract machine with an overhead quadratic in the number of beta-steps. Here we show that also strong call-by-value evaluation is reasonable for time, via a new abstract machine realizing useful sharing and having a linear overhead. Moreover, our machine uses a new mix of sharing techniques, adding on top of useful sharing a form of implosive sharing, which on some terms brings an exponential speed-up. We give examples of families that the machine executes in time logarithmic in the number of beta-steps.
This paper explores two topics at once: the use of denotational semantics to bound the evaluation length of functional programs, and the semantics of strong (that is, possibly under abstractions) call-by-value evaluation. About the first, we analyze de Carvalhos seminal use of relational semantics for bounding the evaluation length of lambda-terms, starting from the presentation of the semantics as an intersection types system. We focus on the part of his work which is usually neglected in its many recent adaptations, despite being probably the conceptually deeper one: how to transfer the bounding power from the type system to the relational semantics itself. We dissect this result and re-understand it via the isolation of a simpler size representation property. About the second, we use relational semantics to develop a semantical study of strong call-by-value evaluation, which is both a delicate and neglected topic. We give a semantic characterization of terms normalizable with respect to strong evaluation, providing in particular the first result of adequacy with respect to strong call-by-value. Moreover, we extract bounds about strong evaluation from both the type systems and the relational semantics. Essentially, we use strong call-by-value to revisit de Carvalhos semantic bounds, and de Carvalhos technique to provide semantical foundations for strong call-by-value.
We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no such proof system has been proposed in the literature.
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism, which were developed in blame calculi and to state the gradual guarantee theorem of gradual typing. Combined with the ordinary extensionality ($eta$) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of Findler and Felleisens definitions of contracts, and use it to build some concrete domain-theoretic models of gradual typing.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
