On the depth of randomly generated circuits

Adequate enco dings of logical systems in UTT Nikos Mylonakis LSI Department Universitat Politecnica de Catalunya (UPC) Abstract. In this pap er, we present an existing and formalized typ e theory (UTT (Luo, 1994) (Goguen, 1994)) as a logical framework. We compare the resulting framework with LF (Harp er et al., 1993) and give the representation of two signicant typ e systems in the framework: the typ ed lamb da calculus which is closely related to higher-order logic and a linear typ e system which is not p ossible to enco de in LF .. 1. Intro duction Typ e theories were initially used as a logical language for the foundations of mathematics. Since they also include a computational language (in particular a functional language), most of them have also b een used as a framework for program development. Some typ e theories have also b een used as logical frameworks like for example the LF typ e theory (Harp er et al., 1993). Other formalisms whichhave b een used as logical frameworks are Isab elle (Paulson, 1994) or rewriting logic (Mart-Oliet et al., 1993) LF can b e seen as a pure typ e system, that is a three-level typ ed lamb da calculus (level of elements, typ es and kinds) with dep endent -typ es. LF has b een used to make adequate enco ding of dierent logics. The enco ding is based on the idea of judgements as typ es, where judgements are seen as families of typ es of their pro ofs. UTT (Luo, 1994)(Goguen, 1994) (Uniform Theory of dep endent typ es) is a typ e theory which adds to the Extended Calculus of Constructions (ECC (Luo, 1994)) the p ossibility to dene inductivetyp es. The whole typ e theory is enco ded in the Martin-Lof Logical F ramework (Nordstrom et al., 1990). A more rened view of UTT can dierentiate two dierent universes: ; A universe of typ es in which dierenttyp es co exist:-typ es (a dep endenttyp e of tuples) -typ es (a dep endenttyp e of functions) and inductivetyp es. ; A universe of prop ositions in which a higher order intuitionistic logic is dened. We refer to this universe using the constant Prop . Mixing inductivetyp es and the universe of prop ositions one can dene inductive relations. In this typ e theory, inductive relations can b e c  2000 Kluwer Academic Publishers. Printed in the Netherlands. utt_lf.tex 26/01/2000 10:08 p.1 2 seen as functional typ es whichgiven some arguments of the appropriate typ e, return the prop osition one has to prove to guarantee that the tuple formed by the given arguments b elongs to the relation. We will use inductivetyp es and inductive relations for the enco ding of syntax and the enco ding of the pro of systems of our logical systems. In this pap er, rst we presentanovel enco ding of the typ ed lambda calculus in UTT together with an explicit pro of of the correctness of the representation which is closely related to the enco ding of higherorder logic tackling the problem of an explicitly dened higher-order substitution op eration. After that, the enco ding of a fragmentof a linear typ e theory which is not p ossible to enco de in LF is presented. These enco dings are adequate, in the sense that there exists a bijection between the closed derivations of a concrete judgement of the pro of systems and the inhabitants of the application of the judgementtothe inductive relation which enco des the pro of systems. It is not the aim of the pap er to compare the dierent existing logical frameworks with ours but to solve the technical problems to give adequate enco dings of logical systems in UTT and to show that the increase of expressivity of UTT solves some imp ortant limitations of the closest logical framework to the one that we prop ose whichis LF. On the other hand, this increase of expressiveness do es not seem to aect signicatively to the eciency of the pro of assistance of this typ e theory. See (Pollack, 1995) for a generic solution to pro of assistance of these typ e theories. Therefore, we encourage the development of future generations of op en pro of checkers for typ e theories with dep endentand inductivetyp es to b e used as logical frameworks. Note that the techniques presented in this pap er have b een applied for the developmentof generic pro of supp ort for algebraic sp ecication languages ((Hennicker et al, 1997), (Hennicker, 1997)) in (Mylonakis, 2000). See also (LEGO, 1998) for many other applications of UTT using the current pro of checker of the typ e theory. In the following, we present some of the advantages of UTT together with the new principle of enco ding with resp ect to LF: ; In UT T it is p ossible to formalize metatheory of the enco ded logic using a higher order logic with inductive principles asso ciated to inductivetyp es and inductive relations whereas LF has not this feature. ; Since in UTT the enco dings of variables and contexts of sequents of logics are also enco ded as inductivetyp es (as a parameter of the inductive relation which enco des the logic), the prop erties of the typ e theory like for example weakening are not inherited bythe enco ded logic. These prop erties havetobe proven for the concrete utt_lf.tex 26/01/2000 10:08 p.2 3 ob ject logic using for example the induction principles asso ciated to the inductive relation which enco des the ob ject logic. Thus, for example the consequence relation of the ob ject logic do es not have to b e intuitionistic as in LF. See for example (Gardner, 1992) for a formal explanation. ; Finally,we b elieve that our enco dings are more readable and easy to use in practice than the ones in LF since we do not use higherorder abstract syntax and our substitution op eration do es not dep end on the implementation of  ; reduction of the pro of checker of LF which can eventually p erform renamings of variables to avoid name clashes. In our approach, the enco ding of syntax is more similar to the informal usual notation and the names of variables are preserved under substitution and from the enco ded formulae we can always recover the original names of variables. This might not b e very relevant for the enco ding of rst order logic, but we think that this is really imp ortant for the enco ding of higher-order calculi including mo dularity or concurrency. 2. Logical Systems The pro of systems which are enco ded in LF are usually formulated as natural deduction systems. See (Gardner, 1992) for a formal description of these systems. Basically, these systems are dened by a nite set of natural deduction rules. These kind of rules are dened byasetof n premises, a conclusion, and side conditions are allowed. Premises and conclusions are dened by sequents with schematic variables and therefore a rule denotes in general a set of (n+1)-tuples of sequents. An instance of a rule is a (n+1)-tuple of sequents of this set. In general, sequents are dened with judgements and for example the only judgement which is used to dene rst-order logic is tr ue whichmeans that the formula  is derivable. The sequent to dene natural deduction systems in (Gardner, 1992) is ; ) X J where ; is a set of judgements (normally referred as environment), J is a judgementand X a nite set of variables. We will always work with logical systems dened by a nite set of rules with premises, conclusion and side conditions as in (Gardner, 1992) but we will not work with just the typ e of sequents presented in (Gardner, 1992): within a logical system, dierent kind of sequents can b e dened. In the following, wegive some extra denitions of logical systems which are needed for the presentation of the enco ding in UT T and its utt_lf.tex 26/01/2000 10:08 p.3 4 pro of of adequacy. The main denitions are given for sequents of the form ; ) X J but they are easily generalisable for any kind of sequents. Denition 2.1 The sequent ; ) X J is closedi J and al l the judgements in ; are closed under X . Remark: In the fol lowing, for any sequent S of a logical system  including a set of free variables, we wil l assume predened the property of closedness in the obvious equivalent way. Denition 2.2 A rule is closedif the sequents of the premises and the sequent of its conclusion are closed. Denition 2.3 The set of derivations of a sequent ; ) X J in the logical system  is denotedby   (; ) X J ) and recursively denedas fol lows: ; if J 2 ; then ; ) X J 2   (; ) X J ) . ; if r 2  , (; ) X J ; 1 ) X 1 J 1 :::  ; n ) X n J n ) is an instance of the rule r,  1 2   (; 1 ) X 1 J 1 ) , ::: and  n 2   (; n ) X n J n ) , then r (; ) X J   1 :::  n ]) 2   (; ) X J ) . Remark: In the fol lowing, we wil l denote by   ( S ) the set of derivations of the sequent S in the logical system  and we wil l denote just by   the whole set of derivations of the logical system  . Denition 2.4 A derivation of a sequent is closed i the sequent is closed and its subderivations areclosed, where the subderivations are the derivations of the instances of the rst-rule premises of the derivation. 3. Notation Inductivetyp es and inductive relations are dened in UTT by a set of constructors. Additionally,wewill always assume predened the induction principle and the primitive recursive op erator asso ciated to the inductive denition to dene primitive recursive functions on that typ e. For example, for the inductivetyp e List : Type 0 ! Type 0 , which is dened by the following set of constructors nil : A : Type 0 :List A cons : A : Type 0 :A ! ( List A ) ! ( List A ) utt_lf.tex 26/01/2000 10:08 p.4 5 the induction principle Ind ( List A )foranytyp e A : Type 0 whichwe will use to reason ab out prop ositions of typ e ( List A ) ! Prop is the following:  P :( List A ) ! P r op: ( P ( nil A ))  ( 8 a : A: 8 l : List A: ( Pl )  ( P ( cons A a l )))  ( 8 l : List A:P l ) and the primitive recursion principle P r imr ec ( List A ) with arity P r imr ec ( List A ): T ! ( A ! ( List A ) ! T ! T ) ! ( List A ) ! T for anytyp e T : Type 0 has the following computational rules: P r imr ec ( List A ) bcl g cl ( nil A ) ! bcl P r imr ec ( List A ) bcl g cl ( cons A a l ) ! ( gclAal ( P r imr ec ( List A ) bcl g cl l )) For example the function reverse of a list with typ e rev erse : T : Type 0 : ( List T ) ! ( List T ) is dened as follows: rev erse T l = P r imr ec ( List T ) rev bc rev g c l w her e rev bc = nil T rev g c a l l 0 = add last a l 0 4. Adequate enco ding of the typ ed lamb da calculus In this subsection we are going to present the adequate enco ding of the typ ed lamb da calculus and its substitution op eration. One of the original formulation of the typ ed lamb da calculus has the following three rules: X I x :  x :  2 X ( Ass ) X f x :  g I e :  0 X I x : :e :  !  0 ( AB S ) X I e :  !  0 X I e 0 :  X I ee 0 :  0 ( AP P L ) where the p ossible typ es ( Type TLC ( B )) are generated by a set of base typ es B and the constructor  !  0 where   0 2 Type TLC ( B )and the set of preterms (variables, lamb da abstraction and application) are denoted by Term TLC ( B ) utt_lf.tex 26/01/2000 10:08 p.5 6 An alternative presentation of the typ ed lamb da calculus is to split thesetoffree variables in two: the initial set of free variables of the derivation and the set of b ound variables of a variables which b ecome free in the derivation pro cess. We will denote this new set of free variables as a pair of the form ( X X 0 ) where the rst is the initial set of free variables and the second the set of b ound variables whichhave b ecome free, and if the second comp onent is emptywe will normally denote the set ( X ]) just by X . This split will b e used to determine the dierence b etween the last DeBruijn index assigned to the b ound variables in the scop e of every o currence of a variable in a higher-order term and the last index assigned in the original set of free variables. This index (which will b e referred as b ound level and it is an information whichevery variable in a higher-order term has) is necessary to up date the indexes of the variables of the higher-order term which replaces a variable in the substitution op eration. Thus, the new formulation of the alternative denition of the typ ed lamb da calculus has the following four rules: ( X X 0 ) I x :  x :  = 2 X 0 x :  2 X ( Ass 1) ( X X 0 ) I x :  x :  2 X 0 ( Ass 2) ( X X 0 f x :  g ) I e :  0 ( X X 0 ) I x : :e :  !  0 ( AB S ) ( X X 0 ) I e :  !  0 ( X X 0 ) I e 0 :  ( X X 0 ) I ee 0 :  0 ( AP P L ) And the substitution op eration f = g : Term TLC ! Term TLC ! X ! Term TLC is inductively dened as follows: y f t= x g = tifx = y = y  other w ise x : :e f e 0 =y g = x 0 : : (( e f x 0 =x g ) f e 0 =y g ) ifx 6 = y = x : :e ifx = y w her e x= 2 FV ( e 0 ) ) x 0 = x ^ x 2 FV ( e 0 ) ) x 0 = 2 FV ( e 0 ) ^ x 0 = 2 FV ( e ) ^ x 0 = 2 BV ( e )  ee 0 f t=x g = e f t=x g ( e 0 f t=x g ) utt_lf.tex 26/01/2000 10:08 p.6 7 where FV ( e ) denotes the set of free variables of e and BV ( e ) denotes the set of b ound variables of e in the usual way. As wehavementioned in previous sections, for the enco ding of this typ e system, the enco ding of variables is not trivial and requires additionally to the variable name and its typ e, twovariable indexes: one to denote the DeBruijn index and the other to denote the b ound level of the variable. Variable names are dened as non-empty strings of characters and since we can assume that the innite set of variables is countable, variable indexes are trivially dened as inductivetyp es. Both indexes are assigned during the enco ding of terms. The DeBruijn index for b ounded variables start from the greatest index assigned to the free variables to avoid name clashes. The DeBruijn index of the b ound variables of the term whichreplaces a variable in the substitution op eration must b e up dated. This up date uses the b ound level of the variable to b e replaced. Additionally, the b ound level of all the variables of the term which replaces a variable must also b e up dated using the b ound level of the variable whichis replaced. Note that we do not lose readability in this pro cess b ecause wealways preserve the original names of the variables. 4.1. Encoding of variables First we dene the enco ding of variables symb ols, variable names as non-empty strings of variable names, and variable indexes isomorphic to the naturals numbers. Denition 4.1 The type Var sy mbol is inductively dened by the following set of constructors: a : : :  z : Var sy mbol A::: Z : Var sy mbol  0  $: Var sy mbol Denition 4.2 For any type T : Type 0 , the inductive type N el ist T is dened by the fol lowing constructors: first Nel : T ! N el ist T cons Nel : T ! ( Nelist T ) ! ( Nelist T ) Denition 4.3 The type Var name is dened as fol lows: Var name = Ne l ist V ar sy mbol utt_lf.tex 26/01/2000 10:08 p.7 8 Denition 4.4 The type Var index is inductively dened by the following set of constructors: first Vi : Var index next Vi : Var index ! Var index We assume predened the following functions on variable indexes:: ; E q bool Vi : Var index ! Var index ! B ool whichisthe b o olean equalityonvariable indexes. ; Ltbool Vi : Var index ! Var index ! B ool whichisthe function lower than on variable indexes. ; add Vi : Var index ! Var index ! Var index which adds two variable indexes like they were naturals. ; decr Vi : Var index ! Var index ! Var index which decrements a variable index likeitwas a natural. ; substr act Vi : Var index ! Var index ! Var index which substracts twovariable indexes liketheywere naturals. Next, we dene the higher-order typ es of variables and higher-order variables. Denition 4.5 The inductive types Holtype for a given set of base types B is dened by the fol lowing set of constructors: f bHolt : Holtype j b 2 B g f func Holt : Holtype ! Holtype ! Holtype g We assume predened the equality function E q bool Hty : Holtype ! Holtype ! Bool Denition 4.6 The type Holvar is denedas: Holvar = pair V ar name H ol ty pe Higher-order variables with indexes are dened as higher-order variables with two indexes: the rst is the deBruijn index and the second is the b ound level of the variable which is the numb er of b ound variables which has the scop e of an o currence of a variable in a term. Denition 4.7 The type Holinvar is denedas: H ol inv ar = pair H ol v ar ( pair V ar index V ar index ) utt_lf.tex 26/01/2000 10:08 p.8 9 We assume predened the following function on Holvar and Holinvar : ; E q bool Hvar : Holvar ! Holvar ! B ool which is the b o olean equality function on higher-order variables. ; E q bool Hivar : H ol inv ar ! Holinvar ! B ool which is true if the two higher-order variables and their deBruijn indexes (not the b ound level) are equal. ; g etindex Hiv : Holinvar ! Var index whichgiven a higherorder variable with indexes returns the DeBruijn index. ; getblevel Hiv : Holinvar ! Var index whichgiven a higherorder variable with indexes returns the b ound level. ; assindex Hiv : Holinvar ! Var index ! Holinvar which given a higher-order variable with indexes and a variable index, assigns the variable index as deBruijn index to the variable. ; assbl ev el Iv : H ol inv ar ! Var index ! Holinvar which given a higher-order variable with indexes and a variable index, assigns the variable index as b ound level to the variable. ; addindex Hiv : Holinvar ! Var index ! Holinvar which given a higher-order variable with indexes and a variable index, adds the variable index with the deBruijn index of the variable ; addbl ev el Hiv : Holinvar ! Var index ! Holinvar which given a higher-order variable with indexes and a variable index, adds the variable index with the b ound level of the variable. 4.2. Encoding of variable sets Variable sets are dened as pairs of twopairs ofa variable index and list of higher-order variables with indexes. The rst pair denotes the set of free variables together with the last deBruijn index assign to the set of free variables and the second pair denotes the set of b ound variables together with the last deBruijn index assign to b ound variables. The deBruijn indexes of b ound variables are always assigned after the deBruijn indexes of free variables. Denition 4.8 The type Holvar set is denedas: Holvar set = pair ( pair V ar index ( List H ol inv ar )) ( pair V ar index ( List H ol inv ar )) utt_lf.tex 26/01/2000 10:08 p.9 16 4.5. Adequacy of the representation Finally,we present the adequacy of the representation with the following theorem and its pro of. Theorem 4.18 There exists a bijection between the closed derivations of a judgement ( ( X ]) I  :  ) and the normal forms of the proofs of the proposition W f hter m (  vs ( X ])) (  ht (  vs X )  )(    ) Pro of: This pro of is not dicult b ecause wehave an exact corresp ondence between rules of the pro of system and constructors of the inductive relation which enco des the pro of system. First, we can easily prove that  td is injective and total To prove the bijection we dene a deco ding function with typ e  ; 1 td : W f hter m (  vs ( X ])) (  ht (  vs ( X ])) e )(    ) !   TLC (( X ]) I e :  ) inductively dened as follows:  ; 1 td ( ass 1 tr v s hv pr pr in )= AS S 1((  ; 1 vs vs ) I (  ; 1 vn ( fst hv ):(  ; 1  ( snd hv )))  ; 1 td ( ass 2 tr v s hv pr )= AS S 2((  ; 1 vs vs ) I (  ; 1 vn ( fst hv ):(  ; 1  ( snd hv )))  ; 1 td ( abs tr v s hv ht hty dpr )= AB S ((  ; 1 vs vs ) I  (  ; 1 vn ( fst hv ):  ; 1  ( snd hv )) : (  ; 1 ht ( addbv ar Hvst hv vs ) ht ): (( snd hv ) ! hty )  (  ; 1 td ( dpr ))])  ; 1 td ( appl tr v s ht ht 0 hty hty 0 wf tpr wf tpr 0 )= AP P L (  ; 1 vs vs ) I (  ; 1 ht vs ht )(  ; 1 ht vs ht 0 ): hty 0  (  ; 1 td ( wf tpr ))  (  ; 1 td w f tpr 0 )] This deco ding function is also injective and total and it holds byaneasy induction that for all closed derivations der iv 2   TLC  ; 1 td (  td der iv )= der iv which is necessary to guarantee the bijection. utt_lf.tex 26/01/2000 10:08 p.16 17 5. Enco ding of a fragment of a linear typ e theory In this section we give an adequate enco ding of the functional fragment of SLR, a lamb da calculus with mo dal and linear function spaces designed by (Homan, 1999). The main dierences with resp ect to typ edlamb da calculus is that contexts contains variables with asp ects where an asp ect is a pair containing the information whether the variable is linear or nonlinear and whether the variable is mo dal or nonmo dal. As we mentioned in the intro duction, it is p ossible to represent this typ e theory in our framework since our principle of enco ding is not the same as in LF and we are able to represent and manipulate nonstandard contexts like a linear one. Another dierence with resp ect to lamb da calculus is that there exists dierent functional spaces like for example a (linear, nonmo dal) functional space and a (nonlinear, nonmo dal) functional space. The formal semantics can b e found in (Homan, 1999) and we do not detail it here b ecause it is not necessary for our purp oses. An interesting application of this typ e theory is to develop functional programs with p olynomial time complexity. Finally,we do not split contexts in contexts with free and b ound variables b ecause we do not represent the substitution op eration. The fragment of SLR whichwe are going to enco de adequately in UTT is formally dened by the following denitions: Denition 5.1 Anaspect is a pair ( l m ) where l 2f linear nonl inear g and m 2f nonmodal  modal g . The aspects areorderedcomponentwise by nonl inear < : linear and modal < : nonmodal . Denition 5.2 The typeexpressions which we wil l consider are the fol lowing: T SLR ::= N natur al number s L ( T SLR ) lists ov er T SLR T ( T SLR ) binar y tr ees l abel l ed ov er T SLR T SLR a !T SLR f unction space of aspect a: T SLR a !T SLR is the generic notation usedtodenethetype system but normal ly the dierent function spaces are denotedinthisway: T SLR a !T SLR is T SLR ( T SLR w hen a = f linear nonmodal g T SLR a !T SLR is T SLR !T SLR w hen a = f nonl inear nonmodal g T SLR a !T SLR is 2 T SLR !T SLR w hen a = f nonl inearmodal g utt_lf.tex 26/01/2000 10:08 p.17 18 Denition 5.3 The expressions which we wil l consider are the fol lowing: " SLR ::= x ( v ariable ) " SLR " SLR ( appl ication ) x : T SLR : " SLR ( abstr action ) Denition 5.4 Acontext is a partial function from term variables to pairs of aspects and types typical ly written as a list of bindings of the form x a : A . For any context ; , Dom (;) denotes the set of variables bound in ; . If x a : A 2 ; then ;( x ) denotes A and ;(( x )) denotes a and ;   denotes the union of the contexts ; and  if Dom (;) and Dom () are disjoint. The following judgements are used to dene the typ e system: ; ; nonl inear which means that all its bindings are of nonlinear asp ect. ; D isj oint ;  which means that the sets Dom (;) and Dom () are disjoint. ; ; ` e : A which means that the expression e has typ e A in the context ;. ; ; < : a which means that for all bindings x a 0 : A in ;, a 0 < : a . Denition 5.5 The judgement ; < : a for any context ; and any aspect a is inductively dened by the fol lowing rules: <>< : a ( bc < :) ; < : a a 0 < : a ;  f x a 0 : A g < : a x= 2 Dom (;) ( gc < :) Denition 5.6 The judgement D isj oint ; for any context ; ,  is inductively dened by the fol lowing rules: D isj oint <>  ( bcdisj ) D isj oint ; D isj oint ;  f x a : A g  x= 2 Dom () ^ x= 2 Dom (;) ( g cdisj ) utt_lf.tex 26/01/2000 10:08 p.18 19 Denition 5.7 The judgement ; nonl inear for any context ; is inductively dened by the fol lowing rules: <> nonl inear ( bcnl ) ; nonl inear ;  f x a : A g nonl inear x= 2 Dom (;) ^ fst ( a )= nonl inear ( gcnl ) Denition 5.8 The functional fragment of the type system SLR is inductively dened by the fol lowing rules: ;  f x a : A g` e : B ; ` x : A:e : A a ! B ( T arri ) D isj oint ; 1 D isj oint ; 2 D isj oint  1  2 ;   1 ` e 1 : A a ! B ;   2 ` e 2 : B ; nonl inear ;   2 < : a ;   1   2 ` e 1 e 2 : B ( T arre ) And, nowwe pro ceed with the enco ding of the typ e theory in a similar way as the enco ding of typ ed lamb da calculus. 5.1. Encoding of variables, contexts and terms First, we represent asp ects and their relation op eration. Denition 5.9 The inductive type Linear ity is dened by the fol lowing constructors: l inear : Linear ity nonl inear : Linear ity Denition 5.10 The inductive relation < : Lin : Linear ity ! Linear ity ! Prop is inductively dened by the fol lowing constructor: nl l : < : Lin nonl inear l inear Denition 5.11 The inductive type M odal ity is dened by the fol lowing constructors: modal : M odal ity nonmodal : M odal ity Denition 5.12 The inductive relation < : Mod : M odal ity ! M odal ity ! Prop is inductively dened by the fol lowing constructor: mnm : < : M od modal nonmodal utt_lf.tex 26/01/2000 10:08 p.19 20 Denition 5.13 The type S LRaspect is denedas P air Linear ity M odal ity . Denition 5.14 The inductive relation < : Asp : S LRaspect ! S LRaspect ! Prop is dened by the fol lowing set of constructors: ref l : l : Linear ity :  m : M odal ity : < : Asp ( mk pair S LRaspect l m )( mk pair S LRaspect l m ) compw ::  l l 0 : Linear ity :  m m 0 : M odal ity :  linr : < : lin l l 0 :  modr : < : mod m m 0 : < : Asp ( mk pair S LRaspect l m )( mk pair S LRaspect l 0 m 0 ) We dene an additional inductive relation on asp ects to check whether an asp ect is nonlinear. Denition 5.15 The inductive relation N onl in Asp : S LRaspect ! Prop is dened by the fol lowing constructor: nonl c Nlm : mod : M odal ity :N onl in Asp ( mk pair S LRaspect nonl inear mod ) Next, wedene thetyp es of the typ e theory. Denition 5.16 The inductive type SLRtype is dened by the fol lowing set of constructors: nat : S LRty pe list : S LRty pe ! SLRtype tr ee : SLRtype ! S LRty pe lmf unc : S LRty pe ! S LRaspect ! SLRtype And next, we dene variables together with an op eration to get the asp ect of the variable, variables with indexes and contexts. Denition 5.17 The type S LRv ar is denedas Pair ( P air V ar name S LRty pe ) S LRaspect Denition 5.18 The function g etaspect SLRv : S LRv ar ! S LRaspect is dened as fol lows: g etaspect S LRv sv ar =( snd sv ar ) Denition 5.19 The type SLRivar is denedas P air S LRv ar V ar index . Denition 5.20 The type S LRcontext is denedas P air V ar index ( List S LRiv ar ) utt_lf.tex 26/01/2000 10:08 p.20 21 We assume predened the following functions and inductive relations of SLRvar , S LRiv ar and S LRcontext which are dened in a very similar wayastheequivalent op erations in the typ ed lamb da calculus: E q bool SLRv : SLRvar ! S LRv ar ! B ool E q bool SLRiv : SLRivar ! S LRiv ar ! B ool empty S LRctxt : S LRcontext addv ar S LRctxt : S LRv ar ! S LRcontext ! S LRcontext g etv ar S LRctxt : Varname ! S LRcontext ! S LRiv ar concat S LRctxt : S LRcontext ! S LRcontext ! S LRcontext Is in S LRctxt : V ar name ! S LRcontext ! Prop Not is in S LRctxt : V ar name ! S LRcontext ! Prop Wehave additionally the following inductive relations on contexts which are needed to represent the dierent judgements on contexts (; < : a , D isj oint ; and ; nonl inear ) used in the denition of this typ e theory. Denition 5.21 The inductive relation < : Ctxt : S LRcontext ! S LRaspect ! Prop is dened by the fol lowing constructors: bc < ::  a : S LRaspect: < : C txt empty S LRctxt a gc < ::  sl r c : S LRcontext:  slrv : S LRv ar:  a : S LRaspect:  apr : < : Asp ( g etaspect S LRv sl r v ) a:  slrcpr : < : C txt slrc a:  isinpr : Not is in S LRctxt ( fst ( f st slrv )) ( snd sl r c ) : < : Ctxt ( addv ar S LRctxt slrv slrc ) a Denition 5.22 The inductive relation N onl inear Ctxt : S LRcontext ! Prop is dened by the fol lowing constructors: bcnl : N onl inear C txt empty S LRctxt g cnl : sl r c : S LRcontext:  sl r v : S LRv ar:  nl pr : N onl inear C txt slrc:  ninpr : Not is in S LRctxt ( fst ( f st slrv )) ( snd slrc ) :  nl apr : Nonlin Asp ( g etaspect S LRv sl r v ) : N onl inear Ctxt ( addv ar S LRctxt sl r v sl r c ) Denition 5.23 The inductive relation D isj oint Ctxt : S LRcontext ! S LRcontext ! Prop is dened by the fol lowing constructors: bcdisj : slrc : S LRcontext:D isj oint C txt empty S LRctxt sl r c g cdisj : slrc slrc 0 : S LRcontext:  slrv : S LRv ar:  ninpr : Not is in S LRctxt ( fst ( f st slrv )) sl r c:  ninpr : Not is in S LRctxt ( fst ( f st slrv )) sl r c 0 :  disj pr : D isj oint C txt sl r c sl r c 0 : D isj oint Ctxt ( addv ar S LRctxt slrv slrc ) slrc 0 utt_lf.tex 26/01/2000 10:08 p.21 22 Finally,wehave the enco ding of terms. Denition 5.24 The inductive type S LRter m is denedbythefollowing constructors: var SLRt : S LRiv ar ! SLRterm appl SLRt : S LRter m ! S LRter m ! S LRter m abs SLRt : SLRivar ! S LRter m ! S LRter m 5.2. Encoding of the type theory We will also assume predened the following enco ding and deco ding functions as in the typ ed lamb da calculus:  a : Aspect ! S LRaspect  ; 1 a : S LRaspect ! Aspect  SLR : T SLR ! SLRtype  ; 1 SLR : S LRty pe !T SLR  ctxtS LR : B inding ] ! S LRcontext  ; 1 ctxtS LR : S LRcontext !  B inding ]  tS LR : S LRcontext ! " SLR ! S LRter m  ; 1 tS LR : S LRcontext ! S LRter m ! " SLR  D j ctxt :( D isj oint  1  2 ) ! ( D isj oint C txt (  ctxtS LR  1 )(  ctxtS LR  2 )) for any 1   2 2  B inding ]  ; 1 D j ctxt :( D isj oint C txt scl r scl r 0 ) ! ( D isj oint (  ; 1 ctxtS LR scl r )(  ; 1 ctxtS LR scl r 0 )) for any scl rsclr 0 : S LRcontext  nlctxt :  nlctxt ( N onl inear ;) ! ( N onl inear Ctxt (  ctxtS LR ;)) for any; 2  B inding ]  ; 1 nlctxt :( N onl inear Ctxt slrc ) !   nlctxt ( N onl inear (  ; 1 nlctxt sl r c )) for any slrc : S LRcontext  < : ctxt :  < : ctxt (; < : a ) ! ( < : Ctxt (  ctxtS LR ;) (  a a )) for any a 2 Aspect ,; 2  B inding ]  ; 1 < : ctxt :( < : C txt slrc a ) !   < : ctxt (  ; 1 ctxtS LR slrc ) < :(  ; 1 a a ) for any a : S LRaspect , slrc : S LRcontext where B inding are triples of typ e ( X  Aspect T SLR ). The representation of the typ e system is by the following inductive relation: Denition 5.25 The inductive relation SLRts : S LRctxt ! S LRter m ! S LRty pe ! Prop utt_lf.tex 26/01/2000 10:08 p.22 23 is dened by the fol lowing constructors: Tarri : slrc : S LRcontext:  sl r v : S LRv ar:  t : S LRter m:  pr : S LRts ( addv ar S LRctxt sl r v sl r c ) t ( snd ( f st slrv )) : S LRts slrc ( abs S LRt ( g etv ar S LRctxt ( fst ( fst slrv )) ( addv ar S LRctxt sl r v sl r c )) t ) Tarre : slrc slrc 0  slrc 00 : S LRcontext:  a : S LRaspect:  t t 0 : S LRter m:  A B : SLRtype:  dpr : D isj oint C txt slrc slrc 0 :  dpr 0 : D isj oint C txt sl r c sl r c 00 :  dpr 00 : D isj oint Ctxt slrc 0 sl r c 00 :  td : S LRts ( concat sl r c 0 slrc ) t ( lmf unc A a B ) :  td 0 : SLRts ( concat sl r c 00 sl r c ) t 0 A:  nl pr : N onl inear C txt sl r c:  rprc : < : Ctxt ( concat sl r c sl r c 0 ) a: SLRts ( concat sl r c 00 ( concat sl r c 00 sl r c )) ( appl SLRt t t 0 ) B The enco ding function of the typ e theory is as follows: Denition 5.26 The encoding function of derivations of SLR  slr td which given a closed derivation in   SLR (; ` e : A ) returns a proof of the proposition SLRts (  ctxtS LR ;) (  tS LR (  ctxtS LR ;) e )(  SLR A ) is inductively dened as fol lows:  slr td ( T arri (; ` x : A:e : A a ! B )    ]) = T arri (  ctxtS LR ;) encx (  tS LR ( addv ar S LRctxt encx (  ctxtS LR ;)) e )(  slr td  ) w her e  2  SLR (;  f x a : A g` e : B ) encx = mk pair S LRv ar ( mk pair V ar name S LRty pe (  vn x )(  SLR  )) (  a a ) utt_lf.tex 26/01/2000 10:08 p.23 24  slr td Tarre (;   1   2 ` e 1 e 2 : B   1  2  3  4  5  6  7 ]) = tarre (  ctxtS LR ;) (  ctxtS LR  1 )(  ctxtS LR  2 )(  a a ) (  tS LR (  ctxtS LR ;   1 ) e 1 ) (  tS LR (  ctxtS LR ;   1 ) e 2 ) (  SLR A )(  SLR B ) (  D j ctxt  1 )(  D j ctxt  2 )(  D j ctxt  3 ) (  SLR  4 )(  SLR  5 )(  nlctxt  6 )(  < : ctxt  7 ) w her e  1 2   Djctxt ( D isj oint ; 1 )  2 2   Djctxt ( D isj oint ; 2 )   3 2   Djctxt ( D isj oint  1  2 )  4 2   SLR (;   1 ` e 1 : A a ! B )   5 2   SLR (;   2 ` e 2 : A )   6 2   nlctxt ( N onl inear ;)  7 2   < : ctxt (;   2 < : a ) 5.3. Adequacy of the representation The adequacy of the representation is stated by the following theorem and its pro of: Theorem 5.27 For any context ; ,for any term t 2 " SLR , for any type  2T SLR ,there exists a bijection between the closed derivations of the judgement ( ; ` t :  ) and the normal forms of the proofs of the proposition SLRts (  ctxtS LR ;) (  tS LR (  ctxtS LR ;) t )(  SLR  ) Pro of 5.28 Toprove the bijection we dene a decoding function with type  ; 1 slr td :( S LRts sl r c t  ) ! (  SLR (  ; 1 ctxtS LR sl r c )(  ; 1 tS LR (  ; 1 ctxtS LR slrc ) t )(  ; 1 SLR  )) utt_lf.tex 26/01/2000 10:08 p.24 25 for any slrc : S LRcontext , t : S LRter m ,  : S LRty pe inductively dened as fol lows:  ; 1 slr td ( T arri slrc slrv t pr )= T arri ((  ; 1 ctxtS LR slrc ) `  (  ; 1 vn ( fst ( f st slrv )) : (  ; 1 SLR ( snd ( fst slrv ))) : (  ; 1 tS LR ( addv ar S LRctx sl r v sl r c ) t )    ; 1 slr td pr ])  ; 1 slr td ( T arre slrc slrc 0 slrc 00 at t 0 A B dpr dpr 0 dpr 00 td td 0 nl pr r pr )= T arre (( concat (  ; 1 ctxtS LR sl r c 00 )( concat (  ; 1 ctxtS LR sl r c 0 )(  ; 1 ctxtS LR slrc ))) (  ; 1 tS LR ( concat (  ; 1 ctxtS LR sl r c 0 )(  ; 1 ctxtS LR slrc )) t ) (  ; 1 tS LR ( concat (  ; 1 ctxtS LR sl r c 00 )(  ; 1 ctxtS LR sl r c )) t 0 ): (  ; 1 tS LR B )    ; 1 D j ctxt dpr ; 1 Dj ctxt dpr 0  ; 1 D j ctxt dpr   ; 1 SLR td  ; 1 SLR td 0  nlctxt nl pr < : ctxt rpr ]) and the rest of the proof fol lows in the same way as in the typedlambda calculus. 6. Conclusions In this pap er, wehave presented how to use the typ e theory UT T as a logical framework. Wehave presented the main advantages with resp ect to LF and how to enco de two dierent kind of pro of systems:an adequate enco ding of the typ ed lamb da calculus with non-trivial substitution op eration on higher-order terms requiring up dating of deBruijn indexes and another adequate enco ding of a linear typ e theory which is not p ossible to enco de in LF b ecause it is not p ossible to identify the variables of LF with the variables with asp ect of the linear t yp e theory. These techniques have b een applied to redesign and implement different pro of systems for the deduction of prop erties from algebraic sp ecications in rst-order and higher-order logic and to implement pro of systems for renement of algebraic sp ecications in (Mylonakis, 2000) References Bengt Nordstrom KentPetersson and Jan Smith. Programming in Martin-Lof 's Typ e Theory:An Intro duction.Oxford University Press,1990 Philippa Gardner. Representing Logics in Typ e Theory. PhD thesis, Universityof Edinburgh, July 1992 utt_lf.tex 26/01/2000 10:08 p.25