%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: main.dvi %%Pages: 8 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%DocumentFonts: Times-Bold Times-Roman Courier Times-Italic %%EndComments %DVIPSCommandLine: dvips main.dvi %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 2000.04.19:1153 %%BeginProcSet: texc.pro /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} forall round exch round exch]setmatrix}N /@landscape{/isls true N}B /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{ /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N /cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add /gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{ dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg} {adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{ adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{] }if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict /eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false} ifelse}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail {dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M} B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{ 4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{ p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet %%BeginFont: Times-Bold % @psencodingfile{ % author = "P. MacKay, Alan Jeffrey, S. Rahtz, K. Berry, B. Horn", % version = "0.2", % date = "7 September 94", % filename = "8r.enc", % email = "kb@cs.umb.edu", % address = "135 Center Hill Rd. // Plymouth, MA 02360", % codetable = "ISO/ASCII", % checksum = "xx", % docstring = "Encoding for TrueType or Type 1 fonts to be used with TeX." % } % % Idea is to have all the characters normally included in Type 1 fonts % available for typesetting. This is effectively the characters in Adobe % Standard Encoding + ISO Latin 1 + extra characters from Lucida. % % Character code assignments were made as follows: % % (1) the Windows ANSI characters are in their Windows ANSI positions, % because Windows users cannot easily reencode the fonts, and it makes % no difference on other systems. The only Windows ANSI characters not % available are those that make no sense for typesetting -- rubout % (127 decimal), nobreakspace (160), softhyphen (173). % % (2) The caron and dotlessi characters are in the positions used by % Y&Y for their modified ATM encoding. % % (3) Remaining characters are assigned arbitrarily to the first few % positions. % % (4) (Y&Y) Lucida Bright includes some extra text characters; in the % hopes that other PostScript fonts, perhaps created for public % consumption, will include them, they are included starting at 0x10. % % (5) Remaining positions left undefined are for use in (hopefully) % upward-compatible revisions, if someday more characters are generally % available in the Type 1 fonts. % % Ligatures are omitted, since this encoding is intended for use at the % driver end. Including ligatures and kerns would make the TFM files % much larger, to no particular purpose. If someone actually wants to % typeset in this encoding, they can pick a different name, and regenerate % the fonts. /TeXBase1Encoding [ % 0x00 (encoded characters from Adobe Standard not in Windows 3.1) /breve /dotaccent /fi /fl /fraction /hungarumlaut /Lslash /lslash /ogonek /ring /tilde /minus % These are the only two remaining unencoded characters, so may as % well include them. /Zcaron /zcaron /.notdef /.notdef % 0x10 (TeX characters from, e.g., Lucida Bright) /dotlessj /ff /ffi /ffl /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef % 0x20 (ASCII begins) /space /exclam /quotedbl /numbersign /dollar /percent /ampersand /quotesingle /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash % 0x30 /zero /one /two /three /four /five /six /seven /eight /nine /colon /semicolon /less /equal /greater /question % 0x40 /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O % 0x50 /P /Q /R /S /T /U /V /W /X /Y /Z /bracketleft /backslash /bracketright /asciicircum /underscore % 0x60 /grave /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o % 0x70 /p /q /r /s /t /u /v /w /x /y /z /braceleft /bar /braceright /asciitilde /.notdef % rubout; ASCII ends % 0x80 /.notdef /.notdef /quotesinglbase /florin /quotedblbase /ellipsis /dagger /daggerdbl /circumflex /perthousand /Scaron /guilsinglleft /OE /caron % Y&Y /.notdef /.notdef % 0x90 /.notdef /quoteleft /quoteright /quotedblleft /quotedblright /bullet /endash /emdash /tildeaccent /trademark /scaron /guilsinglright /oe /dotlessi % Y&Y /.notdef /Ydieresis % 0xA0 /.notdef % nobreakspace /exclamdown /cent /sterling /currency /yen /brokenbar /section /dieresis /copyright /ordfeminine /guillemotleft /logicalnot /hyphen % Y&Y (also at 45); Windows' softhyphen /registered /macron % 0xD0 /degree /plusminus /twosuperior /threesuperior /acute /mu /paragraph /periodcentered /cedilla /onesuperior /ordmasculine /guillemotright /onequarter /onehalf /threequarters /questiondown % 0xC0 /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla /Egrave /Eacute /Ecircumflex /Edieresis /Igrave /Iacute /Icircumflex /Idieresis % 0xD0 /Eth /Ntilde /Ograve /Oacute /Ocircumflex /Otilde /Odieresis /multiply /Oslash /Ugrave /Uacute /Ucircumflex /Udieresis /Yacute /Thorn /germandbls % 0xE0 /agrave /aacute /acircumflex /atilde /adieresis /aring /ae /ccedilla /egrave /eacute /ecircumflex /edieresis /igrave /iacute /icircumflex /idieresis % 0xF0 /eth /ntilde /ograve /oacute /ocircumflex /otilde /odieresis /divide /oslash /ugrave /uacute /ucircumflex /udieresis /yacute /thorn /ydieresis ] def %%EndFont %%BeginProcSet: texps.pro TeXDict begin /rf{findfont dup length 1 add dict begin{1 index /FID ne 2 index /UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics exch def dict begin Encoding{exch dup type /integertype ne{pop pop 1 sub dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def} ifelse}forall Metrics /Metrics currentdict end def[2 index currentdict end definefont 3 -1 roll makefont /setfont load]cvx def}def /ObliqueSlant{dup sin S cos div neg}B /SlantFont{4 index mul add}def /ExtendFont{3 -1 roll mul exch}def /ReEncodeFont{/Encoding exch def}def end %%EndProcSet TeXDict begin 39158280 55380996 1000 300 300 (main.dvi) @start /Fa 2 85 df<120FEA03807F1201A27F1200A27F1370A213781338A2133C137C 13DEEA018EEA030EEA060F487E121C00381380EA700312E038C001C0121A7E9916>21 D<003FB5128038380E010020130012405B1280A348481300A45BA45BA4485AA41203EA7F FC191A7F9916>84 D E /Fb 1 127 df126 D E /Fc 133[22 1[22 22 22 22 22 22 22 1[22 22 22 22 22 22 1[22 22 22 22 22 22 22 22 22 48[22 22 22 22 45[{ TeXBase1Encoding ReEncodeFont}27 37.500000 /Courier rf /Fd 134[17 17 2[19 10 15 15 19 19 19 19 27 10 2[10 19 19 10 17 19 17 19 19 12[21 19 2[23 2[31 21 2[12 2[23 23 27 25 1[23 7[19 4[19 2[19 3[12 3[12 12 12 36[19 2[{ TeXBase1Encoding ReEncodeFont}40 37.500000 /Times-Italic rf /Fe 87[12 17[19 27[17 19 19 27 19 19 10 15 12 1[19 19 19 29 10 19 1[10 19 19 12 17 19 17 19 17 3[12 1[12 1[27 1[35 27 27 23 21 25 1[21 27 27 33 23 27 15 12 27 27 21 1[27 25 25 27 6[10 19 19 19 19 19 19 19 19 19 19 1[9 12 9 2[12 12 12 36[21 2[{TeXBase1Encoding ReEncodeFont}68 37.500000 /Times-Roman rf /Ff 3 116 df102 D<3801E1803803FF00120FEA1C7FEA3807AAEA3C1F383E3780EA3FE7EA1F83EA0F030006 13C0000C138000181300EA3E02EAFF84EA3FF8120FEA03F0121B7F9215>I115 D E /Fg 1 79 df<39FFE00FF8393010032039 0808014090380400C0120CEA0E02EA0D01380C8080EB4040A2EB2020EB1010EB0808EB04 04A2EB0202EB0101EB0080EC40401420A2141014081404140200121301123339FFC000C0 C812401D1D809B20>78 D E /Fh 10 126 df<132013401380EA01005A1206A25AA25AA2 12381230A21270A3126012E0AD12601270A31230A212381218A27EA27EA27E7EEA008013 4013200B317A8113>0 D<7E12407E7E12187EA27EA27EA213801201A213C0A3120013E0 AD13C01201A31380A212031300A21206A25AA25A12105A5A5A0B317F8113>I<12C0B3A9 021B7A800E>12 D80 D<14E01303EB0F80EB1E005B1370A25BB3A5485AA2 485A48C7FC120E123C12F0A2123C120E7E6C7E6C7EA26C7EB3A51370A2133C7FEB0F80EB 03E01300134A7C811C>110 D<12E012F8123E120F6C7EEA01C0A26C7EB3A51370A27F7F 7FEB0780EB01E0A2EB0780EB0E005B5B5BA25BB3A5485AA2EA078048C7FC123E12F812E0 134A7C811C>I122 D<12FCB47E13E013F813FEEA01FF38001F80EB07C0EB01E0EB00F01470 14381418150D818413>I<12C07E126012707E121E6C7EEA07E0EA03FE3801FFF87E133F 130F1301150E818D13>I<141814381430147014E0EB03C0EB0F80EB3F00EA03FEB45A5B 13E0138000FCC7FC150E818D13>I E /Fi 1 49 df<1218A31230A31260A312C0A2050B 7E8B09>48 D E /Fj 2 111 df<12381218A35A13C0EA3360EA3440EA7800127E126313 20EAC340EAC1800B0E7E8D10>107 D110 D E /Fk 2 50 df<121EEA61801240EAC0C0A7EA40801261EA1E 000A0D7E8C0E>48 D<121812F81218AA12FF080D7D8C0E>I E /Fl 1 52 df<134013E0EA01B0EA0318EA060C487E487E38300180386000C0481360A2006013 C03830018038180300EA0C066C5A6C5AEA01B0EA00E0134013147E9318>51 D E /Fm 2 79 df76 D<00FE13FF7E381F8018EA1BC013E01219EA18F01378133C131E131F130FEB0798EB 03D8EB01F81300A21478B41338141818147E931D>78 D E /Fn 2 53 df40 D52 D E /Fo 10 112 df<120212041208121812101230122012601240A212C0AA1240A2126012 20123012101218120812041202071E7D950D>40 D<128012401220123012101218120812 0C1204A21206AA1204A2120C1208121812101230122012401280071E7E950D>I<1360AA B512F0A238006000AA14167E9119>43 D<120FEA30C0EA6060A2EA4020EAC030A9EA4020 EA6060A2EA30C0EA0F000C137E9211>48 D<120C121C12EC120CAFEAFFC00A137D9211> I<121FEA60C01360EAF07013301260EA0070A2136013C012011380EA02005AEA08101210 EA2020EA7FE012FF0C137E9211>I61 D<12F01230A6EA33E0EA3430EA3808EA300C1306A5130CEA3808EA3430EA23E00F147F93 12>98 D<12F01230B212FC06147F9309>108 D111 D E /Fp 16 127 df<1218A31230A4126012 61A212C212C41278080D7F8C0C>19 D26 DII<13701388138CEA010CA4EA308CEA586CEA4C1EEA 9818A21218133012301320136013C0EA1080EA0F000F147F9314>35 D<124012E012601220A31240A2128003097D820A>59 D<3907E01FC00000EB0600380170 04A21338A238021C08A2130EA2486C5AA2EB0390A2380801E0A21300A20018134012FE1A 147F931A>78 D<12041244A41246127E12FC12C41244A91246127E12FC12C41244A31240 071A7E930D>93 D<1206120712061200A41238124CA2128C12981218A212301232A21264 A2123808147F930C>105 D<1330133813301300A4EA01C0EA0260EA0430136012081200 A213C0A4EA0180A4EA630012E312C612780D1A81930E>I<121E12065AA45A1338135C13 9CEA3118EA36001238EA3F80EA61C0EA60C8A3EAC0D013600E147F9312>I<3830F87C38 590C86384E0D06EA9C0EEA980C1218A248485A15801418A23960301900140E190D7F8C1D >109 DI114 D<1204120CA35AEAFF80EA1800A25AA45A1261A212621264123809127F910D>116 D<13C0A2EAFFF0A2EA00C0EA01800C067A9411>126 D E /Fq 7 107 df0 D<124012E0124003037D880A>II<1204A3EAC460EAF5E0EA3F80EA0E00EA3F80EAF5E0EAC460EA0400 A30B0D7E8D11>I10 D<1204120EA2121CA31238A212301270A21260A212C0A2 070F7F8F0A>48 D<12C0B3AB021D7D950A>106 D E /Fr 134[17 17 24 17 17 9 13 11 17 17 17 17 26 9 17 1[9 17 17 11 15 17 15 17 15 17[24 5[11 24 12[9 9 11[8 11 8 4[11 39[{ TeXBase1Encoding ReEncodeFont}33 33.333332 /Times-Roman rf /Fs 206[12 49[{TeXBase1Encoding ReEncodeFont}1 25.000000 /Times-Roman rf /Ft 25 127 df0 D<1380EA0100120212065AA25AA25AA35AA412E0AC1260A47EA37E A27EA27E12027EEA0080092A7C9E10>40 D<7E12407E12307EA27EA27EA37EA41380AC13 00A41206A35AA25AA25A12205A5A092A7E9E10>I<1306ADB612E0A2D80006C7FCAD1B1C 7E9720>43 D48 D<5A1207123F12C71207B3A5EAFFF8 0D1C7C9B15>III<130CA2131C133CA2135C13DC139CEA011C120312021204120C1208121012301220 124012C0B512C038001C00A73801FFC0121C7F9B15>I<126012F0A212601200AA126012 F0A2126004127C910C>58 D61 D70 D<39FFE00FF0391F0003C0EC01806C1400A238078002A213C000035B A2EBE00C00011308A26C6C5AA213F8EB7820A26D5AA36D5AA2131F6DC7FCA21306A31C1D 7F9B1F>86 D<12FEA212C0B3B312FEA207297C9E0C>91 D<12FEA21206B3B312FEA20729 809E0C>93 D97 D<12FC121CAA137CEA1D87381E018038 1C00C014E014601470A6146014E014C0381E018038190700EA10FC141D7F9C17>I<12FC 121CB3A9EAFF80091D7F9C0C>108 D<39FC7E07E0391C838838391D019018001EEBE01C 001C13C0AD3AFF8FF8FF8021127F9124>I111 DI115 D<38FC1F80EA1C03AD1307120CEA0E1B3803E3F014127F9117>117 D<38FF0FE0381E0700EA1C06EA0E046C5AEA039013B0EA01E012007F12011338EA021C12 04EA0C0E487E003C138038FE1FF014127F9116>120 D126 D E /Fu 14 121 df97 D<12FCA3121CA4137CEA1DFEEA1FFFEB0780381E03C0EA1C01EB00E0A6EB01C0EA1E0338 1F0780EBFF00EA1DFEEA0C7813197F9816>I<133FA31307A4EA03C7EA0FF748B4FCEA3C 1F487EEA700712E0A6EA700F12786C5A381FFFE0EA0FF7EA07C713197F9816>100 DI<1203EA0780A2EA0300C7FCA4EAFF80A31203 ACEAFFFC13FE13FC0F1A7C9916>105 D108 D110 DII<387F0FC038FF3FE0EA7F7F3807F040EBC0005BA290C7FCA8EA7FFC12FF127F13 127F9116>114 DI<12035AA4EA7FFFB5FC A20007C7FCA75BEB0380A3EB8700EA03FE6C5A6C5A11177F9616>II<387F1FC0133F131F380F1E006C5AEA03B8 13F012016C5A12017FEA03B8EA073C131CEA0E0E387F1FC038FF3FE0387F1FC013127F91 16>120 D E /Fv 206[15 49[{TeXBase1Encoding ReEncodeFont}1 29.166668 /Times-Roman rf /Fw 135[25 3[25 3[25 2[25 3[25 3[25 20[25 80[{TeXBase1Encoding ReEncodeFont}7 41.666668 /Courier rf /Fx 105[21 27[18 21 21 1[21 23 14 16 18 1[23 21 23 35 12 23 1[12 23 21 14 18 23 18 23 21 9[42 2[28 1[30 1[25 1[30 1[28 2[16 32 1[25 28 30 30 9[21 21 21 21 21 21 21 21 21 21 1[10 14 10 2[14 14 37[23 2[{ TeXBase1Encoding ReEncodeFont}52 41.666668 /Times-Bold rf /Fy 2 52 df1 D<13021307EB0D80EB18C0EB3060497E497E48487E48487E00067F48EB0180 48EB00C0481460481430481418A2006014306C14606C14C06CEB01806CEB03006C13066C 6C5A6C6C5AEB60306D5A6D5AEB0D800107C7FC13021D1E7E9C21>51 D E /Fz 24 121 df<126012F0A2126004047C8B0C>1 D<0040132000C01360006013C0 3830018038180300EA0C066C5A6C5AEA01B0EA00E0A2EA01B0EA0318EA060C487E487E38 300180386000C04813600040132013147A9320>I10 D14 DI20 D<12C012F0123C120FEA03C0EA00F01338130E6D7EEB01E0EB0078141EEC07 80A2EC1E001478EB01E0EB0780010EC7FC133813F0EA03C0000FC8FC123C127012C0C9FC A8007FB5FCB6128019247D9920>I<90387FFF800003B5FCD80780C7FC000CC8FC5A5AA2 5AA25AA81260A27EA27E120E6C7E0001B512806C7E191A7D9620>26 D<153081A381A281811680ED00C0B712F8A2C912C0ED0380160015065DA25DA35D25167E 942A>33 D<13065BA25B13381330017FB512F848B6FCD80380C8FC000EC9FC123C12F012 38120E7EEA01806CB612F87F0130C8FC7FA27FA27F25187E952A>40 D<14036E7EA26E7E811560B612F015FCC8120EED0380ED01E0ED007816E0ED0380ED0700 150CB612F85DC812605DA24A5AA24AC7FC25187E952A>I50 D<1460A214C0A2EB0180A3EB0300A21306A25BA25BA35BA25BA25BA248 5AA248C7FCA31206A25AA25AA25AA35AA25A124013287A9D00>54 D<12C0A612E0A212C0A6030E7E9000>I<0040130400C0130C00601318A36C1330A36C13 60A2381FFFE06C13C0EA0C00A238060180A238030300A3EA0186A3EA00CCA31378A31330 A2161E809C17>I<1304130CEA03CCEA0C38EA1818EA301C133CEA703EEA60361366A2EA E067A213C7A3EAE187A3EAE307A312E6A3EA6606126CEA7C0EEA3C0C1238EA1818EA1C30 EA33C0EA3000A210237E9F15>59 D<0040130200C01306B20060130CA26C1318001C1370 380F01E03803FF803800FE00171A7E981C>91 D<124012C0ACB512E014F000C0C7FCAD12 40141D7E9C19>96 D<133C13E0EA01C013801203AD13005A121C12F0121C12077E1380AD 120113C0EA00E0133C0E297D9E15>102 D<12F0121C12077E1380AD120113C0EA00E013 3C13E0EA01C013801203AD13005A121C12F00E297D9E15>I<134013C0EA0180A3EA0300 A21206A35AA25AA35AA25AA35AA21260A37EA27EA37EA27EA37EA2EA0180A3EA00C01340 0A2A7D9E10>I<12C0A21260A37EA27EA37EA27EA37EA2EA0180A3EA00C0A2EA0180A3EA 0300A21206A35AA25AA35AA25AA35AA20A2A7E9E10>I<12C0B3B3A502297B9E0C>I<121F EA3080EA7040EA6060EAE0E0A2134013001260127012307E121C1233EA7180EA61C012E0 13E0A31260EA70C01231EA1980EA07007EEA018013C0120013E0124012E0A2EAC0C01241 EA2180EA1F000B257D9C12>120 D E /FA 2 53 df40 D<1403A31406A3140C14181470EB01E0EB0F80EBFE00EAFFF0A2EA00FEEB0F80EB01E0EB 00701418140C00F81306EAFF80EA07E038007803131EEB0702EB0180A2EB00C01460A314 30142018227C9920>52 D E /FB 19 123 df<1360EA01E0120F12FF12F31203B3A2387F FF80A2111B7D9A18>49 D76 D<39FFE003FFA2390FF000307FEA0DFCEA0CFE137E7FEB1F8014C0EB 0FE0EB07F01303EB01F814FCEB00FE147F143FEC1FB015F0140F1407140314011400A2D8 FFC013701530201C7E9B25>78 D<3807F820381FFEE0EA3C07EA7801EA700012F01460A2 6C130012FEEAFFE0EA7FFE6C7E1480000F13C06C13E0EA007FEB03F01301130012C0A214 E07E38F001C0EAFC0338EFFF00EA83FC141C7D9B1B>83 D97 D99 DII<137F3801E3803803C7C0EA0787120FEB8380EB8000A5EAFFF8A2EA0F80AEEA7FF0A2 121D809C0F>I104 D<121E123FA4121EC7FCA6127FA2121FAEEAFFC0A20A1E7F9D0E>I108 D<38FF0FC0EB31E0381F40F0EB80F8A21300AB38 FFE7FFA218127F911B>110 DI<38FF3F80EBE1 E0381F80F0EB0078147C143C143EA6143C147C1478EB80F0EBC1E0EB3F0090C7FCA6EAFF E0A2171A7F911B>I 114 DI<1203A45AA25AA2EA3FFC12FFEA1F00A9 130CA4EA0F08EA0798EA03F00E1A7F9913>I<387FFF8038781F00EA703FEA603E5B13FC 5BEA01F01203485AEBC180EA0F81121F1303003E1300EA7E07EA7C0FB5FC11127F9115> 122 D E /FC 87[14 17[21 1[18 18 24[18 21 21 30 21 21 12 16 14 21 21 21 21 32 12 21 12 12 21 21 14 18 21 18 21 18 3[14 1[14 3[39 1[30 25 23 28 2[30 30 37 25 2[14 30 30 23 25 30 28 28 30 5[12 12 21 21 21 21 21 21 21 21 21 21 1[10 14 10 2[14 14 14 35[23 23 2[{ TeXBase1Encoding ReEncodeFont}70 41.666668 /Times-Roman rf /FD 40 127 df<1206120EA35AA45AA35A1340A2EAE080A2EA6300123C0A127E910F> 19 D21 D<007E1360000E13E0A3381C01C0A2EB03801400485A130E130C5B485A5BEA71C000 73C7FC12FC12F013127E9115>23 D<131EEB7180EBC0C0EA01801203EB00E05AA2380E01 C0A31480EA1C0314001306EA1E0CEA3A18EA39E00038C7FCA25AA45AA25A131B7F9115> 26 D<380FFFE05A5A3860C0001240485A12001201A348C7FCA35AA3120E120613127E91 12>28 D35 D<126012F0A2126004047C830C>58 D<126012F0A212701210A41220A212401280 040C7C830C>I<130113031306A3130CA31318A31330A31360A213C0A3EA0180A3EA0300 A31206A25AA35AA35AA35AA35AA210297E9E15>61 D<12C012F0123C120FEA03C0EA00F0 1338130E6D7EEB01E0EB0078141EEC0780A2EC1E001478EB01E0EB0780010EC7FC133813 F0EA03C0000FC8FC123C12F012C0191A7D9620>I78 DI83 D<001FB512F0391C0380703930070030002014201260124013 0E1280A2000014005BA45BA45BA45BA41201EA7FFF1C1C7F9B18>I<39FFC00FF0391C00 038015001402A25C5C121E000E5B143014205CA25C49C7FC120FEA07025BA25BA25B5BEA 03A013C05BA290C8FCA21C1D7D9B18>86 D<3A01FFC0FF803A001E003C00011C13306D13 205D010F5B6D48C7FC1482EB038414CCEB01D814F05C130080EB0170EB0278EB04381308 EB103CEB201CEB401EEB800E3801000F00027F1206001E497E39FF803FF0211C7F9B22> 88 D<1380A21220A713E01227123FEAFF8012FC12E01220AC13E01227123FEAFF8012FC 12E01220A41300A20B277E9D10>93 D<130E131113311361A213C1A2EA01C21382EA0384 A2EA07081310A21320EA0E401380EA0F00A2120E120CA2121C122C124CEA8C02EA060C13 10EA01E0101D809C11>96 DI<123F1207A2120EA45AA4EA39E0EA3A30EA 3C1812381270131CA3EAE038A313301370136013C01261EA2300121E0E1D7E9C12>III102 DIII<1307130FA213061300A61378139CEA010C1202131C12041200A21338A413 70A413E0A4EA01C01261EAF180EAF30012E6127C1024809B11>III<39381F81F0394E20C618394640E81CEB80 F0EA8F00008E13E0120EA2391C01C038A315703938038071A215E115E23970070064D830 03133820127E9124>II<13F8EA030CEA0E0648 7E1218123000701380A238E00700A3130EA25BEA60185BEA30E0EA0F8011127E9114>I< 380787803809C8603808D03013E0EA11C014381201A238038070A31460380700E014C0EB 0180EB8300EA0E86137890C7FCA25AA4123CB4FC151A819115>I114 DI<13C01201A3EA0380A4EAFFF0EA0700 A3120EA45AA4EA3820A21340A2EA1880EA0F000C1A80990F>I<380787803808C8403810 F0C03820F1E0EBE3C03840E1803800E000A2485AA43863808012F3EB810012E5EA84C6EA 787813127E9118>120 D<001C13C0EA27011247A238870380A2120EA2381C0700A4EA18 0EA3EA1C1EEA0C3CEA07DCEA001C1318EA6038EAF0305B485AEA4180003EC7FC121A7E91 14>II<13021303A2B51280A238000700130C 13081108789D15>126 D E /FE 134[18 18 28 18 21 12 16 16 1[21 21 21 30 12 1[12 12 21 21 12 18 21 18 21 21 12[23 3[25 3[23 2[14 2[25 25 3[25 5[14 12[10 14 10 2[14 14 37[21 2[{TeXBase1Encoding ReEncodeFont}37 41.666668 /Times-Italic rf /FF 134[25 25 36 1[28 17 19 22 1[28 25 28 41 14 28 1[14 28 25 17 22 28 22 28 25 12[33 28 36 5[33 2[19 3[33 1[36 1[36 6[17 2[25 25 25 25 25 25 25 49[{TeXBase1Encoding ReEncodeFont} 38 50.000000 /Times-Bold rf /FG 133[30 2[30 1[30 30 30 30 3[30 30 30 30 1[30 30 30 1[30 30 30 1[30 16[30 15[30 17[30 30 45[{TeXBase1Encoding ReEncodeFont}21 50.000000 /Courier rf /FH 3 107 df102 D<12F8120FEA03806C7E6C7E B113707F131EEB03C0EB1E0013385B5BB1485A485A000FC7FC12F812317DA419>I<12C0 B3B3AD02317AA40E>106 D E /FI 87[17 47[25 36 25 25 14 19 17 3[25 39 14 2[14 25 25 1[22 25 22 25 22 11[36 1[28 5[44 30 36 1[17 36 2[30 3[36 6[14 12[17 45[{ TeXBase1Encoding ReEncodeFont}30 50.000000 /Times-Roman rf /FJ 133[27 30 3[33 20 23 27 1[33 30 33 50 17 2[17 1[30 20 27 1[27 1[30 31[43 19[20 45[{TeXBase1Encoding ReEncodeFont}19 59.999973 /Times-Bold rf end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 %%EndSetup %%Page: 1 1 1 0 bop -2 187 a FJ(A)15 b(syntactical)f(analysis)g(of)h(non-size-incr) o(easing)d(polynomial)i(time)g(computation)471 345 y FI(Klaus)f(Aehlig)191 b(Helmut)12 b(Schwichtenber)o(g)701 424 y(Mathematisches)i(Institut)510 482 y(Ludwig-Maximilians-Uni)o(v)o (ersit)s(\250)-20 b(at)11 b(M)t(\250)-21 b(unchen)170 544 y(E-mail:)12 b FH(f)p FG(aehlig)p FH(j)p FG(schwicht)p FH(g)p FG(@rz.mathema)o(tik.uni-m)o(uenchen.d)o(e)308 694 y FF(Abstract)-91 812 y FE(A)h(pur)n(ely)g(syntactical)e(pr)n(oof)h (is)h(given)f(that)f(all)h(functions)f(de\002n-)-91 862 y(able)c(in)g(a)h(certain)g(af)o(\002ne)f(linear)g(typed)h FD(\025)p FE(-calculus)f(with)g(iter)o(ation)-91 911 y(in)i(all)f(types)h(ar)n(e)i(polynomial)c(time)i(computable)o(.)j(The) d(pr)n(oof)g(also)-91 961 y(gives)k(e)o(xplicit)g(polynomial)e(bounds)i (that)e(can)j(easily)f(be)g(calcu-)-91 1011 y(lated.)-91 1188 y FF(1)50 b(Summary)-91 1308 y FC(In)17 b([6])h(Hofmann)f (presented)h(a)h(linear)e(type)h(system)g(for)f(non-)-91 1357 y(size-increasing)c(polynomial)e(time)i(computation)f(allo)o(wing) f(un-)-91 1407 y(restricted)g(recursion)h(for)f(inducti)o(v)o(e)g (datatypes.)18 b(The)13 b(proof)e(that)-91 1457 y(all)d(de\002nable)i (functions)d(of)i(type)f FB(N)k FA(\()g FB(N)d FC(are)h(polynomial)d (time)-91 1507 y(computable)j(essentially)g(used)h(semantic)g (concepts,)g(such)g(as)g(the)-91 1557 y(set-theoretic)e(interpretation) f(of)i(terms.)-91 1624 y(W)m(e)g(present)f(a)h(dif)o(ferent)f(proof)f (of)h(the)h(same)h(result)e(for)g(a)h(slightly)-91 1674 y(modi\002ed)f(v)o(ersion)g(of)h(the)f(term)h(system,)g(which)f(uses)i (syntactical)-91 1724 y(ar)o(guments)k(only)m(.)27 b(Ho)o(we)o(v)o(er)n (,)17 b(this)d(paper)i(is)e(more)i(than)e(a)i(ne)o(w)-91 1773 y(proof)e(of)h(an)g(already)g(kno)o(wn)g(result,)h(as)f(the)g (method)g(choosen)-91 1823 y(has)c(se)o(v)o(eral)g(bene\002ts:)-50 1911 y Fz(\017)21 b FC(A)8 b(reduction)g(relation)f(is)i(de\002ned)g (on)f(the)g(term)h(system)g(such)-8 1961 y(that)h(the)h(term)g(system)g (is)f(closed)h(under)g(reduction.)j(There-)-8 2011 y(fore)e (calculations)g(can)g(be)h(done)f FE(within)e FC(the)i(system.)19 b(This)-8 2061 y(is)8 b(in)g(contrast)g(to)g([6)o(],)h(where)g(no)f (reduction)g(rules)g(are)h(gi)o(v)o(en;)-8 2111 y(instead,)j(the)g (result)g(is)g(obtained)f(via)h(a)g(set)h(theoretic)e(inter)o(-)-8 2160 y(pretation.)-50 2237 y Fz(\017)21 b FC(It)14 b(is)h(not)g(only)f (sho)o(wn)g(that)h(e)o(v)o(ery)h(function)d(is)i(polytime,)-8 2287 y(b)o(ut)f(e)o(xplicit)f(polynomial)g(bounds)g(are)i(gi)o(v)o(en)f (that)g(can)h(be)-8 2337 y(determined)f(easily)g(for)g(e)o(v)o(ery)h (gi)o(v)o(en)f(term.)25 b(An)14 b(e)o(xample)-8 2387 y(\(for)9 b(insertion)g(sort\))h(is)g(gi)o(v)o(en)g(in)f(5.10.)-50 2463 y Fz(\017)21 b FC(The)c(semantical)h(size)f(measure)h(\223minimal) f(upper)f(bound)-8 2513 y(of)g(gro)o(wth\224)f(\(the)h(size)h(function) d(in)i([6,)i Fz(x)p FC(3.2]\))e(for)g(terms)-8 2563 y(of)c(higher)h (type)f(is)h(replaced)g(by)g(the)g(much)g(simpler)n(,)h(com-)-8 2613 y(putable,)19 b(syntactical)f(measure:)29 b(\223number)18 b(of)f(free)i(v)o(ari-)-8 2662 y(ables\224.)1028 694 y Fz(\017)i FC(The)12 b(role)g(of)f(the)h Fy(3)p FC(-type)f(becomes)i (more)f(transparent,)g(for)1070 744 y(the)c(follo)o(wing)f(reasons.)13 b(First,)8 b(all)h(de\002nable)g(functions)e(ob-)1070 794 y(viously)g(are)i(non-size-increasing)f(with)f(respect)i(to)f(our)g (size)1070 844 y(measure,)i(since)f(there)f(will)f(be)h(no)g(reduction) e(rule)i(introduc-)1070 894 y(ing)h(ne)o(w)i(v)o(ariables.)i(Secondly)m (,)d(the)h(facts)f(that)1120 974 y Fx(\226)20 b FC(there)11 b(are)g(no)f(closed)g(terms)h(of)f(type)f Fy(3)p FC(,)1120 1039 y Fx(\226)20 b FC(the)8 b(successor)h(functions)e(ha)o(v)o(e)i (type)f Fy(3)j FA(\()h FB(N)g FA(\()g FB(N)p FC(,)1120 1103 y Fx(\226)20 b FC(we)11 b(ha)o(v)o(e)g(a)g(linear)f(typing)f (discipline)1070 1183 y(together)i(ensure)h(that)f(ground)g(terms)h (that)f(are)h(lar)o(ge)g(in)g(the)1070 1233 y(usual)e(size)h(measure)g (are)g(also)g(lar)o(ge)f(in)g(this)f(ne)o(w)h(size)h(mea-)1070 1283 y(sure.)1028 1364 y Fz(\017)21 b FC(It)c(seems)h(that)f(the)g (simplicity)e(of)i(the)g(present)g(approach)1070 1413 y(makes)e(it)f(easier)i(to)e(design)g(arithmetical)h(systems)g(where) 1070 1463 y(the)10 b(proofs)f(can)i(be)g(normalised)f(in)g(polynomial)e (time.)987 1597 y FF(2)50 b(Intr)o(oduction)10 b(and)i(r)o(elated)g (work)987 1722 y FC(Recent)20 b(research)i(has)e(pro)o(vided)g(man)o(y) g(characterizations)h(of)987 1772 y Fw(Ptime)16 b FC(\(the)f(class)i (of)f(all)f(functions)g(computable)h(in)f(polyno-)987 1822 y(mial)10 b(time\))f(by)h(means)h(of)e(appropriate)g(restrictions) g(of)g(the)h(terms)987 1871 y(in)h(G)s(\250)-17 b(odel')n(s)11 b FD(T)18 b FC([1)o(,)12 b(2,)g(5].)17 b(Consider)11 b(for)g(e)o(xample)h(the)g(follo)o(wing)987 1921 y(functions)g(on)g (unary)h(coded)h(natural)e(numbers)1701 1906 y Fv(1)1718 1921 y FC(,)i(which)f(lead)g(to)987 1971 y(e)o(xponential)c(gro)o(wth:) 1233 2057 y Fu(double)n Ft(\(0\))j(=)g(0)1202 2119 y Fu(double)o Ft(\()p FD(S)r(x)p Ft(\))g(=)g FD(S)r(S)r Fu(double)p Ft(\()p FD(x)p Ft(\))1298 2206 y Fu(exp)o Ft(\(0\))g(=)g FD(S)r Ft(0)1267 2268 y Fu(exp)p Ft(\()p FD(S)r(x)p Ft(\))g(=)g Fu(double)o Ft(\()p Fu(exp)o Ft(\()p FD(x)p Ft(\)\))p 987 2308 394 2 v 1032 2335 a Fs(1)1047 2347 y Fr(Of)f(course,)g(no-one)e(actually)h(uses)h(unary)e(coded)h (numbers)f(when)i(dealing)987 2386 y(with)e(questions)e(of)h (complexity)n(.)i(Ho)o(we)o(ver)o(,)d(examples)g(with)i(unary)e(coded)g (num-)987 2426 y(bers)i(are)h(very)e(general)h(ones,)h(as)g(many)e (data)h(structures)g(can)h(be)f(seen)g(as)h(exten-)987 2465 y(sions)c(of)h(unary)f(coded)g(numbers:)i(binary)e(numerals)g(are) h(unary)f(ones,)g(if)i(we)f(don')o(t)987 2505 y(distinguish)i(the)h (two)g(successor)f(functions;)h(lists)h(can)f(be)f(seen)h(as)g(unary)f (coded)987 2544 y(numbers)e(if)h(we)g(don')o(t)g(care)g(about)f(their)h (elements.)1020 2584 y(In)13 b(other)f(words,)h(as)f(unary)f(numbers)g (can)h(be)g(embedded)f(into)h(many)f(com-)987 2623 y(monly)i(used)h (data)g(structures,)i(counterexamp)o(les)c(with)j(unary)e(numbers)g (also)987 2663 y(work)7 b(with)h(almost)g(any)f(of)h(the)g(interesting) f(data)h(structures.)p eop %%Page: 2 2 2 1 bop -91 42 a FC(Approaches)15 b(based)h(on)e(\223predicati)o(v)o(e) h(recursion\224)g([1,)g(8])g(ar)o(gue)-91 91 y(that)e(this)g(is)h(due)g (to)f(the)h(way)g Fu(double)f FC(is)h(called:)19 b(the)14 b(pre)o(vious)-91 141 y(v)o(alue)9 b(of)g(an)g(outer)g(recursion)g (\(i.e.)h Fu(exp)o Ft(\()p FD(x)p Ft(\))p FC(\))f(is)g(used)h(as)g (recursi)o(v)o(e)-91 191 y(ar)o(gument)h(of)f(an)h(inner)f(recursion)g (\(i.e.)h(is)g(used)g(as)g(ar)o(gument)g(for)-91 241 y Fu(double)o FC(\).)-91 309 y(Ho)o(we)o(v)o(er)n(,)i(although)e(all)g FE(functions)f FC(computable)i(in)f(polynomial)-91 358 y(time)g(can)i(be)e(de\002ned)h(in)f(such)h(a)g(restricted)f(term)h (system,)h(man)o(y)-91 408 y(natural)19 b FE(algorithms)g FC(are)i(e)o(xcluded,)i(particularly)c(if)h(the)o(y)g(in-)-91 458 y(v)o(olv)o(e)12 b(nested)g(recursions.)19 b(Standard)12 b(e)o(xamples)i(are)f(sorting)d(al-)-91 508 y(gorithms)j(like)f (insertion)h(sort,)i(which)e(has)h(the)g(same)i(recursi)o(v)o(e)-91 558 y(structure)9 b(as)i Fw(exp)p FC(:)83 636 y Fu(insert)o Ft(\()p FD(a;)c Ft([]\))j(=)q([)p FD(a)p Ft(])14 698 y Fu(insert)n Ft(\()p FD(a;)d Ft([)p FD(b)k Fz(j)g FD(`)p Ft(]\))g(=)q([)p FD(b)384 681 y Fq(0)406 698 y Fz(j)g Fu(insert)o Ft(\()p FD(a)598 681 y Fq(0)610 698 y FD(;)c(`)p Ft(\)])354 760 y FD(a)376 745 y Fq(0)387 760 y FD(;)g(b)424 745 y Fq(0)445 760 y FC(a)k(permutation)e(of)h FD(a;)d(b)354 822 y FC(with)i FD(b)456 807 y Fq(0)479 822 y Fz(\024)j FD(a)545 807 y Fq(0)211 910 y Fu(sort)o Ft(\([]\))f(=)h([])137 972 y Fu(sort)o Ft(\([)p FD(a)g Fz(j)f FD(`)p Ft(]\))g(=)h Fu(insert)o Ft(\()p FD(a;)7 b Fu(sort)n Ft(\()p FD(`)p Ft(\)\))-91 1050 y FC(Caseiro)k([3)o(])h(observ)o(ed)f(this)f(fact)h (and)h(studied)e(man)o(y)i(related)f(e)o(x-)-91 1100 y(amples;)h(her)g(work)f(resulted)g(in)g(some)h(\(partially)e (semantic\))j(cri-)-91 1149 y(teria)g(for)h(algorithms)e(which)i (ensure)g(that)f(the)o(y)h(run)f(in)g(polyno-)-91 1199 y(mial)f(time.)18 b(In)12 b(the)g(e)o(xample)i(of)d(insertion)g(sort)g (the)h(reason)h(why)-91 1249 y(this)h(recursion)h(does)h(not)e(lead)i (to)f(e)o(xponential)g(gro)o(wth)f(is)h(that)-91 1299 y Fu(insert)8 b FC(does)i(not)e(increase)j(the)e(size)h(of)f(its)g (input.)i(Hofmann)f([6)o(])-91 1349 y(took)e(up)h(this)f(line)h(of)f (research)j(and)e(formulated)g(a)g(ne)o(w)h(term)f(sys-)-91 1399 y(tem)i(with)g(a)h(special)f(type)g Fy(3)g FC(of)g(\223coins\224,) i(which)e(only)f(allo)o(ws)h(to)-91 1448 y(de\002ne)k (non-size-increasing)g Fw(Ptime)f FC(functions,)h(b)o(ut)g(can)g(also) -91 1498 y(accomodate)d(nested)e(recursions.)j(The)e(basic)g(idea)g(is) f(that)f(when-)-91 1548 y(e)o(v)o(er)j(a)f(function)e(increases)j(the)f (size)g(of)g(its)f(ar)o(gument)h(\(like)f(a)h(bi-)-91 1598 y(nary)k(successor)i(function\),)f(then)g(one)f(has)i(to)e (\223pay\224)h(for)g(it)f(by)-91 1648 y(inputting)7 b(a)k(coin)f (\(i.e.)h(a)g(term)f(of)g(type)g Fy(3)p FC(\).)-91 1716 y(The)18 b(present)f(note)g(can)h(be)g(seen)g(as)g(a)g(straightening)e (of)h(Hof-)-91 1765 y(mann')n(s)g([6)o(].)33 b(W)m(e)18 b(present)f(a)g(ne)o(w)g(proof)f(of)h(his)f(main)i(result,)-91 1815 y(which)11 b(apart)i(from)e(being)h(simpler)f(pro)o(vides)h(more)g (insight)f(into)-91 1865 y(what)18 b(actually)f(is)h(going)f(on,)j(and) e(in)f(particular)g(pro)o(vides)h(an)-91 1915 y(e)o(xplicit)e (construction)f(of)h(the)h(polynomials.)30 b(W)m(e)17 b(ha)o(v)o(e)h(listed)-91 1965 y(what)c(we)g(vie)o(w)g(as)g(adv)o (antages)h(of)e(our)h(proof)f(in)g(the)h(summary)-91 2014 y(abo)o(v)o(e.)k(It)11 b(is)g(our)g(hope)g(that)g(this)g (simpli\002cation)e(will)i(make)h(fur)o(-)-91 2064 y(ther)e(progress)g (easier)n(.)-91 2193 y FF(3)50 b(T)l(ypes)13 b(and)e(terms)-91 2314 y FC(T)m(ypes)h(are)g(b)o(uilt)e(from)i(the)g(base)g(types)g FB(N)g FC(\(to)f(be)h(interpreted)f(as)-91 2364 y(binary)f(coded)h (natural)f(numbers\),)i Ft(b)q(o)q(ol)o FC(,)g(and)f(a)g(special)g (type)g Fy(3)p FC(.)-91 2413 y(This)i(type)g(may)h(be)g(interpreted)e (as)i(a)g(pointer)e(to)h(free)h(memory)m(,)-91 2463 y(as)f(in)e([4].)19 b(From)12 b(a)h(more)g(technical)f(point)f(of)h(vie)o(w)m(,)h(lemma)g (5.3)-91 2513 y(will)8 b(sho)o(w)i(that)f(there)g(are)i(no)e(closed)h (terms)g(of)f(this)g(type.)k(There-)-91 2563 y(fore)f(this)e(type)i (can)g(be)h(used)f(to)f(ensure)h(that)f(terms)i(contain)e(free)-91 2613 y(v)o(ariables.)16 b(F)o(or)c(e)o(xample)g(the)g(type)f Fy(3)i FA(\()h FB(N)g FA(\()g FB(N)e FC(of)f(the)g(suc-)-91 2662 y(cessor)k(functions)f(together)f(with)h(the)h(linear)f(typing)f (discipline)987 42 y(will)j(make)h(sure)h(that)e(the)h(usual)g(length)f (measure)i(for)f(natural)987 91 y(numbers)d(and)g(the)g(more)g (technical)g(measure)i(\223number)e(of)g(free)987 141 y(v)o(ariables\224)c(will)f(be)i(the)f(same.)k(As)c(the)g(term)h (system)f(is)g(based)h(on)987 191 y(the)g(intuition)e(that)i(length)g (is)g(e)o(xpressed)i(by)e(the)h(number)f(of)h(free)987 241 y(v)o(ariables,)k(the)f(interesting)e(terms)i(are)h(not)e(only)g (closed)h(terms,)987 291 y(b)o(ut)9 b(more)h(importantly)e(\223almost)i (closed\224)h(terms,)g(i.e.)f(terms)g(with)987 340 y(free)h(v)o (ariables)f(of)g(type)g Fy(3)g FC(only)m(.)987 446 y Fx(De\002nition)g(3.1)g(\(Finite)g(linear)g(types\).)21 b FC(The)40 b(set)f(of)g(linear)987 496 y(types)10 b(is)g(de\002ned)h (inducti)o(v)o(ely)d(as)987 588 y FD(\034)r(;)f(\032)p Ft(::=)22 b Fy(3)11 b Fz(j)g FB(N)h Fz(j)f Ft(b)q(o)q(ol)g Fz(j)g FD(\034)16 b FA(\()c FD(\032)g Fz(j)f FD(\034)j Fz(\012)c FD(\032)i Fz(j)f FD(\034)j Fz(\002)9 b FD(\032)j Fz(j)f FB(L)p Ft(\()p FD(\034)5 b Ft(\))987 737 y FB(L)p Ft(\()p FD(\034)g Ft(\))11 b FC(denotes)f(the)h(list)e(type.)14 b FD(\034)h Fz(\012)10 b FD(\032)h FC(and)g FD(\034)j Fz(\002)c FD(\032)h FC(can)h(both)d(be)i(in-)987 786 y(terpreted)d(as)h(ordered)f(pairs;)g(ho)o(we)o(v)o(er)n(,)i(the)e (meaning)g(of)g(linearity)987 836 y(for)g(those)h(types)f(is)g(dif)o (ferent:)j(from)d(a)i(tensor)o(-product)d FD(\034)h Fz(\012)s FD(\032)h FC(both)987 886 y(components)h(can)g(be)g(used)h(once,)f (whereas)h(in)f(the)f(case)j(of)e(an)g(or)o(-)987 936 y(dinary)j(pair)n(,)j(the)e(pair)g(itself)g(can)h(be)f(used)h(only)e (once,)j(i.e.)f(one)987 986 y(has)g(to)f(choose)g(which)g(component)h (of)f(the)g(pair)g(is)g(to)g(be)h(used.)987 1036 y(As)d(can)h(be)f (seen)h(from)f(4.3,)h Fz(\012)g FC(corresponds)e(to)h FA(\()p FC(,)h(whereas)g Fz(\002)987 1085 y FC(corresponds)d(to)g Ft(b)q(o)q(ol)o FC(.)987 1178 y(T)m(erms)16 b(are)f(b)o(uilt)e(from)h (v)o(ariables)g FD(x;)7 b(y)q(;)g(z)r(;)g(:)g(:)g(:)19 b FC(and)c(constructor)987 1228 y(symbols)d FD(c)p FC(.)18 b(Each)c(v)o(ariable)d(has)i(a)g(type)e(and)i(it)e(is)h(assumed)h(that) 987 1278 y(there)f(are)h(in\002nitely)e(man)o(y)i(v)o(ariables)f(of)g (each)h(type.)19 b(The)13 b(nota-)987 1328 y(tion)c FD(x)1086 1313 y Fp(\034)1117 1328 y FC(should)g(e)o(xpress)i(that)f(the)g(v)o (ariable)g FD(x)g FC(has)h(type)f FD(\034)5 b FC(.)987 1433 y Fx(De\002nition)10 b(3.2)g(\(T)l(erms\).)21 b FC(The)11 b(set)g(of)f(terms)h(is)f(inducti)o(v)o(ely)e(de-)987 1483 y(\002ned)i(by)987 1576 y FD(t;)d(s)p Ft(::=)21 b FD(x)1141 1561 y Fp(\034)1173 1576 y Fz(j)11 b FD(c)h Fz(j)f FD(\025x)1297 1561 y Fp(\034)1324 1576 y FD(t)h Fz(j)f(h)p FD(t;)c(s)p Fz(i)12 b(j)f FD(ts)h Fz(j)f(f)o FD(t)p Fz(g)h(j)f(f)p FD(t;)c(s)p Fz(g)987 1724 y FC(These)13 b(terms)f(should)f(be)h(seen)h(as)g(our)e(\223ra)o(w)i(syntax\224;)f (only)f(cor)o(-)987 1774 y(rectly)g(typed)g(terms)i(\(in)e(the)g(sense) i(of)f(de\002nition)e(3.4\))h(represent)987 1824 y(meaningful)e (functions.)987 1916 y(The)i(idea)f(for)g(the)g Fz(f\001)o(g)g FC(and)h Fz(f)o(\001)p FD(;)c Fz(\001)o(g)j FC(term)g(constructs)g(is)g (taken)g(from)987 1966 y([7].)20 b(T)m(erms)13 b(of)g(this)e(form)i (appear)g(only)f(as)h(ar)o(guments)g(in)f(an)h FB(N)987 2016 y FC(or)c FB(L)p Ft(\()p FD(\034)c Ft(\))k FC(elimination.)i(This) e(e)o(xplicit)f(marking)g(of)h(the)g(step)g(terms)987 2066 y(in)g(iteration)f(constructs)h(is)g(not)g(only)f(technically)h (con)n(v)o(enient)g(b)o(ut)987 2116 y(also)i(allo)o(ws)f(one)h(to)f (see)i(the)e(time)h(comple)o(xity)f(of)h(a)g(term)g(at)g(\002rst)987 2165 y(glance:)17 b(the)12 b(constant)f(coef)o(\002cient)i(of)f(the)g (polynomial)e(de\002ning)987 2215 y(the)j(run-time)f(is)h(simply)g(the) g(number)g(of)g(symbols)g(outside)f(an)o(y)987 2265 y(braces,)k(the)d (coef)o(\002cient)h(for)f FD(X)k FC(is)d(number)f(of)g(symbols)g (within)987 2315 y(one)d(pair)g(of)g(braces)i(and)e(so)g(on.)j(See)e (de\002nition)e(5.5)h(for)g(details.)987 2408 y(The)g(notations)e FD(t)1235 2400 y(~)1238 2408 y(t)h FC(and)g FD(\025)o(~)-20 b(x)1378 2393 y Fp(~)k(\034)1407 2408 y FD(t)9 b FC(are)h(de\002ned)g (as)g(usual,)g(so)f FD(\025x)1869 2393 y Fp(\034)1890 2408 y FD(;)e(y)1930 2393 y Fp(\032)1956 2408 y FD(t)987 2458 y FC(is)j(an)i(abbre)o(viation)d(for)h FD(\025x)1400 2443 y Fp(\034)1421 2458 y Ft(\()p FD(\025y)1482 2443 y Fp(\032)1509 2458 y FD(t)p Ft(\))p FC(.)15 b(T)m(erms)d(that)e(only)g (dif)o(fer)g(in)987 2507 y(the)g(naming)g(of)g(bound)f(v)o(ariables)h (are)h(identi\002ed.)987 2613 y Fx(De\002nition)f(3.3)g(\(Constructor)h (symbols\).)20 b FC(The)57 b(constructor)987 2662 y(symbols)10 b(and)g(their)f(types)h(are)p eop %%Page: 3 3 3 2 bop -70 35 a FB(t)133 b Ft(b)q(o)q(ol)-70 85 y FB(f)k Ft(b)q(o)q(ol)-70 134 y FB(1)128 b(N)-70 184 y(S)-43 190 y Fo(0)82 184 y Fy(3)12 b FA(\()f FB(N)h FA(\()g FB(N)-70 234 y(S)-43 240 y Fo(1)82 234 y Fy(3)g FA(\()f FB(N)h FA(\()g FB(N)-70 284 y(nil)-17 290 y Fp(\034)82 284 y FB(L)p Ft(\()p FD(\034)5 b Ft(\))-70 334 y FB(cons)20 340 y Fp(\034)82 334 y Fy(3)12 b FA(\()f FD(\034)17 b FA(\()11 b FB(L)p Ft(\()p FD(\034)5 b Ft(\))12 b FA(\()f FB(L)p Ft(\()p FD(\034)5 b Ft(\))-70 384 y Fz(\012)-38 390 y Fp(\034)r(;\032)82 384 y FD(\034)17 b FA(\()11 b FD(\032)h FA(\()g FD(\034)i Fz(\012)c FD(\032)-91 496 y FB(1)f FC(is)g(to)g(be)h(interpreted)e(as)i(the)g(natural)e(number)i (one)f(and)h(the)f(suc-)-91 546 y(cessor)i(functions)e FB(S)215 552 y Fp(i)238 546 y FC(as)i(the)f(usual)g(binary)g(successor) h(functions,)-91 596 y(i.e.)g FD(x)g Fz(7!)g Ft(2)e Fz(\001)g FD(x)g Ft(+)g FD(i)p FC(.)-91 672 y(A)i FE(conte)o(xt)i FC(is)e(a)h(set)f(of)g(v)o(ariables.)17 b(F)o(or)11 b(two)g(conte)o (xts)g Ft(\000)747 678 y Fo(1)777 672 y FC(and)h Ft(\000)875 678 y Fo(2)-91 722 y FC(the)e(notation)f Ft(\000)143 728 y Fo(1)162 722 y FD(;)e Ft(\000)207 728 y Fo(2)236 722 y FC(stands)k(for)f(the)h(union,)f(e)o(xpressing)g(that)h Ft(\000)875 728 y Fo(1)-91 772 y FC(and)g Ft(\000)6 778 y Fo(2)36 772 y FC(are)h(disjoint.)h(F)o(or)e(conte)o(xts)g(consisting) f(of)h(one)g(element)-91 822 y(we)g(also)f(write)g FD(x)165 807 y Fp(\034)195 822 y FC(instead)g(of)g Fz(f)p FD(x)413 807 y Fp(\034)434 822 y Fz(g)p FC(.)-91 898 y(The)g(ne)o(xt)f (de\002nition)e(states)j(which)f(terms)g(of)g(our)g(ra)o(w)h(syntax)e (are)-91 948 y(correctly)i(typed.)i Ft(\000)g Fz(`)f FD(t)271 933 y Fp(\034)303 948 y FC(is)e(to)h(be)h(read)f(as)h(\223)p FD(t)g FC(is)f(a)h(typed)e(term)i(of)-91 997 y(type)f FD(\034)15 b FC(with)9 b(free)i(v)o(ariables)f(in)g Ft(\000)p FC(\224.)-91 1074 y(The)h(typing)e(system)j(is)e(based)i(on)e (elimination)f(rules.)15 b(Therefore)-91 1124 y(for)c(e)o(v)o(ery)h (type)g(dif)o(ferent)e(to)h Fy(3)h FC(there)g(is)f(a)i(rule)e (describing)g(ho)o(w)-91 1173 y(to)h(use)i(terms)f(of)g(this)g(type;)g (in)g(all)g(these)g(rules)g(the)g(elimination)-91 1223 y(is)h(written)e(as)j(\(formal\))f(application.)23 b(F)o(or)14 b(the)g(right)e(hand)i(side)-91 1273 y(of)e(such)g(an)h(application)e (a)h(notation)f(is)h(choosen)g(that)g(e)o(xpresses)-91 1323 y(best)g(the)g(computational)f(beha)o(viour)h(of)g(the)g(terms)g (used)h(for)e(the)-91 1373 y(elimination.)g(This)e(a)o(v)o(oids)h (duplication)d(of)i(syntax,)h(e.g.)g(with)e(the)-91 1422 y(pair)15 b Fz(h)p FD(t;)7 b(s)p Fz(i)15 b FC(we)g(ha)o(v)o(e)h(a)g (notation)d(e)o(xpressing)i(that)g(e)o(xactly)g(one)-91 1472 y(of)c(the)h(terms)g FD(t)f FC(and)h FD(s)g FC(will)f(be)h (needed.)17 b(Using)11 b(this)g(syntax)g(also)-91 1522 y(for)j(\223if)h FD(:)7 b(:)g(:)20 b FC(then)14 b FD(:)7 b(:)g(:)21 b FC(else)15 b FD(:)7 b(:)g(:)20 b FC(\224)c(a)o(v)o(oids)e (introducing)f(another)-91 1572 y(notation)8 b(with)h(e)o(xactly)i(the) f(same)i(computational)d(meaning.)-91 1648 y(\223Data)15 b(types\224,)h(i.e.)f(types)f(where)h(it)f(is)g(possible)f(to)h(retrie) o(v)o(e)h(all)-91 1698 y(the)e(stored)h(information)d(by)j(a)g(single)f (use)h(of)g(an)g(object)f(of)g(this)-91 1748 y(type,)d(are)g (introduced)f(by)g(constants.)k(Only)c(\223abstractions\224)h(ha)o(v)o (e)-91 1798 y(special)e(introduction)d(rules.)12 b(\(In)c(the)g(system) g(we)g(ha)o(v)o(e)h(two)e(forms)-91 1847 y(of)15 b(abstraction:)22 b(the)15 b FD(\025)p FC(-abstraction)g(and)h(the)f(pair)n(.\))28 b(This)15 b(way)-91 1897 y(of)g(introduction)e(allo)o(ws)j(the)f (relati)o(v)o(ely)g(simple)h(de\002nition)e(4.4)-91 1947 y(of)h(the)f(term)i(closure)f(of)f(reductions)h(e)o(xpressing)g(that)f (we)i(may)-91 1997 y(reduce)11 b(within)d(data,)j(b)o(ut)f(not)f(under) h(abstractions.)-91 2085 y Fx(De\002nition)f(3.4)i(\()p Ft(\000)g Fz(`)h FD(t)260 2070 y Fp(\034)281 2085 y Fx(\).)21 b FC(The)12 b(relation)f Ft(\000)j Fz(`)h FD(t)636 2070 y Fp(\034)668 2085 y FC(is)d(inducti)o(v)o(ely)-91 2135 y(de\002ned)e(as)h(follo)o(ws:)p -70 2218 224 2 v -50 2253 a Ft(\000)p FD(;)c(x)19 2238 y Fp(\034)51 2253 y Fz(`)12 b FD(x)112 2238 y Fp(\034)693 2252 y Ft(\()p FD(V)e(ar)q Ft(\))-50 2383 y FD(c)h FC(of)f(type)f FD(\034)p -70 2400 220 2 v -17 2434 a Ft(\000)i Fz(`)h FD(c)75 2419 y Fp(\034)693 2434 y Ft(\()p FD(const)p Ft(\))-34 2565 y(\000)d Fz([)g(f)p FD(x)83 2550 y Fp(\034)103 2565 y Fz(g)i(`)h FD(t)187 2550 y Fp(\032)p -70 2581 314 2 v -50 2618 a Ft(\000)g Fz(`)g Ft(\()p FD(\025x)89 2603 y Fp(\034)116 2618 y FD(t)p Ft(\))148 2598 y Fp(\034)s Fn(\()p Fp(\032)693 2617 y Ft(\()p FA(\()755 2602 y Fo(+)783 2617 y Ft(\))1028 35 y(\000)1054 41 y Fo(1)1085 35 y Fz(`)f FD(t)1136 20 y Fp(\034)s Fn(\()p Fp(\032)1294 35 y Ft(\000)1320 41 y Fo(2)1350 35 y Fz(`)h FD(s)1406 20 y Fp(\034)p 1008 51 441 2 v 1107 86 a Ft(\000)1133 92 y Fo(1)1151 86 y FD(;)7 b Ft(\000)1196 92 y Fo(2)1226 86 y Fz(`)12 b Ft(\()p FD(ts)p Ft(\))1330 65 y Fp(\032)1771 86 y Ft(\()p FA(\()1833 71 y Fq(\000)1861 86 y Ft(\))1028 211 y(\000)g Fz(`)g FD(t)1118 196 y Fp(\034)1222 211 y Ft(\000)f Fz(`)h FD(s)1315 196 y Fp(\032)p 1008 227 348 2 v 1070 266 a Ft(\000)f Fz(`)h(h)p FD(t;)7 b(s)p Fz(i)1229 245 y Fp(\034)s Fq(\002)p Fp(\032)1771 264 y Ft(\()p Fz(\002)1819 249 y Fo(+)1847 264 y Ft(\))1032 390 y(\000)12 b Fz(`)g FD(t)1122 375 y Fp(\034)s Fq(\002)p Fp(\032)p 1008 407 203 2 v 1028 442 a Ft(\000)g Fz(`)g Ft(\()p FD(t)p FB(t)p Ft(\))1169 421 y Fp(\034)1771 441 y Ft(\()p Fz(\002)1819 424 y Fq(\000)1819 453 y Fo(1)1848 441 y Ft(\))1032 566 y(\000)f Fz(`)h FD(t)1121 551 y Fp(\034)s Fq(\002)p Fp(\032)p 1008 583 202 2 v 1028 618 a Ft(\000)g Fz(`)g Ft(\()p FD(t)p FB(f)5 b Ft(\))1169 597 y Fp(\032)1771 617 y Ft(\()p Fz(\002)1819 599 y Fq(\000)1819 628 y Fo(0)1848 617 y Ft(\))1028 742 y(\000)1054 748 y Fo(1)1085 742 y Fz(`)11 b FD(t)1136 727 y Fo(b)q(o)q(ol)1284 742 y Ft(\000)1310 748 y Fo(2)1340 742 y Fz(`)h FD(s)1396 727 y Fp(\034)1500 742 y Ft(\000)1526 748 y Fo(2)1556 742 y Fz(`)g FD(r)1613 727 y Fp(\034)p 1008 759 648 2 v 1171 794 a Ft(\000)1197 800 y Fo(1)1215 794 y FD(;)7 b Ft(\000)1260 800 y Fo(2)1290 794 y Fz(`)12 b Ft(\()p FD(t)7 b Fz(h)p FD(s;)g(r)q Fz(i)p Ft(\))1471 773 y Fp(\034)1771 793 y Ft(\(b)q(o)q(ol)1866 775 y Fq(\000)1894 793 y Ft(\))1028 918 y(\000)1054 924 y Fo(1)1085 918 y Fz(`)k FD(t)1136 903 y Fp(\034)s Fq(\012)p Fp(\032)1283 918 y Ft(\000)1309 924 y Fo(2)1328 918 y FD(;)c(x)1371 903 y Fp(\034)1391 918 y FD(;)g(y)1431 903 y Fp(\032)1462 918 y Fz(`)12 b FD(s)1518 903 y Fp(\033)p 1008 935 554 2 v 1078 970 a Ft(\000)1104 976 y Fo(1)1123 970 y FD(;)7 b Ft(\000)1168 976 y Fo(2)1197 970 y Fz(`)12 b Ft(\()p FD(t)p Ft(\()p FD(\025x)1329 954 y Fp(\034)1350 970 y FD(;)7 b(y)1390 954 y Fp(\032)1417 970 y FD(s)p Ft(\)\))1468 949 y Fp(\033)1771 969 y Ft(\()p Fz(\012)1819 954 y Fq(\000)1848 969 y Ft(\))1028 1094 y(\000)12 b Fz(`)g FD(t)1118 1079 y Fm(N)1232 1094 y Fz(;)f(`)h FD(s)1320 1100 y Fp(i)1334 1079 y Fl(3)p Fn(\()p Fp(\034)s Fn(\()p Fp(\034)p 1008 1111 485 2 v 1080 1148 a Ft(\000)f Fz(`)h Ft(\()p FD(t)7 b Fz(f)p FD(s)1232 1154 y Fo(0)1251 1148 y FD(;)g(s)1289 1154 y Fo(1)1307 1148 y Fz(g)p Ft(\))1344 1127 y Fp(\034)s Fn(\()p Fp(\034)1771 1146 y Ft(\()p FB(N)1824 1131 y Fq(\000)1853 1146 y Ft(\))1028 1274 y(\000)12 b Fz(`)g FD(t)1118 1259 y Fm(L)p Fo(\()p Fp(\034)s Fo(\))1270 1274 y Fz(;)f(`)h FD(s)1358 1259 y Fl(3)p Fn(\()p Fp(\034)s Fn(\()p Fp(\032)p Fn(\()p Fp(\032)p 1008 1291 562 2 v 1157 1328 a Ft(\000)f Fz(`)h Ft(\()p FD(t)7 b Fz(f)p FD(s)p Fz(g)p Ft(\))1346 1307 y Fp(\032)p Fn(\()p Fp(\032)1771 1325 y Ft(\()p FB(L)p Ft(\()p FD(\034)e Ft(\))1871 1310 y Fq(\000)1899 1325 y Ft(\))987 1483 y FC(It)17 b(is)g(crucial)g(that)f (we)i(require)f(the)g(step)g(terms)h(in)e Ft(\()p FB(N)1849 1468 y Fq(\000)1878 1483 y Ft(\))h FC(and)987 1533 y Ft(\()p FB(L)p Ft(\()p FD(\034)5 b Ft(\))1087 1518 y Fq(\000)1115 1533 y Ft(\))17 b FC(to)e(be)i(closed.)32 b(Otherwise)16 b(it)g(would)f(not)g(be)i(possi-)987 1582 y(ble)9 b(to)f(de\002ne)i(reduction)e(rules)h(in)g(such)g(a)h(way)f (that)f(the)h(system)h(is)987 1632 y(closed)e(under)g(reduction,)g (since)h(free)g(v)o(ariables)f(in)g(the)g(step)g(terms)987 1682 y(would)h(be)h(duplicated)g(otherwise.)987 1752 y(Immediately)g(ob)o(vious)f(from)h(the)h(de\002nition)d(is)987 1834 y Fx(Pr)o(oposition)i(3.5)g(\(W)m(eakening\).)20 b Ft(\000)d Fz(`)g FD(t)1620 1819 y Fp(\034)1641 1834 y FE(;)d Ft(\000)j Fz(\032)g Ft(\000)1787 1819 y Fq(0)1812 1834 y Ft(=)-7 b Fz(\))13 b Ft(\000)1918 1819 y Fq(0)1946 1834 y Fz(`)987 1884 y FD(t)1002 1869 y Fp(\034)1023 1884 y FE(.)987 1987 y FC(The)i(notation)d FD(t)1231 1972 y Fp(\034)1266 1987 y FC(should)h(e)o(xpress)j(that)d(there)i(is)f (a)g Ft(\000)h FC(such)f(that)987 2037 y Ft(\000)i Fz(`)h FD(t)1086 2022 y Fp(\034)1107 2037 y FC(.)k(The)14 b(smallest)f(such)g Ft(\000)g FC(is)g(called)g(the)g(set)g(of)f(free)i(v)o(ari-)987 2087 y(ables.)24 b(This)14 b(is)g(a)g(meaningful)f(de\002nition;)h (more)g(precisely)m(,)i(by)987 2136 y(induction)8 b(on)i(the)g (de\002nition)f(of)h Ft(\000)h Fz(`)h FD(t)1571 2121 y Fp(\034)1592 2136 y FC(,)e(one)h(easily)f(v)o(eri\002es)987 2218 y Fx(Lemma)f(3.6.)21 b FE(F)l(or)16 b(eac)o(h)g(term)f FD(t)h FE(ther)n(e)g(is)f(at)g(most)g(one)g(type)g FD(\034)987 2268 y FE(suc)o(h)c(that)e FD(t)1163 2253 y Fp(\034)1183 2268 y FE(.)14 b(In)c(this)f(case)i(ther)n(e)g(is)f(a)h(smallest)e Ft(\000)h FE(with)f Ft(\000)j Fz(`)g FD(t)1924 2253 y Fp(\034)1944 2268 y FE(.)987 2371 y FC(The)f(fact)f(that)f(all)h (eliminations)f(are)i(written)e(as)h(applications)f(en-)987 2421 y(sures)g(that)g(all)g(typed)f(terms)i(ha)o(v)o(e)g(a)f(uniform)f (appearance,)k(as)e(can)987 2470 y(easily)g(be)h(v)o(eri\002ed)f(by)g (induction)e(on)i(the)g(de\002nition)f(of)h(the)g Fz(\001)h(`)h(\001) 1959 2455 y Fq(\001)987 2520 y FC(relation.)987 2602 y Fx(Lemma)d(3.7)i(\(Head)f(f)o(orm\).)21 b FE(Assume)11 b Ft(\000)i Fz(`)f FD(t)1674 2587 y Fp(\034)1695 2602 y FE(.)i(Then)d FD(t)g FE(is)g(of)f(the)987 2652 y(form)g FD(x)1097 2644 y(~)1100 2652 y(t)o FE(,)h FD(c)1150 2644 y(~)1153 2652 y(t)p FE(,)g Ft(\()p FD(\025x)1253 2637 y Fp(\032)1279 2652 y FD(s)p Ft(\))1311 2644 y FD(~)1314 2652 y(t)g FE(or)f Fz(h)q FD(s;)d(r)q Fz(i)1482 2644 y FD(~)1484 2652 y(t)p FE(.)p eop %%Page: 4 4 4 3 bop -91 42 a FF(4)50 b(Reductions)-91 166 y FC(W)m(e)14 b(no)o(w)f(de\002ne)i(reduction)e(rules)g(on)h(the)f(terms.)24 b(The)o(y)15 b(are)g(all)-91 216 y(correct)c(with)f(respect)i(to)e(the) h(set-theoretic)g(semantics.)16 b(In)11 b(order)-91 265 y(to)j(be)g(able)h(to)e(control)h(the)g(ef)o(fects)h(of)f(recursion)g (we)g(allo)o(w)g(re-)-91 315 y(duction)8 b(only)h(if)g(the)h(ar)o (gument)g(is)f(already)h(calculated,)h(i.e.)f(if)f(the)-91 365 y(ar)o(gument)h(is)g(a)h(numeral.)-91 442 y Fx(De\002nition)e(4.1)i (\(Numerals,)f(lists\).)20 b FC(T)m(erms)50 b(of)e(the)g(form)-91 492 y FB(S)-64 498 y Fp(i)-52 502 y Fk(1)-35 492 y FD(d)-13 477 y Fl(3)-13 502 y Fo(1)13 492 y Ft(\()p FD(:)7 b(:)g(:)f Ft(\()p FB(S)128 498 y Fp(i)140 502 y Fj(n)162 492 y FD(d)184 477 y Fl(3)184 502 y Fp(n)210 492 y FB(1)p Ft(\)\))14 b FC(are)g(called)g FE(numer)o(als)p FC(.)23 b FE(Lists)13 b FC(are)i(terms)-91 542 y(of)c(the)g(form)h FB(cons)200 548 y Fp(\034)221 542 y FD(d)243 527 y Fl(3)243 552 y Fo(1)269 542 y FD(a)291 527 y Fp(\034)291 552 y Fo(1)312 542 y Ft(\()p FD(:)7 b(:)g(:)e Ft(\()p FB(cons)490 548 y Fp(\034)511 542 y FD(d)533 527 y Fl(3)533 552 y Fp(n)558 542 y FD(a)580 527 y Fp(\034)580 552 y(n)603 542 y FB(nil)656 548 y Fp(\034)677 542 y Ft(\)\))p FC(.)17 b(\(Here)12 b(the)-87 586 y FD(~)-91 597 y(d)e FC(denote)g(arbitrary)f(terms)i(of)f (type)g Fy(3)p FC(.\))-91 674 y Fx(Remark)g(4.2.)21 b FC(It)16 b(should)f(be)i(noted)f(that)f(we)i(could)f(ha)o(v)o(e)h(also) -91 724 y(required)h(the)140 713 y FD(~)135 724 y(d)h FC(to)f(be)h(v)o(ariables)g(and)f(get)h(the)f(same)i(results.)-91 774 y(Ho)o(we)o(v)o(er)n(,)11 b(this)d(de\002nition)g(allo)o(ws)g(more) i(reductions)f(\(see)h(de\002ni-)-91 823 y(tion)h(4.3\))h(and)g (therefore)g(is)g(slightly)d(more)k(\003e)o(xible)f(when)g(deal-)-91 873 y(ing)f(with)g(terms)h(that)g(are)h(not)e(almost)h(closed,)h(i.e.)f (contain)g(v)o(ari-)-91 923 y(ables)e(of)g(types)g(dif)o(ferent)g(to)f Fy(3)p FC(.)-91 1000 y Fx(De\002nition)g(4.3)i(\(Con)n(versions\).)21 b Fz(7!)9 b FC(is)h(de\002ned)h(as:)-70 1065 y Ft(\()p FD(\025x)-6 1050 y Fp(\034)21 1065 y FD(t)p Ft(\))p FD(s)h Fz(7!)f FD(t)p Ft([)p FD(s=x)p Ft(])-70 1115 y Fz(h)p FD(t;)c(s)p Fz(i)g FB(t)k Fz(7!)g FD(t)-70 1165 y Fz(h)p FD(t;)c(s)p Fz(i)g FB(f)15 b Fz(7!)c FD(s)-70 1215 y FB(t)c Fz(h)o FD(t;)g(s)p Fz(i)12 b(7!)f FD(t)-70 1265 y FB(f)g Fz(h)p FD(t;)c(s)p Fz(i)k(7!)g FD(s)-70 1314 y Fz(\012)-38 1320 y Fp(\034)r(;\032)8 1314 y FD(ts)p Ft(\()p FD(\025x)106 1299 y Fp(\034)127 1314 y FD(;)c(y)167 1299 y Fp(\032)194 1314 y FD(r)q Ft(\))k Fz(7!)g FD(r)q Ft([)p FD(t;)c(s=x;)g(y)p Ft(])-70 1364 y FB(1)g Fz(f)o FD(t)-4 1370 y Fo(0)15 1364 y FD(;)g(t)49 1370 y Fo(1)67 1364 y Fz(g)f FD(s)12 b Fz(7!)f FD(s)-70 1414 y FB(S)-43 1420 y Fp(i)-30 1414 y FD(d)-8 1399 y Fl(3)18 1414 y FD(\027)e Fz(f)p FD(t)84 1420 y Fo(0)102 1414 y FD(;)e(t)136 1420 y Fo(1)154 1414 y Fz(g)g FD(s)12 b Fz(7!)f FD(t)281 1420 y Fp(i)295 1414 y FD(d)317 1399 y Fl(3)343 1414 y Ft(\()p FD(\027)e Fz(f)p FD(t)425 1420 y Fo(0)443 1414 y FD(;)e(t)477 1420 y Fo(1)495 1414 y Fz(g)g FD(s)p Ft(\))42 b FD(\027)13 b FC(a)e(numeral)-70 1464 y FB(nil)-17 1470 y Fp(\034)10 1464 y Fz(f)p FD(t)p Fz(g)c FD(s)12 b Fz(7!)f FD(s)-70 1514 y FB(cons)20 1520 y Fp(\034)41 1514 y FD(d)63 1499 y Fl(3)89 1514 y FD(a`)c Fz(f)p FD(t)p Fz(g)f FD(s)12 b Fz(7!)f FD(td)319 1499 y Fl(3)345 1514 y FD(a)p Ft(\()p FD(`)c Fz(f)p FD(t)p Fz(g)g FD(s)p Ft(\))42 b FD(`)11 b FC(a)g(list)-91 1591 y Fx(De\002nition)e(4.4)i(\()p FD(t)g Fz(!)g FD(t)265 1576 y Fq(0)277 1591 y Fx(\).)21 b FC(The)13 b(term)g(closure)f FD(t)k Fz(!)f FD(t)723 1576 y Fq(0)747 1591 y FC(is)d(induc-)-91 1641 y(ti)o(v)o(ely)d (de\002ned)i(as)g(follo)o(ws:)-70 1708 y FD(t)g Fz(7!)g FD(t)24 1693 y Fq(0)p -91 1725 148 2 v -70 1760 a FD(t)g Fz(!)g FD(t)24 1745 y Fq(0)185 1708 y FD(t)g Fz(!)g FD(t)279 1693 y Fq(0)p 140 1725 198 2 v 160 1760 a FD(ts)h Fz(!)22 b FD(t)285 1745 y Fq(0)296 1760 y FD(s)460 1708 y(s)12 b Fz(!)g FD(s)564 1693 y Fq(0)p 420 1725 V 440 1760 a FD(ts)g Fz(!)22 b FD(ts)584 1745 y Fq(0)-91 1904 y FC(Ne)o(xt)11 b(we)h(ha)o(v)o(e)h(to)e(sho)o(w)g(that)g(the)g(term)h(system)g(is)f (closed)h(under)-91 1954 y(reduction,)g(i.e.)i(that)e(the)h(reduct)f (of)h(a)g(typed)f(term)h(is)f(also)h(typed)-91 2003 y(with)c(at)h(most) g(the)h(same)g(free)g(v)o(ariables.)-91 2080 y Fx(Lemma)e(4.5.)21 b Ft(\000)164 2086 y Fo(1)192 2080 y Fz([)9 b(f)p FD(x)274 2065 y Fp(\032)293 2080 y Fz(g)i(`)h FD(t)377 2065 y Fp(\034)398 2080 y FE(;)d Ft(\000)447 2086 y Fo(2)477 2080 y Fz(`)j FD(s)533 2065 y Fp(\032)553 2080 y FE(;)d Ft(\000)602 2086 y Fo(1)621 2080 y FD(;)e Ft(\000)666 2086 y Fo(2)693 2080 y FE(disjoint)f Ft(=)-7 b Fz(\))-91 2130 y Ft(\000)-65 2136 y Fo(1)-47 2130 y FD(;)7 b Ft(\000)-2 2136 y Fo(2)28 2130 y Fz(`)12 b FD(t)p Ft([)p FD(s=x)156 2115 y Fp(\032)175 2130 y Ft(])186 2109 y Fp(\034)-91 2231 y FE(Pr)n(oof)o(.)21 b FC(Induction)8 b(on)h FD(t)g FC(e)o(xploiting)e(the)j(fact)f(that)g(whene)o(v)o(er)h FD(t)841 2237 y Fo(1)860 2231 y FD(t)875 2237 y Fo(2)-91 2281 y FC(is)h(a)g(typed)f(term,)i(then)f(either)f FD(t)381 2287 y Fo(2)411 2281 y FC(is)h(closed)g(or)g(there)g(are)h(disjoint)-91 2331 y Ft(\000)-65 2337 y Fo(11)-30 2331 y FD(;)7 b Ft(\000)15 2337 y Fo(12)60 2331 y FC(with)i Ft(\000)170 2337 y Fo(11)217 2331 y Fz(`)j FD(t)269 2337 y Fo(1)287 2315 y Fp(\034)305 2303 y Fi(0)330 2331 y FC(and)e Ft(\000)426 2337 y Fo(12)473 2331 y Fz(`)h FD(t)524 2337 y Fo(2)543 2315 y Fp(\034)561 2303 y Fi(0)q(0)584 2331 y FC(.)p 875 2305 19 2 v 875 2329 2 25 v 892 2329 V 875 2331 19 2 v -91 2412 a Fx(Lemma)e(4.6)h (\(Closur)o(e)h(under)h(r)o(eduction\).)22 b Ft(\000)e Fz(`)g FD(t)717 2397 y Fp(\034)738 2412 y FE(;)d FD(t)k Fz(!)f FD(t)882 2397 y Fq(0)-91 2462 y Ft(=)-7 b Fz(\))10 b Ft(\000)i Fz(`)f FD(t)75 2447 y Fq(0)87 2441 y Fp(\034)-91 2563 y FE(Pr)n(oof)o(.)21 b FC(Induction)c(on)i FD(t)g FC(sho)o(ws)g(that)f(only)g(con)n(v)o(ersions)h(ha)o(v)o(e)-91 2613 y(to)14 b(be)h(considered.)27 b(The)16 b(only)e(non-tri)o(vial)e (case)17 b(is)d(handled)h(in)-91 2662 y(Lemma)d(4.5.)p 875 2637 V 875 2661 2 25 v 892 2661 V 875 2663 19 2 v 987 42 a(The)h(ne)o(xt)g(step)g(is)g(to)f(sho)o(w)h(is)f(that)h(we)g (ha)o(v)o(e)h(suf)o(\002ciently)e(man)o(y)987 91 y(reduction)j(rules,)k (i.e.)e(that)f(normal)g(forms)h(ha)o(v)o(e)g(the)f(e)o(xpected)987 141 y(form.)g(As)c(the)f(size)h(of)f(a)h(term)f(is)g(represented)h(by)f (its)f(number)i(of)987 191 y(free)i(v)o(ariables,)h(we)f(also)g(ha)o(v) o(e)g(to)f(consider)h(non-closed)f(terms.)987 241 y(As,)f(ho)o(we)o(v)o (er)n(,)g Fy(3)f FC(is)g(the)g(only)f(base)i(type)f(without)e(closed)j (terms,)987 291 y(we)j(can)h(restrict)e(ourselv)o(es)h(to)f(\223almost) h(closed\224)h(terms,)g(i.e.)g(to)987 340 y(terms)11 b(with)e(free)i(v)o(ariables)f(of)g(type)g Fy(3)g FC(only)m(.)987 429 y Fx(Pr)o(oposition)g(4.7.)21 b FE(Every)12 b(normal,)f(almost)e (closed)i(term)g(of)f(type)987 479 y FB(N)j FE(is)e(a)h(numer)o(al.)19 b(Every)14 b(normal,)e(almost)f(closed)h(term)h(of)e(type)987 529 y FB(L)p Ft(\()p FD(\034)5 b Ft(\))15 b FE(is)h(a)f(list.)27 b(Every)18 b(normal,)e(almost)e(closed)i(term)f(of)g(type)987 579 y Ft(b)q(o)q(ol)c FE(is)f FB(t)h FE(or)g FB(f)5 b FE(.)15 b(Every)e(normal,)e(almost)f(closed)h(term)h(of)e(type)h Fy(3)987 629 y FE(is)f(a)g(variable)o(.)987 759 y(Pr)n(oof)o(.)21 b FC(Induction)c(on)h FD(t)h FC(and)f(case)i(distinction,)f(according)f (to)987 808 y(Lemma)12 b(3.7.)p 1953 782 V 1953 807 2 25 v 1970 807 V 1953 809 19 2 v 987 957 a FF(5)50 b(Length)11 b(of)h(r)o(eduction)g(chains)987 1097 y FC(W)m(e)i(use)g(three)g(dif)o (ferent)f(measures)i(for)f(terms:)19 b(the)14 b(number)g(of)987 1147 y(free)20 b(v)o(ariables,)h(which)e(corresponds)f(to)h(the)f (\223size)j(function\224)987 1197 y(in)9 b([6];)g(the)h(length,)f (which)g(is)h(the)f(number)h(of)f(symbols)g(of)h(a)g(term)987 1247 y(that)h(can)h(be)g(seen)h(\(using)d(the)i(interpretation)d(that)i (you)g(can)h(only)987 1297 y(see)f(one)g(component)f(of)g(an)h (ordinary)e(pair\))h(and)g(the)g(polynomial)987 1346 y(which)g(is)g(the)g(upper)g(bound)f(for)h(the)g(comple)o(xity)f(of)h (a)h(function.)987 1435 y Fx(De\002nition)f(5.1)g(\(Length\).)21 b FC(The)15 b(length)f Fz(j)o FD(t)p Fz(j)h FC(of)f(a)i(term)f FD(t)g FC(is)f(de-)987 1485 y(\002ned)c(by)g(induction)e(on)i FD(t)h FC(as)g(follo)o(ws:)1008 1560 y Fz(j)o FD(c)p Fz(j)g Ft(=)h Fz(j)p FD(x)p Fz(j)e Ft(=)i(1)1008 1610 y Fz(j)o FD(ts)q Fz(j)f Ft(=)h Fz(j)o FD(t)p Fz(j)d Ft(+)g Fz(j)p FD(s)p Fz(j)1008 1659 y(j)o FD(\025x)1067 1644 y Fp(\034)1095 1659 y FD(s)p Fz(j)i Ft(=)h Fz(j)p FD(s)p Fz(j)d Ft(+)g(1)1008 1709 y Fz(j)o(h)p FD(t;)e(s)p Fz(ij)k Ft(=)h(max)5 b Fz(fj)p FD(t)p Fz(j)h FD(;)h Fz(j)o FD(s)p Fz(jg)i Ft(+)h(1)1008 1759 y Fz(j)o(f)p FD(t)p Fz(gj)h Ft(=)h Fz(j)o(f)p FD(t)1190 1765 y Fo(1)1208 1759 y FD(;)7 b(t)1242 1765 y Fo(2)1261 1759 y Fz(g)o(j)k Ft(=)h(0)987 1861 y FC(The)f(notation)1208 1825 y Fh(\014)1208 1850 y(\014)1220 1853 y FD(~)1222 1861 y(t)1237 1825 y Fh(\014)1237 1850 y(\014)1261 1861 y FC(is)f(used)h(for)1461 1821 y Fp(n)1450 1830 y Fh(P)1445 1897 y Fp(i)p Fo(=1)1505 1861 y Fz(j)p FD(t)1532 1867 y Fp(i)1546 1861 y Fz(j)o FC(.)987 1973 y Fx(Lemma)e(5.2.)21 b Ft(\000)1242 1979 y Fo(1)1292 1973 y Fz(`)32 b FD(t)1364 1958 y Fp(\034)1385 1973 y FE(,)24 b Ft(\000)1445 1979 y Fo(2)1495 1973 y Fz(`)31 b FD(s)1570 1958 y Fp(\032)1590 1973 y FE(;)26 b Ft(\000)1656 1979 y Fo(1)1675 1973 y FD(;)7 b Ft(\000)1720 1979 y Fo(2)1759 1973 y FE(disjoint)18 b Ft(=)-7 b Fz(\))987 2023 y(j)o FD(t)p Ft([)p FD(s=x)p Ft(])o Fz(j)12 b(\024)f(j)p FD(t)p Fz(j)e Ft(+)g Fz(j)p FD(s)p Fz(j)987 2100 y FE(In)h(particular) -5 b(,)9 b Fz(j)p Ft(\()p FD(\025x)1292 2085 y Fp(\034)1320 2100 y FD(t)p Ft(\))p FD(s)p Fz(j)i FD(>)h Fz(j)p FD(t)p Ft([)p FD(s=x)p Ft(])o Fz(j)o FE(.)987 2230 y(Pr)n(oof)o(.)21 b FC(Induction)9 b(on)h FD(t)p FC(,)g(using)g(the)g(fact)g(that)g FD(t)g FC(is)g(typed.)p 1953 2204 V 1953 2228 2 25 v 1970 2228 V 1953 2230 19 2 v 987 2333 a Fx(Lemma)f(5.3.)21 b Ft(\000)12 b Fz(`)g FD(t)1306 2318 y Fl(3)1342 2333 y Ft(=)-7 b Fz(\))11 b Ft(\000)g Fz(6)p Ft(=)h Fz(;)987 2463 y FE(Pr)n(oof)o(.)21 b FC(Induction)g(on)g Fz(j)p FD(t)p Fz(j)o FC(.)49 b(Case)23 b(distinction)d(according)i(to)987 2513 y(lemma)g(3.7.)13 b(F)o(or)d Fz(\012)1295 2519 y Fp(\034)r(;\032)1339 2505 y FD(~)1342 2513 y(t)g FC(and)g Ft(\()p FD(\025x)d(s)p Ft(\))1540 2505 y FD(~)1543 2513 y(t)k FC(use)g(lemma)g(5.2.)i(F)o(or)e FB(S)1928 2519 y Fo(0)1943 2505 y FD(~)1946 2513 y(t)p FC(,)987 2563 y FB(S)1014 2569 y Fo(1)1029 2555 y FD(~)1032 2563 y(t)f FC(and)f FB(cons)1217 2569 y Fp(\034)1235 2555 y FD(~)1238 2563 y(t)g FC(use)h(induction)e(hypothesis)g(for)h FD(t)1754 2569 y Fo(1)1773 2563 y FC(.)k(F)o(or)d FB(1)1884 2555 y FD(~)1887 2563 y(t)f FC(and)987 2613 y FB(nil)1040 2619 y Fp(\034)1058 2605 y FD(~)1061 2613 y(t)i FC(use)g(induction)e (hypothesis)g(for)i FD(t)1584 2619 y Fo(2)1609 2613 y FD(:)c(:)g(:)f(t)1680 2619 y Fp(n)1702 2613 y FC(.)15 b(The)d(remaining)987 2662 y(cases)g(are)f(tri)o(vial.)p 1953 2637 V 1953 2661 2 25 v 1970 2661 V 1953 2663 19 2 v eop %%Page: 5 5 5 4 bop -91 42 a FC(The)14 b(follo)o(wing)e(corollary)g(is)i (formulated)f(for)h(\002rst-order)f(func-)-91 91 y(tions)c(only)m(.)j (Ho)o(we)o(v)o(er)n(,)f(if)e(one)h(accepts)h(the)f(nubmer)g(of)f(free)i (v)o(ari-)-91 141 y(ables)k(as)g(a)h(size)f(measure)h(for)e (de\002nable)i(functions)d(for)h(higher)-91 191 y(types)e(as)i(well,)f (then)f(the)h(corollary)e(tri)o(vially)g(remains)i(v)o(alid)f(for)-91 241 y FE(e)o(very)g FC(de\002nable)f(function.)-91 326 y Fx(Cor)o(ollary)e(5.4)i(\(Non-size-incr)o(easing)f(pr)o(operty\).)22 b FE(Every)-91 375 y(\002rst-or)n(der)g(function)e(de\002nable)h(by)h (a)g(closed)g(term)h(has)e(the)-91 425 y(pr)n(operty)10 b(that)f(the)h(output)f(is)h(not)f(longer)h(than)f(the)h(input.)-91 537 y(Pr)n(oof)o(.)21 b FC(Lemma)15 b(5.3)f(sho)o(ws)f(that)g(the)h (usual)f(length)g(for)g(ground)-91 587 y(types)d(and)h(the)f(number)h (of)f(free)i(v)o(ariables)e(are)i(the)e(same)i(\(due)f(to)-91 637 y(the)g(typing)f Fy(3)j FA(\()h FB(N)g FA(\()g FB(N)e FC(of)f(the)g(successor)i(functions\).)i(The)-91 686 y(number)g(of)g(free)h(v)o(ariables)g(tri)o(vially)d(does)i(not)g (increase)h(when)-91 736 y(reducing)9 b(the)i(term)f(to)g(normal)g (form.)p 875 710 19 2 v 875 734 2 25 v 892 734 V 875 736 19 2 v -91 848 a(Let)16 b(the)g(set)g Fg(N)7 b Ft([)m FD(X)s Ft(])17 b FC(of)e(polynomials)g(with)f(natural)i(number)g(as)-91 898 y(coef)o(\002cients)10 b(be)g(equipped)e(with)h(the)g(partial)g (ordering)f FA(4)i FC(de\002ned)-91 947 y(by)-37 916 y Fh(P)14 947 y FD(a)36 953 y Fp(i)50 947 y FD(X)87 932 y Fp(i)118 947 y FA(4)166 916 y Fh(P)217 947 y FD(b)235 953 y Fp(i)249 947 y FD(X)286 932 y Fp(i)316 947 y Fz(\()-7 b(\))16 b(8)p FD(i:a)480 953 y Fp(i)510 947 y Fz(\024)g FD(b)576 953 y Fp(i)590 947 y FC(.)21 b(Then)13 b(there)g(e)o(xist)-91 997 y(\002nite)f(suprema)h(with)f(respect)h(to)f FA(4)p FC(;)i(these)f(will)f(be)g(denoted)h(by)-91 1047 y Ft(sup)-29 1057 y Fn(4)6 1047 y Fz(f)p FD(:)7 b(:)g(:)n Fz(g)p FC(.)19 b(Ob)o(viously:)c FD(f)r(;)7 b(g)16 b Fz(2)f Fg(N)7 b Ft([)m FD(X)s Ft(])p FC(;)13 b FD(f)20 b FA(4)15 b FD(g)q FC(;)e FD(n)i Fz(2)g Fg(N)10 b Ft(=)-7 b Fz(\))-91 1097 y FD(f)t Ft(\()p FD(n)p Ft(\))12 b Fz(\024)g FD(g)q Ft(\()p FD(n)p Ft(\))-91 1182 y Fx(De\002nition)d(5.5)i(\(P)o(olynomial)d FD(#)f Ft(\()o Fz(\001)p Ft(\))j Fx(of)g(a)h(term\).)21 b FC(F)o(or)10 b(each)h(\(not)-91 1232 y(neccessarily)j(typed\))e(term) h FD(t)g FC(we)g(de\002ne)h(a)f(polynomial)e FD(#)c Ft(\()p FD(t)p Ft(\))17 b Fz(2)-91 1281 y Fg(N)7 b Ft([)m FD(X)s Ft(])k FC(by)f(induction)e(on)i FD(t)p FC(.)-70 1353 y FD(#)d Ft(\()o FD(x)p Ft(\))12 b(=)f FD(#)c Ft(\()p FD(c)p Ft(\))12 b(=)f(0)-70 1403 y FD(#)c Ft(\()o FD(ts)q Ft(\))k(=)h FD(#)7 b Ft(\()p FD(t)p Ft(\))i(+)h FD(#)d Ft(\()o FD(s)p Ft(\))-70 1453 y FD(#)g Ft(\()o FD(\025x)25 1438 y Fp(\034)53 1453 y FD(t)p Ft(\))k(=)h FD(#)7 b Ft(\()p FD(t)p Ft(\))-70 1503 y FD(#)g Ft(\()o Fz(h)p FD(t;)g(s)p Fz(i)p Ft(\))12 b(=)g(sup)196 1513 y Fn(4)231 1503 y Fz(f)p FD(t;)7 b(s)p Fz(g)-70 1553 y FD(#)g Ft(\()o Fz(f)p FD(t)p Fz(g)p Ft(\))k(=)h FD(X)h Fz(\001)c FD(#)e Ft(\()o FD(t)p Ft(\))j(+)f FD(X)k Fz(\001)c(j)o FD(t)p Fz(j)-70 1603 y FD(#)e Ft(\()o Fz(f)p FD(t;)g(s)p Fz(g)p Ft(\))k(=)h FD(X)h Fz(\001)c Ft(sup)273 1613 y Fn(4)308 1603 y Fz(f)p FD(#)e Ft(\()o FD(t)p Ft(\))h FD(;)f(#)g Ft(\()o FD(s)p Ft(\))p Fz(g)i Ft(+)h FD(X)j Fz(\001)8 b Ft(max)e Fz(f)o(j)p FD(t)p Fz(j)g FD(;)h Fz(j)o FD(s)p Fz(jg)-91 1701 y FC(Moreo)o(v)o(er)k FD(#)114 1668 y Fh(\000)129 1694 y FD(~)132 1701 y(t)147 1668 y Fh(\001)176 1701 y FC(is)g(short)e(for)383 1662 y Fp(n)372 1670 y Fh(P)367 1738 y Fp(i)p Fo(=1)427 1701 y FD(#)e Ft(\()p FD(t)490 1707 y Fp(i)504 1701 y Ft(\))p FC(.)-91 1832 y(Again)i(by)h(tri)o(vial)f(induction)f(on)i(typed)g(terms,)h(we)f(get) -91 1917 y Fx(Lemma)f(5.6.)21 b Ft(\000)164 1923 y Fo(1)218 1917 y Fz(`)36 b FD(t)294 1902 y Fp(\034)315 1917 y FE(,)p Ft(\000)351 1923 y Fo(2)405 1917 y Fz(`)f FD(s)484 1902 y Fp(\032)504 1917 y FE(;)30 b Ft(\000)574 1923 y Fo(1)592 1917 y FD(;)7 b Ft(\000)637 1923 y Fo(2)679 1917 y FE(disjoint)20 b Ft(=)-7 b Fz(\))-91 1967 y FD(#)7 b Ft(\()o FD(t)p Ft([)p FD(s=x)p Ft(])o(\))12 b FA(4)g FD(#)7 b Ft(\()p FD(t)p Ft(\))i(+)g FD(#)e Ft(\()p FD(s)p Ft(\))-91 2074 y FC(W)m(e)j(are)i(no)o(w)d(able)i(to)f(pro)o(v)o(e)g(our)g(main)g (theorem.)-91 2159 y Fx(Theor)o(em)h(5.7.)21 b FE(Assume)12 b Ft(\000)i Fz(`)h FD(t)396 2144 y Fp(\034)428 2159 y FE(and)c FD(N)19 b Fz(\025)14 b(j)p Ft(FV)7 b(\()p FD(t)p Ft(\))q Fz(j)k FE(for)g(some)-91 2209 y FD(N)20 b Fz(2)14 b Fg(N)p FE(.)j(Then)12 b(ther)n(e)h(ar)n(e)g FD(t)i Ft(=)g FD(t)412 2215 y Fo(0)445 2209 y Fz(!)g FD(t)517 2215 y Fo(1)550 2209 y Fz(!)g FD(:)7 b(:)g(:)13 b Fz(!)h FD(t)741 2215 y Fp(k)774 2209 y FE(with)d FD(t)873 2215 y Fp(k)-91 2258 y FE(normal)e(and)71 2352 y FD(#)e Ft(\()p FD(t)134 2358 y Fp(k)154 2352 y Ft(\))h(\()p FD(N)d Ft(\))k(+)g Fz(j)p FD(t)325 2358 y Fp(k)345 2352 y Fz(j)g Ft(+)h FD(k)i Fz(\024)g FD(#)7 b Ft(\()p FD(t)p Ft(\))g(\()p FD(N)e Ft(\))k(+)g Fz(j)p FD(t)p Fz(j)-91 2463 y FE(Pr)n(oof)o(.)21 b FC(Induction)c(on)i FD(#)7 b Ft(\()p FD(t)p Ft(\))g(\()p FD(N)e Ft(\))16 b(+)g Fz(j)o FD(t)p Fz(j)j FC(and)g(case)i(distinction) -91 2513 y(according)g(to)f(Lemma)j(3.7.)45 b(The)22 b(only)d(dif)o(\002cult)h(cases)i(are)-91 2563 y(those)17 b(that)f(are)i(instances)f(of)g FD(t)24 b Ft(=)g FD(r)497 2548 y Fm(N)535 2563 y Fz(f)p FD(h)580 2569 y Fo(0)599 2563 y FD(;)7 b(h)642 2569 y Fo(1)660 2563 y Fz(g)f FD(s)703 2555 y(~)706 2563 y(t)q FC(;)20 b(the)d(case)-91 2613 y FD(r)-71 2598 y Fm(L)p Fo(\()p Fp(\034)s Fo(\))5 2613 y Fz(f)p FD(h)p Fz(g)6 b FD(s)93 2605 y(~)96 2613 y(t)k FC(can)g(be)g(handled)e(similarly)g(and)i(for)f Ft(\()p FD(\025x)e(s)p Ft(\))765 2605 y FD(~)768 2613 y(t)p FC(,)j(Lem-)-91 2662 y(mata)h(5.2)f(and)g(5.6)h(can)g(be)f(used.)987 42 y(Normalize)f FD(r)g FC(to)f FD(r)1260 26 y Fq(0)1280 42 y FC(in)f FD(k)1342 48 y Fo(0)1369 42 y FC(steps)i(using)e(the)h (induction)f(hypothesis.)987 91 y(W)m(e)k(ha)o(v)o(e)1140 183 y FD(#)c Ft(\()p FD(r)1208 166 y Fq(0)1219 183 y Ft(\))g(\()p FD(N)e Ft(\))10 b(+)f Fz(j)p FD(r)1395 166 y Fq(0)1406 183 y Fz(j)g Ft(+)g FD(k)1490 189 y Fo(0)1520 183 y Fz(\024)j FD(#)7 b Ft(\()p FD(r)q Ft(\))f(\()p FD(N)f Ft(\))10 b(+)f Fz(j)p FD(r)q Fz(j)987 295 y FC(The)19 b(only)f(interesting)g(\(and)g(in)h(the)f(case)j(of)d FD(t)h FC(being)g(almost)987 345 y(closed)c(the)g(only\))f(case)j(is)e (that)g(when)g FD(r)1610 330 y Fq(0)1637 345 y FC(is)g(a)h(numeral.)28 b(Con-)987 395 y(sider)11 b FD(r)1099 380 y Fq(0)1124 395 y Ft(=)j FB(S)1197 401 y Fp(i)1209 405 y Fk(1)1227 395 y FD(r)1247 380 y Fl(3)1246 405 y Fo(1)1273 395 y Ft(\()p FD(:)7 b(:)g(:)f Ft(\()p FB(S)1388 401 y Fp(i)1400 405 y Fj(n)1421 395 y FD(r)1441 380 y Fl(3)1440 405 y Fp(n)1468 395 y FB(1)p Ft(\)\))p FC(.)16 b(Using)11 b(lemma)i(5.3)e (and)h(the)987 445 y(fact)h(that)f(the)g(term)h(is)f(linear)h(typed)f (we)h(get)f FD(n)k Fz(\024)h FD(N)5 b FC(.)20 b(In)12 b FD(n)f Ft(+)h(1)987 495 y FC(steps)f(form)g FD(t)1188 480 y Fq(0)1213 495 y Ft(=)i FD(h)1282 501 y Fp(i)1294 505 y Fk(1)1312 495 y FD(r)1332 480 y Fl(3)1331 505 y Fo(1)1358 495 y Ft(\()p FD(:)7 b(:)g(:)e Ft(\()p FD(h)1469 501 y Fp(i)1481 505 y Fj(n)1504 495 y FD(r)1524 480 y Fl(3)1523 505 y Fp(n)1550 495 y FD(s)p Ft(\)\))1598 487 y FD(~)1601 495 y(t)q FC(.)15 b(Using)c(the)f(induction)987 544 y(hypothesis,)f(normalize)h FD(t)1376 529 y Fq(0)1398 544 y FC(to)g FD(t)1456 529 y Fq(00)1488 544 y FC(in)f FD(k)1552 550 y Fo(1)1581 544 y FC(steps;)h(we)h(ha)o(v)o(e)1119 636 y FD(#)c Ft(\()p FD(t)1182 619 y Fq(0)o(0)1203 636 y Ft(\))g(\()p FD(N)e Ft(\))10 b(+)f Fz(j)p FD(t)1374 619 y Fq(0)o(0)1395 636 y Fz(j)g Ft(+)g FD(k)1479 642 y Fo(1)1509 636 y Fz(\024)j FD(#)7 b Ft(\()o FD(t)1615 619 y Fq(0)1627 636 y Ft(\))g(\()p FD(N)e Ft(\))k(+)h Fz(j)o FD(t)1797 619 y Fq(0)1809 636 y Fz(j)c FD(:)987 749 y FC(Because)57 b(of)f(the)f(relations)g FD(#)7 b Ft(\()p FD(t)1640 733 y Fq(0)1652 749 y Ft(\))96 b FA(4)g FD(n)43 b Fz(\001)987 798 y Ft(sup)1049 808 y Fn(4)1084 798 y Fz(f)p FD(#)7 b Ft(\()p FD(h)1177 804 y Fo(0)1195 798 y Ft(\))g FD(;)g(#)g Ft(\()o FD(h)1308 804 y Fo(1)1327 798 y Ft(\))p Fz(g)27 b Ft(+)h FD(#)7 b Ft(\()n FD(~)-19 b(r)p Ft(\))28 b(+)g FD(#)7 b Ft(\()o FD(s)p Ft(\))28 b(+)g FD(#)1824 765 y Fh(\000)1840 791 y FD(~)1842 798 y(t)1857 765 y Fh(\001)1911 798 y FC(and)987 855 y Fz(j)o FD(t)1013 840 y Fq(0)1025 855 y Fz(j)11 b(\024)h FD(n)d Fz(\001)g Ft(max)c Fz(fj)o FD(h)1287 861 y Fo(0)1306 855 y Fz(j)h FD(;)h Fz(j)o FD(h)1378 861 y Fo(1)1397 855 y Fz(j)o(g)i Ft(+)h Fz(j)n FD(~)-20 b(r)q Fz(j)9 b Ft(+)h Fz(j)o FD(s)p Fz(j)f Ft(+)1667 820 y Fh(\014)1667 845 y(\014)1678 848 y FD(~)1681 855 y(t)1696 820 y Fh(\014)1696 845 y(\014)1720 855 y FC(we)i(\002nally)e(get)1090 951 y FD(#)e Ft(\()o FD(t)1152 936 y Fq(00)1173 951 y Ft(\))g(\()p FD(N)e Ft(\))10 b(+)f Fz(j)p FD(t)1344 936 y Fq(0)o(0)1365 951 y Fz(j)g Ft(+)g FD(k)1449 957 y Fo(1)1477 951 y Ft(+)g FD(n)g Ft(+)h(1)f(+)g FD(k)1687 957 y Fo(0)1016 1001 y Fz(\024)42 b FD(#)7 b Ft(\()o FD(t)1152 985 y Fq(0)1164 1001 y Ft(\))g(\()p FD(N)e Ft(\))k(+)h Fz(j)o FD(t)1334 985 y Fq(0)1346 1001 y Fz(j)f Ft(+)g FD(n)g Ft(+)h(1)f(+)g FD(k)1577 1007 y Fo(0)1016 1050 y Fz(\024)42 b FD(n)9 b Fz(\001)f Ft(sup)1207 1061 y Fn(4)1242 1050 y Fz(f)p FD(#)f Ft(\()o FD(h)1334 1056 y Fo(0)1353 1050 y Ft(\))g FD(;)g(#)g Ft(\()o FD(h)1466 1056 y Fo(1)1484 1050 y Ft(\))q Fz(g)f Ft(\()p FD(N)f Ft(\))10 b(+)f FD(#)e Ft(\()n FD(~)-19 b(r)q Ft(\))7 b(\()p FD(N)e Ft(\))1090 1103 y(+)p FD(#)i Ft(\()o FD(s)p Ft(\))h(\()p FD(N)d Ft(\))k(+)h FD(#)1365 1070 y Fh(\000)1381 1096 y FD(~)1383 1103 y(t)1398 1070 y Fh(\001)1424 1103 y Ft(\()p FD(N)5 b Ft(\))1090 1153 y(+)p FD(n)k Fz(\001)g Ft(max)c Fz(fj)o FD(h)1317 1159 y Fo(0)1336 1153 y Fz(j)h FD(;)h Fz(j)o FD(h)1408 1159 y Fo(1)1427 1153 y Fz(j)o(g)i Ft(+)h Fz(j)n FD(~)-20 b(r)q Fz(j)1090 1205 y Ft(+)7 b Fz(j)o FD(s)p Fz(j)j Ft(+)1222 1170 y Fh(\014)1222 1195 y(\014)1233 1198 y FD(~)1236 1205 y(t)1251 1170 y Fh(\014)1251 1195 y(\014)1274 1205 y Ft(+)f FD(n)h Ft(+)f(1)g(+)h FD(k)1485 1211 y Fo(0)1016 1255 y Ft(=)42 b Fz(j)n FD(~)-20 b(r)q Fz(j)9 b Ft(+)g FD(n)g Ft(+)h(1)1090 1283 y Fh(|)p 1109 1283 58 5 v 58 w({z)p 1205 1283 V 58 w(})1161 1324 y Fq(j)p Fp(r)1187 1316 y Fi(0)1198 1324 y Fq(j)1287 1255 y Ft(+)p FD(k)1341 1261 y Fo(0)1368 1255 y Ft(+)g FD(#)d Ft(\()n FD(~)-20 b(r)q Ft(\))1410 1283 y Fh(|)p 1429 1283 5 5 v 5 w({z)p 1472 1283 V 5 w(})1415 1324 y Fp(#)p Fo(\()p Fp(r)1464 1316 y Fi(0)1475 1324 y Fo(\))1493 1255 y Ft(\()p FD(N)5 b Ft(\))1090 1373 y(+)i Fz(j)o FD(s)p Fz(j)j Ft(+)1222 1338 y Fh(\014)1222 1363 y(\014)1233 1365 y FD(~)1236 1373 y(t)1251 1338 y Fh(\014)1251 1363 y(\014)1274 1373 y Ft(+)f FD(#)e Ft(\()p FD(s)p Ft(\))h(\()p FD(N)d Ft(\))k(+)g FD(#)1558 1339 y Fh(\000)1574 1365 y FD(~)1577 1373 y(t)1592 1339 y Fh(\001)1618 1373 y Ft(\()p FD(N)c Ft(\)+)1090 1423 y FD(n)k Fz(\001)f Ft(sup)1207 1433 y Fn(4)1242 1423 y Fz(f)p FD(#)f Ft(\()o FD(h)1334 1429 y Fo(0)1353 1423 y Ft(\))g FD(;)g(#)g Ft(\()o FD(h)1466 1429 y Fo(1)1484 1423 y Ft(\))q Fz(g)f Ft(\()p FD(N)f Ft(\))1090 1473 y(+)p FD(n)k Fz(\001)g Ft(max)c Fz(fj)o FD(h)1317 1479 y Fo(0)1336 1473 y Fz(j)h FD(;)h Fz(j)o FD(h)1408 1479 y Fo(1)1427 1473 y Fz(j)o(g)1016 1526 y(\024)42 b FD(#)7 b Ft(\()o FD(r)q Ft(\))g(\()p FD(N)e Ft(\))10 b(+)f Fz(j)p FD(r)q Fz(j)f Ft(+)i Fz(j)o FD(s)p Fz(j)f Ft(+)1488 1490 y Fh(\014)1488 1515 y(\014)1499 1518 y FD(~)1502 1526 y(t)1517 1490 y Fh(\014)1517 1515 y(\014)1301 1558 y(|)p 1320 1558 78 5 v 78 w({z)p 1436 1558 V 78 w(})1400 1599 y Fq(j)p Fp(t)p Fq(j)1538 1526 y Ft(+)p FD(#)e Ft(\()o FD(s)p Ft(\))h(\()p FD(N)d Ft(\))k(+)h FD(#)1813 1492 y Fh(\000)1829 1518 y FD(~)1831 1526 y(t)1846 1492 y Fh(\001)1872 1526 y Ft(\()p FD(N)5 b Ft(\))1090 1645 y(+)p FD(n)k Fz(\001)g Ft(sup)1239 1655 y Fn(4)1274 1645 y Fz(f)p FD(#)e Ft(\()p FD(h)1367 1651 y Fo(0)1385 1645 y Ft(\))g FD(;)g(#)g Ft(\()o FD(h)1498 1651 y Fo(1)1517 1645 y Ft(\))p Fz(g)g Ft(\()p FD(N)e Ft(\))1090 1696 y(+)p FD(n)k Fz(\001)g Ft(max)c Fz(fj)o FD(h)1317 1702 y Fo(0)1336 1696 y Fz(j)h FD(;)h Fz(j)o FD(h)1408 1702 y Fo(1)1427 1696 y Fz(j)o(g)1016 1745 y(\024)42 b FD(#)7 b Ft(\()o FD(t)p Ft(\))g(\()p FD(N)e Ft(\))10 b(+)f Fz(j)p FD(t)p Fz(j)48 b FC(by)10 b(de\002nition)e(of)i FD(#)d Ft(\()p FD(t)p Ft(\))p 1953 1808 19 2 v 1953 1832 2 25 v 1970 1832 V 1953 1834 19 2 v 987 1918 a Fx(Remark)k(5.8.)21 b FC(The)10 b(special)g(reduction)f(strate)o(gy)g(choosen)h(in)g(the) 987 1967 y(proof)f(can)i(be)g(discribed)f(as)h(follo)o(ws:)g(\223In)f (\(the)g(only)f(non-tri)o(vial\))987 2017 y(case)14 b(of)f(an)g (application)f FD(st)h FC(\002rst)g(normalize)g FD(s)h FC(to)e FD(s)1770 2002 y Fq(0)1782 2017 y FC(,)i(then)f(form)987 2067 y(the)f(\223canonical)g(reduct\224)h(for)e FD(s)1453 2052 y Fq(0)1465 2067 y FD(t)p FC(,)i(i.e.)g(completely)f(unfold)e(an)i (it-)987 2117 y(eration,)d(and)h(\002nally)f(normalize)h(the)f (canonical)h(reduct.)m(\224)j(As)d(this)987 2167 y(strate)o(gy)16 b(depends)g(only)f(on)h(the)g(term)g(structure,)h(the)f(decision)987 2216 y(which)8 b(rede)o(x)h(to)f(choose)h(ne)o(xt)f(can)h(be)g(made)g (in)f(suf)o(\002ciently)f(short)987 2266 y(time.)987 2349 y Fx(Cor)o(ollary)i(5.9)i(\(Hofmann,)f(1999\).)20 b Fz(;)e(`)h FD(t)1665 2327 y Fp(~)1661 2334 y Fm(N)p Fn(\()p Fm(N)1758 2349 y FE(.)24 b(Then)14 b FD(t)g FE(de-)987 2399 y(notes)c(a)g(function)f(computable)g(in)g(polynomial)f(many)j (steps.)987 2504 y(Pr)n(oof)o(.)21 b FC(Let)f FD(~)-21 b(\027)23 b FC(be)d(almost)f(closed)h(normal)g(numerals.)42 b(Then)987 2554 y FD(#)7 b Ft(\()p FD(t)o(~)-20 b(\027)r Ft(\))19 b(=)g FD(#)7 b Ft(\()p FD(t)p Ft(\))p FC(,)16 b(as)f FD(#)7 b Ft(\()o FD(~)-20 b(\027)r Ft(\))19 b(=)g(0)p FC(.)26 b(Therefore)15 b(an)g(upper)f(bound)987 2604 y(for)9 b(the)g(number)g(of)g(steps)h(is)f FD(#)e Ft(\()p FD(t)p Ft(\))g(\()p Fz(j)o Ft(FV)h(\()o FD(~)-20 b(\027)r Ft(\))q Fz(j)o Ft(\))6 b(+)g Fz(j)p FD(t)p Fz(j)f Ft(+)h Fz(j)o FD(~)-20 b(\027)r Fz(j)p FC(,)10 b(which)987 2654 y(is)g(polynomial)e(in)i(the)g(length)f(of)h(the)g(input)e FD(~)-20 b(\027)r FC(.)p 1953 2628 V 1953 2652 2 25 v 1970 2652 V 1953 2654 19 2 v eop %%Page: 6 6 6 5 bop -91 42 a Fx(Example)9 b(5.10)h(\(Insertion)h(sort\).)21 b FC(Let)15 b FD(\034)20 b FC(be)15 b(a)h(type)e(equipped)-91 91 y(with)d(a)j(linear)e(ordering.)19 b(Assume)14 b(that)e(this)g (ordering)g(is)g(repre-)-91 141 y(sented)g(by)f(the)h(term)g Fy(\001)263 147 y Fp(\034)296 141 y FC(of)f(type)g FD(\034)20 b FA(\()14 b FD(\034)19 b FA(\()c Ft(b)q(o)q(ol)9 b Fz(\012)i Ft(\()p FD(\034)k Fz(\012)c FD(\034)5 b Ft(\))p FC(,)-91 191 y(i.e.)12 b Fy(\001)3 197 y Fp(\034)24 191 y FD(ts)j Fz(!)115 176 y Fq(\003)148 191 y Fz(\012)180 197 y Fo(b)q(o)q(ol)p Fp(;\034)s Fq(\012)p Fp(\034)318 191 y FB(t)p Ft(\()p Fz(\012)385 197 y Fp(\034)r(;\034)432 191 y FD(ts)p Ft(\))p FC(,)f(if)d FD(s)h FC(is)g(\223smaller\224)g(than)g FD(t)p FC(,)-91 241 y(and)e Fy(\001)11 247 y Fp(\034)32 241 y FD(ts)i Fz(!)120 226 y Fq(\003)150 241 y Fz(\012)183 247 y Fo(b)q(o)q(ol)o Fp(;\034)s Fq(\012)p Fp(\034)320 241 y FB(f)5 b Ft(\()p Fz(\012)388 247 y Fp(\034)r(;\034)435 241 y FD(ts)p Ft(\))11 b FC(otherwise.)-91 308 y(Using)i(this)h (function,)g(we)g(can)h(de\002ne)g(a)g(sort)e(function)g(of)h(type)-91 357 y FD(\034)22 b FA(\()c FD(\034)k FA(\()c FD(\034)e Fz(\012)c FD(\034)18 b FC(for)13 b(two)g(elements,)i(i.e.)f(a)g (function)e(taking)-91 407 y(two)d(ar)o(guments)i(and)f(returning)e (them)j(in)f(the)g(correct)g(order:)-1 480 y Fy(\001)31 463 y Fq(0)31 490 y Fp(\034)63 480 y Ft(=)i FD(\025p)152 463 y Fp(\034)152 490 y Fo(1)173 480 y FD(;)7 b(p)213 463 y Fp(\034)213 490 y Fo(2)249 480 y Fy(\001)281 486 y Fp(\034)311 480 y FD(p)332 486 y Fo(1)351 480 y FD(p)372 486 y Fo(2)390 480 y Ft(\()p FD(\025y)451 463 y Fo(b)q(o)q(ol)517 480 y FD(;)g(p)557 463 y Fp(\034)s Fq(\012)p Fp(\034)629 480 y FD(p)p Ft(\()p FD(\025p)711 463 y Fp(\034)711 490 y Fo(1)732 480 y FD(;)g(p)772 463 y Fp(\034)772 490 y Fo(2)390 542 y FD(y)i Fz(h\012)467 548 y Fp(\034)r(;\034)515 542 y FD(p)536 548 y Fo(1)554 542 y FD(p)575 548 y Fo(2)594 542 y FD(;)e Fz(\012)645 548 y Fp(\034)r(;\034)692 542 y FD(p)713 548 y Fo(2)732 542 y FD(p)753 548 y Fo(1)771 542 y Fz(i)p Ft(\))-91 615 y FC(No)o(w)i(we)h(can)g(immediately)f (de\002ne)h(a)g(function)e(of)h(type)g FB(L)p Ft(\()p FD(\034)c Ft(\))11 b FA(\()-91 664 y Fy(3)g FA(\()h FD(\034)k FA(\()c FB(L)p Ft(\()p FD(\034)5 b Ft(\))j FC(inserting)f(an)i(element) g(at)g(the)f(correct)h(position)-91 714 y(in)k(a)h(gi)o(v)o(en)g (sorted)f(list.)23 b(At)14 b(each)h(step)f(we)g(compare)h(the)f(gi)o(v) o(en)-91 764 y(element)d(with)e(the)i(\002rst)f(element)h(of)g(the)f (list,)g(take)h(the)f(\223smaller\224)-91 814 y(element)k(at)f(the)g (be)o(ginning)f(of)h(the)h(list)e(and)h(insert)g(the)g(\223lar)o (ger\224)-91 864 y(one)d(in)g(the)g(rest)g(of)g(the)g(list.)-53 928 y Fu(insert)h Ft(=)g FD(\025l)43 b(l)q Fz(f)p FD(\025x)294 913 y Fl(3)294 938 y Fo(1)321 928 y FD(;)7 b(y)361 913 y Fp(\034)360 938 y Fo(1)382 928 y FD(;)g(p)422 913 y Fl(3)p Fn(\()p Fp(\034)s Fn(\()p Fm(L)p Fo(\()p Fp(\034)s Fo(\))606 928 y FD(;)g(x)649 913 y Fl(3)649 938 y Fo(2)675 928 y FD(;)g(y)715 913 y Fp(\034)714 938 y Fo(2)212 978 y Fy(\001)244 963 y Fq(0)244 988 y Fp(\034)265 978 y FD(y)285 984 y Fo(1)304 978 y FD(y)324 984 y Fo(2)343 978 y Ft(\()p FD(\025z)404 963 y Fp(\034)402 988 y Fo(1)426 978 y FD(;)g(z)466 963 y Fp(\034)464 988 y Fo(2)493 978 y FB(cons)583 984 y Fp(\034)604 978 y FD(x)628 984 y Fo(1)646 978 y FD(z)665 984 y Fo(1)684 978 y Ft(\()p FD(px)745 984 y Fo(2)764 978 y FD(z)783 984 y Fo(2)802 978 y Ft(\)\))p Fz(g)212 1027 y Ft(\()p FD(\025x)276 1012 y Fl(3)303 1027 y FD(;)g(y)343 1012 y Fp(\034)371 1027 y FB(cons)461 1033 y Fp(\034)482 1027 y FD(xy)q FB(nil)581 1033 y Fp(\034)601 1027 y Ft(\))-91 1098 y FC(Then)j(insertion-sort)e(is)i(de\002ned)h(as)g(usual:)40 1170 y Fu(sort)f Ft(=)i FD(\025l)219 1153 y Fp(\034)247 1170 y FD(l)267 1124 y Fh(n)295 1170 y FD(\025x)343 1153 y Fl(3)369 1170 y FD(;)7 b(y)409 1153 y Fp(\034)430 1170 y FD(;)g(l)462 1153 y Fm(L)p Fo(\()p Fp(\034)s Fo(\))538 1170 y Fu(insert)o FD(l)q(xy)728 1124 y Fh(o)261 1249 y FB(nil)314 1255 y Fp(\034)-91 1338 y FC(Counting)21 b(braces,)27 b(we)d(get)f FD(#)7 b Ft(\()p Fu(insertionsort)m Ft(\))36 b(=)f FD(X)23 b Fz(\001)-91 1388 y FD(#)7 b Ft(\()o Fu(insert)o Ft(\))14 b(+)g FD(O)q Ft(\()p FD(X)s Ft(\))23 b(=)f FD(X)379 1373 y Fo(2)412 1388 y Fz(\001)13 b FD(#)7 b Ft(\()p Fy(\001)517 1373 y Fq(0)517 1398 y Fp(\034)538 1388 y Ft(\))14 b(+)f FD(O)q Ft(\()p FD(X)699 1373 y Fo(2)719 1388 y Ft(\))22 b(=)h FD(X)849 1373 y Fo(2)882 1388 y Fz(\001)-91 1438 y FD(#)7 b Ft(\()o Fy(\001)-12 1444 y Fp(\034)9 1438 y Ft(\))13 b(+)g FD(O)q Ft(\()p FD(X)169 1423 y Fo(2)188 1438 y Ft(\))p FC(,)j(as)f FD(#)7 b Ft(\()p Fy(\001)359 1423 y Fq(0)359 1448 y Fp(\034)380 1438 y Ft(\))19 b(=)h FD(#)7 b Ft(\()p Fy(\001)547 1444 y Fp(\034)568 1438 y Ft(\))p FC(.)26 b(This)14 b(re\003ects)h(the)-91 1488 y(well)c(kno)o(wn)g(fact)g(that)g(insertion)f(sort)h(is)g (quadratic)g(in)g(the)h(num-)-91 1537 y(ber)e(of)g(comparison)g (operations.)-91 1605 y Fx(Remark)g(5.11.)21 b FC(By)8 b(simple)g(modi\002cations)f(of)h(\(the)g(proof)f(of\))g([6,)-91 1655 y Fz(x)p FC(4.3])12 b(we)h(may)f(conclude)g(that)g(man)o(y)g (\223natural)g(orderings\224,)g(e.g.)-91 1705 y(the)g(normal)g (ordering)f(on)h(binary)g(coded)g(natural)g(numbers,)h FE(can)-91 1755 y FC(be)d(de\002ned)h(in)f(the)g(gi)o(v)o(en)g(term)g (system.)-91 1822 y(Ho)o(we)o(v)o(er)n(,)i(it)d(should)h(be)h(noted)e (that)h(it)g(is)g FE(not)g(necessary)i FC(that)e(e)o(v-)-91 1871 y(ery)i(interesting)e(ordering)g(is)h(de\002nable)h(in)f(the)h(gi) o(v)o(en)f(system.)18 b(It)-91 1921 y(would)12 b(also)h(be)h(possible)f (to)g(just)g(add)h(a)g(ne)o(w)g(symbol)f Fy(\001)785 1927 y Fp(\034)819 1921 y FC(with)-91 1971 y(the)h(con)n(v)o(ersion)g (rules)g Fy(\001)295 1977 y Fp(\034)317 1971 y FD(ts)19 b Fz(7!)g(\012)463 1977 y Fo(b)q(o)q(ol)p Fp(;\034)s Fq(\012)p Fp(\034)601 1971 y FB(t)p Ft(\()p Fz(\012)668 1977 y Fp(\034)r(;\034)715 1971 y FD(ts)p Ft(\))p FC(,)e(if)d FD(s)g FC(is)-91 2021 y(\223smaller\224)h(than)e FD(t)p FC(,)i(and)f Fy(\001)313 2027 y Fp(\034)334 2021 y FD(ts)k Fz(7!)f(\012)478 2027 y Fo(b)q(o)q(ol)o Fp(;\034)s Fq(\012)p Fp(\034)615 2021 y FB(f)5 b Ft(\()p Fz(\012)683 2027 y Fp(\034)r(;\034)730 2021 y FD(ts)p Ft(\))15 b FC(other)o(-)-91 2071 y(wise.)d(W)n(ith)c(the)g(de\002nition)e Fz(j)o Fy(\001)366 2077 y Fp(\034)387 2071 y Fz(j)11 b Ft(=)h(4)c FC(the)g(abo)o(v)o(e)h(theory)e(remains)-91 2120 y(v)o(alid)g(and)h (sho)o(ws)g(that)g(there)g(are)h(at)f(most)g FD(X)563 2105 y Fo(2)591 2120 y FC(of)f(the)h(ne)o(wly)g(intro-)-91 2170 y(duced)k(con)n(v)o(ersions)g(in)g(the)g(normalizing)f(sequence.) 20 b(Therefore)-91 2220 y(this)9 b(theory)h(can)h(be)g(used)g(to)e (calculate)i(the)g(number)f(of)g(calls)h(to)f(a)-91 2270 y(\223subroutine\224,)f(e)o(v)o(en)h(if)f(the)g(subroutine)f(itself)g (is)i(not)e(de\002nable)i(in)-91 2320 y(the)g(gi)o(v)o(en)g(system,)h (or)f(not)f(e)o(v)o(en)i(polynomial)e(time)h(computable.)-91 2445 y FF(6)50 b(Conclusions)11 b(and)h(further)g(work)-91 2563 y FC(F)o(or)c(terms)h(in)f(Hofmann')n(s)g(term)g(calculus)h(from)f ([6])g(we)h(ha)o(v)o(e)g(pre-)-91 2613 y(sented)i(an)f(e)o(xplicit)g (method)g(to)g(calculate)i(a)f(polynomial)e(bound-)-91 2662 y(ing)h(the)h(size)g(of)g(the)g(v)o(alue)f(as)i(well)f(as)g(the)g (number)g(of)f(reduction)987 42 y(steps.)18 b(The)13 b(construction)d(is)i(quite)f(direct,)h(i.e.)h(one)f(can)h(see)g(im-) 987 91 y(mediately)8 b(ho)o(w)g(the)g(polynomial)f(is)h(generated.)13 b(A)8 b(possible)g(ben-)987 141 y(e\002t)14 b(of)f(such)h(a)g (perspicuous)f(approach)h(is)g(that)f(generalizations)987 191 y(should)g(be)h(more)h(manageable,)i(e.g.)e(\226)f(via)g(the)g (Curry-Ho)o(ward)987 241 y(correspondence)e(\226)g(to)f(systems)h(of)f (proof)g(terms)h(for)f(natural)g(de-)987 291 y(duction)e(calculi)h(in)n (v)o(olving)e(induction)g(on)i(notation.)i(This)e(is)g(one)987 340 y(line)g(of)g(research)h(we)g(would)e(like)g(to)h(follo)o(w)e(up.) 987 475 y FF(7)50 b(A)o(ppendix:)39 b(Extending)25 b(the)g(system)h(to) f(full)1062 533 y FG(Ptime)987 660 y FC(Once)10 b(one)g(has)g (understood)f(that)g(the)g(non-size-increasing)g(prop-)987 709 y(erty)14 b(is)h(just)e(a)i(question)f(of)g(free)h(v)o(ariables,)h (it)e(is)g(ob)o(vious)g(ho)o(w)987 759 y(to)j(e)o(xtend)h(the)g(system) h(in)e(such)h(a)h(way)e(that)h(it)f(characterises)987 809 y Fw(Ptime)p FC(:)11 b(just)c(add)h(a)h(type)f FD(\023)g FC(of)g(binary)f(words)g(that)h(can)h(be)f(formed)987 859 y(without)15 b(free)j(v)o(ariables)f(\(and)h(therefore)f(without)e (elimination)987 909 y(rules\).)32 b(A)17 b(similar)f(idea)h(was)f (used)h(by)g(Lei)o(v)o(ant)f(and)h(Marion.)987 959 y(In)10 b([9])g(the)o(y)g(use)h(\223tiers\224)g(in)f(the)g(form)g(of)g(dif)o (ferent)g(forms)g(of)g(data)987 1008 y(representation.)21 b(Their)13 b(\223Church-like)e(abstraction)h(terms\224)i(cor)o(-)987 1058 y(respond)c(to)f(our)h(type)g FB(N)p FC(,)h(and)f(their)g (\223words\224)g(to)g(the)g(ne)o(w)g(type)g FD(\023)p FC(.)987 1108 y(The)h(idea)f(for)g(the)g(proof)g(of)g(theorem)g(7.4)g (is)g(due)h(to)e([6,)i Fz(x)p FC(4.3].)987 1188 y Fx(De\002nition)f (7.1)g(\(Extended)g(term)h(system\).)21 b FC(The)14 b(term)g(system)987 1238 y(is)c(e)o(xtended)h(by)1028 1338 y Fz(\017)21 b FC(adding)9 b(a)i(ne)o(w)g(ground)e(type)g FD(\023)1028 1419 y Fz(\017)21 b FC(adding)c(the)g(follo)o(wing)e(constants)i(with)g (their)g(respecti)o(v)o(e)1070 1469 y(types:)1269 1555 y Fz(\016)222 b FD(\023)1269 1605 y Ff(s)1287 1611 y Fo(0)1512 1605 y FD(\023)11 b FA(\()h FD(\023)1269 1654 y Ff(s)1287 1660 y Fo(1)1512 1654 y FD(\023)f FA(\()h FD(\023)1269 1704 y FB(p)216 b FD(\023)11 b FA(\()h FD(\023)1269 1754 y FB(iszero)123 b FD(\023)11 b FA(\()h Ft(\(b)q(o)q(ol)d Fz(\012)g FD(\023)p Ft(\))1269 1804 y FB(head)144 b FD(\023)11 b FA(\()h Ft(\(b)q(o)q(ol)d Fz(\012)g FD(\023)p Ft(\))1028 1905 y Fz(\017)21 b FC(Extending)9 b Fz(7!)h FC(by)1266 1991 y FB(p)p Fz(\016)h(7!)g(\016)1266 2040 y FB(p)p Ft(\()p Ff(s)1327 2046 y Fp(i)1341 2040 y FD(t)1356 2025 y Fp(\023)1370 2040 y Ft(\))h Fz(7!)f FD(t)1466 2025 y Fp(\023)1266 2090 y FB(iszero)o Fz(\016)g(7!)g(\012)1502 2096 y Fo(b)q(o)q(ol)p Fp(;\023)1589 2090 y FB(t)p Fz(\016)1266 2140 y FB(iszero)o Ft(\()p Ff(s)1419 2146 y Fp(i)1433 2140 y FD(t)1448 2125 y Fp(\023)1462 2140 y Ft(\))h Fz(7!)f(\012)1575 2146 y Fo(b)q(o)q(ol)p Fp(;\023)1662 2140 y FB(f)5 b Ft(\()p Ff(s)1716 2146 y Fp(i)1730 2140 y FD(t)1745 2125 y Fp(\023)1759 2140 y Ft(\))1266 2190 y FB(head)o Fz(\016)11 b(7!)g(\012)1482 2196 y Fo(b)q(o)q(ol)o Fp(;\023)1569 2190 y FB(f)5 b Fz(\016)1266 2240 y FB(head)o Ft(\()p Ff(s)1398 2246 y Fo(0)1417 2240 y FD(t)1432 2225 y Fp(\023)1447 2240 y Ft(\))11 b Fz(7!)g(\012)1560 2246 y Fo(b)q(o)q(ol)o Fp(;\023)1646 2240 y FB(f)5 b Ft(\()p Ff(s)1700 2246 y Fo(0)1719 2240 y FD(t)1734 2225 y Fp(\023)1748 2240 y Ft(\))1266 2290 y FB(head)o Ft(\()p Ff(s)1398 2296 y Fo(1)1417 2290 y FD(t)1432 2274 y Fp(\023)1447 2290 y Ft(\))11 b Fz(7!)g(\012)1560 2296 y Fo(b)q(o)q(ol)o Fp(;\023)1646 2290 y FB(t)p Ft(\()p Ff(s)1699 2296 y Fo(1)1718 2290 y FD(t)1733 2274 y Fp(\023)1748 2290 y Ft(\))987 2393 y FC(The)j(de\002nitions)d(of)i(the)f(relations)g Ft(\000)17 b Fz(`)g FD(t)1620 2378 y Fp(\034)1654 2393 y FC(and)c FD(t)j Fz(!)g FD(t)1831 2378 y Fq(0)1856 2393 y FC(remain)987 2443 y(unchanged.)25 b(W)n(ith)14 b(almost)g(identical) f(proofs)h(it)f(can)i(be)g(sho)o(wn)987 2493 y(that)c(proposition)e (3.5,)k(and)e(Lemmata)j(3.6,)e(3.7,)h(4.5)f(and)f(4.6)h(re-)987 2543 y(main)e(v)o(aild.)987 2613 y(W)m(e)15 b(call)g(terms)h(of)e(the)h (form)g Ff(s)1468 2619 y Fp(i)1480 2623 y Fk(1)1498 2613 y Ft(\()p FD(:)7 b(:)g(:)f Ft(\()p Ff(s)1604 2619 y Fp(i)1616 2623 y Fj(n)1638 2613 y Fz(\016)p Ft(\)\))16 b FE(short)e(numer)o(als)p FC(.)987 2662 y(Then)9 b(proposition)c(4.7)j(remains)h(v)o(alid)f (\(with)f(the)h(proof)f(e)o(xtended)p eop %%Page: 7 7 7 6 bop -91 42 a FC(in)8 b(the)h(ob)o(vious)f(way\);)h(moreo)o(v)o(er)n (,)i(e)o(v)o(ery)f(normal,)f(almost)g(closed)-91 91 y(term)h(of)g(type) g FD(\023)g FC(is)g(a)h(short)e(numeral)i(\(and)f(therefore)g (closed\).)-91 162 y(The)f(de\002nition)e(of)h(the)h(term)f(length)g Fz(j)o FD(t)p Fz(j)g FC(had)h(the)g(property)e(that)h(for)-91 212 y(all)f(reductions)g(dif)o(ferent)g(to)g(induction)f(the)i(length)e (decreased.)14 b(T)m(o)-91 262 y(make)d(this)e(property)g(remain)i(v)o (alid)e(we)i(de\002ne)204 353 y Fz(j)o FB(iszero)o Fz(j)g Ft(=)h Fz(j)o FB(head)p Fz(j)f Ft(=)g(3)-91 445 y FC(and)e(keep)h(the)f (rest)h(of)f(de\002nition)f(5.1.)13 b(\(In)c(particular)n(,)g(e)o(v)o (ery)h(con-)-91 495 y(stant)f(dif)o(ferent)g(to)h FB(iszero)e FC(and)i FB(head)g FC(still)e(has)i(length)f Ft(1)p FC(.\))k(Then)-91 545 y(Lemmata)j(5.2)d(and)h(5.3)g(remain)h(v)o(alid;)f(for)f(the)h (latter)f(\()p Ft(\000)18 b Fz(`)h FD(t)867 530 y Fl(3)-91 594 y Ft(=)-7 b Fz(\))15 b Ft(\000)21 b Fz(6)p Ft(=)g Fz(;)p FC(\))15 b(the)g(follo)o(wing)e(cases)k(ha)o(v)o(e)f(to)f(be)g (added)h(to)e(the)-91 644 y(proof:)-50 749 y Fz(\017)21 b FC(Cases)16 b Fz(\016)122 741 y FD(~)125 749 y(t)p FC(,)h Ff(s)185 755 y Fp(i)196 741 y FD(~)199 749 y(t)e FC(and)g FB(p)328 741 y FD(~)331 749 y(t)p FC(:)22 b(terms)15 b(of)g(this)f(form)h FE(ne)o(ver)j FC(ha)o(v)o(e)-8 798 y(type)10 b Fy(3)p FC(,)g(as)h(there)g(are)g FE(no)f FC(elimination)e(rules)i(for)g(type)g FD(\023)p FC(.)-50 882 y Fz(\017)21 b FC(Cases)13 b FB(iszero)217 874 y FD(~)220 882 y(t)g FC(and)f FB(head)416 874 y FD(~)418 882 y(t)p FC(:)17 b(as)c FD(t)g FC(has)g(type)f Fy(3)g FC(it)g(follo)o(ws)-8 932 y(that)66 924 y FD(~)69 932 y(t)20 b Ft(=)g FD(t)p Ft(1)p FD(;)7 b(:)g(:)g(:)12 b(;)7 b(t)307 938 y Fp(n)343 932 y FC(for)15 b(some)g FD(n)20 b Fz(\025)g Ft(2)p FC(.)27 b(Therefore)15 b(the)-8 982 y(induction)6 b(hypothesis)h(can)i(be)g(applied)f(to)f(the)i FE(shorter)g FC(term)-8 1032 y Fz(\012)24 1038 y Fo(b)q(o)q(ol)p Fp(;\023)111 1032 y FB(t)g Fz(\016)g FD(t)184 1038 y Fo(2)209 1032 y FD(:)e(:)g(:)f(t)280 1038 y Fp(n)302 1032 y FC(.)-91 1136 y(The)i(de\002nition)e(of)i FD(#)f Ft(\()o FD(t)p Ft(\))i FC(remains)f(unchanged.)k(Then)c(\(with)f(iden-) -91 1186 y(tical)j(proof\))f(lemma)j(5.6)e(remains)h(v)o(alid)f(and)g (also)h(the)f(main)h(the-)-91 1236 y(orem)h(5.7.)19 b(F)o(or)12 b(the)g(proof)f(of)h(the)g(latter)f(we)i(notice)f(that)f(the)h(ad-)-91 1285 y(ditional)e(rede)o(x)o(es)k(due)e(to)g(the)g(ne)o(w)h(constants)f FB(p)g FC(and)g FB(head)g FC(can)-91 1335 y(be)h(reduced)h(at)g(an)o(y) f(time,)i(as)f(the)f(reduct)g(has)h(a)f(shorter)g(length.)-91 1385 y(In)g(particular)n(,)i(the)f(e)o(xtended)h(system)f(still)e (consists)i(of)g Fw(Ptime)-91 1435 y FC(functions)9 b(only)m(.)-91 1518 y Fx(Lemma)g(7.2.)21 b FE(If)11 b Ff(f)5 b Ft(:)13 b FD(\034)i Fz(\012)10 b FB(L)p Ft(\()p FD(\032)p Ft(\))k FA(\()g FD(\034)h Fz(\012)10 b FB(L)p Ft(\()p FD(\032)p Ft(\))i FE(is)f(de\002nable)g(by)g(a)-91 1568 y(closed)f(term,)g(then)f (so)h(is)f(a)h(function)d Ff(f)476 1553 y Fp(])496 1568 y Ft(:)13 b FD(\034)f Fz(\012)7 b FB(L)p Ft(\()p FD(\032)p Ft(\))12 b FA(\()g FD(\034)g Fz(\012)7 b FB(L)p Ft(\()p FD(\032)p Ft(\))-91 1618 y FE(with)213 1668 y Ff(f)227 1651 y Fp(])242 1668 y Ft(\()p FD(a)i Fz(\012)h FD(`)p Ft(\))i(=)f Ff(f)433 1651 y Fp(n)455 1668 y Ft(\()p FD(a)f Fz(\012)f FD(`)p Ft(\))p FD(;)-91 1743 y FE(wher)n(e)i FD(n)f FE(is)g(the)h(\(semantical\))d(length)i(of)f FD(`)p FE(.)-91 1848 y(Pr)n(oof)o(.)21 b FC(First,)h(by)d Ft(\()p FB(L)p Ft(\()p FD(\032)p Ft(\))300 1833 y Fq(\000)328 1848 y Ft(\))h FC(de\002ne)g(a)g(function)e Ff(g)5 b Ft(:)17 b FB(L)p Ft(\()p FD(\032)p Ft(\))29 b FA(\()-91 1898 y FB(L)p Ft(\()p FD(\032)p Ft(\))12 b FA(\()f FD(\034)17 b FA(\()11 b FD(\034)k Fz(\012)9 b FB(L)p Ft(\()p FD(\032)p Ft(\))i FC(with)5 1990 y Ff(g)p Ft(\()p FB(nil)95 1996 y Fp(\032)115 1990 y Ft(\)\()p FD(`)164 1973 y Fq(0)176 1990 y Ft(\)\()p FD(b)p Ft(\))h(=)f FD(b)e Fz(\012)h FD(`)383 1973 y Fq(0)-55 2052 y Ff(g)p Ft(\()p FB(cons)73 2058 y Fp(\032)92 2052 y FD(d)114 2035 y Fl(3)140 2052 y FD(a`)p Ft(\))p FD(`)212 2035 y Fq(0)224 2052 y FD(b)i Ft(=)f Ff(f)p Ft(\()p Ff(g)p Ft(\()p FD(`)p Ft(\)\()p Fu(app)p FD(d)501 2035 y Fl(3)527 2052 y Ft(\()p FD(`)560 2035 y Fq(0)572 2052 y Ft(\)\()p FB(cons)695 2058 y Fp(\032)714 2052 y FD(a)p FB(nil)789 2058 y Fp(\032)808 2052 y Ft(\)\)\))-91 2144 y FC(with)g Fu(app)i FC(being)f(the)g(append)h(function)e(for)h (lists)g(of)g(type)g Fy(3)k FA(\()-91 2193 y FB(L)p Ft(\()p FD(\032)p Ft(\))f FA(\()h FB(L)p Ft(\()p FD(\032)p Ft(\))p FC(.)j(\(This)12 b(function)f(ob)o(viously)f(can)j(be)f(de\002ned)h(in) -91 2243 y(the)d(gi)o(v)o(en)g(system.\))-91 2314 y(By)j(induction)f (on)i FD(`)g FC(we)g(note)g(that)f Ff(g)p FD(``)508 2299 y Fq(0)520 2314 y FD(b)18 b Ft(=)h Ff(f)621 2299 y Fp(n)643 2314 y Ft(\()p FD(b)12 b Fz(\012)g Ft(\()p Fu(app)p FD(`)832 2299 y Fq(0)844 2314 y FD(`)p Ft(\)\))-91 2364 y FC(where)i FD(n)f FC(is)g(the)g(length)g(of)g FD(`)p FC(.)23 b(So)13 b(we)h(can)g(de\002ne)g Ff(f)702 2349 y Fp(])717 2364 y Ft(\()p FD(a)d Fz(\012)h FD(`)p Ft(\))18 b(=)-91 2414 y Ff(g)p FD(`)p FB(nil)0 2420 y Fp(\032)19 2414 y FD(a)p FC(.)p 875 2388 19 2 v 875 2412 2 25 v 892 2412 V 875 2414 19 2 v -91 2498 a Fx(Pr)o(oposition)10 b(7.3.)21 b FE(If)10 b Ff(f)5 b Ft(:)13 b FD(\034)18 b FA(\()13 b FD(\034)j FE(is)10 b(de\002nable)h(by)g(a)g(closed)g(term)-91 2548 y(and)e FD(k)k Fz(2)e Fg(N)p FE(,)d(then)i Ff(g)5 b Ft(:)13 b FD(\034)f Fz(\012)d FB(L)p Ft(\()p FD(\032)p Ft(\))j FA(\()f FD(\034)i Fz(\012)c FB(L)p Ft(\()p FD(\032)p Ft(\))h FE(is)g(also)f(de\002nable)-91 2604 y(by)h(a)g(closed)f(term)h (with)f Ff(g)p Ft(\()p FD(a)e Fz(\012)h FD(`)p Ft(\))k(=)g Ff(f)481 2589 y Fp(n)502 2577 y Fj(k)521 2604 y Ft(\()p FD(a)p Ft(\))c Fz(\012)g FD(`)p FE(,)i(wher)n(e)h FD(n)f FE(is)f(the)-91 2654 y(length)g(of)h FD(k)q FE(.)987 42 y(Pr)n(oof)o(.)21 b FC(First)8 b(de\002ne)1301 31 y Ft(~)1305 42 y Ff(f)t Ft(:)22 b FD(\034)8 b Fz(\012)s FB(L)p Ft(\()p FD(\032)p Ft(\))k FA(\()g FD(\034)c Fz(\012)s FB(L)p Ft(\()p FD(\032)p Ft(\))h FC(with)1802 31 y Ft(~)1804 42 y Ff(f)p Ft(\()p FD(a)s Fz(\012)s FD(`)p Ft(\))j(=)987 91 y Ff(f)p Ft(\()p FD(a)p Ft(\))d Fz(\012)g FD(`)p FC(.)14 b(By)c(induction)e(on)i FD(k)q FC(,)h(one)f(v)o(eri\002es)h(that)1238 229 y Ft(~)1241 240 y Ff(f)1294 158 y Fj(k)1255 181 y Fh(z)p 1274 181 10 5 v 10 w(}|)p 1322 181 V 10 w({)1255 222 y FD(])c Fz(\001)g(\001)g(\001)e FD(])1351 240 y Ft(\()p FD(a)10 b Fz(\012)f FD(`)p Ft(\))j(=)g Ff(f)1543 222 y Fp(n)1564 210 y Fj(k)1583 240 y Ft(\()p FD(a)p Ft(\))e Fz(\012)f FD(`;)987 323 y FC(where)i FD(n)f FC(is)g(the)g (length)f(of)h FD(`)p FC(.)p 1953 297 19 2 v 1953 321 2 25 v 1970 321 V 1953 323 19 2 v 987 404 a Fx(Theor)o(em)h(7.4)f (\(completeness)h(f)o(or)g Fw(Ptime)p Fx(\).)20 b FE(Every)43 b Fw(Ptime)987 454 y FE(function)8 b(can)j(be)f(denoted)g(by)h(a)f (closed)g(term)h(of)e(type)i FB(N)h FA(\()f FD(\023)p FE(.)987 555 y(Pr)n(oof)o(.)21 b FC(Let)13 b Ff(f)g FC(be)g(a)g Fw(Ptime)f FC(function.)19 b(Then)14 b(there)e(is)h(a)g(T)n(uring)987 604 y(machine)h(computing)f Ff(f)g FC(in)g(polynomial)f(man)o(y)j (steps.)24 b(W)m(e)14 b(may)987 654 y(assume)9 b(that)f(this)f(machine) h(works)g(o)o(v)o(er)g(the)g(alphabet)g Fz(f)p Ft(0)p FD(;)f Ft(1)p Fz(g)f FC(and)987 704 y(has)15 b FD(N)k FC(states)c Fz(f)p FD(S)1262 710 y Fo(0)1281 704 y FD(;)7 b(:)g(:)g(:)12 b(;)7 b(S)1406 710 y Fp(N)s Fq(\000)p Fo(1)1480 704 y Fz(g)p FC(.)26 b(Let)15 b FD(n)f FC(be)h(the)f(least)h (natural)987 754 y(number)10 b(with)f Ft(2)1229 739 y Fp(n)1263 754 y Fz(\025)j FD(N)5 b FC(.)987 823 y(A)14 b(con\002guration)f(of)h(the)g(machine)h(with)e(the)h(symbols)f FD(i)1855 829 y Fo(0)1881 823 y FD(:)7 b(:)g(:)f(i)1951 829 y Fp(k)987 873 y FC(before)17 b(and)g(including)e(the)i(head)g(and) g(the)g(symbols)g FD(j)1842 879 y Fo(0)1867 873 y FD(:)7 b(:)g(:)f(j)1940 879 y Fp(k)1959 870 y Fi(0)987 922 y FC(follo)o(wed)j(by)h(the)g(non-visited)e(positions)g(after)j(the)f (head)g(and)h(the)987 972 y(machine)g(in)f(state)g FD(S)1292 978 y Fp(m)1334 972 y FC(is)h(coded)f(by)1284 1055 y Fz(\012)p Ft(\()p Ff(s)1350 1061 y Fp(i)1362 1065 y Fj(k)1382 1055 y Ft(\()p FD(:)d(:)g(:)f Ft(\()p Ff(s)1488 1061 y Fp(i)1500 1065 y Fk(0)1518 1055 y Fz(\016)p Ft(\)\)\))1267 1118 y(\()p Fz(\012)q Ft(\()p Ff(s)1350 1124 y Fp(j)1364 1128 y Fk(0)1382 1118 y Ft(\()p FD(:)h(:)g(:)f Ft(\()p Ff(s)1488 1124 y Fp(i)1500 1132 y Fj(k)1516 1126 y Fi(0)1532 1118 y Fz(\016)p Ft(\)\)\))1267 1180 y(\()p Fz(\012)q FD(t)1331 1186 y Fo(1)1349 1180 y Ft(\()p Fz(\012)h FD(:)g(:)g(:)f Ft(\()p Fz(\012)p FD(t)1523 1186 y Fp(n)p Fq(\000)p Fo(1)1589 1180 y FD(t)1604 1186 y Fp(n)1626 1180 y Ft(\)\)\)\))987 1270 y FC(with)12 b(each)i(of)f(the)1273 1262 y FD(~)1275 1270 y(t)h FC(being)e FB(t)h FC(or)g FB(f)18 b FC(such)13 b(that)g(this)f(is)h(the)g(binary)987 1320 y(coding)e(of)h FD(m)p FC(.)20 b(So)12 b(con\002gurations)f(are)i(coded)g(by)f FE(closed)h FC(terms)987 1369 y(of)d(type)g FD(\034)16 b Ft(=)c FD(\023)d Fz(\012)g FD(\023)g Fz(\012)h Ft(b)q(o)q(ol)e Fz(\012)i FD(:)d(:)g(:)h Fz(\012)h Ft(b)q(o)q(ol)p FC(.)987 1438 y(By)e Ft(\()p FB(N)1096 1423 y Fq(\000)1125 1438 y Ft(\))h FC(with)f(result)g(type)h FD(\023)q Fz(\012)q FB(N)g FC(a)g(term)g(can)h(be)f(de\002ned)g(return-)987 1488 y(ing)i(both,)g(its)g(input)f(and)i(a)g(copy)f(of)g(the)h(input)e (as)i(short)f(numeral.)987 1538 y(This)g(is)g(possible)f(as)i(the)f (successor)h(of)f(type)f FD(\023)h FC(can)h(be)f(b)o(uilt)f(with-)987 1588 y(out)h(requiring)f(free)j(v)o(ariables.)i(Using)c(this)g(term,)i (we)f(can)h(de\002ne)987 1638 y(a)h(closed)f(term)h(of)f(type)g FB(N)k FA(\()g FB(N)11 b Fz(\012)g FD(\034)17 b FC(returning)11 b(its)h(input)e(and)987 1687 y(creating)g(the)g(initial)e (con\002guration)h(of)h(the)g(T)n(uring)g(machine.)987 1756 y(The)16 b(one-step)f(transition)e(function)h(can)i(also)f(be)g (de\002ned)h(by)f(a)987 1806 y(closed)f(term:)19 b(via)14 b Ft(\()p Fz(\012)1327 1791 y Fq(\000)1355 1806 y Ft(\))g FC(the)g(coding)f(of)g(the)h(state)g(is)f(split)g(into)987 1856 y(its)e(components;)i(using)e(the)h FE(constants)f FB(iszero)g FC(and)h FB(head)f FC(fol-)987 1906 y(lo)o(wed)d(by)g(more) h(applications)e(of)h Ft(\()p Fz(\012)1540 1891 y Fq(\000)1568 1906 y Ft(\))p FC(,)h(we)g(get)f(additional)f(v)o(ari-)987 1956 y(ables)12 b(of)f(type)g Ft(b)q(o)q(ol)g FC(indicating)e(whether)i (the)h(symbol)e(currently)987 2005 y(read)i(is)f(at)g(the)h(be)o (ginning)d(or)j(the)f(\223end\224)h(of)f(the)g(tape.)17 b(Complete)987 2055 y(case)10 b(distinctions)c(via)i Ft(\(b)q(o)q(ol)1420 2037 y Fq(\000)1448 2055 y Ft(\))h FC(reduce)g(the)f(problem)g(to)f(the)i(con-)987 2105 y(struction)14 b(of)h(the)g(ne)o(w)h(state)f(from)h(the)f(two)f(parts)h (of)h(the)f(tape.)987 2155 y(This)d(can)h(be)f(done)g(easily)g(using)f (the)h(constants)g Ff(s)1746 2161 y Fo(0)1765 2155 y FC(,)h Ff(s)1806 2161 y Fo(1)1825 2155 y FC(,)g FB(p)p FC(,)f Fz(\012)p FC(,)i FB(t)987 2205 y FC(and)c FB(f)5 b FC(.)987 2274 y(Iterating)j(the)h(one-step)g(transition)e(function)h (via)h(proposition)d(7.3)987 2323 y(completes)11 b(the)f(proof.)p 1953 2298 V 1953 2322 2 25 v 1970 2322 V 1953 2324 19 2 v 987 2456 a FF(Refer)o(ences)992 2571 y Fe([1])21 b(S.)9 b(Bellantoni)g(and)e(S.)i(Cook.)j(A)d(ne)o(w)f (recursion-theoretic)g(charac-)1056 2617 y(terization)h(of)g(the)f (polytime)h(functions.)i Fd(Computational)d(comple)o(x-)1056 2663 y(ity)p Fe(,)i(2:97\226110,)e(1992.)p eop %%Page: 8 8 8 7 bop -86 42 a Fe([2])21 b(S.)12 b(Bellantoni,)h(K.-H.)g(Niggl,)h (and)d(H.)h(Schwichtenber)o(g.)21 b(Higher)-22 87 y(type)9 b(recursion,)g(rami\002cation)h(and)e(polynomial)h(time.)16 b(T)m(o)9 b(appear:)-22 133 y(Annals)f(of)i(Pure)e(and)h(Applied)f (Logic.)-86 176 y([3])21 b(V)-5 b(.-H.)22 b(Caseiro.)49 b Fd(Equations)19 b(for)i(De\002ning)e(Poly-time)i(Func-)-22 222 y(tions)p Fe(.)75 b(PhD)28 b(thesis,)33 b(Uni)o(v)o(ersity)c(of)g (Oslo,)34 b(Feb)o(.)27 b(1997.)-22 268 y Fc(ftp.ifi.u)q(io)q(.no)q(/p)q (ub/)q(vu)q(ok)q(ko/)q(0a)q(dm.)q(ps)q Fe(.)-86 311 y([4])21 b(M.)15 b(Hofmann.)30 b(In-place)13 b(update)h(with)h(linear)f(types)g (or)g(ho)o(w)g(to)-22 357 y(compile)8 b(functional)g(programms)f(into)i (malloc\(\)-free)h(C.)h(Preprint,)-22 403 y Fc(www.dcs.e)q(d.)q(ac.)q (uk)q(/)16 b Fb(~)-10 b Fc(mxh/mall)q(oc)q(.ps)q(.g)q(z)p Fe(.)-86 446 y([5])21 b(M.)d(Hofmann.)39 b(T)m(yped)16 b(lambda)h(calculi)g(for)h(polynomial-time)-22 492 y(computation.)27 b(Habilitation)15 b(thesis,)f(TU)g(Darmstadt,)h(German)o(y)n(.)-22 538 y(See)21 b Fc(www.dcs.)q(ed)q(.ac)q(.u)q(k/)q(hom)q(e/)q(mxh)q(/h)q (ab)q(il.)q(ps)q(.gz)q Fe(,)-22 583 y(1998.)-86 627 y([6])g(M.)13 b(Hofmann.)22 b(Linear)11 b(types)g(and)g(non-size-increasing)f (polyno-)-22 672 y(mial)h(time)h(computation.)18 b(In)11 b Fd(Pr)n(oceedings)d(14')o(th)j(Symposium)e(on)-22 718 y(Logic)f(in)h(Computer)f(Science)g(\(Lics'99\))p Fe(,)h(pages)f (464\226473,)f(1999.)-86 762 y([7])21 b(F)m(.)j(Joachimski)d(and)h(R.)i (Matthes.)58 b(Short)24 b(Proofs)f(of)g(Nor)o(-)-22 807 y(malization)h(for)i(the)e(simply-typed)g Fa(\025)p Fe(-calculus,)k (permutati)o(v)o(e)-22 853 y(con)o(v)o(ersions)19 b(and)i(G)s(\250)-15 b(odel')n(s)21 b Fa(T)5 b Fe(.)55 b(Submitted)21 b(to)h(the)f(Archi)o (v)o(e)-22 899 y(for)d(Mathematical)f(Logic,)i Fc(www.tcs.in)q(fo)q (rma)q(ti)q(k.)q(uni)q(-)-22 944 y(muenchen.)q(de)q(/)d Fb(~)-10 b Fc(matthes/)q(pa)q(per)q(s/)q(sn.)q(ht)q(ml)q Fe(,)12 b(1998.)-86 988 y([8])21 b(D.)c(Lei)o(v)o(ant.)35 b(Rami\002ed)16 b(recurrence)f(and)g(computational)g(com-)-22 1034 y(ple)o(xity)f(I:)h(W)m(ord)g(recurrence)e(and)g(poly\226time.)29 b(In)14 b(P)l(.)g(Clote)g(and)-22 1079 y(J.)9 b(Remmel,)h(editors,)f Fd(F)m(easible)f(Mathematics)h(II)p Fe(,)i(pages)c(320\226343.)-22 1125 y(Birkh)r(\250)-14 b(auser)o(,)8 b(Boston,)h(1995.)-86 1169 y([9])21 b(D.)12 b(Lei)o(v)o(ant)e(and)g(J.-Y)-5 b(.)13 b(Marion.)20 b(Lambda)10 b(calculus)f(characteriza-)-22 1214 y(tion)g(of)h(poly\226time.)j(In)d(M.)f(Bezem)f(and)h(J.)g (Groote,)g(editors,)h Fd(T)m(yped)-22 1260 y(Lambda)h(Calculi)h(and)f (Applications)p Fe(,)i(pages)d(274\226288.)h(Springer)-22 1306 y(Lecture)d(Notes)h(in)g(Computer)g(Science)f(V)-5 b(ol.)10 b(664,)e(1993.)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF