arXiv subjects

Giulio Guerrieri

Publications and source records attributed to Giulio Guerrieri.

31 records · Page 2Linked to original sources

arXiv2019

Factorization and Normalization, Essentially

Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi's technique to prove factorization for head reduction. Our technique is both simpler and more powerful, as it works in cases where Takahishi's does not. We then pair factorization with two other abstract properties, defining \emph{essential systems}, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.

cs.LO↗

arXiv2019

Glueability of resource proof-structures: inverting the Taylor expansion (long version)

A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.

cs.LO↗

arXiv2019

Crumbling Abstract Machines

Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications have only values as immediate subterms. This work studies how such a crumbled representation of terms impacts on the design and the efficiency of abstract machines for call-by-value evaluation. About the design, it removes the need for data structures encoding the evaluation context, such as the applicative stack and the dump, that get encoded in the environment. About efficiency, we show that there is no slowdown, clarifying in particular a point raised by Kennedy, about the potential inefficiency of such a representation. Moreover, we prove that everything smoothly scales up to the delicate case of open terms, needed to implement proof assistants. Along the way, we also point out that continuation-passing style transformations--that may be alternatives to our representation--do not scale up to the open case.

cs.LO↗

arXiv2019

Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus

We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value lambda-calculus. For this purpose, we use a linear logic based denotational model that can be seen as a non-idempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proof-nets and untyped call-by-name lambda-calculus. We first prove a qualitative result: a (possibly open) term is normalizable for weak reduction (which does not reduce under abstractions) if and only if its interpretation is not empty. We then show that the size of type derivations can be used to measure the execution time. Finally, we show that, differently from the case of linear logic and call-by-name lambda-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

cs.LO↗

arXiv2019

The Bang Calculus and the Two Girard's Translations

We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both call-by-name and call-by-value lambda-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value lambda-calculi from a syntactic and a semantic viewpoint.

cs.LO↗

arXiv2019

Types by Need (Extended Version)

A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho's system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.

cs.LO↗

arXiv2018

Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version)

We investigate the possibility of a semantic account of the execution time (i.e. the number of β_v-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value λ-calculus. For this purpose, we use a linear logic based denotational model that can be seen as a non-idempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proof-nets and untyped call-by-name λ-calculus. We first prove a qualitative result: a (possibly open) term is normalizable for weak reduction (which does not reduce under abstractions) if and only if its interpretation is not empty. We then show that the size of type derivations can be used to measure the execution time. Finally, we show that, differently from the case of linear logic and call-by-name λ-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

cs.LO↗

arXiv2018

Types of Fireballs (Extended Version)

The good properties of Plotkin's call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate, and the literature contains a number of proposals. Recently, Accattoli and Guerrieri provided detailed operational and implementative studies of these proposals, showing that they are equivalent from the point of view of termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-value, adapting de Carvalho's analysis of call-by-name via multi types (aka non-idempotent intersection types). Our type system characterises normalisation and thus provides an adequate relational semantics. Moreover, type derivations carry quantitative information about the cost of evaluation: their size bounds the number of evaluation steps and the size of the normal form, and we also characterise derivations giving exact bounds. The study crucially relies on a new, refined presentation of the fireball calculus, the simplest proposal for open call-by-value, that is more apt to denotational investigations.

cs.LO↗

arXiv2017

Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characterizations of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin's one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin's call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi's approach of parallel reductions to our set of reduction rules. The standardization is weak (i.e. redexes are not fully sequentialized) because of overlapping interferences between reductions.

cs.LO↗

arXiv2017

Postponement of raa and Glivenko's theorem, revisited (extended version)

This article focuses on the technique of postponing the application of the reduction ad absurdum rule (raa) in classical natural deduction. First, it is shown how this technique is connected with two normalization strategies for classical logic: one given by Prawitz, and the other by Seldin. Secondly, a variant of Seldin's strategy for the postponement of raa is proposed, and the similarities with Prawitz's approach are investigated. In particular, it is shown that, as for Prawitz, it is possible to use this variant of Seldin's strategy in order to induce a negative translation from classical to intuitionistic and minimal logic, which is nothing but a variant of Kuroda's translation. Through this translation, Glivenko's theorem for intuitionistic and minimal logic is proven.

math.LO↗

arXiv2017

Implementing Open Call-by-Value (Extended Version)

The theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required. Open call-by-value is the intermediate setting of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. This paper provides a theory of abstract machines for open call-by-value. The literature contains machines that are either simple but inefficient, as they have an exponential overhead, or efficient but heavy, as they rely on a labelling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements open call-by-value within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead.

cs.LO↗

arXiv2016

Open Call-by-Value (Extended Version)

The elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required, and it is well known that the operational semantics of call-by-value becomes problematic in this case. Here we study the intermediate setting -- that we call Open Call-by-Value -- of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. Various calculi for Open Call-by-Value already exist, each one with its pros and cons. This paper presents a detailed comparative study of the operational semantics of four of them, coming from different areas such as the study of abstract machines, denotational semantics, linear logic proof nets, and sequent calculus. We show that these calculi are all equivalent from a termination point of view, justifying the slogan Open Call-by-Value.

cs.LO↗

arXiv2016

Relational type-checking for MELL proof-structures. Part 1: Multiplicatives

Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $Γ$ acts thus as a type (refining $Γ$) having R as an inhabitant. We are interested in the following type-checking question: given a proof-structure R, a list of formulae $Γ$, and a point x in the relational interpretation of $Γ$, is x in the interpretation of R? This question is decidable. We present here an algorithm that decides it in time linear in the size of R, if R is a proof-structure in the multiplicative fragment of linear logic. This algorithm can be extended to larger fragments of multiplicative-exponential linear logic containing $λ$-calculus.

cs.LO↗