A big-step operational semantics via non-idempotent intersection types 

What is a programming language ?

   A programming language is a set of sequences of symbols where each of these sequences describes more or less an action or a computation. Such sequence of symbols is called a program of this programming language. It is needed to build computer software. For real world programs, these sequences of symbols are written in one or more files in the computer. The most obvious programming language is the machine language which can be directly interpreted by a computer. There are two main reasons why most software are not written in the machine language:
• It is really hard to write anything with it, even small programs.
• There exists a different machine language for each computer architecture. Therefore, we may need to rewrite the entire program if we want to port it on an different platform. Therefore, almost every other software are written in programming languages that are more human readable, more scalable, more portable, more machine-independent and, sometimes, safer. Programs written in these languages cannot be  directly interpreted by a computer.
• There can be a software that transforms a program written in some language to a program written in the machine language. This software is called a compiler.
• There can be a software that interpret a program written in some language and do what the program is supposed to do. This is called an interpreter. Of course, things can be a little more complicated than that:
• A program in some language can be compiled to another language which is not the machine language and, to be executed, the new program obtained requires an interpreter.
• Compilation can be in several steps: the program can be written in several intermediate languages until we reach the target language. This is useful when creating a programming language and its compiler to not have to worry about technical problems that have already been solved by more competent people. Solving these problems ourselves may be called reinventing the wheel. For examples, lots of high-level programming language are compiled to a language called C. Most compiler can compile C to assembler which is a programming language that is just above the machine language in terms of abstraction. Finally, the assembler program can be compiled to machine language and then, we can execute it. Therefore, if someone wants to write the compiler of a new high-level language, they just have to be able to compile it to C, and then they can have quite fast executables. When writing a program, someone might wonder what its meaning is or what it does. We usually have these two approaches:
• We give an intuitive meaning to each construction of the language. The meaning given is not very different from what someone would have written if we were trying to explain in a tutorial or a lesson what a construction does. Of course, this has no mathematical value.
• We say that the meaning of a program is what it does when executed (after compilation if any). This is also not usually suited to do mathematical reasoning on programs. Therefore, if we want to have mathematical results about programs (such as correctness), we need to define formally the meaning of a program. This is called the semantics of a programming language. Ensuring the correctness of a program is useful when there are lives as stake (programs in a plane, etc. . . ) or even when there is money at stake (for example, the crash of a program used in a bank). Even when it is just saving debugging time (time spent searching and correcting mistakes that occurs during the execution of a program) it is well worth it. There are two main approaches:
• The operational semantics: There are syntactic rules (usually reduction rules) that describe what a program does. In some ways, it is paraphrasing the interpreter.
• The denotational semantics: We create a mathematical object and we use it as a model of the programming language: A program is interpreted as “something” in this mathematical object (for example, it can be an element of a set or a morphism in a category). For a given programming language, there are usually lots of possible models. The difference between these two is similar to the difference between “what it is” (denotational semantics) and “what it does” (operational semantics). When studying semantics, we usually start with a minimalistic/toy language. Most of the time, when we are complexifying the language we can easily extend and adapt the definitions, results and proofs. The λ-calculus is one of the most well known minimalistic languages.

What is logic ?

   Set Theory has imposed itself as the main language for doing mathematics. However, at the beginning of the 20th century, mathematicians realized that certain reasoning with sets could lead to contradictions (for example, Russel’s paradox [vH02]: the set of all the sets is not a set). Therefore, it seemed necessary to sanitize the mathematical foundations: deciding what was a valid (or sound) proof and what was not. Of course, to do this, we need to give a mathematical definition of a proof. Such proofs can be represented in a computer. Hence, we can write a Proof Assistant: we write a proof in a computer, and the Proof Assistant checks whether or not the proof is sound. Also, the writing of some parts of the proofs can be automated.

What is intuitionistic logic ?

  Alan Turing proved [Tur36] that some functions (defined mathematically) could not be calculated by a computer. It is not a question of time or memory available. It turns out that the reason we are in this situation is that we can use in mathematics the principle of excluded middle (for every formula A, A is true or the negation of A is true). By dropping excluded middle we we are in a new logic called intuitionistic logic and when we have excluded middle we says that we are in classical logic. The idea of intuitionistic logic is from Brouwer [vH02] and has been developed by Heyting [Hey71]. One of the most modern way of defining intuitionistic logic is Topos Theory: an Lawvere’s Elementary Topos [LS09] can be used as a model of intuitionistic logic. On the one hand, we can prove fewer theorems in intuitionistic logic (compared to classical logic). On the other hand:
• A definition (resp. theorem) that is used (resp. holds) in classical logic might not be intuitionistically friendly (resp. be proved in intuitionistic logic). However, it may be possible to have a definition (resp. theorem) that is equivalent in classical logic but is also intuitionistically friendly (resp. holds in intuitionistic logic) and not more complicated than the original one.
• When something is proved in intuitionistic logic it gives more information than in classical logic: the proof is constructive. In particular, if we can define a function in intuitionistic logic, then this function is computable. This is the reason intuitionistic logic is also called constructive logic. Moreover, we can find a correspondence between intuitionistic proofs and functional programs: This is called the Curry-Howard correspondence [GLT89].

About the λ-calculus

   The λ-calculus is a minimalistic programming language created by Church [Chu85]. In this programming language there is no distinction between programs and data. A program M in the pure λ-calculus is called a λ-term and is either:
• A variable x, y, z, . . .
• An abstraction of the form λx.M. Intuitively, λx.M describes the function that maps x to M. For example, λx.x is the identity function.
• An application of the form MN where M is the function and N is the argument. The fact that this programming language looks simplistic can be balanced as follows:
• It is possible to encode in this calculus, usual data structures (such as booleans, integers, lists, trees, etc . . . ) and more advanced constructions. For example, the integer n is encoded as the λ-term λf.λx.f nx (with f 0x = x and f n+1x = f(f nx)). We can also encode recursion and then prove that the λcalculus is Turing complete: anything that can be “computed” can be written in λ-calculus. This is both a blessing and a curse.
• It is possible to enrich the λ-calculus with usual data structures and more advanced constructions expressed as new primitives of the language rather as encodings. Most definitions, theorems and proofs of the λ-calculus without this enrichment (also called the pure λ-calculus) can be adapted. By taking a step further, we can design real world programming languages based on the λ-calculus. These languages are called functional programming languages. OCaml and Haskell are among those. The syntax of λ-calculus is very simple, but we still have to define what a λ-term formally means. This is defining the semantics of the λ-calculus. The main idea is that (λx.M)N has the same meaning as M{x := N} where M{x := N} is M where we “replaced every x in M by N”. Moreover, going from (λx.M)N to M{x := N} is a step in the computation. An occurrence (λx.M1)M2 inside a term M is called a β-redex; and replacing an occurrence of (λx.M1)M2 by M1{x := M2} is called a β-reduction. When we cannot do any β-reduction, the computation is over and the term M that cannot be reduced is the result of the computation. If from a term M we can reach a term M0 that cannot be reduced, then M0 is called the normal form of M. When defining this semantics formally, several questions and problems arise:
• We have to formally define what the term M{x := N}.is. The definition is quite subtle and relies on an equivalence relation that identifies some terms (like λx.x and λy.y which both describe the identity function). This relation is called α-equivalence. Usually, λ-terms are considered modulo α-equivalence. The easiest way of defining and manipulating this equivalence is probably by using nominal logic techniques (see Section 1.4).
• If there are several β-redexes in a term M, then there are several ways of doing a β-reduction. Therefore, the normal form does not seem to always be unique. Actually, it is unique, and it is a corollary of the confluence property: If M can reach M1 and M can reach M2 then there exists M3 such that M17 and M2 can reach M3. It is possible to prove confluence by using something called parallel reductions [CR36].
• The question about whether or not the normal form exists: Some λ-terms do not have a normal form. For example, (λx.xx)(λx.xx) can only reduce to itself. By the fact that the λ-calculus is Turing complete, we cannot avoid the fact that the computation of some terms does not terminate and we cannot even decide by a program if a term does terminate or not (that would give a solution to the Halting Problem and contradict Turing’s result[Tur36]). Even when the normal form exists, by the fact that a λ-term can be reduced several ways, we can consider the two following cases:
– There exists a β-reduction sequence to the normal form. This is called weak normalisation.
– We do not have an infinite β-reduction sequence: Any β-reduction strategy terminates. This is called strong normalisation. By the fact that a λ-terms has a finite number of β-redexes, strong normalisation of M is equivalent to having a longest reduction sequences from M. For example, (λy.z)((λx.xx)(λy.xx)) (with y 6= z) is weakly normalising (the normal form is z) but is not strongly normalising (it reduces to itself). In this thesis, we are more interested in the strong normalisation property. We have described the operational semantics of the λ-calculus. It is also possible to give a devotional semantics. For example, we can interpret each λ term as an element of a Scott Domain [Sco82a] (which is a partially ordered set that satisfies some properties). If we want to easily manipulate λ-terms and ensure they have some properties (such as strong normalisation), we can use types. If M has some type A (written M : A) then, by a Soundness Theorem, we can prove that M has some  properties described by A. The typing judgment is defined with induction rules. The most basic typing system for λ-calculus are the simple types where a type is either a constant τ or an arrow A → B. If we have M : A → B, it means that M is a “function” that goes from A to B. The main idea is that:
• If M : A → B and N : A, then MN : B.
• If M : B with x : A, then λx.M : A → B.
Actually, more formally, the typing judgments are of the form Γ ` M : A where Γ is something called a context and indicates the type of each variables in M. Simple types have the following interesting property: If M is typable, then M is strongly normalising. It is possible to enrich the types with an intersection construction: If A is a type and B is a type, then A ∩ B is a type. The main idea is that if M : A and M : B, then M : A ∩ B. Usually, we have an equivalence relation ≈ on types (to have associativity, commutativity of intersection etc . . . ). We also usually have A ∩ A ≈ A: the intersection is idempotent. In most of the thesis, we are going to drop the idempotency of intersection and we are going to see how it can give more information about quantitative properties on a λ-term: If M : A ∩ A, then M will be used twice as a program of type A.

Characterisation of the typing system

   In Section 4.3.1, we prove Subject Reduction and Soundness (typable implies strongly normalising). In Section 4.3.2, we prove Subject Expansion and Completeness (strongly normalising implies typable).
Soundness As usual for the proof of Subject Reduction, we first prove a substitution lemma: Lemma 29 (Substitution lemma).
If Γ, x : U ` n M : A and ∆ ` m N : U, then there exists Γ 0 such that Γ 0 ≈ Γ ∩ ∆ and Γ 0 ` n+m M{x := N} : A. Proof. By induction on Γ, x : U ` M : A. The measure of the final typing tree is n + m because, by the fact that the intersection types are non-idempotent, this proof does not do any duplications. See Appendix A.
Theorem 14 (Subject Reduction). If Γ ` n M : A and M →β M0 , then there exist Γ 0 and n 0 such that Γ ⊆ Γ 0 , n > n0 and Γ 0 ` n 0 M0 : A. Proof. First by induction on M →β M0 , then by induction on A. See Appendix A. The rules (F un2) and (App2) do not create any problem because we have to use the rules (F un1) and (App1) to type a β-redex.
In Theorem 14, we have n > n0 because, by the fact that types are nonidempotent, we do not do any duplications in the proof of Subject Reduction. Therefore, by Subject Reduction, for each β-reduction, the measure of the typing tree strictly decreases and then, we have Soundness as a corollary.

Table des matières

Acknowledgements
1 Introduction 
1.1 Generalities
1.2 About the λ-calculus 
1.3 Brief description of the Chapters 
1.4 Introduction to α-equivalence
2 A simple typing system of non-idempotent intersection types for pure λ-calculus 
2.1 Introduction
2.2 Syntax and operational semantics 
2.3 The typing system
2.3.1 Types
2.3.2 Contexts
2.3.3 Rules
2.4 Soundness
2.5 Semantics and applications 
2.5.1 Denotational semantics
2.5.2 Example: System F
2.6 Completeness
2.7 Conclusion 
3 Intersection types with explicit substitutions 
3.1 Introduction
3.2 Syntax
3.3 Typing judgments
3.4 Soundness
3.5 Special property of typing trees: Optimality
3.6 Completeness 
3.7 Complexity 
3.8 Conclusion
4 A big-step operational semantics via non-idempotent intersection types 
4.1 Introduction 
4.2 Basic definitions and properties
4.2.1 Syntax
4.2.2 Intersection types and contexts
4.2.3 Typing system
4.3 Characterisation of the typing system
4.3.1 Soundness
4.3.2 Completeness
4.4 Refined soundness
4.4.1 Complexity
4.4.2 Viewing optimal typing as a big-step semantics
4.5 Alternative systems
4.5.1 Variant with no information about the normal form
4.5.2 Obtaining the exact normal form
4.6 Conclusion 
5 Strong normalisation in a calculus with constructors and fixpoints via non-idempotent intersection types 
5.1 Introduction
5.2 Calculus
5.2.1 Definition of the calculus
5.2.2 Refined notion of reduction
5.3 Strong normalisation 
5.3.1 Intersection types
5.3.2 Soundness
5.3.3 Completeness
5.4 Conclusion
5.5 Confluence
5.6 Example in Caml 
6 Conclusion 
A Full proofs
B A simple presentation of de Bruijn indices
B.1 Definitions
B.2 Binding
B.3 Substitutions
B.4 β-reduction
B.5 Semantics

Télécharger le rapport complet