tutorial-tbt

Description

A tutorial on type-based termination1 2 2Gilles Barthe Benjamin Gr´egoire Colin Riba1IMDEA Software, Madrid, Spain2INRIA Sophia-Antipolis, FranceAbstract. Type-based termination is a method to enforce terminationof recursive definitions through a non-standard type system that intro-duces a notion of size for inhabitants of inductively defined types. Thepurpose of this tutorial is to provide a gentle introduction to a polymor-phically typed λ-calculus with type-based termination, and to the sizeinference algorithm which is used to guarantee automatically terminationof recursive definitions.1 IntroductionFunctional programming languages advocate the use of mathematically intuitiveconstructions to develop programs. In particular, functional programming lan-guages feature mechanisms to introduce and manipulate finite datatypes such aslists and trees, and infinite datatypes such as streams and infinite trees. Thereare two basic ingredients to manipulate elements of a datatype: case analysis,that enables to reason by analysis on the top constructor, and fixpoints, that en-able to define functions by recursion and co-recursion. Traditionally, functionalprogramming languages allow for unrestricted fixpoints, which are subsumed bythe constructionΓ,f : τ ‘ e : τΓ ‘ (letrec f = e) : ττwhose computational behavior is given by the reduction rule(letrec f = e) → e[f := (letrec f = e)]τ τUnrestricted use of fixpoints leads to typable expressions that diverge, i.e. ...

Informations

• Publié par: Vofeg
• Nombre de lectures: 8
• Langue: English

Extrait

A tutorial on type-based termination

Gilles Barthe 1 BemajnrGnioge´eri 2 Colin Riba 2 1 IMDEA Software, Madrid, Spain 2 INRIA Sophia-Antipolis, France

Abstract.Type-based termination is a method to enforce termination of recursive definitions through a non-standard type system that intro- duces a notion of size for inhabitants of inductively defined types. The purpose of this tutorial is to provide a gentle introduction to a polymor- phically typedλ-calculus with type-based termination, and to the size inference algorithm which is used to guarantee automatically termination of recursive definitions.

1 Introduction Functional programming languages advocate the use of mathematically intuitive constructions to develop programs. In particular, functional programming lan- guages feature mechanisms to introduce and manipulate finite datatypes such as lists and trees, and infinite datatypes such as streams and infinite trees. There are two basic ingredients to manipulate elements of a datatype: case analysis, that enables to reason by analysis on the top constructor, and fixpoints, that en- able to define functions by recursion and co-recursion. Traditionally, functional programming languages allow for unrestricted fixpoints, which are subsumed by the construction Γ, f:τ`e:τ Γ`(letrec τ f=e) :τ whose computational behavior is given by the reduction rule (letrec τ f=e)→e[f:= (letrec τ f=e)] Unrestricted use of fixpoints leads to typable expressions that diverge, i.e. that have an infinite reduction sequence. While non-termination is acceptable in func- tional programming languages, logical systems based on type theory must be terminating in order to guarantee coherence and decidability of equivalence be- tween terms. Thus, logical systems based on type theory seek to restrict the usage of recursive definitions to enforce termination. A standard means to enforce termination is to abandon the syntax of func- tional programming languages and to rely instead on combinators, known as recursors. Such recursors allow to define functions of typed→σ, wheredis an inductive datatype such as natural numbers of lists; more generally, the notion of inductive datatype captures in a type-theoretical setting the notion of least fix- point of a monotone operator. To guarantee termination, recursors combine case

2GillesBartheBenjaminGre´goireColinRiba analysis and structural recursion, and their reduction rules ensure that recursive calls are applied to smaller arguments. Unfortunately, recursors are not intuitive to use. Therefore, proof assistants based on type theory, such as Coq and Agda, tend to rely on an alternative approach, that maintains the syntax of functional programming languages, but imposes instead syntactic conditions that ensure termination. Restrictions concern both the typing rule and the reduction rule. Restrictions for the typing rule impose conditions, both on the typeτand on the expressione, under which recursive definitions are well-formed. Essentially, the typeτmust be of the formd→σ, wheredis an inductive datatype, as for recursors. Then, the expressionemust be of the formλx:d. bwhereb can only make recursive calls tofon arguments that are structurally smaller thanx. Finally, reductions must be restricted to the case whereeis applied to an expression of the formctfor some constructorc. While the first and third restrictions are easily enforced, it is difficult to find appropriate criteria that enforce the second restriction. A common means to ensure that recursive calls are performed on smaller arguments is to define a syntactic check on the body bof recursive calls. However, such a syntactic approach is problematic, as shall be explained in the course of this chapter. Type-based termination is an alternative approach to guarantee strong nor- malization of typable expressions through the use of a non-standard typing sys- tem in which inhabitants of inductive datatypes are given a size, which in turn is used to guarantee termination of recursive definitions. Type-based termination draws its inspiration from the set-theoretic and domain-theoretic semantics of inductive definitions, in which inductive sets are viewed as the upper limit of their approximation. In effect, type-based termination embeds these semantical intuitions into the syntax of the type theory, by letting inductive datatypes carry size annotations, and by restricting the rule for fixpoints b Γ, f:d ı →σ`e:d ı →σ Γ`(letrec d∞→σ f=e) :d ∞ →σ wheredis an inductive datatype,ıis an arbitrary (i.e. implicitly quantified b universally) size,d ı denotes theı-approximation ofd, andd ı denotes the next approximation ofd, andd ∞ denotes the inductive datatype itself. As should appear from the typing rule, termination is enforced naturally by requiring that recursive calls, that correspond to occurrences offine, can only be made to smaller elements, asfonly takes as arguments elements of typed ı . Type-based termination benefits from essential characteristics that make it an attractive means to ensure termination of recursive definitions in a typed λ-calculus, both from the point of view of the users and of the designers of the type system. First and foremost, it is intuitive and easy to grasp, since the type system simply captures the idea that a recursive definition terminates whenever the size of arguments decreases in recursive calls. As a consequence, the type system is also predictable (i.e. it is possible to havea priorian intuition as to whether a definition is correct) and transparent (i.e. it is possiblea posteriori to understand why a definition is incorrect) for users, which we view as essen-

A tutorial on type-based termination 3 tial properties of a formal system. Second, type-based termination is expressive: even for the simplest instance of type-based termination, in which the arithmetic of stages only builds on zero, successor and infinity, type-based termination is sufficiently powerful to encode many typedλ-calculi using syntactic termination criteria, and to provide precise typings for some functions that do not increase the size of their arguments (i.e. for unary functions the size of the result is smaller or equal than the size of the argument). Third, type-based termination is based on a solid theoretical foundation, namely that of approximation, which substantially simplifies in the development of realizability models. As shall be illustrated in Section3.4, there is a good match between the syntax of the type system and its semantics, which facilitates the interpretation of recursive defi- nitions in the realizability model. Fourth, type-based termination isolates in the design of the type system itself the components that are relevant for termina- tion, i.e. constructors, case analysis, and fixpoint definitions, from the remaining components, whose syntax and typing rules are unaffected. Such a separation makes type-based termination robust to language extensions, and compatible with modular verification and separate compilation. In summary, type-based termination appears as a suitable approach to guar- antee strong normalization of typable terms, which in the near future may well supplant syntactic methods that are currently in use in logical systems based on type theory. On this account, the main objective of this tutorial is to provide a gentle introduction to type-based termination. For pedagogical purposes, we start with a review of mechanisms to introduce recursive definitions in typed λand proceed to define a type system that uses type-based termination.-calculi, Then, we provide high-level proofs of the essential properties of the type system, in particular of strong normalization and of decidability of type inference; we explain the latter in great length, because of the complexity of the algorithm. We conclude with a brief examination of some possible extensions to our system, and a brief account of related work. For simplicity, we focus on a polymorphi- cally typedλ-calculus, although all of the results that we present in this chapter scale up to dependent types.

2 Computations in polymorphic type systems This section presents the basic framework of this tutorial and the main problem we want to address: having a convenient way for computing in type systems is- sued from the Curry-Howard isomorphism, while preserving crucial logical prop- erties such as subject reduction, strong normalization and coherence. We start in Sect.2.1from Girard’s SystemF, with termsla`aChurch, as presented in [12enjoys strong normalization and coherence, and]. This system can encode every inductive datatype and every function provably total in second order Peano arithmetic [12]. However, the algorithmic behavior of SystemFis unsatisfactory, since basic functions such as the predecessor function on Church’s numerals is not implementable in constant time [15], and it is more generally

4GillesBartheBenjaminGre´goireColinRiba the case of primitive recursion over all inductive datatypes, at least when the computing relation isβ-reduction [16]. Hence, from a computational point of view, it is convenient to add datatypes and recursion to SystemF, leading to SystemF rec presented in Sect.2.2. How- ever,F rec lacks both strong normalization and coherence, because of general recursion and of the ability to define non well-founded datatypes. As a first step towards a well-behaved system, we introduce in Sect.2.3the notion ofinductive datatype. Then, we recall in Sect.2.5a syntactic termina- tion criteria, which allows to retrieve strong normalization and coherence. The limitations of such criteria motivate the use of type-based termination, to be presented in Sect.3. 2.1 SystemF Types.We assume given a setV T of type variables. The setTof types is given by the abstract syntax: T::=V T |T→T|ΠV T .T Types are denoted by lower-case Greek lettersσ, τ, θ, . . .. Free and bound vari- ables are defined as usual. The capture-avoiding substitution ofτforXinσis writtenσ[X:=τ]. We letFV T (e) be the set of type variable occurring free in τ. A typeτisclosedifFV T (τ) =∅. Example 2.1. (i) The type of the polymorphic identity is Π X. X→X (ii) It is well-known that inductive datatypes can be coded into SystemF, see e.g. [12]. For instance, Peano natural numbers can be encoded asChurch’s numerals, whose type is N Ch :=Π X. X→(X→X)→X From this type, we can read that Church numerals represent the free struc- ture built from one nullary constructor (which stands for 0), and one unary constructor (which stands for the successor). (iii) The ”false” proposition is ⊥:=Π X. X

tu Terms and reductions.We assume given a setV E ={x, y, z, . . .}of(object) variables. The setEoftermsis given by the abstract syntax: E::=V E |λV E :T.E|ΛV T .E|E E|E T

A tutorial on type-based termination 5 Free and bound variables, substitution, etc. are defined as usual. The capture- avoiding substitution ofe 0 forxineis writtene[x:=e 0 ]. We letFV E (e) be the set of free term variables occurring ine. We say thateisclosedwhenFV E (e) =∅. The reduction calculus is given byβ-reduction→ β , which is defined as the compatible closure of (λx:τ. e)e 0  β e[x:=e 0 ] and (ΛX. e)τ β e[X:=τ] The relation→ β is confluent. Notation 2.2.We writee→ β n e 0 if there isk≤nsuch that e→ β . . .→ β e 0 | {z } ktimes Example 2.3. (i) The polymorphic identity isΛX. λx:X. x. (ii) The Church’s numerals are terms of the form c n :=ΛX. λx:X. λf:X→X. f n x The numeralc n encodes the natural numbernby computing iterations. Indeed, the expressionc n p fperformsniterations offonp: c n p f→ β ∗ f∙ ∙ ∙(f p) =f n p | {z } ntimes The constructors of Church’s numerals are the termsZandSdefined as: Z:=ΛX. λx:X. λf:X→X. x S:=λn:N Ch  λx. ΛX.:X. λf:X→X. f(n X x f) whereN Ch is the type of Church’s numerals defined in Ex.2.1.(ii). Given τ∈T, we can codeiteration at typeτwith the termIter τ u v n:=n τ u v. For alln, u, v∈Ewe have Iter τ u vZ→ β 2 (λx:τ. λf:τ→τ. x)u v→ β 2 u Iter τ u v(Sn)→ β 2 (λx:τ. λf:τ→τ. f( xn τ f))u v→ β 2 v(n τ u v) Hence,Iter τ u v(Sn)β-reduces in four steps tov(Iter τ u v n). Using this iter- ation scheme, every function provably total in second order Peano arithmetic can be coded in SystemF[12].tu Typing.A context is a mapΓ:V E →Tof finite domain. Givenx∈/dom(Γ) we letΓ, x:τbe the context (Γ, x:τ)(y) = def  Γ τ (y)ot fiy= erhw x ise The notationΓ, x:τalways implicitly assumes thatx /∈dom(Γ). The typing relation of SystemFis defined by the rules of Fig.1.

6GillesBartheBenjaminGr´egoireColinRiba Example 2.4. (i) The polymorphic identity of Ex.2.3.(i)can be given the type of Ex.2.1.(i): `ΛX. λx:X. x:Π X. X→X (ii) Church numerals can be given the typeN Ch : `ΛX. λx:X. λf:X→X. f n x: XΠ X.→(X→X)→X Moreover,Z:N Ch andS:N Ch →N Ch . Iteration can be typed as follows: n:N Ch , u:τ, v:τ→τ`Iter τ n u v:τ

(var) Γ, x:σ`x:σ σ (abs) Γ`λx x,Γ : : τ.e τ`e : : τ→σ (app) Γ`e:τ Γ` → ee σ 0 :σ Γ`e 0 :τ (T-abs) Γ`XΛ Γ` e. e: : σ σ.XΠ ifX /∈Γ(T-app) Γ Γ ` `e:Π [ .X X:= σ τ] e τ:σ Fig. 1.Typing rules of SystemF

ut

Some important properties.The most important properties of SystemF are subject reduction, strong normalization, and coherence. Subject reduction states that types are closed underβ-reduction. Theorem 2.5 (Subject reduction).IfΓ`e:τande→ β e 0 , then also Γ`e 0 :τ. Terms typable in SystemFenjoy a very strong computational property: they arestrongly normalizing. A term is strongly normalizing if every reduction sequence starting from it is finite. We can thus define the setSN β of strongly β-normalizing terms as being the smallest set such that ∀e.(∀e 0 . e→ β e 0 =⇒e 0 ∈SN β ) =⇒e∈SN β Strong normalization is also useful for the implementation of the language, be- cause it ensures that every reduction strategy (i.e. every way of reducing a term) is terminating. Strong normalization can be proved using the reducibility tech- nique [12], which is sketched in Sect.3.4.

A tutorial on type-based termination 7 Theorem 2.6 (Strong normalization).IfΓ`e:τthene∈SN β . We now discuss some logical properties of SystemF. It is easy to see that Γ`e:⊥impliesΓ`e τ:τfor all typeτ. According to the Curry- Howard propositions-as-types isomorphism, this means that the type⊥is the false proposition: every propositionτcan be deduced from it. Therefore, having Γ`e:⊥means that everything can be deduced fromΓ. From a logical perspective, it is crucial to ensure that there is no term of type⊥in the empty context. This property is fortunately satisfied by SystemF. It can be proved by syntactical reasoning, using subject reduction and strong normalization, but a direct reducibility argument is also possible, see Sect.3.4. Theorem 2.7 (Coherence).There is no termesuch that`e:⊥. 2.2 A polymorphic calculus with datatypes and general recursion It is well-known that SystemFhas limited computational power, e.g. it is not possible to encode in SystemFa predecessor function that computes in constant time [15Therefore, programming languages and proof assistants rely on lan-]. guages that extend theλconstants and rewrite rules. In this-calculus with new section, we discuss one such extension of SystemFaal`Church, as presented in Sect.2.1. This system, calledF rec , consists in addingdatatypesand general re- cursion to SystemF. Before giving the formal definitions, we informally present the system with some examples of datatypes. We then recall some well-known examples showing that SystemF rec lacks two of the most important properties of SystemF, namely termination and coherence. Basic features.In SystemF rec , we represent the type natural numbers using a special type constantNat. Furthermore, the language ofλ-terms is extended by two constantso:Natands:Nat→Natrepresenting the two constructors of Nat. All this information is gathered in the datatype definition: DatatypeNat:=o:Nat|s:Nat→Nat This definesNatleast type build from the nullary constructoras the oand the unary constructors. Example 2.8.We can now represent the numbernby the terms n o.ut SystemF rec of computing on datatypes. The first oneprovides two ways performs the destruction of constructor-headed terms, and allows to reason by case-analysis, similarly as in functional programming languages. For instance, we can define the predecessor function as follows: pred:=λx:Nat.case Nat xof{o⇒o |s⇒λy:Nat. y}

8GillesBartheBenjaminGr´egoireColinRiba This function is evaluated as follows: pred o→case Nat o of{o⇒o|s⇒λy:Nat. y} →o pred(sn)→case Nat (sn)of{o⇒o|s⇒λy:Nat. y} →(λy:Nat. y)n→n and is typed using the rule x:Nat`x:Natx:Nat`o:Natx:Nat`λy:Nat. y:Nat→Nat x:Nat`case Nat xof{o⇒o|s⇒λy:Nat. y}:Nat Performing a case analysis over an expressioneof typeNatmeans building an object of a given type, sayσ, by reasoning by cases on the constructors ofNat. We therefore must provide a branche o for the case ofoand a branche s for the case ofs. Ifeevaluates too, then the case-analysis evaluates toe o , and ife evaluates tosn, then the we gete s n: case σ o of{o⇒e o |s⇒e s } →e o case σ (sn)of{o⇒e o |s⇒e s } →e s n Since this case-analysis must evaluate to a term of typeσ, we must havee o :σ ande s :Nat→σ. We therefore arrive at the general rule for case-analysis over natural numbers: se (ca ) Γ`e: Γ N ` at case σ Γ eo ` f e { o o : ⇒e σ o |s Γ ⇒ ` e s e s } : :σ Nat→σ The second computing mechanism of SystemF rec isgeneral recursion. The system is equipped by a general fixpoint operator (letrec τ f=e), which is typed by the rule (rec) Γ, f:τ`e ) : τ τ Γ`(letrec τ f=e: and which reduces as follows: (letrec τ f=e)→e[f:= (letrec τ f=e)] This allows to encode efficiently primitive recursion over natural numbers. Example2.9(G¨odel’sSystemT).InF rec , we can encode primitive recursion on natural numbers as follows: rec:=ΛX.(letrec Nat→X rec=λx:Nat. λu:X. λv:Nat→X→X. case X xof{o⇒u |s⇒λy:Nat. v y(recy u v)} ) :Π X.Nat→(Nat→X→X)→X→X Therefore, writingrec τ for the headβ-reduct ofrecτ, we have the following reductions, which are performed in a constant number of steps: rec τ ou v→ 6 uandrec τ (sn)u v→ 6 v n(rec τ n u v) ut

A tutorial on type-based termination 9 Functions defined by primitive recursion can also be directly coded inF rec . Take for instance the addition and subtraction onNat. Example 2.10 (Addition of two natural numbers). plus:= (letrec Nat→Nat→Nat plus=λx:Nat. λy:Nat. case Nat xof{o⇒y |s⇒λx 0 :Nat.s(plusx 0 y)} ) :Nat→Nat→Nat

ut

Example 2.11 (Subtraction of natural numbers). minus:= (letrec Nat→Nat→Nat ms=λx:Nat. λy:Nat. case Nat xof{o⇒x |s⇒λx 0 :Nat.case Nat yof{o⇒x |s⇒λy 0 :Nat.msx 0 y 0 } } ) :Nat→Nat→Nat tu Since general fixpoints are allowed, we can also give definitions where recur- sive calls are not performed on structurally smaller terms. This is the case of the Euclidean division on natural numbers. We will see in Sect.3that this function terminates provably with typed-based termination. Example 2.12 (Euclidean division).This program for the Euclidean division de- pends on the functionminus. It is not typable in systems with a syntactic guard predicate, as, syntactically, (minusx 0 y) is not properly structurally smaller than xin the program below. div:= (letrec Nat→Nat→Nat div=λx:Nat. λy:Nat. case Nat xof{o⇒o |s⇒λx 0 :Nat.s(div(minusx 0 y)y)} ) :Nat→Nat→Nat

tu Polymorphic datatypes.SystemF rec features polymorphic datatypes, such as polymorphic lists whose constructors,nilandcons, are typed as follows: nil:Π X.ListXcons:Π X. X→ListX→ListX Formally, the datatype of lists is defined as follows: DatatypeListX:=nil:ListX|cons:X→ListX→ListX

10GillesBartheBenjaminGr´egoireColinRiba List are eliminated using case-analysis, along a pattern similar to that of natural numbers. The case-analysis of polymorphic lists is performed on one particular instantiation of the datatype: (case) Γ`e:Listτ Γ`e nil :σ Γ`e cons :τ→Listτ→σ Γ`case σ eof{nil⇒e nil |cons⇒e cons }:σ This means thatnilτcan be the subject of case-analysis, whilenilcan not. Accordingly, the branches of the case-analysis must be typable with the corre- sponding instantiation of the polymorphic type:e cons takes an argument of type Listτ, but not of typeΠ X.ListX. The reduction rules are similar to that of natural numbers: case σ (nilτ)of{nil⇒e nil |cons⇒e cons } →e nil case σ (consτ x xs)of{nil⇒e nil |cons⇒e cons } →e cons x xs Here are two basic functions on lists, namely the concatenation of two lists and the map function. Example 2.13 (The concatenation of two lists). app:=ΛX.(letrec ListX→ListX→ListX app=λx:ListX. λy:ListX. case ListX xof{nil⇒y |cons⇒λz:X. λx 0 :ListX.consX z(appx 0 y) } ) :Π X.ListX→ListX→ListX ut Example 2.14 (The map function on a list). map:=ΛX. ΛY. λf:X→Y.(letrec ListX→ListY map=λx:ListX. case ListY xof{nil⇒nil |cons⇒λz:X. λx 0 :ListX.consY(f z) (mapf x 0 ) } ) :Π X. Π Y.(X→Y)→ListX→ListY ut We can also define the concatenation of a list of lists. InF rec the polymorphic type of lists of lists isΠ X.List(ListX). The concatenation of a list of lists is therefore of typeΠ X.List(ListX)→ListX. Example 2.15 (The concatenation of a list of lists). conc:=ΛX.(letrec List(ListX)→ListX conc=λx:List(ListX). case ListX xof{nil⇒nil |cons⇒λz:ListX. λx 0 :List(ListX).appX z(concx 0 ) } ) :Π X.List(ListX)→ListX ut

A tutorial on type-based termination 11 An other interesting polymorphic type is that of polymorphic finitely branch- ing trees. These trees are composed of leaves, with one token of information, and of inner nodes, with one token of information and a list of successor subtrees. These two kinds of nodes are represented by the same constructor: node: XΠ X.→List(TreeX)→TreeX For instance, the types of trees of natural numbers isTree Nat, and a leave with tokennis represented bynode Natn(nil(Tree Nat)). The important point with this type is that the recursive argument ofnodeτ, which is a list of trees ofτ, is not directly of typeTreeτbut of typeList(Treeτ). This allows to encode trees where each node can have a different, but finite, arity. Like natural numbers and lists, trees are eliminated by case-analysis. Since this type has only one constructor, the scheme of elimination essentially performs the projection of that constructor: (case) Γ`e:Listτ Γ`e node :τ→List(Treeτ)→σ Γ`case σ eof{node⇒e node }:σ The reduction rule is as follows: case σ (node lτ x)of{node⇒e node } →e node x l For instance, the first projection is typed as Γ`e:Listτ Γ`λx:τ. λl:List(Treeτ). x:τ→List(Treeτ)→τ Γ`case τ eof{node⇒λx:τ. λl:List(Treeτ). x}:τ and we havecase τ (node lτ x)of{node⇒λx:τ. λl:List(Treeτ). x} → 3 x. The following example treats the flattening of finitely branching trees. Example 2.16 (Flattening of finitely branching trees).This program depends on map, defined in Ex.2.14and onconc, defined in Ex.2.15. Similarly todiv, it is not typable in systems with a syntactic guard predicate. flatten:=ΛX.(letrec TreeX→ListX flat=λt:TreeX.case ListX tof{ node⇒λx:X. λl:List(TreeX).consx(conc(mapflatl)) } ) :Π X.TreeX→ListX For readability, we have left the instantiation of polymorphic types implicit at the term level.ut

Higher-order datatypes.Up to now, we only have presented first order datatypes, i.e. datatypes whose inhabitants represent particular forms of finitely branching trees.