Report CopyRight/DMCA Form For : Applied Type System An Approach To Practical Programming
gramming paradigms e g functional programming object oriented programming meta programming modular programming can be directly supported in ATSwithout relying on ad hoc extensions attesting to the expressiveness of ATS In this paper the primary focus of study is set on a novel programming paradigm referred to as programming with theorem
ZU064 05 FPR main 15 January 2016 12 51,2 Hongwei Xi. offers a simple and general approach to designing and formalizing type systems it is well. understood that there often exist some acute problems in the presence of dependent types. making it difficult for PTS to accommodate many common realistic programming features. In particular various studies reported in the literature indicate that great efforts are often. required in order to maintain a style of pure reasoning as is advocated in PTS when features. such as general recursion Constable Smith 1987 recursive types Mendler 1987. effects Honsell et al 1995 exceptions Hayashi Nakano 1988 and input output are. The framework ATS is formulated to allow for designing and formalizing type systems. that can readily support common realistic programming features The formulation of ATS. given in this paper is primarily based on the work reported in two previous papers Xi. 2004 Chen Xi 2005 but there are some fundamental changes in terms of the handling. of proofs and proof construction In particular the requirement is dropped that a proof in. ATS must be represented as a normalizing lambda term Xi 2008a. In contrast to PTS the key salient feature of ATS lies in a complete separation between. statics where types are formed and reasoned about from dynamics where programs are. constructed and evaluated This separation with its origin in a previous study on a re. stricted form of dependent types developed in Dependent ML DML Xi 2007 makes it. straightforward to support dependent types in the presence of effects such as references and. exceptions Also with the introduction of two new and thus somewhat unfamiliar forms. of types guarded types and asserting types ATS is able to capture program invariants in. a manner that is similar to the use of pre conditions and post conditions Hoare 1969. By now studies have shown amply and convincingly that a variety of traditional pro. gramming paradigms e g functional programming object oriented programming meta. programming modular programming can be directly supported in ATS without relying on. ad hoc extensions attesting to the expressiveness of ATS In this paper the primary focus. of study is set on a novel programming paradigm referred to as programming with theorem. proving PwTP and its support in ATS In particular a type theoretical foundation for. PwTP is to be formally established and its correctness proven. The notion of type equality plays a pivotal ro le in type system design However the. importance of this ro le is often less evident in commonly studied type systems For in. stance in the simply typed calculus two types are considered equal if and only if they. are syntactically the same in the second order polymorphic calculus 2 Reynolds. 1972 and System F Girard 1986 two types are considered equal if and only if they are. equivalent in the higher order polymorphic calculus two types are considered. equal if and only if they are equivalent This situation immediately changes in ATS. and let us see a simple example that stresses this point. In Figure 1 the presented code implements a function in ATS Xi 2008b which is. a substantial system such that its compiler alone currently consists of more than 165K. lines of code implemented in ATS itself 1 The concrete syntax used in the implementation. should be accessible to those who are familiar with Standard ML SML Milner et al. 1997 Note that ATS is a programming language equipped with a type system rooted in. 1 Please see http www ats lang org for more details. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 3. a type m n nat,xs list a m ys list a n,list a m n,case xs of. nil ys the first clause,cons x xs cons x append xs ys the second clause. end of append,Fig 1 List append in ATS, ATS and the name of ATS derives from that of ATS The type constructor list takes two. arguments when applied to a type T and an integer I list T I forms a type for lists of. length I in which each element is of type T Also the two list constructors nil and cons. are assigned the following types,nil a type list a 0. cons a type n nat a list a n list a n 1, So nil constructs a list of length 0 and cons takes an element and a list of length n to. form a list of length n 1 The header of the function append indicates that append is. assigned the following type,a type m nat n nat list a m list a n list a m n. which simply means that append returns a list of length m n when applied to one list of. length m and another list of length n Note that type is a built in sort in ATS and a static. term of the sort type stands for a type for dynamic terms Also int is a built in sort for. integers in ATS and nat is the subset sort a int a 0 for all nonnegative integers. When the above implementation of append is type checked the following two con. straints are generated,1 m nat n nat m 0 n m n,2 m nat n nat m0 nat m m0 1 m0 n 1 m n. The first constraint is generated when the first clause is type checked which is needed for. determining whether the types list a n and list a m n are equal under the assump. tion that list a m equals list a 0 Similarly the second constraint is generated when. the second clause is type checked which is needed for determining whether the types. list a m0 n 1 and list a m n are equal under the assumption that list a m equals. list a m0 1 Clearly certain restrictions need to be imposed on the form of constraints. allowed in practice so that an effective approach can be found to perform constraint. solving In DML a programming language based on DML Xi 2007 the constraints. generated during type checking are required to be linear inequalities on integers so that. the problem of constraint satisfaction can be turned into the problem of linear integer. programming for which there are many highly practical solvers albeit the problem of. linear integer programming itself is NP complete This is indeed a very simple design but. ZU064 05 FPR main 15 January 2016 12 51,4 Hongwei Xi. it can also be too restrictive sometimes as nonlinear constraints e g n int n n 0 are. commonly encountered in practice Furthermore the very nature of such a design indicates. its being inherently ad hoc, By combining programming with theorem proving a fundamentally different design of. constraint solving can provide the programmer with an option to handle nonlinear con. straints through explicit proof construction For the sake of a simpler presentation let us. assume for this moment that even the addition function on integers cannot appear in the. constraints generated during type checking Under such a restriction it is still possible to. implement a list append function in ATS that is assigned a type capturing the invariant that. the length of the concatenation of two given lists xs and ys equals m n if xs and ys are. of length m and n respectively Let us first see such an implementation given in Figure 2. which is presented here as a motivating example for programming with theorem proving. The datatypes Z and S are declared in Figure 2 solely for representing natural numbers. Z represents 0 and S N represents the successor of the natural number represented by N. The data constructors associated with Z and S are of no use Given a type T and another. type N mylist T N is a type for lists containing n elements of the type T where n is. the natural number represented by N Note that mylist is not a standard datatype as is. supported in ML it is a guarded recursive datatype GRDT Xi et al 2003 which is. also known as generalized algebraic datatype GADT Cheney Hinze 2003 in Haskell. and OCaml The datatype addrel is declared to capture the relation induced by the addition. function on natural numbers Given types M N and R representing natural numbers m. n and r respectively the type addrel M N R is for a value representing some proof. of m n r Note that addrel is also a GRDT or GADT There are two constructors. addrel z and addrel s associated with addrel which encode the following two rules. 0 n n for every natural number n, m 1 n m n 1 for every pair of natural numbers m and n. Let us now take a look at the implementation of myappend Formally the type assigned. to myappend can be written as follows,a type m type n type. mylist a m mylist a n r type addrel m n r mylist a r. In essence this type states the following Given two lists of length m and n myappend. returns a pair such that the first component of the pair is a proof showing that m n equals. r for some natural number r and the second component is a list of length r. Unlike append type checking myappend does not generate any linear constraints on. integers As a matter of fact myappend can be readily implemented in both Haskell and. OCaml extended with support for generalized algebraic datatypes where there is no. built in support for handling linear constraints on integers This is an example of great. significance in the sense that it demonstrates concretely an approach to allowing the pro. grammer to write code of the nature of theorem proving so as to simplify or even eliminate. certain constraints that need otherwise to be solved directly during type checking With. this approach constraint solving is effectively internalized and the programmer can ac. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 5. datatype Z Z of,datatype S a type S of a,mylist type type. a type n type,mycons a S n of a mylist a n,addrel type type type. addrel z Z n n of,m n type r type,addrel s S m n S r of addrel m n r. xs mylist a m,ys mylist a n,addrel m n r mylist a r. case xs of,val pf addrel z in pf ys,end end of mynil. mycons x xs let, val pf res myappend xs ys in addrel s pf mycons x res. end end of mycons,Fig 2 A motivating example for PwTP in ATS. tively participate in constraint simplification gaining a tight control in determining what. constraints should be passed to the underlying constraint solver. There are some major issues with the implementation given in Figure 2 Clearly repre. senting natural numbers as types is inadequate since there are types that do not represent. any natural numbers More seriously this representation turns quantification over natural. numbers which is predicative into quantification over types which is impredicative. causing unnecessary complications Also proof construction that is construction of val. ues of types formed by addrel needs to be actually performed at run time which causes. inefficiency both time wise and memory wise Probably the most important issue is that. proof validity is not guaranteed For instance it is entirely possible to fake proof construc. tion by making use of non terminating functions,ZU064 05 FPR main 15 January 2016 12 51. 6 Hongwei Xi,mynat Z of S of mynat,mylist type mynat. a type n mynat,mycons a S n of a mylist a n,addrel mynat mynat mynat. addrel z Z y y of,x y mynat r mynat,addrel s S x y S r of addrel x y r. xs mylist a m,ys mylist a n,addrel m n r mylist a r. case xs of,val pf addrel z in pf ys,end end of mynil. mycons x xs let, val pf res myappend xs ys in addrel s pf mycons x res. end end of mycons,Fig 3 An example making use of PwTP in ATS. In Figure 3 another implementation of myappend is given that makes use of the support. for PwTP in ATS Instead of representing natural numbers as types a datasort of the. name mynat is declared and natural numbers can be represented as static terms of the. sort mynat Also a dataprop addrel is declared for capturing the relation induced by. the addition function on natural numbers As a dataprop addrel can only form types. for values representing proofs which are erased after type checking and thus need no. construction at run time In the implementation of myappend the bar symbol is used in. place of the comma symbol to separate components in tuples the components appearing. to the left of the bar symbol are proof expressions to be erased and those to the right. are dynamic expressions to be evaluated After proof erasure the implementation of. myappend essentially matches that of append given in Figure 1. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 7. As a framework to facilitate the design and formalization of advanced type systems for. practical programming ATS is first formulated with no support for PwTP Xi 2004 This. formulation is the basis for a type system referred to as ATS0 in this paper The support for. PwTP is added into ATS in a subsequent formulation Chen Xi 2005 which serves as. the basis for a type system referred to as ATSpf in this paper However a fundamentally. different approach is adopted in ATSpf to justify the soundness of PwTP which essentially. translates each well typed program in ATSpf into another well typed one in ATS0 of the. same dynamic semantics The identification and formalization of this approach which is. both simpler and more general than one used previously Chen Xi 2005 consists of a. major technical contribution of the paper, It is intended that the paper should focus on the theoretical development of ATS and. the presentation given is of a minimalist style The organization for the rest of the paper is. given as follows An untyped calculus dyn is first presented in Section 2 for the purpose. of introducing some basic concepts needed to formally assign dynamic that operational. semantics to programs In Section 3 a generic applied type system ATS0 is formulated and. its type soundness established Subsequently ATS0 is extended to ATSpf in Section 4 with. support for PwTP and the type soundness of ATSpf is reduced to that of ATS0 through. a translation from well typed programs in the former to those in the latter Lastly some. closely related work is discussed in Section 5 and the paper concludes. 2 Untyped Calculus dyn, The purpose of formulating dyn an untyped lambda calculus extended with constants in. cluding constant constructors and constant functions is to set up some machinery needed. to formalize dynamic that is operational semantics for programs It is to be proven that a. well typed program in ATS can be turned into one in dyn through type erasure and proof. erasure while retaining its dynamic semantics stressing the point that types and proofs in. ATS play no active ro le in the evaluation of a program In this regard the form of typing. studied in ATS is of Curry style in contrast with Church style Reynolds 1998. There are no static terms in dyn The syntax for the dynamic terms in dyn is given as. dynamic terms e x dcx e he1 e2 i fst e snd e,lam x e app e1 e2 let x e1 in e2. where the notation e is for a possibly empty sequence of dynamic terms Let dcx range. over external dynamic constants which include both dynamic constructors dcc and dy. namic functions dcf The arguments taken by a dynamic constructor or function are often. primitive values instead of those constructed by lam and h i and the result returned by. it is often a primitive value as well The meaning of various forms of dynamic terms should. become clear when the rules for evaluating them are given. The values in dyn are just special forms of dynamic terms and the syntax for them is. given as follows,values v x dcc v hv1 v2 i lam x e. ZU064 05 FPR main 15 January 2016 12 51,8 Hongwei Xi. where v is for a possibly empty sequence of values A standard approach to assigning. dynamic semantics to terms is based on the notion of evaluation contexts. evaluation contexts E dcx v1 vi 1 E ei 1 en,hE ei hv Ei app E e app v E let x E in e. Essentially an evaluation context E is a dynamic term in which a subterm is replaced with. a hole denoted by Note that only subterms at certain positions in a dynamic term can be. replaced to form valid evaluation contexts,Definition 2 1. The redexes in dyn and their reducts are defined as follows. fst hv1 v2 i is a redex and its reduct is v1,snd hv1 v2 i is a redex and its reduct is v2. app lam x e v is a redex and its reduct is e x 7 v. dcf v is a redex if it is defined to equal some value v if so its reduct is v. Note that it may happen later that a new form of redex can have more than one reducts. Given a dynamic term of the form E e1 for some redex e1 E e1 is said to reduce to E e2. in one step if e2 is a reduct of e1 and this one step reduction is denoted by E e1 E e2. Let stand for the reflexive and transitive closure of. Given a program that is a closed dynamic term e0 in dyn a finite reduction sequence. starting from e0 can either lead to a value or a non value If a non value cannot be further. reduced then the non value is said to be stuck or in a stuck form In practice values can. often be represented in special manners to allow various stuck forms to be detected through. checks performed at run time For instance the representation of a value in a dynamically. typed language most likely contains a tag to indicate the type of the value If it is detected. that the evaluation of a program reaches a stuck form then the evaluation can be terminated. abnormally with a raised exception, Detecting potential stuck forms that may occur during the evaluation of a program can. also be done statically that is at compiler time One often imposes a type discipline to. ensure the absence of various stuck forms during the evaluation of a well typed program. This is the line of study to be carried out in the rest of the paper. 3 Formal Development of ATS0, As a generic applied type system ATS0 consists of a static component statics where. types are formed and reasoned about and a dynamic component dynamics where pro. grams are constructed and evaluated The statics itself is a simply typed lambda calculus. extended with certain constants and the types in it are called sorts so as to avoid confu. sion with the types for classifying dynamic terms which are themselves static terms. The syntax for the statics of ATS0 is given in Figure 4 Let b range over the base sorts. in ATS0 which include at least bool for static booleans and type for types assigned to. dynamic terms The base sort int for static integers is not really needed for formalizing. ATS0 but it is often used in the presented examples Let a and s range over static variables. and static terms respectively There may be some built in static constants scx which are. either static constant constructors scc or static constant functions scf A c sort is of the. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 9. sorts b 1 2,static terms s a scx s1 sn a s s1 s2,static var ctx 0 a. static subst a 7 s,Fig 4 The syntax for the statics of ATS0. form 1 n b which can only be assigned to static constants Note that a c sort. is not considered a regular sort Given a static constant scx a static term scx s1 sn. is of sort b if scx is assigned a c sort 1 n b for some sorts 1 n and si can. be assigned the sorts i for i 1 n It is allowed to write scc for scc if there is no. risk of confusion In ATS0 the existence of the following static constants with the assigned. c sorts is assumed,false bool,ty type type bool,type type type. type type type,bool type type,bool type type, Note that infix notation may be used for certain static constants For instance s1 s2. stands for s1 s2 and s1 ty s2 stands for ty s1 s2 In addition a s and a s. stand for a s and a s respectively Given a static constant constructor. scc if the c sort assigned to scc is 1 n type for some sorts 1 n then scc is. a type constructor For instance and are all type constructors Additional. built in base type constructors may be assumed, Given a proposition B and a type T B T is a guarded type and B T is an asserting. type Intuitively if a value v is assigned a guarded type B T then v can be used only if. the guard B is satisfied if a value v of an asserting type B T is generated at a program. point then the assertion B holds at that point For instance suppose that int is a sort for. static integers and int is a type constructor of the sort int type given a static term. s of the sort int int s is a singleton type for the integer equal to s hence the usual type. Int for dynamic integers can be defined as a int int a and the type Nat for natural. numbers can be defined as a int a 0 int a Moreover the following type is for. the dynamic division function on integers,a1 int a2 int a2 6 0 int a1 int a2 int a1 a2. where the meaning of 6 and should be obvious With such a type division by zero is. disallowed during type checking at compile time Also suppose that bool is a type con. structor of the sort bool type such that for each proposition B bool B is a singleton. type for the truth value equal to B Then the usual type Bool for dynamic booleans can. be defined as a bool bool a The following type is an interesting one. a bool bool a a 1,ZU064 05 FPR main 15 January 2016 12 51. 10 Hongwei Xi,scx 1 n b s1 1 sn n,scx s1 sn b,s1 1 2 s2 1. Fig 5 The sorting rules for the statics of ATS0, where 1 stands for the unit type Given a function f of this type we can apply f to a. boolean value v of type bool B for some proposition B if f v returns the B must be true. therefore f acts like dynamic assertion checking, For those familiar with qualified types Jones 1994 which underlies the type class. mechanism in Haskell it should be noted that a qualified type cannot be regarded as a. guarded type The simple reason is that the proof of a guard in ATS0 bears no computational. significance that is it cannot affect the run time behavior of a program while a dictionary. which is just a proof of some predicate on types in the setting of qualified types can and is. mostly likely to affect the run time behavior of a program. The standard rules for assigning sorts to static terms are given in Figure 5 where the. judgement scx 1 n b means that the static constant scx is assumed to be of. the c sort 1 n b Given s s1 sn and 1 n a judgement of the. form s means si i for i 1 n Let B stand for a static term that can be. assigned the sort bool under some context and B a possibly empty sequence of static. boolean terms Also let T stand for a type for dynamic terms which is a static term. that can be assigned the sort type under some context Given contexts 1 and 2 and. a substitution the judgement 1 2 means that 1 a 2 a is derivable for. each a dom dom 2,Proposition 3 1, Assume s is derivable If 1 2 and 1 2 holds then 1 s is. By structural induction on the derivation of s,Definition 3 1 Constraints in ATS0. A constraint in ATS0 is of the form B B0 where B bool holds for each B in B and. B0 bool holds as well and the constraint relation in ATS0 is the one that determines. whether each constraint is true or false, Each regularity rule in Figure 6 is assumed to be met that is the conclusion of each. regularity rule holds if all of its premisses hold and the following regularity conditions on. ty are also satisfied,1 B T ty T holds for every T. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 11. reg var thin,B1 bool B B2,reg bool thin,B a 7 s B a 7 s. B B1 B B1 B2, Fig 6 The regularity rules for the constraint relation in ATS0. dynamic terms e x dcx s e1 en,he1 e2 i fst e snd e lam x e app e1 e2. e e slam a e sapp e s,e let x e1 in e2 hs ei let ha xi e1 in e2. dynamic values v x dcc s v1 vn,hv1 v2 i lam x e e slam a e v hs vi. dynamic var ctx 0 x T,dynamic subst x 7 e,Fig 7 The syntax for the dynamics in ATS0. 2 B T ty T 0 and B T 0 ty T 00 implies B T ty T 00. 3 B T1 T2 ty T10 T20 implies B T1 ty T10 and B T2 ty T20. 4 B T1 T2 ty T10 T20 implies B T10 ty T1 and B T2 ty T20. 5 B B T ty B0 T 0 implies B B B0 and B B T ty T 0, 6 B B T ty B0 T 0 implies B B0 B and B B0 T ty T 0. 7 B a T ty a T 0 implies a B T ty T 0,8 B a T ty a T 0 implies a B T ty T 0. 9 0 scc T1 Tn ty T 0 implies T 0 scc T10 Tn0 for some T10 Tn0. The need for these conditions is to become clear when proofs are constructed in the. following presentation for formally establishing various meta properties of ATS0 For in. stance the last of the above conditions can be invoked to make the claim that T 0 ty T1. T2 implies T 0 being of the form T10 T20 Note that this condition actually implies the. consistency of the constraint relation as not every constraint is valid. Let us now move onto the dynamic component dynamics of ATS0 The syntax for. the dynamics of ATS0 is given in Figure 7 Let x range over dynamic variables and dcx. ZU064 05 FPR main 15 January 2016 12 51,12 Hongwei Xi. dynamic constants which include both dynamic constant constructors dcc and dynamic. constant functions dcf Some unfamiliar forms of dynamic terms are to be understood. when the rules for assigning types to them are presented Let v range over values which. are dynamic terms of certain special forms and range over dynamic variable contexts. which assign types to dynamic variables, During the formal development of ATS0 proofs are often constructed by induction on. derivations represented as trees Given a judgement J D J means that D is a derivation. of J that is the conclusion of D is J Given a derivation D ht D stands for the height of. the tree that represents D, In ATS0 a typing judgement is of the form B e T and the rules for deriving such. a judgement are given in Figure 8 Note that certain obvious side conditions associated with. some of the typing rules are omitted for the sake of brevity For instance the variable a is. not allowed to have free occurrences in B or T when the rule ty intr is applied. Given B B1 Bn B T stands for B1 Bn T Given a a1 an and. 1 n a stands for the sequence of quantifiers a 1 a n A c type. in ATS0 is of the form a B T1 Tn T, The notation dcx a B T1 Tn T means that dcx is assumed to have. the c type following it if dcx is a constructor dcc then T is assumed to be constructed by. some scc and dcc is said to be associated with scc For instance the list constructors and. the integer addition and division functions can be given the following c types. nil a type list a 0,cons a type n int n 0 a list a n list a n 1. iadd a1 int a2 int int a1 int a2 int a1 a2,isub a1 int a2 int int a1 int a2 int a1 a2. imul a1 int a2 int int a1 int a2 int a1 a2,idiv a1 int a2 int a2 6 0 int a1 int a2 int a1 a2. where the type constructors int and list are type constructors of the c sorts int type. and type int type respectively and and are static constant functions of the. c sort int int int, For a technical reason the rule ty var is to be replaced with the following one. x T B T ty T 0, which combines ty var with ty sub This replacement is needed for establishing the. following lemma, Assume D B x T1 e T2 and B T10 ty T1 Then there is a derivation D 0 for. the typing judgement B x T10 e T2 such that ht D 0 ht D. The proof follows from structural induction on D immediately The only interesting case. is the one where the last applied rule is ty var and this case can be handled by simply. merging two consecutive applications of the rule ty var into one with the help of the. regularity condition stating that ty is transitive. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 13. B e T B T ty T 0,dcx a B0 T1 Tn T,s B B a 7 s for each B B0. B ei Ti a 7 s for i 1 n,B dcx s e1 en T a 7 s,B e1 T1 B e2 T2. B he1 e2 i T1 T2,B e T1 T2 B e T1 T2,ty fst ty snd. B fst e T1 B snd e T2,B x T1 e T2,B lam x e T1 T2,B e1 T1 T2 B e2 T1. B app e1 e2 T2,B e B T B B,B e1 B T1 B B x T1 e2 T2. B let x e1 in e2 T2,B slam a e a T,B sapp e s T a 7 s. s B e T a 7 s,B hs di a T,B e1 a T1 a B x T1 e2 T2. B let ha xi e1 in e2 T2,Fig 8 The typing rules for the dynamics of ATS0. Given B 1 2 and the judgement B 1 2 means that the typing judgement. B 1 x 2 x is derivable for each x dom dom 2,Lemma 3 2 Substitution in ATS0. Assume D B e T in ATS0,ZU064 05 FPR main 15 January 2016 12 51. 14 Hongwei Xi, 1 If B B1 B2 and B1 B2 holds then B1 e T is also derivable where. B1 B2 means B1 B holds for each B B2,2 If 1 2 and 1 2 holds then 1 B d T is also deriv. 3 If 1 2 and B 1 2 is derivable then B 1 d T is also. By structural induction on the derivation D,Lemma 3 3 Canonical Forms. Assume D 0 0 v T Then the following statements hold. 1 If T T1 T2 then v is of the form hv1 v2 i,2 If T T1 T2 then v is of the form lam x e. 3 If T B T0 then v is of the form v0,4 If T B T0 then v is of the form e. 5 If T a T0 then v is of the form slam a e,6 If T a T0 then v is of the form hs v0 i. 7 If T scc s1 then v is of the form dcc s2 v for some dcc associated with scc. With Definition 3 1 the lemma follows from structural induction on D If the last applied. rule in D is ty sub then the proof goes through by invoking the induction hypothesis on. the immediate subderivation of D Otherwise the proof follows from a careful inspection. of the typing rules in Figure 8, In order to assign call by value dynamic semantics to the dynamic terms in ATS0 let. us introduce evaluation contexts as follows,eval ctx E. dcx s v E e hE di hv Ei app E e app v E,E E let x E in e sapp E s hs Ei let ha xi E in e. Definition 3 2, The redexes and their reducts are defined as follows. fst hv1 v2 i is a redex and its reduct is v1,snd hv1 v2 i is a redex and its reduct is v2. app lam x e v is a redex and its reduct is e x 7 v. dcf s v is a redex if it is defined to equal some value v if so its reduct is v. e is a redex and its reduct is e, sapp slam a e s is a redex and its reduct is e a 7 s. let x v in e is a redex and its reduct is e x 7 v, let ha xi hs vi in e is a redex and its reduct is e a 7 s x 7 v. Given two dynamic terms e1 and e2 such that e1 E e and e2 E e0 for some redex e. and its reduct e0 e1 is said to reduce to e2 in one step and this one step reduction is denoted. by e1 e2 Let stand for the reflexive and transitive closure of. ZU064 05 FPR main 15 January 2016 12 51,Journal of Functional Programming 15. It is assumed that the type assigned to each dynamic constant function dcf is appropriate. that is 0 0 v T is derivable whenever 0,0 0 dcf s v1 vn T is derivable and. v is a reduct of dcf s v1 vn,Lemma 3 4 Inversion,Assume D B e T in ATS0. 1 If e he1 e2 i then there exists D 0 B e T such that ht D 0 ht D and the. last rule applied in D 0 is ty tup, 2 If e lam x e1 then there exists D 0 B e T such that ht D 0 ht D and. the last applied rule in D 0 is ty lam, 3 If e e1 then there exists D 0 B e T such that ht D 0 ht D and the. last rule applied in D 0 is ty intr, 4 If e e1 then there exists D 0 B e T such that ht D 0 ht D and the. last rule applied in D 0 is ty intr, 5 If e slam a e1 then there exists D 0 B e T such that ht D 0 ht D and. the last rule applied in D 0 is ty intr, 6 If e hs e1 i then there exists D 0 B e T such that ht D 0 ht D and the. last rule applied in D 0 is ty intr, Let D 0 be D if D does not end with an application of the rule ty sub Hence in the rest. of the proof it can be assumed that the last applied rule in D is ty sub that is D is of. the following form,D1 B e T 0 B T 0 ty T, Let us prove 1 by induction on ht D By induction hypothesis on D1 there exists a. derivation D10 B e T 0 such that ht D10 ht D1 and the last applied rule in D10 is. D21 B e1 T10 D22,0 0 B e2 T20,B he1 e2 i T10 T20, where T 0 T10 T20 and e he1 e2 i By one of the regularity condition T T1 T2 for some. T1 and T2 By another regularity condition both B T10 ty T1 and B T20 ty T2 hold. By applying ty sub to D21 0 one obtains D,21 B e1 T1 By applying ty sub to. D22 one obtains D22 B e2 T2 Let D 0 be,D21 B e1 T1 D22 B e2 T2. B he1 e2 i T1 T2, and the proof for 1 is done since ht D 0 1 max ht D21 ht D22 which equals 1. 1 max ht D21 0 ht D 0 1 ht D 0 1 ht D ht D, Let us prove 2 by induction on ht D By induction hypothesis on D1 there exists a. derivation D10 B e T 0 such that ht D10 ht D1 and the last applied rule in D10 is.