Project topics and materials
Get Complete Project Material File(s) Now! »
Tools
Multi types
We shall give a type-theoretical presentation of the normalization process of our useful call-by-need reduction relation. Given the intrinsically complex nature of the subject, we shall first cover several related cases before attaining the final one. Thus, in the process of deriving the type system for the useful call-by-need relation, we shall study several other reduction relations and derive a separate type system for each one of them, in a well-principled and incremental manner.
All of these type systems fall into the category of multi type systems. Multi types were introduced as non-idempotent intersection types in Philippa Gardner’s “Discovering Needed Reductions Using Type Theory”[Gar94]. The reasons for which multi type systems have recently become trending are numerous; our interest in them lies particularly in that each of them are designed specifically to characterize a certain notion of normalization. Moreover, type derivations shall provide upper bounds on the consumption of resources in the corresponding normalization process. These upper bounds may be obtained in such a precise way that some of them are even exact bounds, or simply measures of the normalization process. For this reason, multi types are said to be resource aware, as they allow us to reason about resources from a type-theoretical standpoint.
Multi types were first used to give precise measurements on operational quantities in de Car-valho’s “Execution Time of lambda-Terms via Denotational Semantics and Intersection Types” [Car09]. The starting point therein is a multiset-based relational model of Linear Logic2, called System R, which induces a relational semantics of the type-free λ-calculus. De Carvalho then proves that the size of type derivations and the size of types in System R are closely related to the execution time of λ-terms in Krivine’s machine.
Since then, [Car09] has inspired numerous lines of research, and its results have been re-fined and extended to encompass different normalization processes as well as different operational measurements—this thesis intends to be one of such recent works.
Unlike de Carvalho, however, abstract machines are not our operational semantics of reference. Instead, when defining our reduction relations we shall resort to the Linear Substitution Calculus— or LSC for short3—a calculus which may be seen as intermediate in between the λ-calculus and abstract machines.
Operational semantics
Among the different kinds of argument-passing styles that reduction relations may adopt, we shall be concerned with the three that we dim central to the theory of the λ-calculus: call-by-name, call-by-value and call-by-need:
Since call-by-name is by far the most studied one—from a theoretical and foundational point of view—we shall not present novel results about it, and just use the ones from the literature to build upon. Call-by-name is the argument-passing technique implemented by the standard evaluation strategy of the λ-calculus, called leftmost-outermost reduction.
Call-by-value has been relatively neglected when compared to the theoretical foundations given to call-by-name. Despite that, it is probably the most implemented argument-passing style among programming languages.
Call-by-need, is probably the least studied one, theoretically-wise. In practice, call-by-need has nevertheless received considerable attention since its inception; however, this has always been restricted to technological implementations—like the Haskell programming language, or the Coq proof assistant—or theoretical foundations that only covered the most basic case—of weak reduction on closed λ-terms. This work intends to revert this, by providing results that might expand its theoretical understanding and foundational solidity beyond the usual weak and closed settings.
We shall begin our study of call-by-need by realizing that it may be understood (in the weak and closed setting) as a combination of call-by-name and call-by-value. Hence, some of the results given for call-by-name or call-by-value shall contribute to our understanding of call-by-need.
Our operational results are based on three recent and important advances in the operational theory of the λ-calculus, namely:
Firstly, the publishing in 2017 of Balabonski, Barenbaum, Bonelli and Kesner’s “Foundations of Strong Call by Need” [Bal+17], where the authors propose a first-ever, call-by-need strategy computing strong normal forms and acting on potentially open terms. This is a call-by-need strategy in the sense that it guarantees that arguments are only reduced once and only if—and when—needed4.
Secondly, the publishing of Accattoli and Dal Lago’s “(Leftmost-outermost) Beta Reduction is Invariant, Indeed” [AL16] in 2016, where the authors provide a unitary time cost model of the λ-calculus and show it is polynomially related to that of Turing machines or random access machines.
As explained above, it required implementing useful reduction on leftmost-outermost reduc-tion. In addition, it requires defining the useful variant of leftmost-outermost in a formalism implementing some notion of sharing, like the LSC.
Finally, Accattoli and Guerrieri isolated the so called Open Call-by-Value calculus in [AG16], a setting halfway between the most basic and restricted variant of the call-by-value λ-calculus and the most general one: respectively, they are the Weak Call-by-Value—which only acts on closed λ-terms—and the Strong Call-by-Value—which may act on open λ-terms. The value of this result is that Strong Call-by-Value may be seen as the Open Call-by-Value iterated under λ-abstractions.
Remarkably, they use techniques involving multi types in [Bal+17] to prove that their strategy is complete with respect to β-reduction to strong normal forms.
Development and outcomes
The starting point of this thesis are the multi type systems given in the literature for the weak and closed variants of CbN—that is, System R given by de Carvalho—and of CbV—see Ehrhard’s call-by-value variant of System R in [Ehr12]. Since multi types model CbN and CbV well, it was only natural to try to apply this technique to CbNeed, more so considering the fact that CbNeed may be seen as a combination of CbN and CbV—in the particular way we shall explain in Chapter 4 (CbN, CbV and CbNeed).
We believe that the understanding of Useful Open CbNeed, both operationally and type-theoretically, is likely the most interesting result in our work. It is presented in Chapter 8 (Useful Open CbNeed) and intends to connect two of the recent advances in the operational theory of the λ-calculus—that we listed in Subsect. 1.2 (Operational semantics): we begin by taking a reduction sub-relation from [Bal+17]—which we call Open CbNeed—then we take the notion of usefulness as presented in [AL16], and we finally use it to adapt Open CbNeed to perform useful reduction, thus obtaining Useful Open CbNeed.
As we shall see in Chapter 6 (Open CbNeed), Open CbNeed is itself interesting, in particular because it happens to be the natural way to factor the difficulties faced in the development of a theory of strong reduction in a call-by-need setting. Moreover, it constitutes the natural setting where the restriction to useful reductions may be implemented and studied, as it is a significantly simpler scenario compared to variants of call-by-need implementing strong reduction.
Another natural intermediate step to achieving the results for Useful Open CbNeed is under-standing Open Call-by-Value, for which a multi type system with a class of type derivations pro-viding exact bounds is given in [AG18]. Here, we shall extend the reduction relation of Open Call-by-Value to define the more general Strong Call-by-Value relation—which encompasses Open Call-by-Value—and then provide a multi type system whose notion of typability matches that of normalization in Strong Call-by-Value. As a matter of fact, the multi type system for Strong Call-by-Value served as inspiration for the one for Useful Open CbNeed during the preparation of this work. Nevertheless, we shall not merely present it as an intermediate step towards the latter—unlike all other multi type systems—but rather as a separate case study, interesting in itself.
We would also like to remark the importance of studying strong reduction in a call-by-value set-ting, both operationally and type-theoretically. This is a previous and necessary step to attaining the final goal of producing a multi type system characterizing and providing measurements for a strong and useful call-by-need reduction relation. Unfortunately, this final goal remains unachieved by the time we write these lines.
With intention to keep matters as simple as possible, all the case studies in this work shall morally follow the same structure, methodologically speaking:
We begin by defining the reduction relation and proving that it enjoys some kind of deter-minism. Next, we provide a set of predicates that characterize the normal forms of said reduction relation. This may be extremely intricate, in particular in the cases of Open CbNeed and Useful Open CbNeed.
We then move on to define the multi type system meant to characterize normalization in the reduction relation. To attain this, we must prove that the type system is sound and complete with respect to normalizing terms. Needless to say, proving this requires an ex-tremely detailed understanding of the operational aspects of the reduction relation from a type-theoretical perspective. An overview of the way in which we prove this—which is con-sistently applied to every case study—is presented in upcoming Chapter 3 (A bird’s eye view).
Turning now to the features of the multi type systems, we hope that the reader may find them quite simple. They are derived in a principled way, following an incremental approach:
The multi type system for Strong CbV is obtained almost effortlessly from the one given by Ehrhard for the weak and closed variant of CbV.
The multi type system for Open CbNeed is obtained by adding a few typing rules to the one for CbNeed.
Finally, the multi type system for Useful Open CbNeed is obtained from the one for Open CbNeed by refining the axioms. We believe this is quite remarkable, and was in fact our first intuition for understanding useful reduction from a (multi) type-theoretical perspective in the Open CbNeed setting.
Unfortunately, the same level of simplicity was not found at the rewriting-theoretical level. That is, while designing the multi type systems turned out to be relatively simple, conducting the operational studies of most of our case studies was not as easy as expected. For instance, the Open CbNeed and Useful Open CbNeed cases turned out to be extremely subtle, requiring in particular very long proofs for the characterization of their normal forms via predicates. This was somewhat surprising.
Considerations
Each one of the four case studies have two dedicated chapters, one where we study its operational aspects and another one where we study its multi type system. The distribution of contents goes as follows:
In Chapter 4 (CbN, CbV and CbNeed) we develop an operational account on the weak and closed versions of call-by-name (CbN), call-by-value (CbV) and call-by-need (CbNeed).
In Chapter 5 (Multi types for CbN, CbV and CbNeed) we analyze the multi type systems for CbN and for CbV given in the literature, and use them to derive the one for CbNeed.
In Chapter 6 (Open CbNeed) we present the Open CbNeed evaluation strategy, which extends the CbNeed one by including reduction on (possibly) open terms, and reducing on arguments.
In Chapter 7 (Multi types for Open CbNeed) we present the multi type system for the Open CbNeed evaluation strategy.
In Chapter 8 (Useful Open CbNeed) we refine the Open CbNeed evaluation strategy to make it useful.
In Chapter 9 (Multi types for Useful Open CbNeed) we present the multi type system for the Useful Open CbNeed evaluation strategy.
In Chapter 10 (Strong CbV) we present the Strong CbV evaluation strategy.
Finally, in Chapter 11 (Multi types for Strong CbV) we present the multi type system for the Strong CbV evaluation strategy.
With respect to the other chapters:
Chapter 2 (Preliminaries) gives a relatively detailed presentation of topics. Although they are probably known to the reader, the purpose of this chapter is to agree on notation and definitions.
Chapter 3 (A bird’s eye view) intends to extend the intuitions that we just gave here by incorporating some of the technical details introduced in Chapter 2 (Preliminaries). We also use Chapter 3 to show that the technical development in each of the case studies—in particular what concerns the multi type systems—follows the exact same structure, thus heightening the value of our approach.
Chapter 12 (Conclusion) reviews the results attained throughout this work, and provides a list of some future lines of research that might derive from this work.
Proofs and appendices. We have made the presentation choice of keeping explanations and technical proofs apart. Thus, Chapter 4 (CbN, CbV and CbNeed) to Chapter 11 (Multi types for Strong CbV) mostly provide definitions, analyses and examples, while Chapter 13 mostly provides proofs.
In Chapter 13 (Technical appendix) we provide all the proofs for for this work. Of course, this excludes Chapter 2 (Preliminaries), Chapter 3 (A bird’s eye view) and Chapter 12 (Conclusion). All other chapters, from Chapter 4 (CbN, CbV and CbNeed) to Chapter 11 (Multi types for Strong CbV), have numerous links to Chapter 13. Indeed, the complete technical development of each one of these chapters appears in Chapter 13 in the form of a dedicated section. In addition, every statement appearing in chapters from Chapter 4 (CbN, CbV and CbNeed) to Chapter 11 (Multi types for Strong CbV) is followed by links taking the reader back and forth Chapter 13 (Technical Appendix). Conversely, some (less important) statements only appear in Chapter 13, as they are considered to be relevant only as part of the technical development, and not for any meaningful conceptual understanding. We believe this should help the reader study a proof whenever he or she sees fit, while keeping matters as split as possible.
Table of contents :
1 Introduction
1.1 Background and objectives
1.2 Tools
1.3 Development and outcomes
1.4 Considerations
2 Preliminaries
2.1 The -calculus
2.2 The Linear Substitution Calculus
2.3 Usefulness
2.4 Multi types
3 A bird’s eye view
3.1 Properties of evaluation strategies
3.2 Properties of multi type systems
3.3 Case study: CbNeed
3.4 Case study: Open CbNeed
3.5 Case study: Useful Open CbNeed
3.6 Case study: Strong CbV
3.7 Design principles for multi type systems
4 CbN, CbV and CbNeed
4.1 Duplication and erasure
4.2 CbN = silly duplication + wise erasure
4.3 CbV = wise duplication + silly erasure
4.4 CbNeed = wise duplication + wise erasure
4.5 Erasing steps
4.6 Characterizing closed normal forms
5 Multi types for CbN, CbV and CbNeed
5.1 Different flavors of multi types
5.2 Multi type system for CbN
5.3 Multi type system for CbV
5.4 Multi type system for CbNeed
5.5 CbN and CbNeed are termination-equivalent
5.6 CbNeed is as efficient as CbV
6 Open CbNeed
6.1 The Open CbNeed evaluation strategy
6.2 Characterizing Open CbNeed-normal forms
6.3 Determinism
7 Multi types for Open CbNeed
7.1 Multi type system for Open CbNeed
7.2 Counting techniques for exponential steps
8 Useful Open CbNeed
8.1 The Useful Open CbNeed evaluation strategy
8.2 Characterizing Useful Open CbNeed-normal forms
8.3 Determinism
9 Multi types for Useful Open CbNeed
9.1 Multi type system for Useful Open CbNeed
10 Strong CbV
10.1 Variants of Open CbV
10.2 The Value Substitution Calculus
10.3 The Strong CbV strategy
11 Multi types for Strong CbV
11.1 Shrinkingness
11.2 Multi type system for Strong CbV
11.3 A semantical proof of VSC-normalization via Strong CbV
12 Conclusion
13 Technical appendix
13.1 Proofs of Chapter 4 (CbN, CbV and CbNeed)
13.2 Proofs of Chapter 5 (Multi types for CbN, CbV and CbNeed)
13.3 Proofs of Chapter 6 (Open CbNeed)
13.4 Proofs of Chapter 7 (Multi types for Open CbNeed)
13.5 Proofs of Chapter 8 (Useful Open CbNeed)
13.6 Proofs of Chapter 9 (Multi types for Useful Open CbNeed
13.7 Proofs of Chapter 10 (Strong CbV)
13.8 Proofs of Chapter 11 (Multi types for Strong CbV)
Bibliography
