A constructive proof of dependent choice in classical arithmetic via memoization
\'Etienne Miquey
TL;DR
This paper proves normalization and soundness of a calculus combining dependent types, classical logic, and memoization, advancing the understanding of constructive proofs for dependent choice.
Contribution
It introduces a sequent calculus variant of dPAω and proves its normalization using Krivine realizability, addressing complex features like dependent types and control operators.
Findings
Proved normalization and soundness of the calculus
Developed a realizability interpretation for the calculus
Extended previous work on classical realizability and dependent types
Abstract
In a recent paper, Herbelin developed dPA, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of choice functions. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type into streams ()) and of lazy evaluation with sharing (for memoizing these coinductive objects). Elaborating on previous works, we introduce in this paper a variant of dPA presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability that we developed to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
A constructive proof of dependent choice in classical arithmetic via memoization
Étienne Miquey
Équipe Gallinette, INRIA, Laboratoire des Sciences du Numérique de Nantes, France
Abstract.
In a recent paper [29], Herbelin developed dPA, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of choice functions. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type into streams ) and of lazy evaluation with sharing (for memoizing these coinductive objects).
Elaborating on previous works, we introduce in this paper a variant of dPA presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability that we developed to prove the normalization of classical call-by-need [55]. On the other hand, we benefit from dL, a classical sequent calculus with dependent types in which type safety is ensured by using delimited continuations together with a syntactic restriction [54]. By combining the techniques developed in these papers, we manage to define a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness. This paper goes over the whole process, starting from Herbelin’s calculus dPA until our introduction of its sequent calculus counterpart dLPA.
keywords:
formula with parameters
1. Introduction
1.1. The axiom of choice
The axiom of choice is certainly one of the most intriguing pieces of the foundations of mathematics. Understanding the axiomatization of a theory as an intent to give a formal and truthful representation of a given world or structure, as long as this structure only deals with finite objects it is easier to agree on what it “is” or “should be”. However, as soon as the theory involves infinite objects, this question quickly turns out to be much trickier. In particular, some undeniable properties of finite objects become much more questionable in the case of infinite sets. The axiom of choice is precisely one of these properties. Consider for instance the following problem, as presented by Russell [64, pp.125-127]:
[Imagine a] millionaire who bought a pair of socks whenever he bought a pair of boots, and never at any other time, and who had such a passion for buying both that at last he had pairs of boots and pairs of socks. The problem is: How many boots had he, and how many socks?
The cardinal defines exactly the infinite quantity of natural numbers, and in particular, since there is a bijection from to , is not increased by doubling. Hence, as suggested by Russell:
One would naturally suppose that he had twice as many boots and twice as many socks as he had pairs of each, and that therefore he had of each […].
To prove this claim, it is thus necessary and sufficient to give an enumeration of the millionaire’s boots and socks. Yet, if it is easy to enumerate the boots—take each pair one after the other, consider the left boot first then the right one— this is not possible a priori in the case of socks without assuming the possibility of making an infinite number of arbitrary choices: for each pair, one has to decide which sock to pick first.
Formally, the possibility of making these choices is expressed by the axiom of choice, which was first introduced by Zermelo in the realm of set theory [72]. Among its different formulations, its relational variant is given by:
[TABLE]
which stipulates the existence of a choice function111If we define the predicate as , it exactly says that if all the sets are non-empty, there exists a choice function: .. This axiom was shown to be independent of Zermelo-Fraenkel set theory (ZF)222Gödel proved that the theory ZF + AC is consistent, and Cohen proved the same for the theory ZF + AC [35]..
While it might be tempting to consider the axiom of choice as natural, it leads to very surprising consequences. The most striking example is certainly the Banach-Tarski paradox [6], which shows that the unit ball:
[TABLE]
in three dimensions can be disassembled into a finite number of pieces, which can then be reassembled (after translating and rotating each of the pieces) to form two disjoint copies of the ball . Nonetheless, many standard mathematical results require the axiom of choice (e.g., every vector space has a basis, the product of compact topological spaces is compact, every field has an algebraic closure) or one of its restricted variants (e.g., the axiom of dependent choice for Bolzano-Weierstrass’ theorem, countable choice to prove that every infinite set is Dedekind-infinite). Especially, many proofs in analysis relies on the definition of an adequate converging sequence, whose existence itself relies on the axiom of dependent choice.
1.2. Constructive interpretation of AC
Russell’s presentation of his paradox leads us to wonder how the millionaire should perform the choices necessary to obtain the enumeration. Regarding the axiom of choice as expressed above, this amounts to wonder how to compute the choice function whose existence is stated by the axiom.
This point of view is in line with a constructive vision of mathematics such as the one given by the Brouwer-Heyting-Kolmogorov interpretation [69]. In that settings, a proof of is defined as a function that, given a proof of constructs a proof of ; a proof of is a function that turns any into a proof of while a proof of is a pair where and is a proof of . Therefore, a proof of the premise of the relational axiom of choice (for a given relation ) has to be a function which, for any , constructs a proof of . The function then defines a valid choice function, and the axiom is easily satisfied.
While the concepts of “proof” and “function” above can be interpreted in different ways333For instance, Kleene realizability corresponds to the case where “proofs” are natural numbers and “functions” are taken as being computable functions [36]. and as such remains meta-notions, the same idea is internalized within Martin-Löf’s type theory. To this end, one of the key features of Martin-Löf’s type theory is the concept of dependent types, which allows formulas to refer to terms [48]. Notably, the existential quantification rule is defined so that a proof term of type is a pair where —the witness—is of type , while —the proof—is of type . Dually, the theory enjoys two elimination rules: one with a destructor to extract the witness, the second one with a destructor to extract the proof. This allows for a simple and constructive proof of the full axiom of choice [48]:
[TABLE]
This term is nothing more that an implementation of Brouwer-Heyting-Kolomogoroff (BHK) interpretation of the axiom of choice: given a proof of , it constructs a choice function which simply maps any to the witness of , while the proof that this function is sound w.r.t. returns the corresponding certificate.
1.3. Incompatibility with classical logic
Unsurprisingly, this proof does not scale to classical logic. Imagine indeed that we could dispose, in a type theoretic (or BHK interpretation, realizability) fashion, of a classical framework including a proof term for the axiom of choice:
[TABLE]
Consider now any undecidable predicate over a domain . Taking advantage of the exceluded middle, we can strengthen the formula (which is true for any ) into:
[TABLE]
which is provable as well in a classical framework and thus should have a proof term . Now, this has the shape of the hypothesis of the axiom of choice, so that by application of to , we should obtain a term:
[TABLE]
In particular, the term would be a function which, for any , outputs if is true, and [math] otherwise. This is absurd, since is undecidable. This informal explanation gives us a metamathematical argument on the impossibility of having a proof system which is classical as a logic, entails the axiom of choice and where proofs fully compute. Since the existence of consistent classical theories with the axiom of choice (like set theory) has been proven, the incompatibility is to be found within the constructive character of proofs.
1.4. The computational content of classical logic
In 1990, Griffin discovered that the control operator call/cc (for call with current continuation) of the Scheme programming language could be typed by Peirce’s law . As Peirce’s law is known to imply, in an intuitionistic framework, all the other forms of classical reasoning (excluded middle, reductio ad absurdum, double negation elimination, etc.), this discovery opened the way for a direct computational interpretation of classical proofs, using control operators and their ability to backtrack. Several calculi were born from this idea, such as Parigot’s -calculus [61], Barbanera and Berardi’s symmetric -calculus [7], Krivine’s -calculus [40] or Curien and Herbelin’s -calculus [15].
Notably, in order to address the incompatibility of intuitionistic realizability with classical logic, Krivine used the -calculus to develop in the middle of the 90s the theory of classical realizability [40]. Krvine realizability is a complete reformulation444As observed in several articles [60, 50], classical realizability can in fact be seen as a reformulation of Kleene’s realizability through Friedman’s -translation [22]. of the very principles of realizability to make them compatible with classical reasoning. Although it was initially introduced to interpret the proofs of classical second-order arithmetic (PA2), the theory of classical realizability can be scaled to more expressive theories such as Zermelo-Fraenkel set theory [38] or the calculus of constructions with universes [49]. Krivine realizability has shown in the past twenty years to be a very powerful framework, both as a way to build new models of set theory [42, 43, 45] and as a tool to analyze programs [33, 25, 23]; we shall use it several times in this paper to prove the correctness of different calculi.
Last but not least, Griffin’s discovery led to an important paradigmatic shift from the point of view of logic. Instead of trying to get an axiom by means of logical translations (e.g. Gödel’s negative translation for classical reasoning), and then transfer this translation to program along the Curry-Howard correspondence (e.g. continuation-passing style for negative translation), one can rather try to directly add an operator whose computational behavior is adequate with the expected axiom. Several works over the past twenty years have emphasized the fact that adding new programming primitives (and in particular side effects) to a calculus may bring new reasoning principles [39, 34, 51, 28, 32]. The present work is totally in line with this philosophy: we will show how to use a form of memoization to give a computational content to the axioms of dependent and countable choices in a framework that is compatible with classical logic. That is, we will take advantage of several computational features (namely: control operators, dependent types, streams, lazy evaluation and shared memory) to build proof terms for these axioms.
1.5. Realizing ACN and DC in presence of classical logic
As we explained earlier, the full axiom of choice and computational classical logic are a priori incompatible. In particular, extending Martin-Löf’s type theory with control operators leads to an inconsistent theory. This was observed by Herbelin [27]: starting from a sound minimal language with dependent types, he showed that the further addition of control operators allows to derive a proof of false. The main idea behind Herbelin’s paradox, which we will detail in Section 5.1, is that control operators allows to define a proof of type that will first give a wrong witness for (say 0) together with a certificate which, if it is evaluated, will backtrack to furnish the appropriate witness (i.e. ) and the usual equality proof for the equality . Yet, extracting the witness from this proof with returns [math], while extracting the certificate with reduces to the usual proof of equality (after backtracking). The paradox arises from the fact that is of type , while is convertible to [math].
The bottom line of this example is that the same proof is behaving differently in different contexts thanks to control operators, causing inconsistencies between the witness and its certificate. In 2012, Herbelin proposed a way of scaling up Martin-Löf’s proof to classical logic while preventing the previous paradox to occur. The first idea is to restrict dependent types to the fragment of negative-elimination-free proofs (nef) which, intuitively, only contains constructive proofs behaving as values555For instance, in the previous example is not nef, and the restriction thus precludes us from writing or .. The second idea is to share the computation of the choice function, in order to avoid inconsistencies coming from classical proofs behaving differently in different places. To this purpose, Herbelin considered the cases of choice functions whose domain is the set of natural numbers (i.e., the axioms of countable and dependent choices) and proposed to memoize their computations. While the presence of control operators induces the possibility for a proof of type to furnish different for a same depending on the evaluation context, the memoization ensures that it will be computed at most once. Technically, the key is to encode functions of type by streams that are lazily evaluated, that is to say infinite sequences represented coinductively and whose components are evaluated only if necessary.
This allows us to internalize into a formal system the realizability approach [9, 19] as a direct proofs-as-programs interpretation. The resulting calculus, called dPA, thus contains dependent types (for the constructive part of choices), control operators (for classical logic), coinductive objects (to define streams) and a lazy evaluation strategy with shared memory for these objects.
1.6. Normalization of dPAω
In [29], the property of normalization (on which relies the one of consistency) was only conjectured, and the proof sketch that was given turned out to be difficult to formalize properly. Our first attempt to prove the normalization of dPA was to derive a continuation-passing style translation (CPS)666Indeed, removing the control part of dPA (which CPS translations do through an encoding) would leave us with an intuitionistic system whose normalization would be easier to prove (in particular, it would be a subsystem of the Calculus of Inductive Constructions)., but translations appeared to be hard to obtain for dPA as such. In addition to the difficulties caused by control operators and co-fixpoints, dPA reduction system is defined in a natural deduction fashion, with contextual rules involving meta-contexts of arbitrary depth. This kind of rules are particularly difficult to faithfully translate through a CPS.
Rather than directly proving the normalization of dPA, we choose to first give an alternative presentation of the system under the shape of a sequent calculus, which we call dLPA. Indeed, sequent calculus presentations of a calculus usually provides good intermediate steps for CPS translations [56, 57, 18] since they enforce a decomposition of the reduction system into finer-grained rules. To this aim, we first handled separately the difficulties peculiar to the definition of such a calculus: on the one hand, we proved with Herbelin the normalization of a calculus with control operators and lazy evaluation [55]; on the other hand, we defined a classical sequent calculus with dependent types [54]. By combining the techniques developed in these frameworks, we finally managed to define dLPA, which we present here and prove to be sound and normalizing.
In each case, we were guided by a methodology first described by Danvy, who highlighted what he called the unity of semantic artifacts [16]: for a given notion of operational semantics, there is a calculus, an abstract machine, and a continuation-passing style translation that correspond exactly with one another. Therefore, from any one of these semantic artifacts, the others may be systematically derived. We extend this observation by showing how it can be used to ease the definition of a realizability interpretation à la Krivine, which we actually do in each case to prove the normalization and consistency of the considered calculi.
1.7. Outline of the paper
In this paper, we describe the complete path from Herbelin’s conjecture [29] to the normalization proof of dLPA in [53] (of which this paper is an extended version). This article will thus cover and summarize a significant amount of different papers authored by Herbelin and myself during the whole process [29, 3, 54, 55, 53].
In details, we will start in Section 2.2 by presenting the main ingredients of Herbelin’s dPA calculus, and the intuitions underlying the proof terms for the axioms of countable and dependent choices. In Section 3, we will recap the main ideas of the Curien-Herbelin’s -calculus [15], the sequent calculus on which we will base all the calculi developed afterwards, and in particular dLPA. We shall also take advantage of this section to illustrate Danvy’s
methodology on the call-by-name -calculus in order to obtain a continuation-passing style translation and a Krivine realizability interpretation. We then present in Section 4 the -calculus, a lazy classical sequent calculus, which was originally defined by Ariola et al. using Danvy’s method of semantic artifacts [3]. After summarizing the successive steps leading to the definition of the -calculus, we will recall the type system and realizability interpretation we developed together with Herbelin in order to prove its normalization [55]. In Section 5, we will present dL, a classical sequent calculus with dependent types [54]. In particular, we will explain how the seek of a dependently typed continuation-passing style unveiled the need for using delimited continuations and the restriction to the nef fragment. Finally, we shall gather these two systems to define dLPA in Section 6, whose normalization is proved by means of a realizability interpretation combining the interpretations for dL and the -calculus.
Along the way, we will use the unity of semantic artifacts for each of the calculi aforementioned. While we would like to avoid boring the reader stiff with recalling the full process each time, we still intend to outline it in each case. Indeed, we believe that the core ideas used in our realizability interpretation for dLPA directly stem from the subcases of -calculus and dL, and that they are easier to understand in these specific contexts which only contains the core ingredients. We hope that this will help the reader to understand the different technicalities induced by the expressiveness of dLPA before its introduction in Section 6.
2. A proof of dependent choice compatible with classical logic
We shall begin by presenting dPA, the proof system that was introduced by Herbelin as a mean to give a computational content to the axiom of choice in a classical setting [29]. As explained in the introduction, the calculus is a fine adaptation of Martin-Löf proof which circumvents the different difficulties caused by classical logic. Rather than restating dPA in full details, for which we refer the reader to [29], let us describe informally the rationale guiding its definition and the properties that it verifies. We shall then dwell on the missing piece in the puzzle that led us to this work, namely the normalization property, and outline our approach to prove it.
2.1. A constructive proof of dependent choices compatible with classical logic
The dependent sum type of Martin-Löf’s type theory provides a strong existential elimination, which allows us to prove the full axiom of choice. The proof is simple and constructive:
[TABLE]
To scale up this proof to classical logic, the first idea in Herbelin’s work [29] is to restrict the dependent sum type to a fragment of his system which is called negative-elimination-free (nef). This fragment contains slightly more proofs than just values, but is still computationally compatible with classical logic. We shall see in Section 5.3 how this restriction naturally appears when trying to define a dependently-typed continuation-passing style translation.
The second idea is to represent a countable universal quantification as an infinite conjunction. This allows us to internalize into a formal system the realizability approach of Berardi, Bezem and Coquand or Escardi and Oliva [9, 19] as a direct proofs-as-programs interpretation. Informally, let us imagine that given a proof , we could create the sequence and select its -element with some function nth. Then one might wish that:
[TABLE]
could stand for a proof for .
However, even if we were effectively able to build such a term, might still contain some classical proofs. Therefore, two copies of might end up behaving differently according to the contexts in which they are executed, and then return two different witnesses. This problem could be fixed by using a shared version of , say:
[TABLE]
It only remains to formalize the intuition of . This is done by means of a coinductive fixpoint operator. We write for the co-fixpoint operator binding the variables and , where is a proof and a term. Intuitively, such an operator is intended to reduce according to the rule:
[TABLE]
This is to be compared with the usual inductive fixpoint operator which we write (which binds the variables and ) and which reduces as follows:
[TABLE]
The presence of coinductive fixpoints allows us to consider the term , which implements a stream eventually producing the (informal) infinite sequence . Indeed, this proof term reduces as follows:
[TABLE]
This allows for the following definition of a proof term for the axiom of countable choice:
[TABLE]
Whereas the construction suggests a call-by-value discipline, we cannot afford to pre-evaluate each component of the stream. In turn, this imposes a lazy call-by-value evaluation discipline for coinductive objects. However, this still might be responsible for some non-terminating reductions, all the more as classical proofs may backtrack.
If we analyze what this construction does at the level of types777We delay the formal introduction of a type system and the given of the typing derivation for to Section 6.5., in first approximation it turns a proof () of the formula (with in that case) into a proof (the stream ) of the (informal) infinite conjunction . Formally, a proof is an inhabitant of a coinductive formula, written (where is a term and which binds the variables and ). The typing rule is given by:
[TABLE]
with the side condition that can only occurs in positive position in . Coinductive formulas are defined with a reduction rules which is very similar to the rule for the co-fixpoint:
[TABLE]
In particular, the term is thus an inhabitant of a coinductively defined (infinite) conjunction, written . This formula indeed reduces accordingly to the reduction of the stream:
[TABLE]
More generally, at the level of formulas, the key is to identify the formula and a suitable law to turn a proof of into the conjunction . In the case of the axiom of countable choice, this law is simply this identity. As for the axiom of dependent choice, the law we are looking for is precisely the choice function. We can thus use the same trick to define a proof term for the axiom of dependent choice:
[TABLE]
The stream we actually construct corresponds again to a coinductive formula, defined here by and which ultimately unfolds into888As we shall explain afterwards, is a non-dependent eliminator for the existential type, it destructs a proof of as in and reduces as follows: .:
[TABLE]
Given a proof and a term , we can define a stream corresponding to this coinductive formula by . This term reduces as expected:
[TABLE]
where . From there, it is almost direct to extract the choice function (which maps any to ) and the corresponding certificate that . In practice, it essentially amounts to define the adequate nth function. We will give a complete definition of the proof term for the axiom of dependent choice in Section 6.5.
2.2. An overview of dPA
Formally, the calculus dPA is a proof system for the language of classical arithmetic in finites types (abbreviated PAω), where the ‘d’ stands for “dependent”. It adopts a stratified presentation of dependent types, by syntactically distinguishing terms— that represent mathematical objects—from proof terms—that represent mathematical proofs. In other words, we syntactically separate the categories corresponding to witnesses and proofs in dependent sum types. Finite types and formulas are thus separated as well, corresponding to the following syntax:
[TABLE]
Terms, denoted by are meant to represent arithmetical objects, their syntax thus includes:
- •
a term [math] and a successor ;
- •
an operator for recursion, which binds the variables and : where is the term on which the recursion is performed, is the term for the case ans is the term for case ;
- •
-abstraction to define functions and terms application ;
- •
a constructor to extract the witness of a dependent sum.
As for proofs, denoted by , they contain:
- •
a proof term which is the proof of atomic equalities ;
- •
which eliminates an equality proof to get a proof of from a proof ;
- •
pairs to prove logical conjunctions and destructors of pairs (which binds the variables and in );
- •
injections for the logical disjunction and pattern-matching which binds the variables in and in ;
- •
pairs where is a term and a proof for the dependent sum type;
- •
which allows us to extract the certificate of a dependent pair;
- •
non-dependent destructors which binds the variables and in ;
- •
abstractions over terms for the universal quantification and applications ;
- •
(possibly) dependent abstractions over proofs and applications ;
- •
a construction , which binds the variable in and which allows for sharing;
- •
operators and that we already described for inductive and coinductive reasoning;
- •
control operators (which binds the variable in ) and (where is a variable and a proof)
- •
where is intended to be a proof of false.
This results in the following syntax:
[TABLE]
The problem of degeneracy caused by the conjoint presence of classical proofs and dependent types is solved by enforcing a compartmentalization between them. Dependent types are restricted to the set of negative-elimination-free proofs (nef), which are a generalization of values preventing backtracking evaluations from occuring by excluding expressions of the form , , , or which are outside the body of a or . Syntactically, they are defined by:
[TABLE]
This allows us to restrict typing rules involving dependencies, notably the rules for or :
[TABLE]
About reductions, let us simply highlight the fact that they globally follow a call-by-value discipline, for instance in this sample:
[TABLE]
except for co-fixpoints which are lazily evaluated:
[TABLE]
In the previous rules, the first one expresses the fact that evaluation of co-fixpoints under contexts are momentarily delayed. The second rules precisely corresponds to a context where the co-fixpoint is linked to a variable whose value is needed, a step of unfolding is then performed. The full type system, as well as the complete set of reduction rules, are given in [29], and will be restated with a different presentation in Section 6. In the same paper, some important properties of the calculus are given. In particular, dPA verifies the property of subject reduction, and provided it is normalizing, there is no proof of false.
Theorem \thethm (Subject reduction).
If and , then .
Proof (sketch).
By induction on the derivation of , see [29]. ∎
Theorem \thethm (Conservativity).
Provided dPA is normalizing, if is ----free, and \vdash_{\textrm{dPA\textsuperscript{\omega}}}p:A, there is a value such that .
Proof (sketch).
Considering a closed proof of , can be reduced. By analysis of the different possible cases, it can be found a closed value of type . Then using the fact that is a ----free formula, does not contain any subexpression of the form or , by extension it does not contain either any occurrence of , or and is thus a proof of already in . ∎
Theorem \thethm (Consistency).
Provided dPA is normalizing, it is consistent, that is: .
Proof.
The formula is a particular case of ----free formula, thus the existence of a proof of false in dPA would imply the existence of a contradiction already in , which is absurd. ∎
The last two results rely on the property of normalization. Unfortunately, the proof sketch that is given in [29] to support the claim that dPA normalizes turns out to be hard to formalize properly. Since, moreover, dPA contains both control operators (allowing for backtrack) and co-fixpoints (allowing infinite objects, like streams), which can be combined and interleaved, we should be very suspicious a priori about this property. Anyhow, the proof sketch from [29] relies on metamathematical arguments while we are rather interested in a fine analysis of the interactions between the different computational features of dPA. Indeed, our goal is not limited to adding an axiom to the theory or to finding a way to realize it. In turns, we are looking for an adapted calculus with an appropriate operational semantics: such an approach mixing syntax and semantics let us hope to develop a better calculus (from a programming point of view) and to get a better understanding of the proof arguments (from the point of view of logic). The proposal of Herbelin is already in line with this philosophy: as we saw, the proofs terms for and DC in dPA are build using usual programming primitives rather than one monolithic extra-instruction.
2.3. Toward a proof of normalization for dPA
This paper recounts a long process devoted to the search for a proof of normalization for dPA by means of a realizability interpretation or by a continuation-passing-style translation. Aside from the very result of normalization, such an approach is of interest in itself in that, as advocated earlier, it requires and provides us with a fine understanding of the computational features of dPA. In particular, the difficulty in obtaining a continuation-passing style translation directly for dPA highlights several problems. The first one is the simultaneous presence of control operators and of lazily evaluated streams, thus allowing to define programs that may backtrack and require the evaluation of of potentially infinit object. program that The second is the presence of dependent types. Indeed, dependent types (and in particular the dependent sum) are known to be incompatible with a continuation-passing style translation [8]. Last, the reduction system is defined in a natural-deduction style with contextual rules (as in the rule to reduce proofs of the shape ) where the contexts involved can be of arbitrary depth. This kind of rules are, in general and especially in this case, very difficult to translate faithfully through a continuation-passing style translation.
All in all, there are several difficulties in getting a direct proof of normalization for dPA. Hence, we shall study them separately before combining the solutions to each subproblem in order to attack the main problem. Roughly, our strategy consists of two steps:
- (1)
reduce dPA to an equivalent presentation in a sequent calculus fashion, 2. (2)
use the methodology of semantic artifacts to define a CPS or a realizability interpretation.
Defining a sequent calculus presentation of a calculus is indeed known to be a good intermediate step for the definition of continuation-passing style translations [56, 57, 18]. In our case it forces to us to rephrase the contextual rules into abstract-machine like reduction rules which only depend of the top-level command, thus solving the last difficulty evoked above. This presentation should of course verify at least the property of subject reduction and its reduction system should mimic the one of dPA. Schematically, this corresponds to the following roadmap where question marks indicate what is to be done:
[TABLE]
[TABLE]
[TABLE]
?Target language? Subject reduction ✓Subject reduction ?Normalization ✓CPS?
To be fair, this approach is idealistic. In particular, we will not formally define an embedding for the first arrow, since we are not interested in dPA for itself, but rather in the computational content of the proofs for countable and dependent choice. Hence, we will content ourself with a sequent calculus presentation of dPA which allows for similar proof terms, which we call dLPA, without bothering to prove that the reduction systems are strictly equivalent (see Section 6.5). As for the second arrow, as we shall explain in the next sections, the search for a continuation-passing style translation or a realizability interpretation can coincide for a large part. We shall thus apply the methodology of semantic artifacts and in the end, choose the easiest possibility (in that case, defining a realizability interpretation).
From this roadmap actually arises two different subproblems that are already of interest in themselves. Forgetting about the general context of dPA, we shall first wonder whether these easier questions have an answer:
- (1)
Can we prove the normalization of a call-by-need calculus with control operators? Can we define a Krivine realizability interpretation of such a calculus? 2. (2)
Is it possible to define a (classical) sequent calculus with a form of dependent types? If so, would it be compatible with a typed continuation-passing style translation?
We shall treat the first question in Section 4 and the second one in Section 5, before combining the ideas of both systems to define dLPA in Section 6. As explained in Section 1.7, in each case we will define variants of Curien-Herbelin’s -calculus, so that we shall begin with presenting the latter. We will take advantage of this introduction to illustrate our global methodology (that is, refining the system into an abstract-machine like calculus in order to get a continuation-passing style translation or a realizability interpretation that allows us t o prove normalization and soundness).
3. The -calculus and Danvy’s semantics artifacts
3.1. Continuation-passing style translation and Danvy’s methodology
The terminology of continuation-passing style (CPS) was first introduced in 1975 by Sussman and Steele in a technical report about the Scheme programming language [68]. In this report, after giving the usual recursive definition of the factorial, they explained how the same computation could be driven differently:
“It is always possible, if we are willing to specify explicitly what to do with the answer, to perform any calculation in this way: rather than reducing to its value, it reduces to an application of a continuation to its value. That is, in this continuation-passing programming style, a function always “returns” its result by “sending” it to another function. This is the key idea.”
Interestingly, by making explicit the order in which reduction steps are computed, continuation-passing style translations indirectly specify an operational semantics for the translated calculus. In particular, different evaluation strategies for a calculus correspond to different continuation-passing style translations. This was for instance studied by Plotkin for the call-by-name and call-by-value strategies within the -calculus [62].
Continuations and their computational benefits have been deeply studied since then, and there exists a wide literature on continuation-passing style translations. Among other things, these translations have been used to ease the definitions of compilers [2, 21], one of their interests being that they make explicit the flow of control. As such, continuation-passing style translations de facto provide us with an operational semantics for control operators, as observed in [20] for the operator. Continuation-passing style translations therefore bring an indirect computational interpretation of classical logic. This observation can be strengthened on a purely logical aspect by considering the logical translations they induce at the level of types: the translation of types through a CPS mostly amounts to a negative translation allowing to embed classical logic into intuitionistic logic [24, 58].
In addition to the operational semantics, continuation-passing style translations allow to benefit from properties already proved for the target calculus. For instance, we will see how to define a translation from the simply-typed call-by-name -calculus to the simply-typed -calculus along which the properties of normalization and soundness can be transfered. In details, these translations will preserve reduction, in that a reduction step in the source language gives rise to a step (or more) in the target language:
[TABLE]
We say that a translation is typed when it comes with a translation from types of the source language to types of the target language, such that a typed proof in the source language is translated into a typed proof of the target language:
[TABLE]
Last, we are interested in translations mapping the type into a type which is not inhabited:
[TABLE]
Assuming that the previous properties hold, one automatically gets:
Proposition \thethm (Benefits of the translation).
If the target language of the translation is sound and normalizing, and if besides the equations (1), (2) and (3) hold, then:
- (1)
If normalizes, then normalizes 2. (2)
If is typed, then normalizes 3. (3)
The source language is sound, i.e. there is no proof
Proof.
- (1)
By contrapositive, if does not normalizes, then according to equation (1) neither does . 2. (2)
If is typed, then is also typed by(2), and thus normalizes. Using the first item, normalizes. 3. (3)
By reductio ad absurdum, direct consequence of (3).∎
Continuation-passing style translations are thus a powerful tool both on the computational and the logical facets of the proofs-as-programs correspondence. We shall illustrate afterwards its use to prove normalization and soundness of the call-by-name -calculus. Rather than giving directly the appropriate definitions, we would like to insist on a convenient methodology to obtain CPS translations as well as realizability interpretations (which are deeply connected). This methodology is directly inspired from Danvy et al. method to derive hygienic semantics artifacts for a call-by-need calculus [17]. Reframed in our setting, it essentially consists in the successive definitions of:
- (1)
an operational semantics, 2. (2)
a small-step calculus or abstract machine, 3. (3)
a continuation-passing style translation, 4. (3’)
a realizability model.
The first step is nothing more than the usual definition of a reduction system. The second step consists in refining the reduction system to obtain small-step reduction rules (as opposed to big-step ones), that are finer-grained reduction steps. These steps should be as atomic as possible, and in particular, they should correspond to an abstract machine in which the sole analysis of the term (or the context) should determine the reduction to perform. Such a machine is called in context-free form [17]. If so, the definition of a CPS translation is almost straightforward, as well as the realizability interpretation. Let us now illustrate this methodology on the call-by-name -calculi.
3.2. A short primer to the -calculus
We recall here the spirit of the -calculus, for further details and references please refer to the original article [15]. The key notion of the -calculus is the notion of command. A command {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle} can be understood as a state of an abstract machine, representing the evaluation of a proof (the program) against a co-proof (the stack) that we call context. The syntax and reduction rules (parameterized over a subset of proofs and a subset of evaluation contexts ) are given in Figure 1, where can be read as a context . The operator comes from Parigot’s -calculus [61], binds a context to a context variable in the same way that binds a proof to some proof variable .
The -calculus can be seen as a proof-as-program correspondence between sequent calculus and abstract machines. Right introduction rules correspond to typing rules for proofs, while left introduction are seen as typing rules for evaluation contexts. In contrast with Gentzen’s original presentation of sequent calculus, the type system of the -calculus explicitly identifies at any time which formula is being worked on. In a nutshell, this presentation distinguishes between three kinds of sequents:
- (1)
sequents of the form for typing proofs, where the focus is put on the (right) formula ; 2. (2)
sequents of the form for typing contexts, where the focus is put on the (left) formula ; 3. (3)
sequents of the form for typing commands, where no focus is set.
In a right (resp. left) sequent , the singled out formula999This formula is often referred to as the formula in the stoup, a terminology due to Girard. reads as the conclusion “where the proof shall continue” (resp. hypothesis “where it happened before”).
For example, the left introduction rule of implication can be seen as a typing rule for pushing an element on a stack leading to the new stack :
[TABLE]
As for the reduction rules, we can see that there is a critical pair if and are not restricted enough:
[TABLE]
The difference between call-by-name and call-by-value can be characterized by how this critical pair101010Observe that this critical pair can be also interpreted in terms of non-determinism. Indeed, we can define a fork instruction by {\pitchfork}\triangleq\lambda ab.\mu\alpha.{\mbox{\langle}}{\mu\_{\mbox{\langle}}{a}{|\!|}{\alpha}\mbox{\rangle}}{|\!|}{{\tilde{\mu}}\_.{\mbox{\langle}}{b}{|\!|}{\alpha}\mbox{\rangle}}\mbox{\rangle}, which verifies indeed that {\mbox{\langle}}{{\pitchfork}}{|\!|}{p_{0}\cdot p_{1}\cdot e}\mbox{\rangle}\rightarrow{\mbox{\langle}}{p_{0}}{|\!|}{e}\mbox{\rangle} and {\mbox{\langle}}{{\pitchfork}}{|\!|}{p_{0}\cdot p_{1}\cdot e}\mbox{\rangle}\rightarrow{\mbox{\langle}}{p_{1}}{|\!|}{e}\mbox{\rangle}. is solved, by defining and such that the two rules do not overlap. Defining the subcategories of values and co-values by:
[TABLE]
the call-by-name evaluation strategy amounts to the case where Proofs and Co-values, while call-by-value corresponds to Values and Contexts. Both strategies can also be characterized through different CPS translations [15, Section 8].
Remark \thethm (Application).
The reader unfamiliar with the -calculus might be puzzled by the absence of a syntactic construction for the application of proof terms. Intuitively, the usual application of the -calculus is recovered by considering the command it reduces to in an abstract machine, that is, given an evaluation context , the application of the proof to the stack of the shape 111111To pursue the analogy with the -calculus, the rest of the stack can be viewed as a context surrounding the application , the command {\mbox{\langle}}{p}{|\!|}{q\cdot e}\mbox{\rangle} thus being identified with the term . Similarly, the whole stack can be seen as the context , whence the terminology.:
[TABLE]
The usual application can thus be obtained by solving the previous equation, that is through the following shorthand:
[TABLE]
Finally, it is worth noting that the binder is a control operator, since it allows for catching evaluation contexts and backtracking further in the execution. This is the key ingredient that makes the -calculus a proof system for classical logic. To illustrate this, let us draw the analogy with the call/cc operator of Krivine’s -calculus [40]. Let us define the following proof terms:
[TABLE]
The proof can be understood as a proof term where the context has been encapsulated. As expected, call/cc is a proof for Peirce’s law (see Figure 2), which is known to imply other forms of classical reasoning (e.g., the law of excluded middle, the double negation elimination).
Let us observe the behavior of call/cc (in call-by-name evaluation strategy, as in Krivine -calculus): in front of a context of the shape with of type , it will catch the context thanks to the binder and reduce as follows:
[TABLE]
We notice that the proof term {\bm{k}}_{e}=\lambda a^{\prime}.\mu\beta.{\mbox{\langle}}{a^{\prime}}{|\!|}{e}\mbox{\rangle} on top of the stack (which, if was of type , is of type , see Figure 2) contains a second binder . In front of a stack , this binder will now catch the context and replace it by the former context :
[TABLE]
This computational behavior corresponds exactly to the usual reduction rule for call/cc in the Krivine machine [40]:
[TABLE]
3.3. Small-step abstract machine
Following Danvy’s methodology, the next step towards the definition of continuation-passing style translation consists in refining the reduction rules to obtain context-free reduction rules. We recall here the (big-step) reduction rules of the call-by-name -calculus, where the operator gets the priority over the operator:
[TABLE]
As such, these rules define an abstract machine which is not in context-free since to reduce a command one need to analyze simultaneously the term and the context.
To alleviate this ambiguity, we refine the reduction system into small-step rules always specifying which part of the command is being analyzed. If we examine the big-step rules, the only case where the knowledge of only one side suffices is when the context is of the form , which has the absolute priority. Therefore, we can start our analysis of a command by looking at its left-hand side. If it is a , we reduce it, otherwise, we can look at the right-hand side. Now, if the term is of the shape , it should be reduced, otherwise, we can analyze the left-hand side again. The only case left is when the context is a stack and the term is a function , in which case the command reduces.
The former case suggests two things: first, that the reduction should proceed by alternating examination of the left-hand and the right-hand side of commands. Second, that there is a descent in the syntax from the most general level (context ) to the most specific one (values121212Observe that values usually include variables, but here we rather consider them in the category . This is due to the fact that the operator catches proofs at level and variables are hence intended to be substituted by proofs at this level. Through the CPS, we will see that we actually need values to be considered at level as they are indeed substituted by proofs translated at this level. ), passing by and in the middle:
[TABLE]
So as to stick to this intuition, we denote commands with the level of syntax we are examining (), and define a new set of reduction rules which are of two kinds: computational steps, which reflect the former reduction steps, and administrative steps, which organize the descent in the syntax. For each level in the syntax, we define one rule for each possible construction. For instance, at level , there is one rule if the context is of the shape , and one rule if it is of shape . This results in the following set of small-step reduction rules:
[TABLE]
where the last two rules could be compressed in one rule:
[TABLE]
Note that there is no rule for variables and co-variables, since they block the reduction. It is obvious that theses rules are indeed a decomposition of the previous ones, in the sense that if are two commands such that c\mathrel{\mathop{\rightarrow}\limits^{\vbox to0.0pt{\kern-2.0pt\hbox{\scriptsize1}\vss}}}c^{\prime}, then there exists such that c\mathrel{\mathop{\rightsquigarrow}\limits^{\vbox to0.0pt{\kern-2.0pt\hbox{\scriptsizen}\vss}}}c^{\prime}.
The previous subdivision of the syntax and reductions also suggests a fine-grained type system, where sequents are annotated with the adequate syntactic categories (see Figure 3). While this does not bring any benefit when building typing derivations (when collapsed at level and , this type system is exactly the original one), it has the advantage of splitting the rules in more atomic ones which are closer from the reduction system. Hence it will be easier to prove that the CPS translation is typed using these rules as induction bricks.
3.4. Continuation-passing style translation
3.4.1. Translation of terms
Once we have an abstract-machine in context-free form at hands, the corresponding continuation-passing style translation is straightforward. It suffices to start from the higher level in the descent (here ) and to define a translation for each level which, for each element of the syntax, simply describe the corresponding small-step rule. In the current case, this leads to the following definition:
[TABLE]
where administrative reductions peculiar to the translation (like continuation-passing) are compressed, and where \llbracket{\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}\rrbracket_{c}\triangleq\llbracket e\rrbracket_{e}\,\llbracket p\rrbracket_{p}. The expanded version is simply:
[TABLE]
This induces a translation of commands at each level of the translation:
[TABLE]
which is easy to prove correct with respect to computation, since the translation is defined from the reduction rules. We first prove that substitution is sound through the translation, and then prove that the whole translation preserves the reduction.
Lemma \thethm.
For any variable (co-variable ) and any proof (co-value ), the following holds for any command :
[TABLE]
The same holds for substitution within proofs and contexts.
Proof.
Easy induction on the syntax of commands, proofs and contexts, the key cases corresponding to (co-)variables:
[TABLE]
∎
Proposition \thethm.
For all levels of , and any commands , if c_{\iota}\mathrel{\mathop{\rightsquigarrow}\limits^{\vbox to0.0pt{\kern-2.0pt\hbox{\scriptsize1}\vss}}}c^{\prime}_{o}, then \llbracket c\rrbracket_{c}^{\iota}\mathrel{\mathop{\longrightarrow_{\beta}}\limits^{\vbox to0.0pt{\kern-2.0pt\hbox{\scriptsize+\leavevmode\nobreak\ \leavevmode\nobreak\ }\vss}}}\llbracket c^{\prime}\rrbracket_{c}^{o}.
Proof.
The proof is an easy induction on the reduction . Administrative reductions are trivial, the cases for and correspond to the previous lemma, which leaves us with the case for :
[TABLE]
∎
3.4.2. Translation of types
The computational translation naturally induces a translation on types, which follows the same descent in the syntax:
[TABLE]
and where we take as return type for continuations. This extends naturally to typing contexts, where the translation of is defined at level while is translated at level :
[TABLE]
As we did not include any constant of atomic types, the choice for the translation of atomic types is somehow arbitrary, and corresponds to the idea that a constant would be translated into . We could also have translated atomic types at level , with constants translated as themselves. In any case, the translation of proofs, contexts and commands is well-typed:
Proposition \thethm.
For any contexts and , we have
- (1)
if then 2. (2)
if then 3. (3)
if then
Proof.
The proof is done by induction over the typing derivation. We can refine the statement by using the type system presented in Figure 3, and proving two additional statements: if then (and similarly for ). We only give two cases, other cases are easier or very similar.
• Case .
If c={\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle} is a command typed under the hypotheses :
[TABLE]
then by induction hypotheses for and , we have that and that , thus we deduce that .
• Case .
If has type :
[TABLE]
then by induction hypothesis, we get that . By definition, we have , which we can type:
[TABLE]
∎
Up to this point, we already proved enough to obtain the normalization of the -calculus for the operational semantics considered:
Theorem \thethm (Normalization).
Typed commands of the simply typed call-by-name -calculus are normalizing.
Proof.
By applying the generic result for translations (Section 3.1) since the required conditions are satisfied: the simply-typed -calculus is normalizing and Sections 3.4.1 and 3.4.2 correspond exactly to Equations (5.1) and (5.2). ∎
It only remains to prove that there is no term of the type to ensure the soundness of the -calculus.
Proposition \thethm.
There is no term in the simply typed -calculus such that .
Proof.
By definition, . Since is of type , if there was such a term , then we would obtain , which is absurd. ∎
Theorem \thethm.
There is no proof (in the simply typed call-by-name -calculus) such that \leavevmode\nobreak\ \vdash p:\bot\mid\leavevmode\nobreak\.
Proof.
Simple application of Section 3.1. ∎
3.5. Krivine classical realizability
We shall present in this section a realizability interpretation à la Krivine for the call-by-name -calculus. In a nutshell131313For a more detailed introduction to the topic, we refer the reader to Krivine introductory paper [40] or Rieg’s Ph.D. thesis [63]., Krivine realizability associates to each type a set of terms whose execution is guided by the structure of . These terms are the ones usually called realizers in Krivine’s classical realizability. Their definition is in fact indirect, that is from a set of execution contexts that are intended to challenge the truth of . Intuitively, the set —which we shall call the falsity value of —can be understood as the set of all possible counter-arguments to the formula . In this framework, a program realizes the formula —i.e. belongs to the truth value —if and only if it is able to defeat all the attempts to refute using a context in . Realizability interpretations are thus parameterized by a set of “correct” computations, called a pole. The choice of this set is central when studying the models induced by classical realizability, but in what follows we will mainly pay attention to the particular pole of terminating computations141414As such, the proof of normalization that this interpretation provides is also very close to a proof by reducibility (see for instance the proof of normalization for system presented in [37, 3.2]).. The central piece of the interpretation, called the adequacy lemma, consists in proving that typed terms belong to the corresponding sets of realizers, and are thus normalizing.
3.5.1. Extension to second-order
As Krivine classical realizability is naturally suited for a second-order setting, we shall first extend the type system to second-order logic. As we will see, the adequacy of the typing rules for universal quantification almost comes for free. However, we could also have sticked to the simple-typed setting, whose interpretation would have required to explicitly interpret each atomic type by a falsity value. We give the usual typing rules à la Curry for first- and second-order universal quantifications in the framework of the -calculus. Note that in the call-by-name setting, these rules are not restricted and defined at the highest levels of the hierarchy ( for context, for proofs).
[TABLE]
3.5.2. Realizability interpretation
We shall now present the realizability interpretation for the call-by-name -calculus151515As shown in Section 3.2, the call-by-name evaluation strategy allows to fully embed the -calculus. It is no surprise that the respective realizability interpretations for these calculi are very close. The major difference lies in the presence of the operator which has no equivalent in the -calculus, and which will force us to add a level in the interpretation.. Rather than directly stating the definition of the interpretation, we wish to attract the reader attention to the fact that this definition is again a consequence of the small-steps operational semantics. Indeed, we are intuitively looking for sets of proofs (truth values) and set of contexts (falsity values) which are “well-behaved” against their respective opponents. That is, given a formula , we are looking for players for which compute “correctly” in front of any contexts opposed to . If we take a closer look at the definition of the context-free abstract machine (cf. Section 3.3), we see that the four levels , , , are precisely defined as sets of objects computing “correctly” in front of any object in the previous category: for instance, proofs in are defined together with their reductions in front of any context in . This was already reflected in the continuation-passing style translation. This suggests a four-level definition of the realizability interpretation, which we compact in three levels as the lowest level can easily be inlined at level (this was already the case in the small-step operational semantics and we could have done it also for the CPS).
As is usual in Krivine realizability, the interpretation uses the standard model for the interpretation of first-order expressions and is parameterized by a pole :
Definition \thethm (Pole).
A pole is any subset of commands which is closed by anti-reduction, that is for all commands , if and , then .
We try to stick as much as possible to the notations and definitions of Krivine realizability [40]. In particular, we define (the base set for falsity values) as the set of all co-values: . In order to interpret second-order variables that occur in a given formula , it is convenient to enrich the language of PA2 with a new predicate symbol of arity for every falsity value function of arity , that is, for every function that associates a falsity value to every -tuple . A formula of the language enriched with the predicate symbols is then called a . Formally, this corresponds to the formulas defined by:
[TABLE]
where are first-order expressions which we will interpret in the standard model .
The interpretation of formulas with parameters is defined by induction on the structure of formulas:
[TABLE]
This definition exactly matches Krivine’s interpretation for the -calculus, considering that the “extra” level of interpretation is hidden in the latter, since all stacks are co-values. The expected monotonicity properties are satisfied:
Proposition \thethm (Monotonicity).
For any formula , the following hold:
- (1)
** 2. (2)
** 3. (3)
** 4. (4)
** 5. (5)
** 6. (6)
**
Proof.
These properties actually hold for arbitrary sets and orthogonality relation . Facts 1 and 2 are simply the usual properties of bi-orthogonal sets: and . Facts 3 and 4 are the usual equality . Facts 5 and 6 are the inclusion . ∎
In order to state the central lemma, we need to introduce a few more technical concepts. A valuation is defined as a function which associates a natural number to every first-order variable and a falsity value function to every second-order variable of arity . A substitution, written , is a function mapping variables to closed proofs (written ) and co-variables to co-values (written ). We denote by (resp. ) the closed formula (resp. proofs, context,…) where all variables are substituted by their values through .
Given two closed left and right contexts , we say that a substitution realizes , which we write , if for any , and if for any , . We are now equipped to prove the adequacy of the typing rules for the (call-by-name) -calculus with respect to the realizability interpretation we defined.
Proposition \thethm (Adequacy).
Let be typing contexts, be any valuation and be a substitution such that , then
- (1)
if , then 2. (2)
if , then 3. (3)
if , then
Proof.
By mutual induction over the typing derivation.
• Case .
We are in the following situation:
[TABLE]
By induction, we have and , thus {\mbox{\langle}}{p[\sigma]}{|\!|}{e[\sigma]}\mbox{\rangle}\in{\bot\!\!\!\bot}.
• Case .
We are in the following situation:
[TABLE]
Since , we deduce that .
• Case .
We are in the following situation:
[TABLE]
Since , we deduce that .
• Case .
We are in the following situation:
[TABLE]
Let be any context in , then . By induction, we can deduce that . By definition,
[TABLE]
thus we can conclude by anti-reduction.
• Case .
We are in the following situation:
[TABLE]
Let be a proof in , by assumption we have . As a consequence, we deduce from the induction hypothesis that . By definition, we have:
[TABLE]
so that we can conclude by anti-reduction.
• Case .
We are in the following situation:
[TABLE]
Let be a stack in , that is to say that and . By definition, since , we have . By induction hypothesis, this implies in particular that and thus {\mbox{\langle}}{p[\sigma,a:=q]}{|\!|}{e}\mbox{\rangle}\in{\bot\!\!\!\bot}. We can now use the closure by anti-reduction to get the expected result:
[TABLE]
• Case .
We are in the following situation:
[TABLE]
By induction hypothesis, we obtain that and . By definition, we thus have that .
• Case .
We are in the following situation:
[TABLE]
By induction hypothesis, since , we have for any and thus . We obtain by induction hypothesis that for any , i.e. that . The case is identical to this one.
• Case .
We have that
[TABLE]
thus by induction hypothesis we get that . Therefore we have in particular that (Section 3.5.2). The case is identical to this one. ∎
Once the adequacy is proved, normalization and soundness almost come for free. The normalization is a direct corollary of the following observation, whose proof is the same as for Section 4.4:
Proposition \thethm.
The set of normalizing commands defines a valid pole.
Proof.
We only have to check that is closed under antireduction, which is indeed the case: if and normalizes, then normalizes too. ∎
Theorem \thethm (Normalization).
For any contexts and any command , if , then normalizes.
Proof.
By adequacy, any typed command belongs to the pole modulo the closure under a substitution realizing the typing contexts. It suffices to observe that to obtain a closed term, any free variable of type in can be substituted by an inert constant which will realize its type (since it forms a normalizing command in front of any in ). Thus normalizes and so does . ∎
Similarly, the soundness is an easy consequence of adequacy, since the existence of a proof of type would imply that for any pole . For any consistent pole (say the empty pole), this is absurd.
Theorem \thethm (Soundness).
There is no proof (in the second-order call-by-name -calculus) such that \leavevmode\nobreak\ \vdash p:\bot\mid\leavevmode\nobreak\.
4. Classical call-by-need
Let us start this section with a story, borrowed from [17], illustratingdemand-driven computation and memoization of intermediate results, two key features of the call-by-need evaluation strategy that distinguish it from the call-by-name and call-by-value evaluation strategies:
A famous functional programmer once was asked to give an overview talk. He began with : “This talk is about lazy functional programming and call by need.” and paused. Then, quizzically looking at the audience, he quipped: “Are there any questions?” There were some, and so he continued: “Now listen very carefully, I shall say this only once.”
The call-by-name evaluation strategy indeed passes arguments to functions without evaluating them, postponing their evaluation to each place where the argument is needed, re-evaluating the argument several times if needed. It has in common with the call-by-value evaluation strategy that all places where a same argument is used share the same value. Nevertheless, it observationally behaves like the call-by-name evaluation strategy, in the sense that a given computation eventually evaluates to a value if and only if it evaluates to the same value (up to inner reduction) along the call-by-name evaluation161616In particular, in a setting with non-terminating computations, it is not observationally equivalent to the call-by-value evaluation: if the evaluation of a useless argument loops in the call-by-value evaluation, the whole computation loops (e.g. in ), which is not the case of call-by-name and call-by-need evaluations.. The call-by-name, call-by-value and call-by-need evaluation strategies can be turned into equational theories. For call-by-name and call-by-value, this was done by Plotkin [62] through continuation-passing style semantics characterizing these theories. For the call-by-need evaluation strategy, a continuation-passing style semantics was proposed in the 90s by Okasaki, Lee and Tarditi [59]. However, this semantics does not ensure normalization of simply-typed call-by-need evaluation, as shown in [3], thus failing to ensure a property which holds in the simply-typed call-by-name and call-by-value cases.
The semantics of calculi with control can also be reconstructed from an analysis of the duality between programs and their evaluation contexts, and the duality between the let construct (which binds programs) and a control operator such as Parigot’s (which binds evaluation contexts). As explained in Section 3, such an analysis can be done in the context of the -calculus [15, 26]. To attack the problem, Ariola et al. [5] first proposed the -calculus, a call-by-need variant of Curien-Herbelin’s -calculus [15]. Thanks to Danvy’s methodology of semantics artifacts, they then refined the reduction system until to a get a calculus with context-free reduction rules, from which they derived an untyped continuation-passing style translation [3]. This calculus, named the -calculus, relies on the use of an explicit environment to store substitutions. By pushing one step further Danvy’s methodology, we finally showed with Herbelin how to obtain a realizability interpretation à la Krivine for this framework [55]. The main idea, in contrast to usual models of Krivine realizability [40], is that realizers are defined as pairs of a term and a substitution. The adequacy of the interpretation directly provided us with a proof of normalization, and we shall follow the same methodology in Section 6 to prove the normalization of dLPA.
We shall now recap the different aforementionned steps leading to the correct definition of a classical call-by-need sequent calculus.
4.1. The -calculus: call-by-need with control
Recall from Section 3 that the reduction rules of the -calculus are given by:
[TABLE]
where the set of terms and the set of evaluation contexts parameterize the evaluation strategy: the call-by-name evaluation strategy amounts to the case where Co-values while call-by-value dually corresponds to Values. For the call-by-need case, intuitively, we would like to set Values (we only substitute evaluated terms of which we share the value) and Co-values (a term is only reduced if it is in front of a co-value). However, such a definition is clearly not enough since any command of the shape {\mbox{\langle}}{\mu\alpha.c}{|\!|}{{\tilde{\mu}}a.c^{\prime}}\mbox{\rangle} would be blocked. We thus need to understand how the computation is driven forward, that is to say when we need to reduce terms.
Observe that applicative contexts171717Note that we need to restrict the shape of applicative contexts: the general form is not necessarily a valid application, since for example in {\mbox{\langle}}{\mu\alpha.c}{|\!|}{q\cdot{\tilde{\mu}}a{\mbox{\langle}}{b}{|\!|}{\alpha}\mbox{\rangle}}\mbox{\rangle}, the context p\cdot{\tilde{\mu}}a{\mbox{\langle}}{b}{|\!|}{\alpha}\mbox{\rangle} forces the execution of even though its value is not needed. Applicative contexts are thus considered of the restricted shape . eagerly demand a value. Such contexts are called forcing contexts, and denoted by . When a variable is in front of a forcing context, that is in {\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}, the variable is said to be needed or demanded. This allows us to identify meta-contexts which are nesting of commands of the form {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle} for which neither is in (meaning it is some ) nor in (meaning it is an instance of some which is not a forcing context). These contexts, defined by the following grammar:
[TABLE]
are such that in a -binding of the form {\tilde{\mu}}a.C[{\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}], is needed and a value is thus expected. These contexts, called demanding contexts, are evaluation contexts whose evaluation is blocked on the evaluation of , therefore requiring the evaluation of what is bound to . In this case, we say that the bound variable has been forced.
All this suggests another refinement of the syntax, introducing a division between weak co-values (resp. weak values), also called catchable contexts (since they are the one caught by a binder), and strong co-values (resp. strong values), which are precisely the forcing contexts. Formally, the syntax (to which we add constants and co-constants ) is defined by181818In the definition, we implicitly assume to only cover the cases which are not of the form {\tilde{\mu}}a.C[{\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}].:
[TABLE]
We can finally define Weak values and Catchable contexts. The so-defined call-by-need calculus is close to the calculus called in Ariola et al [3]191919The difference lies in the fact that we add constants to preserve the duality. .
The reduction, written as , denotes thus the compatible reflexive transitive closure of the rules:
[TABLE]
Observe that the next reduction is not necessarily at the top of the command, but may be buried under several bound computations . For instance, the command {\mbox{\langle}}{\mu\alpha.c}{|\!|}{{\tilde{\mu}}a_{1}.{\mbox{\langle}}{a_{1}}{|\!|}{{\tilde{\mu}}a_{2}.{\mbox{\langle}}{a_{2}}{|\!|}{F}\mbox{\rangle}}\mbox{\rangle}}\mbox{\rangle}, where is not needed, reduces to {\mbox{\langle}}{\mu\alpha.c}{|\!|}{{\tilde{\mu}}a_{1}.{\mbox{\langle}}{a_{1}}{|\!|}{F}\mbox{\rangle}}\mbox{\rangle}, which now demands .
The -calculus can easily be equipped with a type system made of the usual rules of the classical sequent calculus [15], and adopting the convention that constants and co-constants come with a signature which assigns them a type. We delay the introduction of such a type system for our next object of study, the -calculus.
4.2. The -calculus
Since the call-by-need evaluation strategy imposes to share the evaluation of arguments across all the places where thay are need, abstract machines implementing it require a form of global memory [65, 14, 46, 1]. In order to obtain such an abstract machine from the -calculus, Ariola et al. first define the -calculus, which is reformulation of the former using explicit environments. We call stores these environments, which we denote by . Stores consists of a list of bindings of the shape , where is a term variable and a term, and of bindings of the shape where is a context variable and a context. For instance, in the closure , the variable is bound to in and . Besides, the term might be an unevaluated term (i.e. lazily stored), so that if is eagerly demanded at some point during the execution of this closure, will be reduced in order to obtain a value. In the case where indeed produces a value , the store will be updated with the binding . However, a binding of this shape (with a value) is fixed for the rest of the execution. As such, our so-called stores somewhat behave like lazy explicit substitutions or mutable environments 202020To draw the comparison between our structures and the usual notions of stores and environments, two things should be observed. First, the usual notion of store refers to a structure of list that is fully mutable, in the sense that the cells can be updated at any time and thus values might be replaced. Second, the usual notion of environment designates a structure in which variables are bounded to closures made of a term and an environment. In particular, terms and environments are duplicated, i.e. sharing is not allowed. Such a structure resemble to a tree whose nodes are decorated by terms, as opposed to a machinery allowing sharing (like ours) whose the underlying structure is broadly a directed acyclic graphs..
The lazy evaluation of terms allows us to reduce a command {\mbox{\langle}}{\mu\alpha.c}{|\!|}{{\tilde{\mu}}a.c^{\prime}}\mbox{\rangle} to the command together with the binding . In this case, the term is left unevaluated (“frozen”) in the store, until possibly reaching a command in which the variable is needed. When evaluation reaches a command of the form {\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}\tau[a:=\mu\alpha.c]\tau^{\prime}, the binding is opened and the term is evaluated in front of the context {\tilde{\mu}}[a].{\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}\tau^{\prime}:
[TABLE]
The reader can think of the previous rule as the “defrosting” operation of the frozen term : this term is evaluated in the prefix of the store which predates it, in front of the context {\tilde{\mu}}[a].{\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}\tau^{\prime} where the binder is waiting for an (unfrozen) value. This context keeps trace of the suffix of the store that was after the binding for . This way, if a value is indeed furnished for the binder , the original command {\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle} is evaluated in the updated full store:
[TABLE]
The brackets are used to express the fact that the variable is forced at top-level (unlike contexts of the shape {\tilde{\mu}}a.C[{\mbox{\langle}}{a}{|\!|}{F}\mbox{\rangle}] in the -calculus). The reduction system resembles the one of an abstract machine. Especially, it allows us to keep the standard redex at the top of a command and avoids searching through the meta-context for work to be done.
Note that our approach slightly differ from [3] in that we split values into two categories: strong values () and weak values (). The strong values correspond to values strictly speaking. The weak values include the variables which force the evaluation of terms to which they refer into shared strong value. Their evaluation may require capturing a continuation. The syntax of the language is given by:
[TABLE]
The reduction, written , is the compatible reflexive transitive closure of the rules given in Figure 4.
The different syntactic categories can again be understood as the different levels of alternation in a context-free abstract machine: the priority is first given to contexts at level (lazy storage of terms), then to terms at level (evaluation of into values), then back to contexts at level and so on until level . These different categories are thus directly reflected in the definition of the context-free abstract machine (that we will present in Section 4.3) and of the realizability interpretation but also in the type system we define. We indeed consider nine kinds of (one-sided212121To this end, observe that we write for a type that would have been in the context in two-sided sequents. While this is only used to compact notations, this will become crucial when using dependent types in the next sections.) sequents, one for typing each of the nine syntactic categories. We write them with an annotation on the sign, using one of the letters , , , , , , , , . Sequents typing values and terms are asserting a type, with the type written on the right; sequents typing contexts are expecting a type with the type written ; sequents typing commands and closures are black boxes neither asserting nor expecting a type; sequents typing substitutions are instantiating a typing context. In other words, we have the following nine kinds of sequents:
[TABLE]
where types and typing contexts are defined by:
[TABLE]
The typing rules are given on Figure 5 where we assume that a variable (resp. co-variable ) only occurs once in a context (we implicitly assume the possibility of renaming variables by -conversion). We also adopt the convention that constants and co-constants come with a signature which assigns them a type. Regarding the type system introduced earlier for the -calculus, the main novelties are the rules , and to handle stores, and the rule for the new binder .
This type system enjoys the property of subject reduction:
Theorem \thethm (Subject reduction).
If and then .
Proof.
By induction on typing derivations, see [52] for the complete proof. ∎
4.3. Abstract machine in context-free form
Reduction rules of the -calculus can again be refined in order to finally obtain small-step reduction rules of a context-free abstract machine [3]. This essentially consists in annotating again commands with the level of syntax we are examining (), and in defining a new set of reduction rules which separates computational steps (corresponding to big-step reductions), and administrative steps, which organize the descent in the syntax. In order, a command first put the focus on the context at level , then on the term at level , and so on following the hierarchy . This results again in an abstract machine in context-free form, since each step only analyzes one component of the command, the “active” term or context, and is parametric in the other “passive” component. In essence, for each phase of the machine, either the term or the context is fully in control and independent, regardless of what the other half happens to be.
We recall the resulting abstract machine from [3] in Figure 6. These rules directly lead to the definition of the CPS in [3] that we shall type in the next sections. Furthermore, the realizability interpretation à la Krivine (that we are about to present in the coming section) is deeply based upon this set of rules. Indeed, remember that a realizer is precisely a term which is going to behave well in front of any opponent in the opposed falsity value. We shall thus take advantage of the context-free rules where, at each level, the reduction step is defined independently of the passive component.
4.4. Realizability interpretation
We shall now see how to adapt the realizability interpretation for the -calculus to this setting, and in particular to handle stores. As for the -calculus, we are guided by the small-step abstract-machine. First of all, given a formula we now define its interpretation at each typing level (of ) a set (resp. ) of proof terms (resp. contexts) in the corresponding syntactic category. Second, we generalize the usual notion of closed term to the notion of closed proof-in-store. Intuitively, this is due to the fact that we are no longer interested in closed terms and substitutions to close opened terms, but rather in terms that are closed when considered in the current store. This is based on the simple observation that a store is nothing more than a shared substitution whose content might evolve along the execution. Last, we adapt the notion of pole to be sets of closures, which ask to be closed by anti-evaluation and store extension. In particular, the set of normalizing closures defines a valid pole.
We begin with a bunch of definitions related to stores. These notions will be re-used later when defining the interpretation for dLPA.
Definition \thethm (Closed store).
We extend the notion of free variable to stores:
[TABLE]
so that we can define a closed store to be a store such that .
Definition \thethm (Compatible stores).
We say that two stores and are independent and note when . We say that they are compatible and note whenever for all variables (resp. co-variables ) present in both stores: ; the corresponding terms (resp. contexts) in and coincide: formally and . Finally, we say that is an extension of and note whenever and .
Definition \thethm (Compatible union).
We denote by the compatible union of closed stores and , defined by:
[TABLE]
The following lemma (which follows easily from the previous definition) states the main property we will use about union of compatible stores.
Lemma \thethm.
If and are two compatible stores, then and . Besides, if is of the form , then is of the form with and .
As we explained, we will not consider closed terms in the usual sense. Indeed, while it is frequent in the proofs of normalization (e.g. by realizability or reducibility) of a calculus to consider only closed terms and to perform substitutions to maintain the closure of terms, this only makes sense if it corresponds to the computational behavior of the calculus. For instance, to prove the normalization of in typed call-by-name -calculus, one would consider a substitution that is suitable with respect to the typing context , then a context of type , and evaluates :
[TABLE]
Then we would observe that and deduce that is suitable for realizing , which would allow us to conclude by induction.
However, in the -calculus we do not perform global substitution when reducing a command, but rather add a new binding in the store:
[TABLE]
Therefore, the natural notion of closed term invokes the closure under a store, which might evolve during the rest of the execution (this is to contrast with a substitution).
Definition \thethm (Terms-in-store).
We call closed proof-in-store (resp. closed context-in-store, closed closures) the combination of a proof (resp. context , command ) with a closed store such that . We use the notation to denote such a pair.
We should note that in particular, if is a closed term, then is a proof-in-store for any closed store . The notion of closed proof-in-store is thus a generalization of the notion of closed terms, and we will (ab)use of this terminology in the sequel. We denote the sets of closed closures by , and will identify and the closure when is closed in . Observe that if is a closure in and is a store extending , then is also in . We are now ready to define the notion of pole, and verify that the set of normalizing closures is indeed a valid pole.
Definition \thethm (Pole).
A subset is said to be saturated or closed by anti-reduction whenever for all , if and then . It is said to be closed by store extension if whenever , for any store extending : , . A pole is defined as any subset of that is closed by anti-reduction and store extension.
Proposition \thethm.
The set is a pole.
Proof.
As we only considered closures in , both conditions (closure by anti-reduction and store extension) are clearly satisfied:
- •
if and normalizes, then normalizes too;
- •
if is closed in and normalizes, if then will reduce as does (since is closed under , it can only use terms in that already were in ) and thus will normalize.∎
Definition \thethm (Orthogonality).
Given a pole , we say that a proof-in-store is orthogonal to a context-in-store and write if and are compatible and {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}\overline{\tau\tau^{\prime}}\in{\bot\!\!\!\bot}.
Remark \thethm.
The reader familiar with Krivine’s forcing machine [41] might recognize his definition of orthogonality between terms of the shape and stacks of the shape , where and are forcing conditions:
[TABLE]
(The meet of forcing conditions is indeed a refinement containing somewhat the “union” of information contained in each, just like the union of two compatible stores.)
We can now relate closed terms and contexts by orthogonality with respect to a given pole. This allows us to define for any formula the sets (resp. ,, ) of realizers (or reducibility candidates) at level , , (resp , , ) for the formula . It is to be observed that realizers are here closed CPS.
Definition \thethm (Realizers).
Given a fixed pole , we set:
[TABLE]
Remark \thethm.
We draw the reader attention to the fact that we should actually write , etc… and , because the corresponding definitions are parameterized by a pole . As it is common in Krivine’s classical realizability, we ease the notations by removing the annotation whenever there is no ambiguity on the pole.
If the definition of the different sets might seem complex at first sight, we insist on the fact that they naturally follow from the abstract machine in context-free form where the term and the context (in a command) behave independently of each other. Intuitively, a realizer at a given level is precisely a term which is going to behave well (be in the pole) in front of any opponent chosen in the previous level (in the hierarchy ,etc…). The definition of the different sets , etc… directly stems from this intuition.
In comparison with the usual definition of Krivine’s classical realizability, we only considered orthogonal sets restricted to some syntactical subcategories. However, the definition still satisfies the usual monotonicity properties of bi-orthogonal sets:
Proposition \thethm.
For any type and any given pole , we have the following inclusions:
- (1)
; 2. (2)
.
Proof.
See [55]. ∎
We now extend the notion of realizers to stores, by stating that a store realizes a context if it binds all the variables and in to a realizer of the corresponding formula.
Definition \thethm.
Given a closed store and a fixed pole , we say that realizes , which we write222222Once again, we should formally write but we will omit the annotation by as often as possible. , if:
- (1)
for any , and 2. (2)
for any , and
We are now equipped to prove the adequacy of the type system for the -calculus with respect to the realizability interpretation.
Theorem \thethm (Adequacy).
The typing rules of Figure 5 for the -calculus without co-constants are adequate with any pole. In other words, if is a typing context, a pole and a store such that , then the following holds:
- (1)
If is a strong value such that , then . 2. (2)
If is a forcing context such that , then . 3. (3)
If is a weak value such that , then . 4. (4)
If is a catchable context such that , then . 5. (5)
If is a term such that , then . 6. (6)
If is a context such that , then . 7. (7)
If is a command such that , then . 8. (8)
If is a store such that , then . 9. (9)
If is a closure such that , then .
Proof.
By induction on typing rules. Most of the case are similar to the proof of adequacy for the call-by-name -calculus, hence we only give a few key cases. See [52, Chapter 6] for a complete proof.
• Case .
Assume that
[TABLE]
and let be a pole and a store such that . Let be a closed term in the set such that , then we have:
[TABLE]
By definition of , this closure is in the pole, and we can conclude by anti-reduction.
• Case .
Assume that
[TABLE]
and let be a pole and a store such that . As , we know that is of the form with . Let be in , with . By Lemma 7.2, we know that is of the form . Hence we have:
[TABLE]
and it suffices by anti-reduction to show that the last closure is in the pole . By induction hypothesis, we know that thus we only need to show that it is in front of a catchable context in . This corresponds exactly to the next case that we shall prove now.
• Case .
Assume that
[TABLE]
and let be a pole and a store such that . Let be a closed term in such that . We have that :
[TABLE]
By induction hypothesis, we obtain . Up to -conversion in and , so that the variables in are disjoint from those in . Therefore, we have that and then . By induction hypothesis again, we obtain that (this was an assumption in the previous case) and as , we finally get that and conclude again by anti-reduction. ∎
In particular, we can now prove the normalization of typed closures. As we already saw in Proposition 4.4, the set of normalizing closure is a valid pole, so that it only remains to prove that any typing rule for co-constants is adequate with .
Lemma \thethm.
Any typing rule for co-constants is adequate with the pole , i.e. if is a typing context, and is a store such that , if is a co-constant such that , then .
Proof.
This lemma directly stems from the observation that for any store and any closed strong value , {\mbox{\langle}}{v}{|\!|}{\bm{\kappa}}\mbox{\rangle}\overline{\tau\tau^{\prime}} does not reduce and thus belongs to the pole . ∎
As a consequence, we get:
Theorem \thethm.
If is a closure of the -calculus such that is derivable, then normalizes.
This concludes our study of classical call-by-need, and we shall use the same methodology to derive a proof of normalization for dLPA in Section 6. We shall now turn to our second preliminary problem, namely the definition of a sequent calculus with dependent types.
5. A classical sequent calculus with dependent types
We shall now turn to the second problem prior to the definition of dLPA: the definition of classical sequent calculus with dependent types. In addition of being a necessary step in our process, this question was also of great interest in itself. Indeed, not only are we interested in the definition of such calculus, but also we are considering the possibility of using it in order to define a dependently typed continuation-passing style translation. The latter was actually regarded as impossible232323 To quote their paper, they indeed say: “We investigate CPS translatability of typed -calculi with inductive and coinductive types. […] These translations also work in the presence of control operators […] No translation is possible along the same lines for small -types and sum types with dependent case.” since an article by Barthe and Uustalu on the subject [8]. Nonetheless, such a translation would provide us with a way of soundly compiling a calculus with dependent types and a form of classical logic into a usual type theory. Regarding the translation as a syntactic model, it would thus enable to give a way of soundly extending a type theory (for instance, those underlying the foundations of proof assistants, e.g. CIC for Coq) with a form of computational classical logic.
Yet, in addition to the problem of safely combining control operators and dependent types [27], the presentation of a dependently typed language under the form of a sequent calculus is a challenge in itself. In [54], we introduced such a system, called dL, which is a call-by-value sequent calculus with classical control and dependent types. In comparison with usual type systems, we decorate typing derivations with a list of dependencies to ensure subject reduction. We managed to prove the soundness of the calculus by means of a CPS translation taking the dependencies into account. The very definition of the translation constrained us to use delimited continuations in the calculus when reducing dependently typed terms. At the same time, this unveiled the need for the syntactic restriction of dependencies to the negative-elimination-free fragment as in dPA [29]. Additionally, we showed how to relate our calculus to a similar system by Lepigre [47], whose consistency is proved by means of a realizability interpretation. In Section 6, we will use the same techniques, namely a list of dependencies and delimited continuations, to ensure the soundness of dLPA, and we will follow Lepigre’s interpretation of dependent types for the definition of our realizability model. Let us then recall here the main intuitions leading to the definition of dL in [54].
5.1. Herbelin’s paradox
The first step in order to soundly mix dependent types and control operators is to understand the difficulty in doing so, and in particular Herbelin’s paradox [27]. Let us briefly recap his argument here. Consider a minimal logic of -types and equality, whose formulas, terms (only representing natural number) and proofs are defined as follows:
[TABLE]
Let us explain the different proof terms by presenting their typing rules. First, the pair is as expected a proof for an existential formula (or ) where is a witness for and is a certificate for . This implies that both formulas and proofs are dependent on terms, which is usual in mathematics. What is less usual in mathematics is that, as in Martin-Löf type theory, dependent types also allow for terms (and thus for formulas) to be dependent on proofs, by means of the constructions and . The corresponding typing rules are given by:
[TABLE]
Then, is a proof term for equality, and allows to use a proof of an equality to convert a formula into :
[TABLE]
The reduction rules for this language, which are safe with respect to typing, are then:
[TABLE]
Starting from this (sound) minimal language, Herbelin showed that its classical extension with the control operators and permits to derive a proof of [27]. The operator, which is a binder for the variable , is intended to catch its surrounding evaluation context. On the contrary, (in which is bound) discards the current context and restores the context captured by . The addition to the type system of the typing rules for these operators:
[TABLE]
allows the definition of the following proof:
[TABLE]
Intuitively such a proof catches the context, give 0 as witness (which is incorrect), and a certificate that will backtrack and give 1 as witness (which is correct) with a proof of the equality.
If besides, the following reduction rules242424We do not want to enter into the details of the reduction rules etc., but rather focus on the intuition of the causes of the problem. For a detailed proof, please refer to [27, Section 2]., are added:
[TABLE]
then we can formally derive a proof of . Indeed, the seek of a witness by the term will reduce to , which itself reduces to [math]. The proof term is thus a proof of , and we obtain indeed a proof of :
[TABLE]
The bottom line of this example is that the same proof is behaving differently in different contexts thanks to control operators, causing inconsistencies between the witness and its certificate. The easiest and usual approach to prevent this is to impose a restriction to values (which are already reduced) for proofs appearing inside dependent types and within the operators and , together with a call-by-value discipline. In particular, in the present example this would prevent us from writing and .
5.2. A naive sequent calculus with dependent types
Here again, rather than directly trying to define a continuation-passing style we first pay attention to the possibility of extending the -calculus with a form of dependent types. Let us momentarily assume that we naively add a dependent product to the -calculus type system while restricting dependencies to values (in order to prevent Herbelin’s paradox from occurring). In other words, we authorize functions to inhabit the type if is of typed under the assumption that and, dually, stacks if is a value of type and a context of type . Assuming that we have such terms at hands, we can thus get the following derivation:
[TABLE]
The first difficulties arise when trying to prove subject reduction. Indeed, the previous command should reduce (following a call-by-value discipline as we eventually would like to have for dLPA) as follows:
[TABLE]
On the right-hand side, we see that , whose type is , is now cut with whose type is . Consequently, we are not able to derive a typing judgment252525Observe that the problem here arises independently of the value restriction or not (that is whether we consider that is a value or not), and is peculiar to the sequent calculus presentation). for this command anymore:
[TABLE]
Our intuition is that in the full command, has been linked to at a previous level of the typing judgment. In particular, the command is still safe, since the head-reduction imposes that the command {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle} will not be executed before the substitution of by 262626Note that even if we were not restricting ourselves to values, this would still hold: if at some point the command {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle} is executed, it is necessarily after that has produced a value to substitute for . is performed and by then the problem would have been solved. Roughly speaking, this phenomenon can be seen as a desynchronization of the typing process with respect to computation. The synchronization can be re-established by making explicit a list of dependencies in the typing rules, which links variables (here ) to the associate proof term on the left-hand side of the command (here ):
[TABLE]
We spare the reader from the formal definition of the corresponding type system272727See [54] for further details., the main idea lying in the use of list of dependencies when typing commands. In particular, this is enough to extend the -calculus with dependent types (restricted to values) and prove that the resulting calculus satisfies subject reduction, is normalizing and consistent as a logic.
5.3. A dependently typed continuation-passing style
Nonetheless, in addition to the fact that the value restriction is unsatisfactory (it is too restrictive), a problem still subsists: such a calculus remains incompatible with the definition of a continuation-passing style translation. Indeed, considering the naive translation of the very same command, assuming that a type is translated into 282828Recall the translation given for the call-by-name calculus in Section 3.4., we get:
[TABLE]
We are thus facing the same problem when trying to type the translation of the command {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}. This does not come as a surprise, insofar as we observed a desynchronization between the computation and the typing process which we only have compensated within the type system. In order to obtain a well-typed continuation-passing style translation, we thus need to understand how to tackle we need to tackle the problem through the operational semantics.
To this end, we follow the idea that the correctness is guaranteed by the head-reduction strategy, preventing {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle} from reducing before the substitution of was made. We would like to ensure the same thing happens in the target language (that will also be equipped with a head-reduction strategy), namely that cannot be applied to before has furnished a value to substitute for . This would correspond informally to the term:
[TABLE]
Assuming that eventually produces a value , the previous term would indeed reduce as follows:
[TABLE]
Since now has a type convertible to , the term that is produced in the end is well-typed292929 Readers should now be familiar with realizability may observe that intuitively such a term defines an appropriate realizer, since it eventually terminates on a correct term .. We are now facing three questions about the term : (1) Would any term be compatible with such a reduction? (2) Is this term typable? (3) Does it matches the translation of a term in the source calculus?
Regarding the first question, we observe that if , instead of producing a value, was a classical proof throwing the current continuation away (for instance where ), this would lead to the following unsafe reduction:
[TABLE]
Indeed, through such a translation, would only be able to catch the local continuation, and the term ends in instead of . We thus need to restrict ourselves at least to proof terms that could not throw the current continuation. Syntactically, these are proof terms that can be expressed (up to -conversion) with only one continuation variable and without applicative context of the shape . In other words, this corresponds exactly to Herbelin’s restriction to the fragment of negative-elimanation-free (nef) proofs (see Section 2.2).
The second question concerns the typability of the term , which is clearly not possible using the naive translation for the . Nonetheless, the whole term can be typed by turning the type of the continuation that is waiting for into a (dependent) type parameterized by . This way, we can have instead of , and for , the whole term is well-typed303030This is precisely where lies the difference with Barthe and Uustalu’s work, who implicitly assume the return type to be fixed to [8].. It only remains to wonder if any translated term can be given such a type, and, fortunately, this is the case for all nef terms. Indeed, nef proofs are precisely terms which, through the translation, can only use once the continuation. They hence satisfy some kind of parametricity equation [70] and can be given a parametric (and dependent) return type (generalizing Friedman -translation [22]). We prefer not enter into the details of the complete continuation-passing style translation and refer the interested reader to [54].
Last, the term suggests the use of delimited continuations313131We stick here to the presentations of delimited continuations in [31, 4], where is used to denote the top-level delimiter. to temporarily encapsulate the evaluation of when reducing such a command:
[TABLE]
Intuitively, a term momentarily moves the top-level focus to and freezes its own evaluation context until reduces to a command of the shape {\mbox{\langle}}{p}{|\!|}{{\hat{{{\texttt{t}\!\texttt{p}}}}}}\mbox{\rangle}:
[TABLE]
Once more, the command {\mbox{\langle}}{\mu{{\hat{{{\texttt{t}\!\texttt{p}}}}}}.{\mbox{\langle}}{q}{|\!|}{\tilde{\mu}a.{\mbox{\langle}}{p}{|\!|}{{\hat{{{\texttt{t}\!\texttt{p}}}}}}\mbox{\rangle}}\mbox{\rangle}}{|\!|}{e}\mbox{\rangle} is safe under the guarantee that will not throw away the continuation \tilde{\mu}a.{\mbox{\langle}}{p}{|\!|}{{\hat{{{\texttt{t}\!\texttt{p}}}}}}\mbox{\rangle}, and will mimic the aforedescribed reduction:
[TABLE]
It is now easy to define the translation of delimited continuations so that our modified reduction systems semantics matches the expected translation:
[TABLE]
In addition to providing an operational semantics that is now compatible with a continuation-passing style translation, delimited continuations bring us a finer control on the use of the list of dependencies in typing derivations. Indeed, the places where a desynchronization needs to be compensated correspond exactly to commands within delimited continuations. Even more, the only type that needs to be adjusted with the list of dependencies is the one of . This allows us to distinguish between two typing mode, a regular mode with sequents without list of dependencies, and a dependent one, which is activated when going beyond a and whose sequents we denote by (where is a list of dependencies). The main novelties of this extended syntax, which we summarize in Figure 7, are thus: (1) the fragment of nef proofs, (2) the use of delimited continuations (3) a distinction between a regular and a dependent typing modes.
As we shall explain in Section 7.1, similar phenomena will occur in dLPA with the dependent types and (remember that we consider a stratified presentation with terms and proofs). While the former can be solved with the exact same ideas, the latter will require the introduction of the dual notion of co-delimited continuations, just as the general dependent sum would have. Let us briefly go through the same process to highlight the corresponding intuitions. Consider now a command formed by a pair of type and a context :
[TABLE]
This situation is exactly dual to the case of a stack above323232In fact, they could even be identified in a polarized version of the calculus inspired from Munch-Maccagnoni’s system L [56], observing that . In other words, and are both a pair whose second component depends on the first one., hence it does not come as a surprise that the command it naturally reduces to:
[TABLE]
can not be typed without using a list of dependencies. Indeed, the pair that is now put in front of require to remember a link between and to be typed:
[TABLE]
Similarly, if the former can be solved within the type system with the simple addition of a list of dependencies, the naive continuation-passing style translation of the pair is again ill-typed:
[TABLE]
Following the intuition that should not be applied to its continuation before has reduced and provided a value to substitute for , we can twist this term into:
[TABLE]
This translated term is now well-typed provided that can be given the parametric dependent type (which is possible for any nef term , and in particular for any term in dPA—remember that terms are objects of the arithmetic in finite types and do not have access to control operators). Once again, such a translation can be obtained by extending the original operational semantics with co-delimited continuations:
[TABLE]
where is somehow frozen to put the focus on the command {\mbox{\langle}}{t}{|\!|}{\tilde{\mu}x.{\mbox{\langle}}{{{\check{{{\texttt{t}\!\texttt{p}}}}}}}{|\!|}{{\tilde{\mu}}a.{\mbox{\langle}}{(x,a)}{|\!|}{e}\mbox{\rangle}}\mbox{\rangle}}\mbox{\rangle}. It should now be clear to the reader why, when defining a small-step reduction system that explicit the evaluation of dLPA terms in Section 7.1, we will introduce this notion of co-delimited continuations.
5.4. Realizability interpretation
Last but not least, we shall say a few words about the realizability interpretation of dL. This interpretation takes advantage of a recent paper in which Lepigre presented a classical system allowing the use of dependent types with a semantic value restriction [47],. In practice, the type system of his calculus does not contain a dependent product strictly speaking, but it contains a predicate allowing the decomposition of the dependent product into:
[TABLE]
as it is usual in Krivine’s classical realizability [40]. In his system, the relativization is restricted to values, so that we can only type :
[TABLE]
However, typing judgments are defined up to observational equivalence, so that if is observationally equivalent to , one can derive the judgment .
Interestingly, as highlighted through the continuation-passing style translation333333More precisely, this is exactly the counterpart of the usual parametricity equation evoked earlier. See [54, Lemma 4.1]., any nef proof is observationally equivalent to some value , so that we can derive from . The nef fragment is thus compatible with the semantical value restriction. The converse is obviously false, observational equivalence allowing us to type realizers that would be untyped otherwise343434In particular, Lepigre’s semantical restriction is so permissive that it is not decidable, while it is easy to decide whether a proof term of dL is in nef.. As a matter of fact, in [54] we defined an embedding from dL into Lepigre’s calculus that not only preserves typing, but also to transfer normalization and correctness properties along this translation. Additionally, this embedding has the benefits of providing us with an adequate realizability interpretation for dL our calculus. We shall also mention that the translation from dL to Lepigre’s calculus could not have been defined without the use of delimited continuations. Actually we would have encountered a problem very similar to the one for the continuation-passing style translation. Moreover, the translation of delimited continuations is informative in that it somehow decompiles them in order to simulate the corresponding reductions in a natural deduction fashion. We refer to [54, Section 5] the reader interested into further details.
In the current paper, we will follow Lepigre’s realizability interpretation regarding dependent types. We shall thus introduce a predicate whose interpretation will be defined for proof terms observationally equivalent to a value.
6. A sequent calculus with dependent types for classical arithmetic
Drawing on the calculi we introduced in the last sections, we shall now present dLPA, our sequent calculus counterpart of Herbelin’s dPA. This calculus provides us with dependent types restricted to the nef fragment, for which dLPA is an extension of dL. In addition to the language of dL, dLPA has terms for classical arithmetic in finite types (PAω). More importantly, it includes a lazily evaluated co-fixpoint operator. To this end, the calculus uses a shared store, as in the -calculus.
We first present the language of dLPA with its type system and its reduction rules. We prove that the calculus verifies the property of subject reduction and that it is as expressive as dPA. In particular, the proof terms for and DC of dPA can be directly defined in dLPA. We then apply once again the methodology of Danvy’s semantic artifacts to derive a small-step calculus (Section 7.1), from which we deduce a realizability interpretation (Section 7.2), which relies on a combination of the corresponding ones developed for the -calculus and dL. This interpretation will lead us to the main result of this paper: the normalization of dLPA.
Nonetheless, we should say before starting this section that we already have a guardrail for the normalization. Informally, we could argue that authorizing infinite stores in the -calculus would not alter its normalization. Indeed, from the point of view of existing programs (which are finite and typed in finite contexts), they are computing with a finite knowledge of the memory (and it is easy to see that through the realizability interpretation, terms are compatible with store extensions [55]). Note that in the store, we could theoretically replace any co-fixpoint that produces a stream by the (fully developed) stream in question. Due to the presence of backtracks in co-fixpoints, the store would contain all the possible streams (possibly an infinite number of it) produced when reducing co-fixpoints. In this setting, if a term were to perform an infinite number of reductions steps, it would necessarily have to explore an infinite number of cells in the pre-computed memory, independently from its production. This should not be possible.
This argument is actually quite close from Herbelin’s original proof sketch, which this work precisely aims at replacing with a formal proof. These unprecise explanations should be taken more as spoilers of the final result than as proof sketches. We shall now present formally dLPA and prove its normalization, which will then not come as a surprise.
*Most of the proofs in this section will resemble a lot to the corresponding ones in the previous sections. Yet, as dLPA gathers all the expressive power and features of the -calculus and dL, the different proofs also combined all the tools and tricks used in each case. We will hence try to avoid repetitions and only highlight the most interesting parts as much as possible. *
6.1. Syntax
The language of dLPA is based on the syntax of dL [54], extended with the expressive power of dPA [29] and with explicit stores as in the -calculus [3]. We stick to the stratified presentation of dependent types, that is to say that we syntactically distinguish terms—that represent mathematical objects—from proof terms—that represent mathematical proofs. In particular, types and formulas are separated as well, matching the syntax of dPA’s formulas. Types are defined as finite types with the set of natural numbers as the sole ground type, while formulas are inductively built on atomic equalities of terms, by means of conjunctions, disjunctions, first-order quantifications, dependent products and co-inductive formulas:
[TABLE]
The syntax of terms is identical to the one in dPA, including functions and applications , as well as a recursion operator , so that terms represent objects in arithmetic of finite types. As for proof terms (and contexts, commands), they are now defined with all the expressiveness of dPA. Each constructor in the syntax of formulas is reflected by a constructor in the syntax of proofs and by the dual co-proof (i.e. destructor) in the syntax of evaluation contexts. Amongst other things, the syntax includes pairs where is a term and a proof, which inhabit the dependent sum type ; dual co-pairs which bind the (term and proof) variables and in the command ; functions inhabiting the type together with their dual, stacks where is a context whose type might be dependent in ; functions which inhabit the dependent product type , and, dually, stacks , where is a context whose type might be dependent in ; a proof term which is the proof of atomic equalities and a destructor which allows us to type the command modulo an equality of terms; operators and , as in dPA, for inductive and coinductive reasoning; delimited continuations through proofs and the context ; a distinguished context of type , which allows us to reason ex-falso.
As in dL, the syntax of nef proofs, contexts and commands is defined as a restriction of the previous syntax. Technically, they are defined (modulo -conversion) with only one distinguished context variable (and consequently only one binder ), and without stacks of the shape or to avoid applications (recall that one can understand nef proofs as the proofs that cannot drop their continuation). The commands within delimited continuations are defined as commands of the shape {\mbox{\langle}}{p}{|\!|}{{\hat{{{\texttt{t}\!\texttt{p}}}}}}\mbox{\rangle} or formed by a nef proof and a context of the shape , , or .
We adopt a call-by-value evaluation strategy except for fixpoint operators353535To highlight the duality between inductive and coinductive fixpoints, we evaluate both in a lazy way. Even though this is not indispensable for inductive fixpoints, we find this approach more natural in that we can treat both in a similar way in the small-step reduction system and thus through the realizability interpretation., which are evaluated in a lazy way. To this purpose, we use stores in the spirit of the -calculus, which are again defined as lists of bindings of the shape where is now a value or a (co-)fixpoint, and of bindings of the shape where is any context. We assume that each variable occurs at most once in a store , we thus reason up to -reduction and we assume the capability of generating fresh names. Apart from evaluation contexts of the shape and co-variables , all the contexts are forcing contexts which eagerly require a value to be reduced and trigger the evaluation of lazily stored terms. The resulting language is given in Figure 8.
6.2. Reduction rules
The reduction system of dLPA is given in Figure 9. The basic rules are those of the call-by-value -calculus and of dL. The rules for delimited continuations are exactly the same as in dL, except that we have to prevent from being caught and stored by a proof . We thus distinguish two rules for commands of the shape {\mbox{\langle}}{\mu\alpha.c}{|\!|}{e}\mbox{\rangle}, depending on whether is of the shape or not. In the former case, we perform the substitution , which is linear since is necessarily nef. We should also mention in passing that we abuse the syntax in every other rules, since should actually refer to or (or the reduction of delimited continuations would be stuck). Elimination rules correspond to commands where the proof is a constructor (say of pairs) applied to values, and where the context is the matching destructor. Call-by-value rules correspond to () rule of Wadler’s sequent calculus [71]. The next rules express the fact that (co-)fixpoints are lazily stored, and reduced only if their value is eagerly demanded by a forcing context. Observe that in that case, the unfolding of (co-)fixpoints is entirely done within the store. Last, terms are reduced according to the usual -reduction, with the operator rec computing with the usual recursion rules. It is worth noting that the stratified presentation allows to define the reduction of terms as external: within proofs and contexts, terms are reduced in place. Consequently, as in dL the very same happen for nef proofs embedded within terms. Computationally speaking, this corresponds indeed to the intuition that terms are reduced on an external device.
6.3. Typing rules
As often in Martin-Löf’s intensional type theory, formulas are considered up to equational theory on terms. We denote by the reflexive-transitive-symmetric closure of the relation induced by the reduction of terms and nef proofs as follows:
[TABLE]
in addition to the reduction rules for equality and for coinductive formulas:
[TABLE]
We work with one-sided sequents where typing contexts are defined by:
[TABLE]
using the notation for an assumption of the refutation of . This allows us to mix hypotheses over terms, proofs and contexts while keeping track of the order in which they are added (which is necessary because of the dependencies). We assume that a variable occurs at most once in a typing context.
We define nine syntactic kinds of typing judgments:
- •
six in regular mode, that we write :
- (1)
for terms, 2. (2)
for proofs, 3. (3)
for contexts, 4. (4)
for commands, 5. (5)
for closures, 6. (6)
for stores;
- •
three more for the dependent mode, that we write :
- (7)
for typing contexts, 2. (8)
for typing commands, 3. (9)
for typing closures.
In each case, is a list of dependencies—we explain the presence of a list of dependencies in each case thereafter—, which are defined from the following grammar:
[TABLE]
The substitution on formulas according to a list of dependencies is defined by:
[TABLE]
Because the language of proof terms include constructors for pairs, injections, etc, the notation does not refer to usual substitutions properly speaking: can be a pattern (for instance ) and not only a variable.
We shall attract the reader’s attention to the fact that all typing judgments include a list of dependencies. Indeed, as in the -calculus, when a proof or a context is caught by a binder, say and , the substitution is not performed but rather put in the store: . Now, consider for instance the reduction of a dependent function (of type ) applied to a stack :
[TABLE]
Since still contains the variable , whence his type is still , whereas the type of is . We thus need to compensate the missing substitution363636On the contrary, the reduced command in dL would have been {\mbox{\langle}}{p[V/a]}{|\!|}{e}\mbox{\rangle}, which is typable with the rule over the formula ..
We are mostly left with two choices. Either we mimic the substitution in the type system, which would amount to the following typing rule:
[TABLE]
Or we type stores in the spirit of the -calculus, and we carry along the derivations all the bindings liable to be used in types, which constitutes again a list of dependencies.
The former solution has the advantage of solving the problem before typing the command, but it has the flaw of performing computations which would not occur in the reduction system. For instance, the substitution could duplicate co-fixpoints (and their typing derivations), which would never happen in the calculus. That is the reason why we favor the other solution, which is closer to the calculus in our opinion. Yet, it has the drawback that it forces us to carry a list of dependencies even in regular mode. Since this list is fixed (it does not evolve in the derivation except when stores occur), we differentiate the denotation of regular typing judgments, written , from the one of judgments in dependent mode, which we write to highlight that grows along derivations. The type system we obtain is given in Figure 11.
6.4. Subject reduction
We shall now prove that typing is preserved along reduction. As for the -calculus, the proof is simplified by the fact that substitutions are not performed (except for terms), which keeps us from proving the safety of the corresponding substitutions. Yet, we first need to prove some technical lemmas about dependencies. To this aim, we define a relation between lists of dependencies, which expresses the fact that any typing derivation obtained with could be obtained as well as with :
[TABLE]
We first show that the cases which we encounter in the proof of subject reduction satisfy this relation:
Lemma \thethm (Dependencies implication).
The following holds for any :
- (1)
** 2. (2)
** 3. (3)
** 4. (4)
** 5. (5)
** 6. (6)
** 7. (7)
**
where the fourth item abuse the definition of list of dependencies to include a substitution of terms.
Proof.
All the properties are trivial from the definition of the substitution . ∎
We can now prove that the relation indeed matches the expected intuition:
Proposition \thethm (Dependencies weakening).
If are two lists of dependencies such that , then any derivation using can be done using instead. In other words, the following rules are admissible:
[TABLE]
for any judgment among ,,.
Proof.
Simple induction on the typing derivations. The rules and where the list of dependencies is used exactly match the definition of . Every other case is direct using the first item of Section 6.4. ∎
To simplify the proof of subject reduction, we prove that the concatenation of stores is typable:
Lemma \thethm.
The following rule is admissible:
[TABLE]
Proof.
By induction on the structure of . ∎
As explained, we only need to prove that term substitution is safe:
Lemma \thethm (Safe term substitution).
If then for any conclusion for typing proofs, contexts, terms, etc; the following holds:
- (1)
If then . 2. (2)
*If then . *
Proof.
By induction on typing rules. ∎
We can prove the safety of reduction with respect to typing:
Theorem \thethm (Subject reduction).
For any context and any closures and such that , we have:
- (1)
If then . 2. (2)
If then .
Proof.
The proof follows the usual proof of subject reduction, by induction on the typing derivation and the reduction . Since there is no substitution but for terms (proof terms and contexts being stored), there is no need for auxiliary lemmas about the safety of substitution. We sketch it by examining all the rules from Figure 11 from top to bottom.
• The cases for reductions of are identical to the cases proven in the previous chapter for dL.
• The rules for reducing and are almost the same except that elements are stored, which makes it even easier. For instance in the case of , the reduction rule is:
[TABLE]
A typing derivation in regular mode for the command on the left-hand side is of the shape:
[TABLE]
Thus we can type the command on the right-hand side:
[TABLE]
where . As for the dependent mode, the binding within the list of dependencies is compensated when typing the store as shown in the last derivation.
• Similarly, elimination rules for contexts , , or are easy to check, using Section 6.4 and the rule in dependent mode to prove the safety with respect to dependencies.
• The cases for delimited continuations are identical to the corresponding cases for dL.
• The cases for the so-called “call-by-value” rules opening constructors are straightforward, using again Section 6.4 in dependent mode to prove the consistency with respect to the list of dependencies.
• The cases for the lazy rules are trivial.
• The first case in the “lookup” section is trivial. The three lefts correspond to the usual unfolding of inductive and co-inductive fixpoints. We only sketch the latter in regular mode. The reduction rule is:
[TABLE]
The crucial part of the derivation for the left-hand side command is the derivation for the cofix in the store:
[TABLE]
Then, using this derivation, we can type the store of the right-hand side command:
[TABLE]
It only remains to type (we avoid the rest of the derivation, which is less interesting) the proof with this new store to ensure us that the reduction is safe (since the variable will still be of type when typing the rest of the command):
[TABLE]
• The cases for reductions of terms are easy. Since terms are reduced in place within proofs, the only things to check is that the reduction of preserves types (which is trivial) and that the -reduction verifies the subject reduction (which is a well-known fact). ∎
6.5. Natural deduction as macros
We can recover the usual proof terms for elimination rules in natural deduction systems by defining them as macros in our language. In particular, this provides us with an embedding of dPA proof terms into dLPA syntax. The definitions are straightforward and follow the same intuition than for defining the application in the -calculus (see Section 3.2): we consider the expected reduction rule in an abstract machine (for instance {\mbox{\langle}}{\mathop{\texttt{throw}}\,{e}\,p}{|\!|}{e^{\prime}}\mbox{\rangle}\to{\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}) and define the macro by solving the induced equation (in that case, \mathop{\texttt{throw}}\,{e}\,p\triangleq\mu\beta.{\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}). Observe that we use delimited continuations to define and the constructors over nef proofs which might be dependently typed:
[TABLE]
where if is nef and otherwise. It is then easy to check that the macros match the expected typing rules from dPA’s type system [29].
Proposition \thethm (Natural deduction).
The typing rules from dPA, given in Figure 12, are admissible.
Proof.
Straightforward derivations, as an example we give here the two cases for the macros and (in natural deduction) that are admissible in dLPA. Recall that we have the following typing rules in dLPA:
[TABLE]
and that we defined and as syntactic sugar:
[TABLE]
Observe that is now only definable if is a nef proof term. For any and any variables , we can prove the admissibility of the -rule:
[TABLE]
Similarly, we can prove that the ()-rule is admissible:
[TABLE]
One can even check that the reduction rules in dLPA for these proofs almost mimic the ones of dPA. To be more precise, the rules of dLPA do not allow to simulate each rule of dPA, due to the head-reduction strategy amongst other things. Nonetheless, up to a few details the reduction of a command in dLPA follows one particular reduction path of the corresponding proof in dPA, or in other words, one reduction strategy.
Noteworthily, through the embedding of dPA the same proof terms are suitable for the axioms of countable and dependent choices [29]. We do not state it here, but following the approach of [29], we could also extend dLPA to obtain a proof for the axiom of bar induction.
Theorem \thethm (Countable choice [29]).
We have:
[TABLE]
where .
Proof.
The complete typing derivation of the proof term for from Herbelin’s paper [29] is given in Figure 13. ∎
Theorem \thethm (Dependent choice [29]).
We have:
[TABLE]
*where
and .*
Proof.
Left to the reader. ∎
7. Normalization and consistency of dLPA
We shall now present our realizability interpretation for dLPA, which will eventually allow us to prove its normalization and consistency. Once more, we will follow Danvy’s methodology of semantic artifacts [17, 3] to first define a small-step calculus (or context-free abstract machine). The resulting realizability interpretation will be similar in its structure to the one presented in Section 4 for the -calculus.
7.1. Small-step calculus
We start by decomposing the reduction system of dLPA into small-step reduction rules, that we denote by . This requires a refinement and an extension of the syntax, that we shall now present. To keep us from boring the reader stiff with new (huge) tables for the syntax, typing rules and so forth, we will introduce them step by step. We hope it will help the reader to convince herself of the necessity and of the somewhat naturality of these extensions.
7.1.1. Values
First of all, we need to refine the syntax to distinguish between strong and weak values in the syntax of proof terms. As in the -calculus, this refinement is induced by the computational behavior of the calculus: weak values are the ones which are stored by binders, but which are not values enough to be eliminated in front of a forcing context, that is to say variables. Indeed, if we observe the reduction system, we see that in front of a forcing context , a variable leads a search through the store for a “stronger” value, which could incidentally provoke the evaluation of some fixpoints. On the other hand, strong values are the ones which can be reduced in front of the matching forcing context, that is to say functions, , pairs of values, injections or dependent pairs:
[TABLE]
This allows us to distinguish commands of the shape {\mbox{\langle}}{v}{|\!|}{f}\mbox{\rangle}\tau, where the forcing context (and next the strong value) are examined to determine whether the command reduces or not; from commands of the shape {\mbox{\langle}}{a}{|\!|}{f}\mbox{\rangle}\tau where the focus is put on the variable , which leads to a lookup for the associated proof in the store.
7.1.2. Terms
Next, we need to explicit the reduction of terms. To this purpose, we include a machinery to evaluate terms in a way which resemble the evaluation of proofs. In particular, we define new commands which we write {\mbox{\langle}}{t}{|\!|}{\pi}\mbox{\rangle} where is a term and is a context for terms (or co-term). Co-terms are either of the shape or stacks of the shape . These constructions are the usual ones of the -calculus (which are also the ones for proofs). We also extend the definitions of commands with delimited continuations to include the corresponding commands for terms:
[TABLE]
We give typing rules for these new constructions, which are the usual rules for typing contexts in the -calculus:
[TABLE]
It is worth noting that the syntax as well as the typing and reduction rules for terms now match exactly the ones for proofs373737Except for substitutions of terms, which we could store as well.. In other words, with these definitions, we could abandon the stratified presentation without any trouble, since reduction rules for terms will naturally collapse to the ones for proofs.
7.1.3. Co-delimited continuations
Finally, in order to maintain typability when reducing dependent pairs of the strong existential type, we need to add what we call co-delimited continuations. As observed in Section 5.3, the CPS translation of pairs in dL is not the expected one, reflecting the need for a special reduction rule (remember that the usual reduction rule for opening pairs, following the global call-by-value evaluation strategy, was causing subject reduction to fail). To remediate this, we instead use a rule where is reduced within a context where is not linked to but to a co-reset (dually to reset ), whose type can be changed from to thanks to a list of dependencies:
[TABLE]
We thus equip the language with new contexts , which we call co-shifts and where is a command whose last cut is of the shape {\mbox{\langle}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}{|\!|}{e}\mbox{\rangle}. This corresponds formally to the following syntactic sets, which are dual to the ones introduced for delimited continuations:
[TABLE]
This might seem to be a heavy addition to the language, but we insist on the fact that these artifacts are merely the dual constructions of delimited continuations introduced in dL, with a very similar intuition. In particular, it might be helpful for the reader to think of the fact that we introduced delimited continuations for type safety of the evaluation of dependent products in (which naturally extends to the case ). Therefore, to maintain type safety of dependent sums in , we need to introduce the dual constructions of co-delimited continuations. We also give typing rules to these constructions, which are dual to the typing rules for delimited-continuations:
[TABLE]
Note that we also need to extend the definition of list of dependencies to include bindings of the shape for terms, and that we have to give the corresponding typing rules to type commands of terms in dependent mode:
[TABLE]
where .
The small-step reduction system we obtained is given in Figure 15. We write for the reduction rules, where the annotation on commands are indices (i.e. ) indicating which part of the command is in control. As in the -calculus, we observe an alternation of steps descending from to for proofs and from to for terms. The descent for proofs can be divided in two main phases. During the first phase, from to we observe the call-by-value process, which extracts values from proofs, opening recursively the constructors and computing values. In the second phase, the core computation takes place from to , with the destruction of constructors and the application of function to their arguments. The laziness corresponds precisely to skipping the first phase, waiting to possibly reach the second phase before actually going through the first one.
Proposition \thethm (Subject reduction).
The small-step reduction satisfies subject reduction.
Proof.
The proof is again a tedious induction on the reduction . There is almost nothing new in comparison with the cases for the big-step reduction rules: the cases for reduction of terms are straightforward, as well as the administrative reductions changing the focus on a command. We only give the case for the reduction of pairs . The reduction rule is:
[TABLE]
Consider a typing derivation for the command on the left-hand side, which is of the shape (we omit the rule and the store for conciseness):
[TABLE]
Then we can type the command on the right-hand side with the following derivation:
[TABLE]
where is as expected. ∎
It is also direct to check that the small-step reduction system simulates the big-step one, and in particular that it preserves the normalization :
Proposition \thethm.
If a closure normalizes for the reduction , then it also normalizes for the reduction .
Proof.
By contraposition, one proves that if a command produces an infinite number of steps for the reduction , then it does not normalize for either. This is proved by showing by induction on the reduction that each step, except for the contextual reduction of terms, is reflected in at least on for the reduction . The rules for term reductions require a separate treatment, which is really not interesting at this point. We claim that the reduction of terms, which are usual simply-typed -terms, is known to be normalizing anyway and does not deserve that we spend another page proving it in this particular setting. ∎
7.2. A realizability interpretation of dLPAω
We shall now present the realizability interpretation of dLPA, which will finally give us a proof of its normalization. Here again, the interpretation combines ideas of the interpretations for the -calculus [55] and for dL through its embedding in Lepigre’s calculus (see Section 5.4). Namely, as for the -calculus, formulas will be interpreted by sets of proofs-in-store of the shape , and the orthogonality will be defined between proofs-in-store and contexts-in-store such that the stores and are compatible. On the other hand, we will follow Lepigre’s decomposition of dependent types into a quantification bounded by a predicate whose interpretation is defined modulo observational equivalence.
We recall the main definitions necessary to the realizability interpretation:
Definition \thethm (Proofs-in-store).
We call closed proof-in-store (resp. closed context-in-store, closed term-in-store, etc) the combination of a proof (resp. context , term , etc) with a closed store such that . We use the notation to denote such a pair. In addition, we denote by (resp. , etc.) the set of all proofs and by (resp. , etc.) the set of all proofs-in-store. We denote the sets of closed closures by , and we identify with the closure when is closed in .
We recall the definition of compatible stores (Section 4.4) in this context, which allows us to define an orthogonality relation between proofs- and contexts-in-store.
Definition \thethm (Compatible stores and union).
Let and be stores, we say that:
- •
they are independent and note if .
- •
they are compatible and note if for all variables (resp. co-variables ) present in both stores: ; the corresponding proofs (resp. contexts) in and coincide.
- •
is an extension of and we write whenever and .
- •
is *the compatible union * of compatible closed stores and . It is defined as , which itself given by:
[TABLE]
where .
The next lemma (which follows from the previous definition) states the main property we will use about union of compatible stores.
Lemma \thethm.
If and are two compatible stores, then and . Besides, if is of the form , then is of the form with and .
We can now define the notion of pole, which has to satisfy an extra condition due to the presence of delimited continuations
Definition \thethm (Pole).
A subset is said to be saturated or closed by anti-reduction whenever for all , we have:
[TABLE]
It is said to be closed by store extension if whenever is in , for any store extending , is also in :
[TABLE]
It is said to be closed under delimited continuations if whenever (resp. ) is in , then {\mbox{\langle}}{\mu{{\hat{{{\texttt{t}\!\texttt{p}}}}}}.c}{|\!|}{e}\mbox{\rangle}\tau (resp .{\mbox{\langle}}{V}{|\!|}{{\tilde{\mu}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}.c}\mbox{\rangle}\tau) belongs to :
[TABLE]
[TABLE]
A pole is defined as any subset of that is closed by anti-reduction, by store extension and under delimited continuations.
Proposition \thethm.
The set is a pole.
Proof.
The first two conditions are already verified for the -calculus [55]. The third one is straightforward, since if a closure {\mbox{\langle}}{\mu{{\hat{{{\texttt{t}\!\texttt{p}}}}}}.c}{|\!|}{e}\mbox{\rangle}\tau is not normalizing, it is easy to verify that is not normalizing either. Roughly, there is only two possible reduction steps for a command {\mbox{\langle}}{\mu{{\hat{{{\texttt{t}\!\texttt{p}}}}}}.c}{|\!|}{e}\mbox{\rangle}\tau: either it reduces to {\mbox{\langle}}{\mu{{\hat{{{\texttt{t}\!\texttt{p}}}}}}.c^{\prime}}{|\!|}{e}\mbox{\rangle}\tau^{\prime}, in which case also reduces to a closure which is almost ; or is of the shape {\mbox{\langle}}{p}{|\!|}{{\hat{{{\texttt{t}\!\texttt{p}}}}}}\mbox{\rangle} and it reduces to . In both cases, if {\mbox{\langle}}{\mu{{\hat{{{\texttt{t}\!\texttt{p}}}}}}.c}{|\!|}{e}\mbox{\rangle}\tau can reduce, so can . The same reasoning allows us to show that if normalizes, then so does {\mbox{\langle}}{V}{|\!|}{{\tilde{\mu}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}.c}\mbox{\rangle}\tau for any value . ∎
We finally recall the definition of the orthogonality relation w.r.t. a pole, which is identical to the one for the -calculus:
Definition \thethm (Orthogonality).
Given a pole , we say that a proof-in-store is orthogonal to a context-in-store and write if and are compatible and {\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}\overline{\tau\tau^{\prime}}\in{\bot\!\!\!\bot}. The orthogonality between terms and co-terms is defined identically.
We are now equipped to define the realizability interpretation of dLPA. Firstly, in order to simplify the treatment of coinductive formulas, we extend the language of formulas with second-order variables and we replace by . The typing rule for co-fixpoint operators then becomes:
[TABLE]
where has to be positive in .
Secondly, as in the interpretation of dL through Lepigre’s calculus, we introduce two new predicates, for nef proofs and for terms. This allows us to decompose the dependent products and sums into:
[TABLE]
This corresponds to the language of formulas and types defined by:
[TABLE]
and to the following inference rules:
[TABLE]
[TABLE]
These rules are exactly the same as in Lepigre’s calculus [47] up to our stratified presentation in a sequent calculus fashion, and modulo our syntactic restriction to nef proofs instead of his semantical restriction. It is a straightforward verification to check that the typability is maintained through the decomposition of dependent products and sums.
Another similarity with Lepigre’s realizability model is that truth/falsity values will be closed under observational equivalence of proofs and terms. To this purpose, for each store we introduce the relation , which we define as the reflexive-transitive-symmetric closure of the relation :
[TABLE]
All this being settled, it only remains to determine how to interpret coinductive formulas. While it would be natural to try to interpret them by fixpoints in the semantics, this poses difficulties for the proof of adequacy. We discuss this matter in Section 8, but as for now, we will give a simpler interpretation. We stick to the intuition that since cofix operators are lazily evaluated, they actually are realizers of every finite approximation of the (possibly infinite) coinductive formula. Consider for instance the case of a stream:
[TABLE]
of type . Such stream will produce on demand any tuple where denotes the fact that it could be any term, in particular . Therefore, should be a successful defender of the formula
[TABLE]
Since cofix operators only reduce when they are bound to a variable in front of a forcing context, it suggests interpreting the coinductive formula at level as the union of all the opponents to a finite approximation.
To this end, given a coinductive formula where is positive in , we define its finite approximations by:
[TABLE]
Since is positive in , we have for any integer and any term that . We can finally define the interpretation of coinductive formulas by:
[TABLE]
The realizability interpretation of closed formulas and types is defined in Figure 16 by induction on the structure of formulas at level , and by orthogonality at levels . When is a subset of (resp. ), we use the notation (resp. , etc.) to denote its orthogonal set restricted to :
[TABLE]
At level , closed formulas are interpreted by sets of strong forcing contexts-in-store . As explained earlier, these sets are besides closed under the relation along their component , we thus denote them by . Second-order variables are then interpreted by functions from the set of terms to and as is usual in Krivine realizability [40], for each such function we add a predicate symbol in the language.
7.3. Adequacy of the interpretation
We shall now prove the adequacy of the interpretation with respect to the type system. To this end, we need to recall a few definitions and lemmas. Since stores only contain proof terms, we need to define valuations for term variables in order to close formulas383838Alternatively, we could have modified the small-step reduction rules to include substitutions of terms.. These valuations are defined by the usual grammar:
[TABLE]
We denote by (resp. , ) the proof-in-store where all the variables (resp. ) have been substituted by the corresponding term (resp. falsity value ).
Definition \thethm.
Given a closed store , a valuation and a fixed pole , we say that the pair realizes , which we write393939Once again, we should formally write but we will omit the annotation by as often as possible. , if:
- (1)
for any , , 2. (2)
for any , , 3. (3)
for any , , 4. (4)
for any , and .
We recall two key properties of the interpretation, whose proofs are similar to the proofs for the corresponding statements in the -calculus [55]:
Lemma \thethm (Store weakening).
Let and be two stores such that , let be a typing context, let be a pole and a valuation. The following statements hold:
- (1)
** 2. (2)
If for some closed proof-in-store and formula , then . The same holds for each level of the interpretation. 3. (3)
If then .
Proposition \thethm (Monotonicity).
For any closed formula , any type and any given pole , we have the following inclusions:
[TABLE]
We can check that the interpretation is indeed defined up to the relations :
Proposition \thethm.
For any store and any valuation , the component along of the truth and falsity values defined in Figure 16 are closed under the relation :
- (1)
if and , then , 2. (2)
if and , then .
The same applies with , , etc.
Proof.
By induction on the structure of and the different levels of interpretation. The different base cases (, , ) are direct since their components along are defined modulo , the other cases are trivial inductions. ∎
We can now prove the main property of our interpretation:
Proposition \thethm (Adequacy).
The typing rules are adequate with respect to the realizability interpretation. In other words, if is a typing context, a pole, a valuation and a store such that , then the following hold:
- (1)
If is a strong value s.t. or , then . 2. (2)
If is a forcing context s.t. or , then . 3. (3)
If is a weak value s.t. or , then . 4. (4)
If is a context s.t. or , then . 5. (5)
If is a proof term s.t. or , then . 6. (6)
If is a term value s.t. , then . 7. (7)
If is a term context s.t. , then . 8. (8)
If is a term s.t. , then . 9. (9)
If is a store s.t. , then . 10. (10)
If is a command s.t. or , then . 11. (11)
If is a closure s.t. or , then .
Proof.
The proof is done by induction on the typing derivation such as given in the system extended with the small-step reduction . Most of the cases correspond to the proof of adequacy for the interpretation of the -calculus, so that we only give the most interesting cases. To lighten the notations, we omit the annotation by the valuation whenever it is possible.
• Case .
We recall the typing rule through the decomposition of dependent sums:
[TABLE]
By induction hypothesis, we obtain that and . Consider thus any context-in-store such that and are compatible, and let us denote by the union . We have:
[TABLE]
so that by anti-reduction, we need to show that {\tilde{\mu}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}.{\mbox{\langle}}{t}{|\!|}{\tilde{\mu}x.{\mbox{\langle}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}{|\!|}{{\tilde{\mu}}a.{\mbox{\langle}}{(x,a)}{|\!|}{e}\mbox{\rangle}}\mbox{\rangle}}\mbox{\rangle}\in\|A[u]\|_{e}. Let us then consider a value-in-store such that and are compatible, and let us denote by the union . By closure under delimited continuations, to show that {\mbox{\langle}}{V}{|\!|}{{\tilde{\mu}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}.{\mbox{\langle}}{t}{|\!|}{\tilde{\mu}x.{\mbox{\langle}}{{\check{{{\texttt{t}\!\texttt{p}}}}}}{|\!|}{{\tilde{\mu}}a.{\mbox{\langle}}{(x,a)}{|\!|}{e}\mbox{\rangle}}\mbox{\rangle}}\mbox{\rangle}}\mbox{\rangle}_{p}\tau_{1} is in the pole it is enough to show that the closure {\mbox{\langle}}{t}{|\!|}{\tilde{\mu}x.{\mbox{\langle}}{V}{|\!|}{{\tilde{\mu}}a.{\mbox{\langle}}{(x,a)}{|\!|}{e}\mbox{\rangle}}\mbox{\rangle}}\mbox{\rangle}\tau_{1} is in ,. Thus it suffices to show that the coterm-in-store (\tilde{\mu}x.{\mbox{\langle}}{V}{|\!|}{{\tilde{\mu}}a.{\mbox{\langle}}{(x,a)}{|\!|}{e}\mbox{\rangle}}\mbox{\rangle}|\tau_{1}) is in .
Consider a term value-in-store , such that and are compatible, and let us denote by the union . We have:
[TABLE]
It is now easy to check that and to conclude, using Section 7.3 to get , that this closure is finally in the pole.
• Case ,.
These cases are direct consequences of Section 7.3 since if are two formulas such that , in particular and thus .
• Case ,.
The case for is trivial, while it is trivial to show that ({\tilde{\mu}}\leavevmode\resizebox{3.33333pt}{0.0pt}{=}.{\mbox{\langle}}{p}{|\!|}{e}\mbox{\rangle}|\tau) is in if and . Indeed, either and thus (Section 7.3, or and .
• Case .
This case is standard in a call-by-value language with value restriction. We recall the typing rule:
[TABLE]
The induction hypothesis gives us that is in for any valuation . Then for any , we have so that . Therefore, if belongs to , we have by definition that .
• Case .
We recall the typing rule:
[TABLE]
We want to show that , let us then consider such that and are compatible, and let us denote by the union . By induction hypothesis, we have404040Recall that any term of type can be given the type . and we have:
[TABLE]
so that by anti-reduction and closure under delimited continuations, it is enough to show that the coterm-in-store (\tilde{\mu}y.{\mbox{\langle}}{a}{|\!|}{e}\mbox{\rangle}[a:=\texttt{fix}^{y}_{bx}[p_{0}\,|\,p_{S}]]|\tau_{0}) is in . Let us then consider such that and are compatible, and let us denote by the union . By definition, for some and , and we have:
[TABLE]
We conclude by showing by induction on the natural numbers that for any , the value-in-store is in . Let us consider such that the store and are compatible, and let us denote by their union.
- •
If , we have:
[TABLE]
We conclude by anti-reduction and the induction hypothesis for , since it is easy to show that ({\tilde{\mu}}a.{\mbox{\langle}}{a}{|\!|}{f}\mbox{\rangle}\tau^{\prime}_{2}|\tau_{2})\in\|A[0]\|_{e}.
- •
If , we have:
[TABLE]
Since we have by induction that is in , we can conclude by anti-reduction, using the induction hypothesis for and the fact that ({\tilde{\mu}}a.{\mbox{\langle}}{a}{|\!|}{f}\mbox{\rangle}\tau^{\prime}_{2}|\tau_{2}) belongs to .
• Case .
We recall the typing rule:
[TABLE]
We want to show that , let us then consider such that and are compatible, and let us denote by the union . By induction hypothesis, we have and we have:
[TABLE]
so that by anti-reduction and closure under delimited continuations, it is enough to show that the coterm-in-store (\tilde{\mu}y.{\mbox{\langle}}{a}{|\!|}{e}\mbox{\rangle}[a:={\texttt{cofix}}^{y}_{bx}{[p]}]|\tau_{0}) is in . Let us then consider such that and are compatible, and let us denote by the union . We have:
[TABLE]
It suffices to show now that the value-in store is in . By definition, we have:
[TABLE]
We conclude by showing by induction on the natural numbers that for any and any , the value-in-store is in .
The case is trivial since . Let then be an integer and any be a term value. Let us consider such that and are compatible, and let us denote by their union. By definition, we have:
[TABLE]
It is straightforward to check, using the induction hypothesis for , that is in . Thus we deduce by induction hypothesis for , denoting by the function , that:
[TABLE]
It only remains to show that ({\tilde{\mu}}a.{\mbox{\langle}}{a}{|\!|}{f}\mbox{\rangle}\tau^{\prime}_{2}|\tau_{2})\in\|F^{n+1}_{A,V_{t}}\|_{e}, which is trivial from the hypothesis for . ∎
We can finally deduce that dLPA is normalizing and sound.
Theorem \thethm (Normalization).
If , then is normalizable.
Proof.
Direct consequence of Sections 7.2 and 7.3. ∎
Theorem \thethm (Consistency).
\nvdash_{\text{{dLPA\textsuperscript{\omega}}}}p:\bot**
Proof.
Assume there is such a proof , by adequacy is in for any pole. Yet, the set is a valid pole, and with this pole, , which is absurd. ∎
8. About the interpretation of coinductive formulas
While our realizability interpretation give us a proof of normalization and soundness for dLPA, it has two aspects that we should discuss. First, regarding the small-step reduction system, one could have expected the lowest level of interpretation to be instead of . Moreover, if we observe our definition, we notice that most of the cases of are in fact defined by orthogonality to a subset of strong values. Indeed, except for coinductive formulas, we could indeed have defined instead an interpretation of formulas at level and then the interpretation by orthogonality:
[TABLE]
If this definition is somewhat more natural, it poses a problem for the definition of coinductive formulas. Indeed, there is a priori no strong value in the orthogonal of , which is:
[TABLE]
For instance, consider again the case of a stream of type , a strong value in the intersection should be in every , which is not possible due to the finiteness of terms414141Yet, it might possible to consider interpretation with infinite proof terms, the proof of adequacy for proofs and contexts (which are finite) will still work exactly the same. However, another problem will arise for the adequacy of the cofix operator. Indeed, with the interpretation above, we would obtain the inclusion:
which is strict in general. By orthogonality, this gives us that , while the proof of adequacy only proves that belongs to the latter set.. Thus, the definition would give .
Interestingly, and this is the second aspect that we shall discuss here, we could have defined instead the truth value of coinductive formulas directly by :
[TABLE]
Let us sketch the proof that such a definition is well-founded. We consider the language of formulas without coinductive formulas and extended with formulas of the shape where are parameters. At level , closed formulas are interpreted by sets of strong values-in-store , and as we already observed, these sets are besides closed under the relation along their component . If is a formula whose only free variable is , the function which associates to each term the set is thus a function from to , let us denote the set of these functions by .
Proposition \thethm.
The set is a complete lattice with respect to the order defined by:
[TABLE]
Proof.
Trivial since the order on functions is defined pointwise and the co-domain is itself a complete lattice. ∎
We define valuations, which we write , as functions mapping each parameter to a function . We then define the interpretations of formulas with parameters exactly as above with the additional rule424242Observe that this rule is exactly the same as in the previous section (see Figure 16).:
[TABLE]
Let us fix a formula which has one free variable and a parameter such that sub-formulas of the shape only occur in positive positions in .
Lemma \thethm.
Let is a formula without parameters whose only free variable is , and let be a valuation which maps to the function . Then
Proof.
By induction on the structure of , all cases are trivial, and this is true for the basic case :
[TABLE]
∎
Let us now define as the following function:
[TABLE]
Proposition \thethm.
The function is monotone.
Proof.
By induction on the structure of , where can only occur in positive positions. The case is trivial, and it is easy to check that truth values are monotonic with respect to the interpretation of formulas in positive positions, while falsity values are anti-monotonic. ∎
We can thus apply Knaster-Tarski theorem to , and we denote by its greatest fixpoint. We can now define:
[TABLE]
This definition satisfies the expected equality:
Proposition \thethm.
We have:
[TABLE]
Proof.
Observe first that by definition, the formula satisfies the hypotheses of Section 8 and that . Then we can deduce :
[TABLE]
∎
Back to the original language, it only remains to define as the set that we just defined. This concludes our proof that the interpretation of coinductive formulas through the equation in Section 8 is well-founded.
We could also have done the same reasoning with the interpretation from the previous section, by defining as the set of functions from to . The function , which is again monotonic, is then:
[TABLE]
We recognize here the definition of the formula . Defining as the function and we have:
[TABLE]
However, in both cases (defining primitively the interpretation at level or ), this definition does not allow us to prove434343To be honest, we should rather say that we could not manage to find a proof, and that we would welcome any suggestion from insightful readers. the adequacy of the rule. In the case of an interpretation defined at level , the best that we can do is to show that for any , is a post-fixpoint since for any term , we have:
[TABLE]
With defined as the greatest fixpoint of , for any term and any we have the inclusion and thus:
[TABLE]
By orthogonality, we get:
[TABLE]
and thus our proof of adequacy from the last section is not enough to conclude that . For this, we would need to prove that the inclusion is an equality. An alternative to this would be to show that the function is a fixpoint for . In that case, we could stick to this definition and happily conclude that it satisfies the equation:
[TABLE]
This would be the case if the function was Scott-continuous on (which is a dcpo), since we could then apply Kleene fixed-point theorem444444In fact, Cousot and Cousot proved a constructive version of Kleene fixed-point theorem which states that without any continuity requirement, the transfinite sequence is stationary [13]. Yet, we doubt that the gain of the desired equality is worth a transfinite definition of the realizability interpretation. to prove that is the stationary limit of . However, is not Scott-continuous454545In fact, this is nonetheless a good news about our interpretation. Indeed, it is well-know that the more “regular” a model is, the less interesting it is. For instance, Streicher showed that the realizability model induced by Scott domains (using it as a realizability structure) was not only a forcing model by also equivalent to the ground model.
(the definition of falsity values involves double-orthogonal sets which do not preserve supremums), and this does not apply.
9. Conclusion and perspectives
9.1. Conclusion
At the end of the day, we met our main objective, namely proving the soundness and the normalization of a language which includes proof terms for dependent and countable choice in a classical setting. This language, which we called dLPA, provides us with the same computational features as dPA but in a sequent calculus fashion. These computational features allow dLPA to internalize the realizability approach of [9, 19] as a direct proofs-as-programs interpretation: both proof terms for countable and dependent choices furnish a lazy witness for the ideal choice function which is evaluated on demand. This interpretation is in line with the slogan that with new programing principles—here the lazy evaluation and the co-inductive objects—come new reasoning principles—here the axioms and .
Interestingly, in our search for a proof of normalization for dLPA, we developed novel tools to study these side effects and dependent types in presence of classical logic. On the one hand, we set out in [54] the difficulties related to the definition of a sequent calculus with dependent types. On the other hand, building on [55], we developed a variant of Krivine realizability adapted to a lazy calculus where delayed substitutions are stored in an explicit environment. The sound combination of both frameworks led us to the definition of dLPA together with its realizability interpretation.
9.2. Krivine’s interpretations of dependent choice
The computational content we give to the axiom of dependent choice is pretty different of Krivine’s usual realizer of the same [39]. Indeed, our proof uses dependent types to get witnesses of existential formulas, and we represent choice functions through the lazily evaluated stream of their values. A similar idea can also be found in NuPrl BITT type theory, where choice sequences are used in place of functions [12]. In turn, Krivine realizes a statement which is logically equivalent to the axiom of dependent choice thanks to the instruction quote, which injectively associates a natural number to each closed -term. In a more recent work [44], Krivine proposes a realizability model which has a bar-recursor and where the axiom of dependent choice is realized using the bar-recursion. This realizability model satisfies the continuum hypothesis and many more properties, in particular the real numbers have the same properties as in the ground model. However, the very structure of this model, where is of cardinal (in particular infinite streams of integer are terms), makes it incompatible with quote.
It is clear that the three approaches are different in terms of programming languages. Nonetheless, it could be interesting to compare them from the point of view of the realizability models they give rise to. In particular, our analysis of the interpretation of co-inductive formulas may suggest that the interest of lazy co-fixpoints is precisely to approximate the limit situation where has infinite objects.
9.3. Reduction of the consistency of classical arithmetic in
finite types with dependent choice to the consistency of second-order arithmetic
The standard approach to the computational content of classical dependent choice in the classical arithmetic in finite types is via realizability as initiated by Spector [67] in the context of Gödel’s functional interpretation, and later adapted to the context of modified realizability by Berardi et al [9]. The aforementioned works of Krivine [39, 44] in the different settings of PA2 and ZFε also give realizers of dependent choice. In all these approaches, the correctness of the realizer, which implies consistency of the system, is itself justified by a use at the meta-level of a principle classically equivalent to dependent choice (dependent choice itself in [39], bar induction or update induction [10] in the case of [67, 9].).
Our approach is here different, since we directly interpret proofs of dependent choice in classical arithmetic computationally. Besides, the structure of our realizability interpretation for dLPA suggests the definition of a typed CPS to an extension of system 464646See [52, Chapitre 8] for further details., but it is not clear whether its consistency is itself conservative or not over system . Ultimately, we would be interested in a computational reduction of the consistency of dPA or dLPA to the one of PA2, that is to the consistency of second-order arithmetic. While it is well-known that is conservative over second-order arithmetic with full comprehension (see [66, Theorem VII.6.20]), it would nevertheless be very interesting to have such a direct computational reduction. The converse direction has been recently studied by Valentin Blot, who presented in [11] a translation of System F into a simply-typed total language with a variant of bar recursion.
9.4. The axiom of choice
The computational content of the axiom of countable and dependent choices being understood, it is natural to wonder whether our approach extends to the full axiom of choice. To that end, the main difficulty seems to be related to the memoization technique we use: in both proof terms for and DC, the choice function ranges over the domain of natural numbers, hence it is easy to know whether the computation for a given has already been performed. In turn, when considering an arbitrary domain as is the case for the full axiom of choice AC, if the equality on is not decidable, we might not be able to know whether the computation for has already been done or not. At first sight, our approach seems to extend to any type with decidable equality, but handling arbitrary types with undecidable equality would require a more careful treatment of equality during the memoization process.
On a similar line of work, there exists a wide literature on different form of choices (e.g., the axiom of dependent choice, König’s Lemma), as well as on bar induction principles or the Fan theorem, which can be seen as their contrapositives. Recently, Herbelin and Brede undertook a systematical classification of these principles, including also the Ultrafilter Theorem in the picture, aiming at highlighting dualities and studying logical equivalences in different frameworks (classical, intuitionistic and linear logic) [30]. In that regard, having a precise understanding of the computational content of each of these principles as well as on the translations existing between them is an interesting perspective, for which this work or Blot’s work on bar induction [11] might be the first steps.
Acknowledgment
The author warmly thanks Hugo Herbelin for numerous discussions and attentive reading of this work during his PhD years, and Amina Doumane for her helpful comments on coinductive fixpoints which led to the Section 8 of this paper.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming , ICFP ’14, pages 363–376, New York, NY, USA, 2014. ACM. URL: http://doi.acm.org/10.1145/2628136.2628154 , doi:10.1145/2628136.2628154 . · doi ↗
- 2[2] A. W. Appel. Compiling with Continuations . Cambridge University Press, New York, NY, USA, 1992.
- 3[3] Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin. Classical call-by-need sequent calculi: The unity of semantic artifacts. In T. Schrijvers and P. Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings , Lecture Notes in Computer Science, pages 32–46. Springer, 2012. doi:10.1007/978-3-642-29822-6 . · doi ↗
- 4[4] Z. M. Ariola, H. Herbelin, and A. Sabry. A type-theoretic foundation of delimited continuations. Higher-Order and Symbolic Computation , 22(3):233–273, 2009. URL: http://dx.doi.org/10.1007/s 10990-007-9006-0 , doi:10.1007/s 10990-007-9006-0 . · doi ↗
- 5[5] Z. M. Ariola, H. Herbelin, and A. Saurin. Classical call-by-need and duality. In C.-H. L. Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings , volume 6690 of Lecture Notes in Computer Science , pages 27–44. Springer, 2011. doi:10.1007/978-3-642-21691-6\_6 . · doi ↗
- 6[6] S. Banach and A. Tarski. Sur la décomposition des ensembles de points en parties respectivement congruentes. Fundamenta Mathematicae , 6(1):244–277, 1924.
- 7[7] F. Barbanera and S. Berardi. A symmetric lambda calculus for classical program extraction. Inf. Comput. , 125(2):103–117, 1996.
- 8[8] G. Barthe and T. Uustalu. Cps translating inductive and coinductive types. In Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation , PEPM ’02, pages 131–142, New York, NY, USA, 2002. ACM. URL: http://doi.acm.org/10.1145/503032.503043 , doi:10.1145/503032.503043 . · doi ↗