+++ /dev/null
-%!PS-Adobe-2.0\r
-%%Creator: dvips 5.47 Copyright 1986-91 Radical Eye Software\r
-%%Title: latex8.dvi\r
-%%Pages: 2 1\r
-%%BoundingBox: 0 0 612 792\r
-%%DocumentFonts: Times-Roman Times-Bold Times-Italic Helvetica-Bold\r
-%%EndComments\r
-%%BeginProcSet: /usr/local/lib/tex/ps/psfig.pro\r
-/TeXscale { 65536 div } def\r
-\r
-/DocumentInitState [ matrix currentmatrix currentlinewidth currentlinecap\r
-currentlinejoin currentdash currentgray currentmiterlimit ] cvx def\r
-\r
-/startTexFig {\r
- /SavedState save def\r
- userdict maxlength dict begin\r
- currentpoint transform\r
-\r
- DocumentInitState setmiterlimit setgray setdash setlinejoin setlinecap\r
- setlinewidth setmatrix\r
-\r
- itransform moveto\r
-\r
- /ury exch TeXscale def\r
- /urx exch TeXscale def\r
- /lly exch TeXscale def\r
- /llx exch TeXscale def\r
- /y exch TeXscale def\r
- /x exch TeXscale def\r
- \r
- currentpoint /cy exch def /cx exch def\r
-\r
- /sx x urx llx sub div def % scaling for x\r
- /sy y ury lly sub div def % scaling for y\r
-\r
- sx sy scale % scale by (sx,sy)\r
-\r
- cx sx div llx sub\r
- cy sy div ury sub translate\r
- \r
- /DefFigCTM matrix currentmatrix def\r
-\r
- /initmatrix {\r
- DefFigCTM setmatrix\r
- } def\r
- /defaultmatrix {\r
- DefFigCTM exch copy\r
- } def\r
-\r
- /initgraphics {\r
- DocumentInitState setmiterlimit setgray setdash \r
- setlinejoin setlinecap setlinewidth setmatrix\r
- DefFigCTM setmatrix\r
- } def\r
-\r
- /showpage {\r
- initgraphics\r
- } def\r
- /erasepage {\r
- initgraphics\r
- } def\r
- /copypage {} def\r
-\r
-} def\r
-/clipFig {\r
- currentpoint 6 2 roll\r
- newpath 4 copy\r
-\r
- 4 2 roll moveto\r
- 6 -1 roll exch lineto\r
- exch lineto\r
- exch lineto\r
- closepath clip\r
- newpath\r
- moveto\r
-} def\r
-/doclip { llx lly urx ury clipFig } def\r
-/endTexFig {\r
- end SavedState restore\r
-} def\r
-%%EndProcSet\r
-%%BeginProcSet: tex.pro\r
-/TeXDict 200 dict def TeXDict begin /N /def load def /B{bind def}N /S /exch\r
-load def /X{S N}B /TR /translate load N /isls false N /vsize 10 N /@rigin{\r
-isls{[0 1 -1 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale\r
-Resolution VResolution vsize neg mul TR matrix currentmatrix dup dup 4 get\r
-round 4 exch put dup dup 5 get round 5 exch put setmatrix}N /@letter{/vsize 10\r
-N}B /@landscape{/isls true N /vsize -1 N}B /@a4{/vsize 10.6929133858 N}B /@a3{\r
-/vsize 15.5531 N}B /@ledger{/vsize 16 N}B /@legal{/vsize 13 N}B /@manualfeed{\r
-statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N\r
-/FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn begin\r
-/FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array\r
-/BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2\r
-array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx FMat N df-tail}\r
-B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{pop nn dup definefont\r
-setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup\r
-length 4 sub get}B /ch-xoff{128 ch-data dup length 3 sub get sub}B /ch-yoff{\r
-ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B\r
-/ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0\r
-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\r
-dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0\r
-ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice\r
-ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 add]{ch-image}\r
-imagemask restore}B /D{/cc X dup type /stringtype ne{]}if nn /base get cc ctr\r
-put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf\r
-div put}if put /ctr ctr 1 add N}B /I{cc 1 add D}B /bop{userdict /bop-hook\r
-known{bop-hook}if /SI save N @rigin 0 0 moveto}N /eop{clear SI restore\r
-showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook\r
-known{start-hook}if /VResolution X /Resolution X 1000 div /DVImag X /IE 256\r
-array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for}N /p /show load N\r
-/RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X\r
-/rulex X V}B /V statusdict begin /product where{pop product dup length 7 ge{0\r
-7 getinterval(Display)eq}{pop false}ifelse}{false}ifelse end{{gsave TR -.1 -.1\r
-TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1\r
--.1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /a{\r
-moveto}B /delta 0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{\r
-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\r
-/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\r
-}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\r
-a}B /bos{/SS save N}B /eos{clear SS restore}B end\r
-%%EndProcSet\r
-%%BeginProcSet: texps.pro\r
-TeXDict begin /rf{655360 div mul Resolution mul 7227 div /PixPerEm X findfont\r
-dup length 1 add dict /nn X{1 index /FID ne{nn 3 1 roll put}{pop pop}ifelse}\r
-forall 256 dict begin nn /Encoding get 0 1 255{2 copy get 3 index 2 index get\r
-1000 mul PixPerEm div def pop}for pop pop nn /Metrics currentdict put end\r
-/fontname X /nn dup nn definefont[PixPerEm 0 0 PixPerEm neg 0 0]makefont N\r
-fontname{/foo setfont}2 array copy cvx N fontname load 0 nn put}N\r
-/ObliqueSlant{dup sin S cos div neg}B /SlantFont{/foo X[1 0 foo 1 0 0]\r
-TransFont}N /ExtendFont{/foo X 3 2 roll[S{foo div}forall]3 1 roll[foo 0 0 1 0\r
-\r
-0]TransFont}N /TransFont{S findfont S makefont dup length dict /nn X{1 index\r
-/FID ne{nn 3 1 roll put}{pop pop}ifelse}forall dup nn definefont pop}N end\r
-%%EndProcSet\r
-TeXDict begin 1000 300 300 @start /Fa [ 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 9 12 16 19 19 31\r
-29 12 12 12 19 25 9 12 9 10 19 19 19 19 19 19 19 19 19 19 12\r
-12 25 25 25 19 34 23 23 25 27 23 23 27 27 12 17 25 21 31 25\r
-27 23 27 23 19 21 27 23 31 23 21 21 15 10 15 16 19 12 19 19\r
-17 19 17 10 19 19 10 10 17 10 27 19 19 19 19 15 15 10 19 17\r
-25 17 17 15 15 10 15 20 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 15 19 19 6 19 19 19 19 8 21\r
-19 12 12 19 19 0 19 19 19 9 0 20 13 12 21 21 19 33 37 0 19\r
-0 12 12 12 12 12 12 12 12 0 12 12 0 12 12 12 33 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 33 0 10 0 0 0 0 21 27 35 12 0 0 0 0 0 25\r
-0 0 0 10 0 0 10 19 25 19 0 0 0 0 ] /Times-Italic 1000 589824\r
-rf /Fb [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 9 12 15 19 19 31 29 12 12 12 19 21 9 12 9 10\r
-19 19 19 19 19 19 19 19 19 19 10 10 21 21 21 17 34 27 25 25\r
-27 23 21 27 27 12 15 27 23 33 27 27 21 27 25 21 23 27 27 35\r
-27 27 23 12 10 12 18 19 12 17 19 17 19 17 12 19 19 10 10 19\r
-10 29 19 19 19 19 12 15 10 19 19 27 19 19 17 18 7 18 20 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 12 19 19 6 19 19 19 19 7 17 19 12 12 21 21 0 19 19 19 9\r
-0 17 13 12 17 17 19 37 37 0 17 0 12 12 12 12 12 12 12 12 0\r
-12 12 0 12 12 12 37 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 33 0 10\r
-0 0 0 0 23 27 33 12 0 0 0 0 0 25 0 0 0 10 0 0 10 19 27 19 0\r
-0 0 0 ] /Times-Roman 1000 589824 rf /Fc [ 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 8 11 14 17 17\r
-28 26 11 11 11 17 19 8 11 8 9 17 17 17 17 17 17 17 17 17 17\r
-9 9 19 19 19 15 31 24 22 22 24 20 18 24 24 11 13 24 20 30 24\r
-24 18 24 22 18 20 24 24 31 24 24 20 11 9 11 16 17 11 15 17\r
-15 17 15 11 17 17 9 9 17 9 26 17 17 17 17 11 13 9 17 17 24\r
-17 17 15 16 7 16 18 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 11 17 17 6 17 17 17 17 6 15 17\r
-11 11 18 18 0 17 17 17 8 0 15 12 11 15 15 17 33 33 0 15 0 11\r
-11 11 11 11 11 11 11 0 11 11 0 11 11 11 33 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 30 0 9 0 0 0 0 20 24 30 10 0 0 0 0 0 22 0 0\r
-0 9 0 0 9 17 24 17 0 0 0 0 ] /Times-Roman 1000 524288 rf /Fd\r
-[ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 6 8 10 12 12 21 19 8 8 8 12 14 6 8 6 7 12 12 12 12 12\r
-12 12 12 12 12 7 7 14 14 14 11 23 18 17 17 18 15 14 18 18 8\r
-10 18 15 22 18 18 14 18 17 14 15 18 18 24 18 18 15 8 7 8 12\r
-12 8 11 12 11 12 11 8 12 12 7 7 12 7 19 12 12 12 12 8 10 7\r
-12 12 18 12 12 11 12 5 12 13 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 8 12 12 4 12 12 12 12\r
-4 11 12 8 8 14 14 0 12 12 12 6 0 11 9 8 11 11 12 25 25 0 11\r
-0 8 8 8 8 8 8 8 8 0 8 8 0 8 8 8 25 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 22 0 7 0 0 0 0 15 18 22 8 0 0 0 0 0 17 0 0 0 7 0 0\r
-7 12 18 12 0 0 0 0 ] /Times-Roman 1000 393216 rf /Fe [ 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-7 10 12 15 15 24 23 10 10 10 15 16 7 10 7 8 15 15 15 15 15\r
-15 15 15 15 15 8 8 16 16 16 13 27 21 19 19 21 18 16 21 21 10\r
-11 21 18 26 21 21 16 21 19 16 18 21 21 27 21 21 18 10 8 10\r
-14 15 10 13 15 13 15 13 10 15 15 8 8 15 8 23 15 15 15 15 10\r
-11 8 15 15 21 15 15 13 14 6 14 16 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 10 15 15 5 15 15\r
-15 15 5 13 15 10 10 16 16 0 15 15 15 7 0 13 10 10 13 13 15\r
-29 29 0 13 0 10 10 10 10 10 10 10 10 0 10 10 0 10 10 10 29\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 26 0 8 0 0 0 0 18 21 26 9 0\r
-0 0 0 0 19 0 0 0 8 0 0 8 15 21 15 0 0 0 0 ] /Times-Roman 1000\r
-458752 rf /Ff [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 12 14 20 23 23 37 30 12 14 14 16 24 12\r
-14 12 12 23 23 23 23 23 23 23 23 23 23 14 14 24 24 24 25 40\r
-\r
-30 30 30 30 28 25 32 30 12 23 30 25 35 30 32 28 32 30 28 25\r
-30 28 39 28 28 25 14 12 14 24 23 12 23 25 23 25 23 14 25 25\r
-12 12 23 12 37 25 25 25 25 16 23 14 25 23 32 23 23 21 16 12\r
-16 24 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 14 23 23 7 23 23 23 23 10 21 23 14 14 25 25 0\r
-23 23 23 12 0 23 15 12 21 21 23 42 42 0 25 0 14 14 14 14 14\r
-14 14 14 0 14 14 0 14 14 14 42 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 42 0 15 0 0 0 0 25 32 42 15 0 0 0 0 0 37 0 0 0 12 0 0 12\r
-25 39 25 0 0 0 0 ] /Helvetica-Bold 1000 655360 rf /Fg 1 3 df<400020C000606000\r
-C03001801803000C0600060C0003180001B00000E00000E00001B000031800060C000C06001803\r
-003001806000C0C0006040002013147A9320>2 D E /Fh 1 59 df<60F0F06004047C830C>58\r
-D E /Fi [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 11 15 25 23 23 46 38 15 15 15 23 26 11 15 11\r
-13 23 23 23 23 23 23 23 23 23 23 15 15 26 26 26 23 42 33 30\r
-33 33 30 28 36 36 18 23 36 30 43 33 36 28 36 33 25 30 33 33\r
-46 33 33 30 15 13 15 27 23 15 23 25 20 25 20 15 23 25 13 15\r
-25 13 38 25 23 25 25 20 18 15 25 23 33 23 23 20 18 10 18 24\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 15 23 23 8 23 23 23 23 13 23 23 15 15 25 25 0 23 23\r
-23 11 0 25 16 15 23 23 23 46 46 0 23 0 15 15 15 15 15 15 15\r
-15 0 15 15 0 15 15 15 46 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 46\r
-0 14 0 0 0 0 30 36 46 15 0 0 0 0 0 33 0 0 0 13 0 0 13 23 33\r
-25 0 0 0 0 ] /Times-Bold 1000 720896 rf /Fj [ 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 10 14 17\r
-21 21 35 32 14 14 14 21 23 10 14 10 12 21 21 21 21 21 21 21\r
-21 21 21 12 12 23 23 23 18 38 30 28 28 30 25 23 30 30 14 16\r
-30 25 37 30 30 23 30 28 23 25 30 30 39 30 30 25 14 12 14 19\r
-21 14 18 21 18 21 18 14 21 21 12 12 21 12 32 21 21 21 21 14\r
-16 12 21 21 30 21 21 18 20 8 20 22 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 14 21 21 7 21 21\r
-21 21 7 18 21 14 14 23 23 0 21 21 21 10 0 19 15 14 18 18 21\r
-42 42 0 18 0 14 14 14 14 14 14 14 14 0 14 14 0 14 14 14 42\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 37 0 11 0 0 0 0 25 30 37 13\r
-0 0 0 0 0 28 0 0 0 12 0 0 12 21 30 21 0 0 0 0 ] /Times-Roman\r
-1000 655360 rf /Fk [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 10 14 17 21 21 35 32 14 14 14 21\r
-28 10 14 10 12 21 21 21 21 21 21 21 21 21 21 14 14 28 28 28\r
-21 38 25 25 28 30 25 25 30 30 14 18 28 23 35 28 30 25 30 25\r
-21 23 30 25 35 25 23 23 16 12 16 18 21 14 21 21 18 21 18 12\r
-21 21 12 12 18 12 30 21 21 21 21 16 16 12 21 18 28 18 18 16\r
-17 11 17 22 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 16 21 21 7 21 21 21 21 9 23 21 14 14 21\r
-21 0 21 21 21 10 0 22 15 14 23 23 21 37 42 0 21 0 14 14 14\r
-14 14 14 14 14 0 14 14 0 14 14 14 37 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 37 0 11 0 0 0 0 23 30 39 13 0 0 0 0 0 28 0 0 0 12\r
-0 0 12 21 28 21 0 0 0 0 ] /Times-Italic 1000 655360 rf /Fl\r
-[ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 12 17 28 25 25 50 41 17 17 17 25 28 12 17 12 14 25 25\r
-25 25 25 25 25 25 25 25 17 17 28 28 28 25 46 36 33 36 36 33\r
-30 39 39 19 25 39 33 47 36 39 30 39 36 28 33 36 36 50 36 36\r
-33 17 14 17 29 25 17 25 28 22 28 22 17 25 28 14 17 28 14 41\r
-28 25 28 28 22 19 17 28 25 36 25 25 22 20 11 20 26 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-17 25 25 8 25 25 25 25 14 25 25 17 17 28 28 0 25 25 25 12 0\r
-27 17 17 25 25 25 50 50 0 25 0 17 17 17 17 17 17 17 17 0 17\r
-17 0 17 17 17 50 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 50 0 15 0\r
-0 0 0 33 39 50 16 0 0 0 0 0 36 0 0 0 14 0 0 14 25 36 28 0 0\r
-0 0 ] /Times-Bold 1000 786432 rf /Fm [ 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 12 17 20 25 25\r
-41 39 17 17 17 25 28 12 17 12 14 25 25 25 25 25 25 25 25 25\r
-25 14 14 28 28 28 22 46 36 33 33 36 30 28 36 36 17 19 36 30\r
-44 36 36 28 36 33 28 30 36 36 47 36 36 30 17 14 17 23 25 17\r
-\r
-22 25 22 25 22 17 25 25 14 14 25 14 39 25 25 25 25 17 19 14\r
-25 25 36 25 25 22 24 10 24 27 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 17 25 25 8 25 25 25 25\r
-9 22 25 17 17 28 28 0 25 25 25 12 0 23 17 17 22 22 25 50 50\r
-0 22 0 17 17 17 17 17 17 17 17 0 17 17 0 17 17 17 50 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 44 0 14 0 0 0 0 30 36 44 15 0 0 0\r
-0 0 33 0 0 0 14 0 0 14 25 36 25 0 0 0 0 ] /Times-Roman 1000\r
-786432 rf /Fn 1 3 df<60000006F000000FF800001F7C00003E3E00007C1F0000F80F8001F0\r
-07C003E003E007C001E0078001F00F8000F81F00007C3E00003E7C00001FF800000FF0000007E0\r
-000007E000000FF000001FF800003E7C00007C3E0000F81F0001F00F8001E0078003E007C007C0\r
-03E00F8001F01F0000F83E00007C7C00003EF800001FF000000F600000062022769F35>2\r
-D E /Fo 4 59 df<000600001E0003FE00FFFE00FFFE007CFE0000FE0000FE0000FE0000FE0000\r
-FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000\r
-FE0000FE007FFFFE7FFFFE7FFFFE171C7B9B22>49 D<0C0003000F803F000FFFFE000FFFFC000F\r
-FFF8000FFFF0000FFFE0000FFFC0000FFE00000E0000000E0000000E0000000E0000000E000000\r
-0E0000000E3FC0000EFFF0000FC0FC000F007E000C003F000C003F8000001F8000001FC000001F\r
-C000001FE000001FE018001FE07C001FE0FE001FE0FE001FE0FE001FE0FE001FC0FC001FC07800\r
-1FC070003F8038003F001C007E000F81FC0007FFF80003FFE00000FF00001B297D9B22>53\r
-D<003FC00001FFF00003FFF80007C07C000F003E001F001F001E000F803E000F803E000F803E00\r
-0F803F000F803F000F803FC00F003FF01F001FFC1E001FFE3C000FFFF80007FFE00003FFF80001\r
-FFFC0001FFFE0007FFFF000F0FFF801E03FFC03E01FFC07C007FC07C001FE0F8000FE0F80007E0\r
-F80003E0F80003E0F80003E0F80003C07C0003C07C0007C03E0007803F000F001FC07E0007FFFC\r
-0003FFF000007FC0001B297DA722>56 D<1C003E007F00FF80FF80FF807F003E001C0009097B88\r
-13>58 D E /Fp [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 15 19 32 29 29 58 48 19 19 19 29 33 15\r
-19 15 16 29 29 29 29 29 29 29 29 29 29 19 19 33 33 33 29 54\r
-42 39 42 42 39 36 45 45 23 29 45 39 55 42 45 36 45 42 32 39\r
-42 42 58 42 42 39 19 16 19 34 29 19 29 32 26 32 26 19 29 32\r
-16 19 32 16 48 32 29 32 32 26 23 19 32 29 42 29 29 26 23 13\r
-23 30 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 19 29 29 10 29 29 29 29 16 29 29 19 19 32 32\r
-0 29 29 29 15 0 31 20 19 29 29 29 58 58 0 29 0 19 19 19 19\r
-19 19 19 19 0 19 19 0 19 19 19 58 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 58 0 17 0 0 0 0 39 45 58 19 0 0 0 0 0 42 0 0 0 16 0 0\r
-16 29 42 32 0 0 0 0 ] /Times-Bold 1000 917504 rf /Fq [ 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-12 15 19 23 23 39 36 15 15 15 23 26 12 15 12 13 23 23 23 23\r
-23 23 23 23 23 23 13 13 26 26 26 21 43 34 31 31 34 28 26 34\r
-34 15 18 34 28 41 34 34 26 34 31 26 28 34 34 44 34 34 28 15\r
-13 15 22 23 15 21 23 21 23 21 15 23 23 13 13 23 13 36 23 23\r
-23 23 15 18 13 23 23 34 23 23 21 22 9 22 25 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 15 23 23\r
-8 23 23 23 23 8 21 23 15 15 26 26 0 23 23 23 12 0 21 16 15\r
-21 21 23 46 46 0 21 0 15 15 15 15 15 15 15 15 0 15 15 0 15\r
-15 15 46 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 41 0 13 0 0 0 0 28\r
-34 41 14 0 0 0 0 0 31 0 0 0 13 0 0 13 23 34 23 0 0 0 0 ] /Times-Roman\r
-1000 734003 rf /Fr [ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 0 0 0 15 19 24 29 29 48 45 19 19 19 29\r
-33 15 19 15 16 29 29 29 29 29 29 29 29 29 29 16 16 33 33 33\r
-26 54 42 39 39 42 36 32 42 42 19 23 42 36 52 42 42 32 42 39\r
-32 36 42 42 55 42 42 36 19 16 19 27 29 19 26 29 26 29 26 19\r
-29 29 16 16 29 16 45 29 29 29 29 19 23 16 29 29 42 29 29 26\r
-28 12 28 31 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 0 0 0 0 19 29 29 10 29 29 29 29 10 26 29 19 19\r
-32 32 0 29 29 29 15 0 26 20 19 26 26 29 58 58 0 26 0 19 19\r
-19 19 19 19 19 19 0 19 19 0 19 19 19 58 0 0 0 0 0 0 0 0 0 0\r
-0 0 0 0 0 0 52 0 16 0 0 0 0 36 42 52 18 0 0 0 0 0 39 0 0 0\r
-\r
-16 0 0 16 29 42 29 0 0 0 0 ] /Times-Roman 1000 917504 rf end\r
-%%EndProlog\r
-%%BeginSetup\r
-%%Feature: *Resolution 300\r
-TeXDict begin \r
-%%EndSetup\r
-%%Page: 1 1\r
-bop 69 187 a Fr(L)84 179 y Fq(A)109 187 y Fr(T)135 205 y(E)162\r
-187 y(X)15 b Fp(Author)g(Guidelines)h(for)29 b Fo(8:5)16 b\r
-Fn(\002)g Fo(11)p Fp(-Inch)f(Pr)o(oceedings)f(Manuscripts)414\r
-371 y Fm(Paolo)e(Ienne)155 429 y(Swiss)h(Federal)f(Institute)f(of)h(T)m\r
-(echnology)248 487 y(Microcomputing)f(Laboratory)91 545 y(IN-F)g(Ecublens,)j\r
-(1015)e(Lausanne,)i(Switzerland)298 603 y(Paolo.Ienne@di.ep\257.ch)1294\r
-371 y(Second)f(Author)1330 429 y(Institution2)1128 487 y(First)e(line)i(of)f\r
-(institution2)f(address)1100 545 y(Second)h(line)g(of)g(institution2)g\r
-(address)1115 603 y(SecondAuthor@institution2.com)308 778 y\r
-Fl(Abstract)-41 878 y Fk(The)h(ABSTRACT)h(is)e(to)g(be)i(in)e\r
-(fully-justi\256ed)e(italicized)h(text,)-91 928 y(at)k(the)h(top)e(of)i(the)f\r
-(left-hand)f(column,)j(below)e(the)g(author)g(and)-91 978 y(af\256liation)f\r
-(information.)34 b(Use)18 b(the)g(wor)n(d)f(\252Abstract\272)h(as)f(the)-91\r
-1027 y(title,)c(in)f(12-point)f(T)n(imes,)j(boldface)e(type,)j(center)n(ed)f\r
-(r)n(elative)g(to)-91 1077 y(the)g(column,)i(initially)c(capitalized.)28\r
-b(The)15 b(abstract)f(is)g(to)h(be)g(in)-91 1127 y(10-point,)g(single-spaced)\r
-g(type.)33 b(The)16 b(abstract)f(may)h(be)g(up)g(to)-91 1177\r
-y(3)f(inches)g(\(7.62)g(cm\))g(long.)28 b(Leave)17 b(two)d(blank)g(lines)h\r
-(after)f(the)-91 1227 y(Abstract,)c(then)g(begin)g(the)g(main)f(text.)-91\r
-1389 y Fl(1.)k(Intr)o(oduction)-41 1494 y Fj(Please)f(follow)e(the)i(steps)f\r
-(outlined)f(below)h(when)h(submitting)-91 1544 y(your)c(manuscript)h(to)g\r
-(the)h(IEEE)g(Computer)f(Society)g(Press.)15 b(Note)-91 1593\r
-y(there)g(have)h(been)f(some)h(changes)g(to)f(the)g(measurements)h(from)-91\r
-1643 y(previous)9 b(instructions.)-91 1756 y Fl(2.)k(Instructions)-41\r
-1861 y Fj(Please)e(read)g(the)f(following)e(carefully)m(.)-91\r
-1961 y Fi(2.1.)k(Language)-41 2062 y Fj(All)d(manuscripts)h(must)g(be)h(in)e\r
-(English.)-91 2162 y Fi(2.2.)j(Printing)f(your)h(paper)-41\r
-2262 y Fj(Print)c(your)h(properly)f(formatted)h(text)g(on)h(high-quality)m(,)\r
-d(8)p Fh(:)p Fj(5)g Fg(\002)-91 2312 y Fj(11-inch)g(white)g(printer)f(paper)n\r
-(.)15 b(A4)8 b(paper)g(is)f(also)h(acceptable,)i(but)-91 2362\r
-y(please)k(leave)f(the)g(extra)g(0.5)g(inch)f(\(1.27)g(cm\))i(at)f(the)g\r
-(BOTT)o(OM)-91 2412 y(of)d(the)g(page.)-91 2512 y Fi(2.3.)i(Margins)f(and)h\r
-(page)g(numbering)-41 2613 y Fj(All)18 b(printed)g(material,)j(including)c\r
-(text,)k(illustrations,)e(and)-91 2662 y(charts,)14 b(must)f(be)g(kept)g\r
-(within)e(a)i(print)f(area)i(6-7/8)e(inches)h(\(17.5)987 778\r
-y(cm\))e(wide)g(by)f(8-7/8)g(inches)g(\(22.54)g(cm\))i(high.)j(Do)c(not)f\r
-(write)g(or)987 828 y(print)j(anything)f(outside)h(the)h(print)f(area.)27\r
-b(Number)15 b(your)e(pages)987 878 y(lightly)m(,)k(in)f(pencil,)j(on)d(the)h\r
-(upper)g(right-hand)e(corners)i(of)g(the)987 928 y(BACKS)9\r
-b(of)h(the)g(pages)h(\(for)e(example,)i(1/10,)f(2/10,)f(or)h(1)g(of)f(10,)i\r
-(2)987 978 y(of)f(10,)g(and)g(so)g(forth\).)j(Please)f(do)d(not)g(write)h(on)\r
-f(the)h(fronts)f(of)h(the)987 1027 y(pages,)h(nor)f(on)g(the)g(lower)g\r
-(halves)g(of)g(the)g(backs)h(of)f(the)g(pages.)987 1136 y Fi(2.4.)i\r
-(Formatting)f(your)h(paper)1037 1245 y Fj(All)17 b(text)h(must)h(be)f(in)g(a)\r
-h(two-column)f(format.)39 b(The)19 b(total)987 1295 y(allowable)13\r
-b(width)g(of)g(the)h(text)f(area)i(is)f(6-7/8)e(inches)i(\(17.5)g(cm\))987\r
-1345 y(wide)9 b(by)f(8-7/8)g(inches)h(\(22.54)g(cm\))g(high.)14\r
-b(Columns)8 b(are)i(to)e(be)i(3-)987 1395 y(1/4)g(inches)h(\(8.25)g(cm\))h\r
-(wide,)f(with)f(a)i(5/16)e(inch)g(\(0.8)h(cm\))h(space)987\r
-1445 y(between)17 b(them.)34 b(The)17 b(main)g(title)e(\(on)h(the)h(\256rst)f\r
-\r
-(page\))h(should)987 1494 y(begin)8 b(1.0)i(inch)e(\(2.54)h(cm\))h(from)f\r
-(the)g(top)f(edge)i(of)e(the)h(page.)16 b(The)987 1544 y(second)9\r
-b(and)f(following)e(pages)j(should)e(begin)h(1.0)g(inch)g(\(2.54)g(cm\))987\r
-1594 y(from)j(the)g(top)f(edge.)18 b(On)11 b(all)g(pages,)h(the)f(bottom)f\r
-(mar)o(gin)h(should)987 1644 y(be)f(1-1/8)f(inches)h(\(2.86)f(cm\))i(from)e\r
-(the)h(bottom)e(edge)j(of)e(the)h(page)987 1694 y(for)g(8)p\r
-Fh(:)p Fj(5)e Fg(\002)i Fj(11-inch)f(paper;)i(for)f(A4)g(paper)n(,)h\r
-(approximately)f(1-5/8)987 1744 y(inches)g(\(4.13)g(cm\))h(from)f(the)g\r
-(bottom)f(edge)i(of)f(the)g(page.)987 1853 y Fi(2.5.)i(T)m(ype-style)g(and)g\r
-(fonts)1037 1962 y Fj(Wherever)f(T)o(imes)f(is)h(speci\256ed,)g(T)o(imes)g\r
-(Roman)f(may)h(also)f(be)987 2011 y(used.)17 b(If)10 b(neither)g(is)h\r
-(available)f(on)h(your)f(word)g(processor)n(,)i(please)987\r
-2061 y(use)i(the)g(font)f(closest)i(in)e(appearance)j(to)d(T)o(imes)i(that)e\r
-(you)h(have)987 2111 y(access)e(to.)1037 2163 y(MAIN)j(TITLE.)j(Center)e(the)\r
-f(title)g(1-3/8)f(inches)i(\(3.49)g(cm\))987 2212 y(from)d(the)g(top)g(edge)g\r
-(of)g(the)h(\256rst)f(page.)24 b(The)14 b(title)e(should)g(be)i(in)987\r
-2262 y(T)o(imes)j(14-point,)g(boldface)f(type.)35 b(Capitalize)16\r
-b(the)h(\256rst)f(letter)987 2312 y(of)c(nouns,)h(pronouns,)f(verbs,)h\r
-(adjectives,)g(and)g(adverbs;)g(do)f(not)987 2362 y(capitalize)g(articles,)g\r
-(coordinate)f(conjunctions,)g(or)g(prepositions)987 2412 y(\(unless)f(the)g\r
-(title)f(begins)h(with)f(such)i(a)g(word\).)j(Leave)e(two)e(blank)987\r
-2461 y(lines)g(after)g(the)g(title.)1037 2513 y(AUTHOR)c(NAME\(s\))g(and)g\r
-(AFFILIA)-5 b(TION\(s\))6 b(are)g(to)g(be)g(ce)q(n-)987 2563\r
-y(tered)13 b(beneath)g(the)g(title)e(and)i(printed)f(in)g(T)o(imes)h\r
-(12-point,)f(non-)987 2613 y(boldface)i(type.)26 b(This)14\r
-b(information)e(is)i(to)f(be)i(followed)d(by)i(two)987 2662\r
-y(blank)c(lines.)p eop\r
-%%Page: 2 2\r
-bop -41 42 a Fj(The)13 b(ABSTRACT)f(and)h(MAIN)g(TEXT)g(are)h(to)e(be)h(in)f\r
-(a)h(two-)-91 91 y(column)d(format.)-41 142 y(MAIN)g(TEXT)m(.)i(T)m(ype)f\r
-(main)f(text)g(in)g(10-point)e(T)o(imes,)j(single-)-91 192\r
-y(spaced.)k(Do)6 b(NOT)g(use)g(double-spacing.)14 b(All)6 b(paragraphs)g\r
-(should)-91 241 y(be)13 b(indented)f(1)h(pica)g(\(approx.)23\r
-b(1/6)12 b(inch)g(or)h(0.422)g(cm\).)24 b(Make)-91 291 y(sure)12\r
-b(your)f(text)g(is)g(fully)f(justi\256ed\320that)g(is,)i(\257ush)g(left)f\r
-(and)g(\257ush)-91 341 y(right.)i(Please)8 b(do)f(not)f(place)i(any)f\r
-(additional)f(blank)g(lines)h(between)-91 391 y(paragraphs.)27\r
-b(Figure)14 b(and)h(table)f(captions)g(should)f(be)h(10-point)-91\r
-441 y(Helvetica)c(boldface)h(type)e(as)i(in)113 572 y Ff(Figure)h(1.)f\r
-(Example)g(of)h(caption.)-91 674 y Fj(Long)e(captions)g(should)f(be)h(set)h\r
-(as)g(in)-41 805 y Ff(Figure)17 b(2.)f(Example)g(of)g(long)h(caption)g\r
-(requiring)-41 855 y(more)e(than)h(one)f(line.)26 b(It)14 b(is)g(not)i(typed)\r
-f(centered)-41 905 y(but)f(aligned)h(on)f(both)h(sides)f(and)h(indented)g\r
-(with)-41 955 y(an)d(additional)f(margin)h(on)g(both)h(sides)f(of)f(1)h\r
-(pica.)-91 1098 y Fj(Callouts)k(should)g(be)h(9-point)e(Helvetica,)20\r
-b(non-boldface)c(type.)-91 1148 y(Initially)11 b(capitalize)j(only)f(the)h\r
-(\256rst)g(word)f(of)h(section)f(titles)g(and)-91 1198 y(\256rst-,)d\r
-(second-,)h(and)f(third-order)e(headings.)-41 1248 y(FIRST)l(-ORDER)i\r
-(HEADINGS.)h(\(For)f(example,)i Fl(1.)20 b(Intr)o(o-)-91 1298\r
-y(duction)p Fj(\))7 b(should)h(be)h(T)o(imes)g(12-point)e(boldface,)j\r
-(initially)c(cap-)-91 1348 y(italized,)i(\257ush)h(left,)g(with)e(one)i\r
-(blank)f(line)g(before,)i(and)e(one)h(blank)-91 1398 y(line)g(after)n(.)-41\r
-1448 y(SECOND-ORDER)23 b(HEADINGS.)i(\(For)f(example,)29 b\r
-Fi(1.1.)-91 1498 y(Database)13 b(elements)p Fj(\))g(should)e(be)h(T)o(imes)h\r
-(11-point)d(boldface,)-91 1548 y(initially)h(capitalized,)k(\257ush)f(left,)g\r
-\r
-(with)f(one)h(blank)g(line)f(before,)-91 1597 y(and)18 b(one)g(after)n(.)37\r
-b(If)18 b(you)f(require)h(a)g(third-order)e(heading)h(\(we)-91\r
-1647 y(discourage)11 b(it\),)h(use)g(10-point)d(T)o(imes,)k(boldface,)f\r
-(initially)d(capi-)-91 1697 y(talized,)k(\257ush)f(left,)g(preceded)h(by)f\r
-(one)g(blank)f(line,)i(followed)e(by)-91 1747 y(a)g(period)e(and)h(your)g\r
-(text)f(on)h(the)g(same)i(line.)-91 1853 y Fi(2.6.)g(Footnotes)-41\r
-1958 y Fj(Please)c(use)g(footnotes)f(sparingly)454 1943 y Fe(1)476\r
-1958 y Fj(and)h(place)g(them)g(at)g(the)f(bot-)-91 2008 y(tom)g(of)h(the)g\r
-(column)f(on)h(the)g(page)g(on)g(which)f(they)h(are)h(referenced.)-91\r
-2058 y(Use)i(T)o(imes)f(8-point)f(type,)h(single-spaced.)-91\r
-2163 y Fi(2.7.)i(Refer)o(ences)-41 2269 y Fj(List)d(and)g(number)h(all)f\r
-(bibliographical)e(references)k(in)e(9-point)-91 2319 y(T)o(imes,)14\r
-b(single-spaced,)f(at)g(the)f(end)h(of)f(your)g(paper)n(.)22\r
-b(When)13 b(ref-)-91 2369 y(erenced)i(in)f(the)h(text,)g(enclose)g(the)f\r
-(citation)g(number)g(in)g(square)-91 2419 y(brackets,)h(for)d(example)i([1].)\r
-24 b(Where)14 b(appropriate,)f(include)f(the)-91 2468 y(name\(s\))f(of)f\r
-(editors)f(of)h(referenced)i(books.)p -91 2505 394 2 v -46\r
-2532 a Fd(1)-31 2544 y Fc(Or)o(,)c(better)f(still,)j(try)e(to)f(avoid)g\r
-(footnotes)g(altogether)n(.)k(T)n(o)d(help)f(your)g(readers,)-91\r
-2584 y(avoid)j(using)g(footnotes)g(altogether)g(and)g(include)h(necessary)e\r
-(peripheral)h(obser)o(-)-91 2623 y(vations)f(in)h(the)f(text)h(\(within)g\r
-(parentheses,)f(if)h(you)f(prefer)o(,)h(as)g(in)f(this)h(sentence\).)987\r
-42 y Fi(2.8.)i(Illustrations,)f(graphs,)h(and)g(photographs)1037\r
-145 y Fj(All)f(graphics)i(should)e(be)i(centered.)22 b(Y)l(our)12\r
-b(artwork)g(must)g(be)987 195 y(in)f(place)h(in)f(the)h(article)f\r
-(\(preferably)g(printed)g(as)h(part)f(of)h(the)f(text)987 245\r
-y(rather)e(than)g(pasted)g(up\).)14 b(If)9 b(you)g(are)h(using)e(photographs)\r
-f(and)j(are)987 295 y(able)k(to)e(have)i(halftones)f(made)h(at)g(a)g(print)d\r
-(shop,)j(use)g(a)g(100-)f(or)987 345 y(110-line)c(screen.)16\r
-b(If)10 b(you)g(must)g(use)g(plain)g(photos,)f(they)h(must)g(be)987\r
-394 y(pasted)e(onto)g(your)f(manuscript.)15 b(Use)9 b(rubber)f(cement)h(to)f\r
-(af)o(\256x)h(the)987 444 y(images)f(in)e(place.)15 b(Black)7\r
-b(and)g(white,)g(clear)n(,)i(glossy-\256nish)d(photos)987 494\r
-y(are)k(preferable)h(to)e(color)n(.)14 b(Supply)9 b(the)g(best)h(quality)e\r
-(photographs)987 544 y(and)i(illustrations)d(possible.)15 b(Penciled)10\r
-b(lines)f(and)h(very)g(\256ne)h(lines)987 594 y(do)g(not)h(reproduce)g(well.)\r
-19 b(Remember)n(,)c(the)d(quality)e(of)i(the)f(book)987 643\r
-y(cannot)h(be)h(better)f(than)g(the)h(originals)e(provided.)21\r
-b(Do)12 b(NOT)h(use)987 693 y(tape)d(on)g(your)g(pages!)987\r
-797 y Fi(2.9.)i(Color)1037 901 y Fj(The)i(use)h(of)f(color)f(on)h(interior)e\r
-(pages)j(\(that)e(is,)i(pages)g(other)987 951 y(than)e(the)f(cover\))h(is)g\r
-(prohibitively)d(expensive.)23 b(W)m(e)14 b(publish)d(in-)987\r
-1000 y(terior)h(pages)i(in)f(color)f(only)g(when)h(it)g(is)g(speci\256cally)g\r
-(requested)987 1050 y(and)h(budgeted)f(for)g(by)g(the)h(conference)h(or)o\r
-(ganizers.)25 b(DO)14 b(NOT)987 1100 y(SUBMIT)c(COLOR)g(IMAGES)g(IN)g(YOUR)g\r
-(P)l(APERS)g(UNLESS)987 1150 y(SPECIFICALL)l(Y)g(INSTRUCTED)h(T)o(O)g(DO)f\r
-(SO.)987 1254 y Fi(2.10.)i(Symbols)1037 1357 y Fj(If)19 b(your)g(word)f\r
-(processor)i(or)f(typewriter)f(cannot)i(produce)987 1407 y(Greek)9\r
-b(letters,)g(mathematical)g(symbols,)g(or)g(other)f(graphical)g(ele-)987\r
-1457 y(ments,)13 b(please)g(use)f(pressure-sensitive)g(\(self-adhesive\))g\r
-(rub-on)987 1507 y(symbols)i(or)g(letters)g(\(available)h(in)f(most)g\r
-(stationery)g(stores,)i(art)987 1557 y(stores,)11 b(or)e(graphics)h(shops\).)\r
-987 1660 y Fi(2.11.)i(Copyright)f(forms)1037 1764 y Fj(Y)l(ou)16\r
-\r
-b(must)g(include)g(your)f(signed)h(IEEE)h(copyright)e(release)987\r
-1814 y(form)i(when)h(you)f(submit)g(your)g(\256nished)g(paper)n(.)37\r
-b(W)m(e)18 b(MUST)987 1864 y(have)d(this)f(form)h(before)g(your)f(paper)h\r
-(can)h(be)f(published)e(in)i(the)987 1914 y(proceedings.)987\r
-2017 y Fi(2.12.)d(Conclusions)1037 2121 y Fj(Please)k(direct)g(any)f\r
-(questions)g(to)g(the)g(production)f(editor)g(in)987 2171 y(char)o(ge)e(of)g\r
-(these)g(proceedings)f(at)g(the)h(IEEE)g(Computer)f(Society)987\r
-2221 y(Press:)k(Phone)10 b(\(714\))g(821-8380,)e(or)i(Fax)h(\(714\))e\r
-(761-1784.)987 2337 y Fl(Refer)o(ences)992 2441 y Fb([1])21\r
-b(I.)8 b(M.)g(Author)n(.)h(Some)d(related)h(article)h(I)f(wrote.)j\r
-Fa(Some)c(Fine)h(Journal)p Fb(,)1056 2487 y(99\(7\):1\261100,)h(January)g\r
-(1999.)992 2530 y([2])21 b(A.)8 b(N.)h(Expert.)i Fa(A)d(Book)e(He)i(W)n(r)o\r
-(ote)p Fb(.)i(His)e(Publisher)o(,)g(Erewhon,)f(NC,)1056 2576\r
-y(1999.)930 2787 y Fj(2)p eop\r
-%%Trailer\r
-end\r
-userdict /end-hook known{end-hook}if\r
-%%EOF\r
+++ /dev/null
-========== file: LATEX.TXT =======================\r
-\r
-The following files contain the LaTeX macros necessary for you to format \r
-your paper based on the instructions/measurements in the INSTRUCT.TXT \r
-attachment in our standard author kit for 8.5 x 11-inch proceedings. \r
-The files appear in the following order:\r
-\r
-latex8.sty -- the style file\r
-latex8.tex -- the main macro set\r
-latex8.bib -- the sample bibliography macros\r
-latex8.bst -- the bibliography main macro set\r
-latex8ps.txt -- this file, when printed out, will give you a sample \r
-of how your paper should look when it's finished. This file is in a \r
-separate attachment from the first four LaTeX files. Remember to save \r
-it as a .ps file and strip out any extraneous lines at the top of the \r
-file to enable successful printing.\r
-\r
-Note that both current versions of LaTeX, 2e and 2.09, have the same \r
-macros -- refer to the start of the latex8.sty file for the opening \r
-statement for each. \r
-\r
+++ /dev/null
-all:
- latex t
- latex t
- latex t
- dvips -ta4 t
+++ /dev/null
-\r
-%\r
-% $Description: Sample bibliography$ \r
-% \r
-% $Author: ienne $ \r
-% $Date: 1995/09/15 15:19:53 $\r
-% $Revision: 1.3 $\r
-%\r
-\r
-@Article{ex1,\r
- author = "Author, Ivan Marc",\r
- title = "Some Related Article {I} Wrote", \r
- journal = "Some Fine Journal",\r
- month = "January",\r
- number = "7",\r
- year = "1999",\r
- volume = "99",\r
- pages = "1-100",\r
-}\r
-\r
-\r
-@Book{ex2,\r
- author = "Expert, Andreas Nikolaos", \r
- title = "A Book He Wrote", \r
- publisher = "His Publisher",\r
- address = "Erewhon, NC",\r
- year = "1999"\r
-}\r
-\r
+++ /dev/null
-\r
-% ---------------------------------------------------------------\r
-%\r
-% $Id: latex8.bst,v 1.1 1995/09/15 15:13:49 ienne Exp $\r
-%\r
-% by Paolo.Ienne@di.epfl.ch\r
-%\r
-\r
-% ---------------------------------------------------------------\r
-%\r
-% no guarantee is given that the format corresponds perfectly to \r
-% IEEE 8.5" x 11" Proceedings, but most features should be ok.\r
-%\r
-% ---------------------------------------------------------------\r
-%\r
-% `latex8' from BibTeX standard bibliography style `abbrv'\r
-% version 0.99a for BibTeX versions 0.99a or later, LaTeX version 2.09.\r
-% Copyright (C) 1985, all rights reserved.\r
-% Copying of this file is authorized only if either\r
-% (1) you make absolutely no changes to your copy, including name, or\r
-% (2) if you do make changes, you name it something other than\r
-% btxbst.doc, plain.bst, unsrt.bst, alpha.bst, and abbrv.bst.\r
-% This restriction helps ensure that all standard styles are identical.\r
-% The file btxbst.doc has the documentation for this style.\r
-\r
-ENTRY\r
- { address\r
- author\r
- booktitle\r
- chapter\r
- edition\r
- editor\r
- howpublished\r
- institution\r
- journal\r
- key\r
- month\r
- note\r
- number\r
- organization\r
- pages\r
- publisher\r
- school\r
- series\r
- title\r
- type\r
- volume\r
- year\r
- }\r
- {}\r
- { label }\r
-\r
-INTEGERS { output.state before.all mid.sentence after.sentence after.block }\r
-\r
-FUNCTION {init.state.consts}\r
-{ #0 'before.all :=\r
- #1 'mid.sentence :=\r
- #2 'after.sentence :=\r
- #3 'after.block :=\r
-}\r
-\r
-STRINGS { s t }\r
-\r
-FUNCTION {output.nonnull}\r
-{ 's :=\r
- output.state mid.sentence =\r
- { ", " * write$ }\r
- { output.state after.block =\r
- { add.period$ write$\r
- newline$\r
- "\newblock " write$\r
- }\r
- { output.state before.all =\r
- 'write$\r
- { add.period$ " " * write$ }\r
- if$\r
- }\r
- if$\r
- mid.sentence 'output.state :=\r
- }\r
- if$\r
- s\r
-}\r
-\r
-FUNCTION {output}\r
-{ duplicate$ empty$\r
- 'pop$\r
- 'output.nonnull\r
- if$\r
-}\r
-\r
-FUNCTION {output.check}\r
-{ 't :=\r
- duplicate$ empty$\r
- { pop$ "empty " t * " in " * cite$ * warning$ }\r
- 'output.nonnull\r
- if$\r
-}\r
-\r
-FUNCTION {output.bibitem}\r
-{ newline$\r
- "\bibitem{" write$\r
- cite$ write$\r
- "}" write$\r
- newline$\r
- ""\r
- before.all 'output.state :=\r
-}\r
-\r
-FUNCTION {fin.entry}\r
-{ add.period$\r
- write$\r
- newline$\r
-}\r
-\r
-FUNCTION {new.block}\r
-{ output.state before.all =\r
- 'skip$\r
- { after.block 'output.state := }\r
- if$\r
-}\r
-\r
-FUNCTION {new.sentence}\r
-{ output.state after.block =\r
- 'skip$\r
- { output.state before.all =\r
- 'skip$\r
- { after.sentence 'output.state := }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {not}\r
-{ { #0 }\r
- { #1 }\r
- if$\r
-}\r
-\r
-FUNCTION {and}\r
-{ 'skip$\r
- { pop$ #0 }\r
- if$\r
-}\r
-\r
-FUNCTION {or}\r
-{ { pop$ #1 }\r
- 'skip$\r
- if$\r
-}\r
-\r
-FUNCTION {new.block.checka}\r
-{ empty$\r
- 'skip$\r
- 'new.block\r
- if$\r
-}\r
-\r
-FUNCTION {new.block.checkb}\r
-{ empty$\r
- swap$ empty$\r
- and\r
- 'skip$\r
- 'new.block\r
- if$\r
-}\r
-\r
-FUNCTION {new.sentence.checka}\r
-{ empty$\r
- 'skip$\r
- 'new.sentence\r
- if$\r
-}\r
-\r
-FUNCTION {new.sentence.checkb}\r
-{ empty$\r
- swap$ empty$\r
- and\r
- 'skip$\r
- 'new.sentence\r
- if$\r
-}\r
-\r
-FUNCTION {field.or.null}\r
-{ duplicate$ empty$\r
- { pop$ "" }\r
- 'skip$\r
- if$\r
-}\r
-\r
-FUNCTION {emphasize}\r
-{ duplicate$ empty$\r
- { pop$ "" }\r
- { "{\em " swap$ * "}" * }\r
- if$\r
-}\r
-\r
-INTEGERS { nameptr namesleft numnames }\r
-\r
-FUNCTION {format.names}\r
-{ 's :=\r
- #1 'nameptr :=\r
- s num.names$ 'numnames :=\r
- numnames 'namesleft :=\r
- { namesleft #0 > }\r
- { s nameptr "{f.~}{vv~}{ll}{, jj}" format.name$ 't :=\r
- nameptr #1 >\r
- { namesleft #1 >\r
- { ", " * t * }\r
- { numnames #2 >\r
- { "," * }\r
- 'skip$\r
- if$\r
- t "others" =\r
- { " et~al." * }\r
- { " and " * t * }\r
- if$\r
- }\r
- if$\r
- }\r
- 't\r
- if$\r
- nameptr #1 + 'nameptr :=\r
-\r
- namesleft #1 - 'namesleft :=\r
- }\r
- while$\r
-}\r
-\r
-FUNCTION {format.authors}\r
-{ author empty$\r
- { "" }\r
- { author format.names }\r
- if$\r
-}\r
-\r
-FUNCTION {format.editors}\r
-{ editor empty$\r
- { "" }\r
- { editor format.names\r
- editor num.names$ #1 >\r
- { ", editors" * }\r
- { ", editor" * }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.title}\r
-{ title empty$\r
- { "" }\r
- { title "t" change.case$ }\r
- if$\r
-}\r
-\r
-FUNCTION {n.dashify}\r
-{ 't :=\r
- ""\r
- { t empty$ not }\r
- { t #1 #1 substring$ "-" =\r
- { t #1 #2 substring$ "--" = not\r
- { "--" *\r
- t #2 global.max$ substring$ 't :=\r
- }\r
- { { t #1 #1 substring$ "-" = }\r
- { "-" *\r
- t #2 global.max$ substring$ 't :=\r
- }\r
- while$\r
- }\r
- if$\r
- }\r
- { t #1 #1 substring$ *\r
- t #2 global.max$ substring$ 't :=\r
- }\r
- if$\r
- }\r
- while$\r
-}\r
-\r
-FUNCTION {format.date}\r
-{ year empty$\r
- { month empty$\r
- { "" }\r
- { "there's a month but no year in " cite$ * warning$\r
- month\r
- }\r
- if$\r
- }\r
- { month empty$\r
- 'year\r
- { month " " * year * }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.btitle}\r
-{ title emphasize\r
-}\r
-\r
-FUNCTION {tie.or.space.connect}\r
-{ duplicate$ text.length$ #3 <\r
- { "~" }\r
- { " " }\r
- if$\r
- swap$ * *\r
-}\r
-\r
-FUNCTION {either.or.check}\r
-{ empty$\r
- 'pop$\r
- { "can't use both " swap$ * " fields in " * cite$ * warning$ }\r
- if$\r
-}\r
-\r
-FUNCTION {format.bvolume}\r
-{ volume empty$\r
- { "" }\r
- { "volume" volume tie.or.space.connect\r
- series empty$\r
- 'skip$\r
- { " of " * series emphasize * }\r
- if$\r
- "volume and number" number either.or.check\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.number.series}\r
-{ volume empty$\r
- { number empty$\r
- { series field.or.null }\r
- { output.state mid.sentence =\r
- { "number" }\r
- { "Number" }\r
- if$\r
- number tie.or.space.connect\r
- series empty$\r
- { "there's a number but no series in " cite$ * warning$ }\r
- { " in " * series * }\r
- if$\r
- }\r
- if$\r
- }\r
- { "" }\r
- if$\r
-}\r
-\r
-FUNCTION {format.edition}\r
-{ edition empty$\r
- { "" }\r
- { output.state mid.sentence =\r
- { edition "l" change.case$ " edition" * }\r
- { edition "t" change.case$ " edition" * }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-INTEGERS { multiresult }\r
-\r
-FUNCTION {multi.page.check}\r
-{ 't :=\r
- #0 'multiresult :=\r
- { multiresult not\r
- t empty$ not\r
- and\r
- }\r
- { t #1 #1 substring$\r
- duplicate$ "-" =\r
- swap$ duplicate$ "," =\r
- swap$ "+" =\r
- or or\r
- { #1 'multiresult := }\r
- { t #2 global.max$ substring$ 't := }\r
- if$\r
- }\r
- while$\r
- multiresult\r
-}\r
-\r
-FUNCTION {format.pages}\r
-{ pages empty$\r
- { "" }\r
- { pages multi.page.check\r
- { "pages" pages n.dashify tie.or.space.connect }\r
- { "page" pages tie.or.space.connect }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.vol.num.pages}\r
-{ volume field.or.null\r
- number empty$\r
- 'skip$\r
- { "(" number * ")" * *\r
- volume empty$\r
- { "there's a number but no volume in " cite$ * warning$ }\r
- 'skip$\r
- if$\r
- }\r
- if$\r
- pages empty$\r
- 'skip$\r
- { duplicate$ empty$\r
- { pop$ format.pages }\r
- { ":" * pages n.dashify * }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.chapter.pages}\r
-{ chapter empty$\r
- 'format.pages\r
- { type empty$\r
- { "chapter" }\r
- { type "l" change.case$ }\r
- if$\r
- chapter tie.or.space.connect\r
- pages empty$\r
- 'skip$\r
- { ", " * format.pages * }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.in.ed.booktitle}\r
-{ booktitle empty$\r
- { "" }\r
- { editor empty$\r
- { "In " booktitle emphasize * }\r
- { "In " format.editors * ", " * booktitle emphasize * }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {empty.misc.check}\r
-\r
-{ author empty$ title empty$ howpublished empty$\r
- month empty$ year empty$ note empty$\r
- and and and and and\r
- key empty$ not and\r
- { "all relevant fields are empty in " cite$ * warning$ }\r
- 'skip$\r
- if$\r
-}\r
-\r
-FUNCTION {format.thesis.type}\r
-{ type empty$\r
- 'skip$\r
- { pop$\r
- type "t" change.case$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.tr.number}\r
-{ type empty$\r
- { "Technical Report" }\r
- 'type\r
- if$\r
- number empty$\r
- { "t" change.case$ }\r
- { number tie.or.space.connect }\r
- if$\r
-}\r
-\r
-FUNCTION {format.article.crossref}\r
-{ key empty$\r
- { journal empty$\r
- { "need key or journal for " cite$ * " to crossref " * crossref *\r
- warning$\r
- ""\r
- }\r
- { "In {\em " journal * "\/}" * }\r
- if$\r
- }\r
- { "In " key * }\r
- if$\r
- " \cite{" * crossref * "}" *\r
-}\r
-\r
-FUNCTION {format.crossref.editor}\r
-{ editor #1 "{vv~}{ll}" format.name$\r
- editor num.names$ duplicate$\r
- #2 >\r
- { pop$ " et~al." * }\r
- { #2 <\r
- 'skip$\r
- { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =\r
- { " et~al." * }\r
- { " and " * editor #2 "{vv~}{ll}" format.name$ * }\r
- if$\r
- }\r
- if$\r
- }\r
- if$\r
-}\r
-\r
-FUNCTION {format.book.crossref}\r
-{ volume empty$\r
- { "empty volume in " cite$ * "'s crossref of " * crossref * warning$\r
- "In "\r
- }\r
- { "Volume" volume tie.or.space.connect\r
- " of " *\r
- }\r
- if$\r
- editor empty$\r
- editor field.or.null author field.or.null =\r
- or\r
- { key empty$\r
- { series empty$\r
- { "need editor, key, or series for " cite$ * " to crossref " *\r
- crossref * warning$\r
- "" *\r
- }\r
- { "{\em " * series * "\/}" * }\r
- if$\r
- }\r
- { key * }\r
- if$\r
- }\r
- { format.crossref.editor * }\r
- if$\r
- " \cite{" * crossref * "}" *\r
-}\r
-\r
-FUNCTION {format.incoll.inproc.crossref}\r
-{ editor empty$\r
- editor field.or.null author field.or.null =\r
- or\r
- { key empty$\r
- { booktitle empty$\r
- { "need editor, key, or booktitle for " cite$ * " to crossref " *\r
- crossref * warning$\r
- ""\r
- }\r
- { "In {\em " booktitle * "\/}" * }\r
- if$\r
- }\r
- { "In " key * }\r
- if$\r
- }\r
- { "In " format.crossref.editor * }\r
- if$\r
- " \cite{" * crossref * "}" *\r
-}\r
-\r
-FUNCTION {article}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.title "title" output.check\r
- new.block\r
- crossref missing$\r
- { journal emphasize "journal" output.check\r
- format.vol.num.pages output\r
- format.date "year" output.check\r
- }\r
- { format.article.crossref output.nonnull\r
- format.pages output\r
- }\r
- if$\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {book}\r
-{ output.bibitem\r
- author empty$\r
- { format.editors "author and editor" output.check }\r
- { format.authors output.nonnull\r
- crossref missing$\r
- { "author and editor" editor either.or.check }\r
- 'skip$\r
- if$\r
- }\r
- if$\r
- new.block\r
- format.btitle "title" output.check\r
- crossref missing$\r
- { format.bvolume output\r
- new.block\r
- format.number.series output\r
- new.sentence\r
- publisher "publisher" output.check\r
- address output\r
- }\r
- { new.block\r
- format.book.crossref output.nonnull\r
- }\r
- if$\r
- format.edition output\r
- format.date "year" output.check\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {booklet}\r
-{ output.bibitem\r
- format.authors output\r
- new.block\r
- format.title "title" output.check\r
- howpublished address new.block.checkb\r
- howpublished output\r
- address output\r
- format.date output\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {inbook}\r
-{ output.bibitem\r
- author empty$\r
- { format.editors "author and editor" output.check }\r
- { format.authors output.nonnull\r
-\r
- crossref missing$\r
- { "author and editor" editor either.or.check }\r
- 'skip$\r
- if$\r
- }\r
- if$\r
- new.block\r
- format.btitle "title" output.check\r
- crossref missing$\r
- { format.bvolume output\r
- format.chapter.pages "chapter and pages" output.check\r
- new.block\r
- format.number.series output\r
- new.sentence\r
- publisher "publisher" output.check\r
- address output\r
- }\r
- { format.chapter.pages "chapter and pages" output.check\r
- new.block\r
- format.book.crossref output.nonnull\r
- }\r
- if$\r
- format.edition output\r
- format.date "year" output.check\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {incollection}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.title "title" output.check\r
- new.block\r
- crossref missing$\r
- { format.in.ed.booktitle "booktitle" output.check\r
- format.bvolume output\r
- format.number.series output\r
- format.chapter.pages output\r
- new.sentence\r
- publisher "publisher" output.check\r
- address output\r
- format.edition output\r
- format.date "year" output.check\r
- }\r
- { format.incoll.inproc.crossref output.nonnull\r
- format.chapter.pages output\r
- }\r
- if$\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {inproceedings}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.title "title" output.check\r
- new.block\r
- crossref missing$\r
- { format.in.ed.booktitle "booktitle" output.check\r
- format.bvolume output\r
- format.number.series output\r
- format.pages output\r
- address empty$\r
- { organization publisher new.sentence.checkb\r
- organization output\r
- publisher output\r
- format.date "year" output.check\r
- }\r
- { address output.nonnull\r
- format.date "year" output.check\r
- new.sentence\r
- organization output\r
- publisher output\r
- }\r
- if$\r
- }\r
- { format.incoll.inproc.crossref output.nonnull\r
- format.pages output\r
- }\r
- if$\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {conference} { inproceedings }\r
-\r
-FUNCTION {manual}\r
-{ output.bibitem\r
- author empty$\r
- { organization empty$\r
- 'skip$\r
- { organization output.nonnull\r
- address output\r
- }\r
- if$\r
- }\r
- { format.authors output.nonnull }\r
- if$\r
- new.block\r
- format.btitle "title" output.check\r
- author empty$\r
- { organization empty$\r
- { address new.block.checka\r
- address output\r
- }\r
- 'skip$\r
- if$\r
- }\r
- { organization address new.block.checkb\r
- organization output\r
- address output\r
- }\r
- if$\r
- format.edition output\r
- format.date output\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {mastersthesis}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.title "title" output.check\r
- new.block\r
- "Master's thesis" format.thesis.type output.nonnull\r
- school "school" output.check\r
- address output\r
- format.date "year" output.check\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {misc}\r
-{ output.bibitem\r
- format.authors output\r
- title howpublished new.block.checkb\r
- format.title output\r
- howpublished new.block.checka\r
- howpublished output\r
- format.date output\r
- new.block\r
- note output\r
- fin.entry\r
- empty.misc.check\r
-}\r
-\r
-FUNCTION {phdthesis}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.btitle "title" output.check\r
- new.block\r
- "PhD thesis" format.thesis.type output.nonnull\r
- school "school" output.check\r
- address output\r
- format.date "year" output.check\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {proceedings}\r
-{ output.bibitem\r
- editor empty$\r
- { organization output }\r
- { format.editors output.nonnull }\r
-\r
- if$\r
- new.block\r
- format.btitle "title" output.check\r
- format.bvolume output\r
- format.number.series output\r
- address empty$\r
- { editor empty$\r
- { publisher new.sentence.checka }\r
- { organization publisher new.sentence.checkb\r
- organization output\r
- }\r
- if$\r
- publisher output\r
- format.date "year" output.check\r
- }\r
- { address output.nonnull\r
- format.date "year" output.check\r
- new.sentence\r
- editor empty$\r
- 'skip$\r
- { organization output }\r
- if$\r
- publisher output\r
- }\r
- if$\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {techreport}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.title "title" output.check\r
- new.block\r
- format.tr.number output.nonnull\r
- institution "institution" output.check\r
- address output\r
- format.date "year" output.check\r
- new.block\r
- note output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {unpublished}\r
-{ output.bibitem\r
- format.authors "author" output.check\r
- new.block\r
- format.title "title" output.check\r
- new.block\r
- note "note" output.check\r
- format.date output\r
- fin.entry\r
-}\r
-\r
-FUNCTION {default.type} { misc }\r
-\r
-MACRO {jan} {"Jan."}\r
-\r
-MACRO {feb} {"Feb."}\r
-\r
-MACRO {mar} {"Mar."}\r
-\r
-MACRO {apr} {"Apr."}\r
-\r
-MACRO {may} {"May"}\r
-\r
-MACRO {jun} {"June"}\r
-\r
-MACRO {jul} {"July"}\r
-\r
-MACRO {aug} {"Aug."}\r
-\r
-MACRO {sep} {"Sept."}\r
-\r
-MACRO {oct} {"Oct."}\r
-\r
-MACRO {nov} {"Nov."}\r
-\r
-MACRO {dec} {"Dec."}\r
-\r
-MACRO {acmcs} {"ACM Comput. Surv."}\r
-\r
-MACRO {acta} {"Acta Inf."}\r
-\r
-MACRO {cacm} {"Commun. ACM"}\r
-\r
-MACRO {ibmjrd} {"IBM J. Res. Dev."}\r
-\r
-MACRO {ibmsj} {"IBM Syst.~J."}\r
-\r
-MACRO {ieeese} {"IEEE Trans. Softw. Eng."}\r
-\r
-MACRO {ieeetc} {"IEEE Trans. Comput."}\r
-\r
-MACRO {ieeetcad}\r
- {"IEEE Trans. Comput.-Aided Design Integrated Circuits"}\r
-\r
-MACRO {ipl} {"Inf. Process. Lett."}\r
-\r
-MACRO {jacm} {"J.~ACM"}\r
-\r
-MACRO {jcss} {"J.~Comput. Syst. Sci."}\r
-\r
-MACRO {scp} {"Sci. Comput. Programming"}\r
-\r
-MACRO {sicomp} {"SIAM J. Comput."}\r
-\r
-MACRO {tocs} {"ACM Trans. Comput. Syst."}\r
-\r
-MACRO {tods} {"ACM Trans. Database Syst."}\r
-\r
-MACRO {tog} {"ACM Trans. Gr."}\r
-\r
-MACRO {toms} {"ACM Trans. Math. Softw."}\r
-\r
-MACRO {toois} {"ACM Trans. Office Inf. Syst."}\r
-\r
-MACRO {toplas} {"ACM Trans. Prog. Lang. Syst."}\r
-\r
-MACRO {tcs} {"Theoretical Comput. Sci."}\r
-\r
-READ\r
-\r
-FUNCTION {sortify}\r
-{ purify$\r
- "l" change.case$\r
-}\r
-\r
-INTEGERS { len }\r
-\r
-FUNCTION {chop.word}\r
-{ 's :=\r
- 'len :=\r
- s #1 len substring$ =\r
- { s len #1 + global.max$ substring$ }\r
- 's\r
- if$\r
-}\r
-\r
-FUNCTION {sort.format.names}\r
-{ 's :=\r
- #1 'nameptr :=\r
- ""\r
- s num.names$ 'numnames :=\r
- numnames 'namesleft :=\r
- { namesleft #0 > }\r
- { nameptr #1 >\r
- { " " * }\r
- 'skip$\r
- if$\r
- s nameptr "{vv{ } }{ll{ }}{ f{ }}{ jj{ }}" format.name$ 't :=\r
- nameptr numnames = t "others" = and\r
- { "et al" * }\r
- { t sortify * }\r
- if$\r
- nameptr #1 + 'nameptr :=\r
- namesleft #1 - 'namesleft :=\r
- }\r
- while$\r
-}\r
-\r
-FUNCTION {sort.format.title}\r
-{ 't :=\r
- "A " #2\r
- "An " #3\r
- "The " #4 t chop.word\r
- chop.word\r
- chop.word\r
- sortify\r
- #1 global.max$ substring$\r
-}\r
-\r
-FUNCTION {author.sort}\r
-{ author empty$\r
- { key empty$\r
- { "to sort, need author or key in " cite$ * warning$\r
- ""\r
- }\r
- { key sortify }\r
- if$\r
- }\r
- { author sort.format.names }\r
- if$\r
-}\r
-\r
-FUNCTION {author.editor.sort}\r
-{ author empty$\r
- { editor empty$\r
- { key empty$\r
- { "to sort, need author, editor, or key in " cite$ * warning$\r
- ""\r
- }\r
- { key sortify }\r
- if$\r
- }\r
- { editor sort.format.names }\r
- if$\r
- }\r
- { author sort.format.names }\r
- if$\r
-}\r
-\r
-FUNCTION {author.organization.sort}\r
-{ author empty$\r
-\r
- { organization empty$\r
- { key empty$\r
- { "to sort, need author, organization, or key in " cite$ * warning$\r
- ""\r
- }\r
- { key sortify }\r
- if$\r
- }\r
- { "The " #4 organization chop.word sortify }\r
- if$\r
- }\r
- { author sort.format.names }\r
- if$\r
-}\r
-\r
-FUNCTION {editor.organization.sort}\r
-{ editor empty$\r
- { organization empty$\r
- { key empty$\r
- { "to sort, need editor, organization, or key in " cite$ * warning$\r
- ""\r
- }\r
- { key sortify }\r
- if$\r
- }\r
- { "The " #4 organization chop.word sortify }\r
- if$\r
- }\r
- { editor sort.format.names }\r
- if$\r
-}\r
-\r
-FUNCTION {presort}\r
-{ type$ "book" =\r
- type$ "inbook" =\r
- or\r
- 'author.editor.sort\r
- { type$ "proceedings" =\r
- 'editor.organization.sort\r
- { type$ "manual" =\r
- 'author.organization.sort\r
- 'author.sort\r
- if$\r
- }\r
- if$\r
- }\r
- if$\r
- " "\r
- *\r
- year field.or.null sortify\r
- *\r
- " "\r
- *\r
- title field.or.null\r
- sort.format.title\r
- *\r
- #1 entry.max$ substring$\r
- 'sort.key$ :=\r
-}\r
-\r
-ITERATE {presort}\r
-\r
-SORT\r
-\r
-STRINGS { longest.label }\r
-\r
-INTEGERS { number.label longest.label.width }\r
-\r
-FUNCTION {initialize.longest.label}\r
-{ "" 'longest.label :=\r
- #1 'number.label :=\r
- #0 'longest.label.width :=\r
-}\r
-\r
-FUNCTION {longest.label.pass}\r
-{ number.label int.to.str$ 'label :=\r
- number.label #1 + 'number.label :=\r
- label width$ longest.label.width >\r
- { label 'longest.label :=\r
- label width$ 'longest.label.width :=\r
- }\r
- 'skip$\r
- if$\r
-}\r
-\r
-EXECUTE {initialize.longest.label}\r
-\r
-ITERATE {longest.label.pass}\r
-\r
-FUNCTION {begin.bib}\r
-{ preamble$ empty$\r
- 'skip$\r
- { preamble$ write$ newline$ }\r
- if$\r
- "\begin{thebibliography}{" longest.label * \r
- "}\setlength{\itemsep}{-1ex}\small" * write$ newline$\r
-}\r
-\r
-EXECUTE {begin.bib}\r
-\r
-EXECUTE {init.state.consts}\r
-\r
-ITERATE {call.type$}\r
-\r
-FUNCTION {end.bib}\r
-{ newline$\r
- "\end{thebibliography}" write$ newline$\r
-}\r
-\r
-EXECUTE {end.bib}\r
-\r
-% end of file latex8.bst\r
-% ---------------------------------------------------------------\r
-\r
-\r
-\r
+++ /dev/null
-\r
-% --------------------------------------------------------------- \r
-%\r
-% $Id: latex8.sty,v 1.2 1995/09/15 15:31:13 ienne Exp $\r
-% \r
-% by Paolo.Ienne@di.epfl.ch \r
-%\r
-% --------------------------------------------------------------- \r
-%\r
-% no guarantee is given that the format corresponds perfectly to \r
-% IEEE 8.5" x 11" Proceedings, but most features should be ok.\r
-%\r
-% --------------------------------------------------------------- \r
-% with LaTeX2e:\r
-% =============\r
-%\r
-% use as \r
-% \documentclass[times,10pt,twocolumn]{article} \r
-% \usepackage{latex8}\r
-% \usepackage{times}\r
-%\r
-% --------------------------------------------------------------- \r
-\r
-% with LaTeX 2.09:\r
-% ================\r
-%\r
-% use as \r
-% \documentstyle[times,art10,twocolumn,latex8]{article}\r
-%\r
-% --------------------------------------------------------------- \r
-% with both versions:\r
-% ===================\r
-%\r
-% specify \pagestyle{empty} to omit page numbers in the final \r
-% version\r
-%\r
-% specify references as\r
-% \bibliographystyle{latex8}\r
-% \bibliography{...your files...}\r
-%\r
-% use Section{} and SubSection{} instead of standard section{} \r
-% and subsection{} to obtain headings in the form \r
-% "1.3. My heading"\r
-%\r
-% ---------------------------------------------------------------\r
-\r
-\typeout{IEEE 8.5 x 11-Inch Proceedings Style `latex8.sty'.}\r
-\r
-% ten point helvetica bold required for captions\r
-% in some sites the name of the helvetica bold font may differ, \r
-% change the name here:\r
-\font\tenhv = phvb at 10pt\r
-%\font\tenhv = phvb7t at 10pt\r
-\r
-% eleven point times bold required for second-order headings \r
-% \font\elvbf = cmbx10 scaled 1100\r
-\font\elvbf = ptmb scaled 1100\r
-\r
-% set dimensions of columns, gap between columns, and paragraph indent \r
-\setlength{\textheight}{8.875in}\r
-\setlength{\textwidth}{6.875in}\r
-\setlength{\columnsep}{0.3125in}\r
-\setlength{\topmargin}{0in}\r
-\setlength{\headheight}{0in}\r
-\setlength{\headsep}{0in}\r
-\setlength{\parindent}{1pc}\r
-\setlength{\oddsidemargin}{-.304in}\r
-\setlength{\evensidemargin}{-.304in}\r
-\r
-% memento from size10.clo\r
-% \normalsize{\@setfontsize\normalsize\@xpt\@xiipt} \r
-% \small{\@setfontsize\small\@ixpt{11}}\r
-% \footnotesize{\@setfontsize\footnotesize\@viiipt{9.5}} \r
-% \scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt}\r
-% \tiny{\@setfontsize\tiny\@vpt\@vipt}\r
-% \large{\@setfontsize\large\@xiipt{14}} \r
-% \Large{\@setfontsize\Large\@xivpt{18}} \r
-% \LARGE{\@setfontsize\LARGE\@xviipt{22}} \r
-% \huge{\@setfontsize\huge\@xxpt{25}}\r
-% \Huge{\@setfontsize\Huge\@xxvpt{30}}\r
-\r
-\def\@maketitle\r
- {\r
- \newpage\r
- \null\r
- \vskip .375in \r
- \begin{center}\r
- {\Large \bf \@title \par} \r
- % additional two empty lines at the end of the title \r
- \vspace*{24pt} \r
- {\r
- \large \r
- \lineskip .5em\r
- \begin{tabular}[t]{c}\r
- \@author \r
- \end{tabular}\r
- \par\r
- } \r
- % additional small space at the end of the author name \r
- \vskip .5em \r
- {\r
- \large \r
- \begin{tabular}[t]{c}\r
- \@affiliation \r
- \end{tabular}\r
- \par \r
- \ifx \@empty \@email\r
- \else\r
- \begin{tabular}{r@{~}l}\r
- E-mail: & {\tt \@email}\r
- \end{tabular}\r
- \par\r
- \fi\r
- }\r
- % additional empty line at the end of the title block \r
- \vspace*{12pt} \r
- \end{center}\r
- } \r
-\r
-\def\abstract\r
- {%\r
- \centerline{\large\bf Abstract}%\r
- \vspace*{12pt}%\r
- \it%\r
- }\r
-\r
-\def\endabstract\r
- {\r
- % additional empty line at the end of the abstract \r
- \vspace*{12pt} \r
- }\r
-\r
-\def\affiliation#1{\gdef\@affiliation{#1}} \gdef\@affiliation{}\r
-\r
-\def\email#1{\gdef\@email{#1}}\r
-\gdef\@email{}\r
-\r
-\newlength{\@ctmp}\r
-\newlength{\@figindent}\r
-\setlength{\@figindent}{1pc}\r
-\r
-\long\def\@makecaption#1#2{\r
- \vskip 10pt\r
- \setbox\@tempboxa\hbox{\tenhv\noindent #1.~#2} \r
- \setlength{\@ctmp}{\hsize}\r
- \addtolength{\@ctmp}{-\@figindent}\addtolength{\@ctmp}{-\@figindent} \r
- % IF longer than one indented paragraph line\r
- \ifdim \wd\@tempboxa >\@ctmp\r
- % THEN set as an indented paragraph\r
- \begin{list}{}{\leftmargin\@figindent \rightmargin\leftmargin} \r
- \item[]\tenhv #1.~#2\par\r
- \end{list}\r
- \else\r
- % ELSE center\r
- \hbox to\hsize{\hfil\box\@tempboxa\hfil} \r
- \fi}\r
-\r
-% correct heading spacing and type\r
-\def\section{\@startsection {section}{1}{\z@}\r
- {14pt plus 2pt minus 2pt}{14pt plus 2pt minus 2pt} {\large\bf}} \r
-\def\subsection{\@startsection {subsection}{2}{\z@}\r
- {13pt plus 2pt minus 2pt}{13pt plus 2pt minus 2pt} {\elvbf}}\r
-\r
-% add the period after section numbers \r
-\newcommand{\Section}[1]{\section{\hskip -1em.~#1}} \r
-\newcommand{\SubSection}[1]{\subsection{\hskip -1em.~#1}}\r
-\r
-% end of file latex8.sty\r
-% ---------------------------------------------------------------\r
+++ /dev/null
-\r
-%\r
-% $Description: Author guidelines and sample document in LaTeX 2.09$ \r
-%\r
-% $Author: ienne $\r
-% $Date: 1995/09/15 15:20:59 $\r
-% $Revision: 1.4 $\r
-%\r
-\r
-\documentclass[times, 10pt,twocolumn]{article} \r
-\usepackage{latex8}\r
-\usepackage{times}\r
-\r
-%\documentstyle[times,art10,twocolumn,latex8]{article}\r
-\r
-%------------------------------------------------------------------------- \r
-% take the % away on next line to produce the final camera-ready version \r
-\pagestyle{empty}\r
-\r
-%------------------------------------------------------------------------- \r
-\begin{document}\r
-\r
-\title{\LaTeX\ Author Guidelines \r
- for {\boldmath $8.5 \times 11$-Inch} Proceedings Manuscripts}\r
-\r
-\author{Paolo Ienne\\\r
-Swiss Federal Institute of Technology\\ Microcomputing Laboratory \\ IN-F \r
-Ecublens, 1015 Lausanne, Switzerland\\ Paolo.Ienne@di.epfl.ch\\\r
-% For a paper whose authors are all at the same institution, \r
-% omit the following lines up until the closing ``}''.\r
-% Additional authors and addresses can be added with ``\and'', \r
-% just like the second author.\r
-\and\r
-Second Author\\\r
-Institution2\\\r
-First line of institution2 address\\ Second line of institution2 address\\ \r
-SecondAuthor@institution2.com\\\r
-}\r
-\r
-\maketitle\r
-\thispagestyle{empty}\r
-\r
-\begin{abstract}\r
- The ABSTRACT is to be in fully-justified italicized text, at the top \r
- of the left-hand column, below the author and affiliation \r
- information. Use the word ``Abstract'' as the title, in 12-point \r
- Times, boldface type, centered relative to the column, initially \r
- capitalized. The abstract is to be in 10-point, single-spaced type. \r
- The abstract may be up to 3 inches (7.62 cm) long. Leave two blank \r
- lines after the Abstract, then begin the main text. \r
-\end{abstract}\r
-\r
-\r
-\r
-%------------------------------------------------------------------------- \r
-\Section{Introduction}\r
-\r
-Please follow the steps outlined below when submitting your \r
-manuscript to the IEEE Computer Society Press. Note there have \r
-been some changes to the measurements from previous instructions. \r
-\r
-%------------------------------------------------------------------------- \r
-\Section{Instructions}\r
-\r
-Please read the following carefully.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Language}\r
-\r
-All manuscripts must be in English.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Printing your paper}\r
-\r
-Print your properly formatted text on high-quality, $8.5 \times 11$-inch \r
-white printer paper. A4 paper is also acceptable, but please leave the \r
-extra 0.5 inch (1.27 cm) at the BOTTOM of the page.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Margins and page numbering}\r
-\r
-All printed material, including text, illustrations, and charts, must be \r
-kept within a print area 6-7/8 inches (17.5 cm) wide by 8-7/8 inches \r
-(22.54 cm) high. Do not write or print anything outside the print area. \r
-Number your pages lightly, in pencil, on the upper right-hand corners of \r
-the BACKS of the pages (for example, 1/10, 2/10, or 1 of 10, 2 of 10, and \r
-so forth). Please do not write on the fronts of the pages, nor on the \r
-lower halves of the backs of the pages.\r
-\r
-\r
-%------------------------------------------------------------------------ \r
-\SubSection{Formatting your paper}\r
-\r
-All text must be in a two-column format. The total allowable width of \r
-the text area is 6-7/8 inches (17.5 cm) wide by 8-7/8 inches (22.54 cm) \r
-high. Columns are to be 3-1/4 inches (8.25 cm) wide, with a 5/16 inch \r
-(0.8 cm) space between them. The main title (on the first page) should \r
-begin 1.0 inch (2.54 cm) from the top edge of the page. The second and \r
-following pages should begin 1.0 inch (2.54 cm) from the top edge. On \r
-all pages, the bottom margin should be 1-1/8 inches (2.86 cm) from the \r
-bottom edge of the page for $8.5 \times 11$-inch paper; for A4 paper, \r
-approximately 1-5/8 inches (4.13 cm) from the bottom edge of the page.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Type-style and fonts}\r
-\r
-Wherever Times is specified, Times Roman may also be used. If neither is \r
-available on your word processor, please use the font closest in \r
-appearance to Times that you have access to.\r
-\r
-MAIN TITLE. Center the title 1-3/8 inches (3.49 cm) from the top edge of \r
-the first page. The title should be in Times 14-point, boldface type. \r
-Capitalize the first letter of nouns, pronouns, verbs, adjectives, and \r
-adverbs; do not capitalize articles, coordinate conjunctions, or \r
-prepositions (unless the title begins with such a word). Leave two blank \r
-lines after the title.\r
-\r
-AUTHOR NAME(s) and AFFILIATION(s) are to be centered beneath the title \r
-and printed in Times 12-point, non-boldface type. This information is to \r
-be followed by two blank lines.\r
-\r
-The ABSTRACT and MAIN TEXT are to be in a two-column format. \r
-\r
-MAIN TEXT. Type main text in 10-point Times, single-spaced. Do NOT use \r
-double-spacing. All paragraphs should be indented 1 pica (approx. 1/6 \r
-inch or 0.422 cm). Make sure your text is fully justified---that is, \r
-flush left and flush right. Please do not place any additional blank \r
-lines between paragraphs. Figure and table captions should be 10-point \r
-Helvetica boldface type as in\r
-\begin{figure}[h]\r
- \caption{Example of caption.}\r
-\end{figure}\r
-\r
-\noindent Long captions should be set as in \r
-\begin{figure}[h] \r
- \caption{Example of long caption requiring more than one line. It is \r
- not typed centered but aligned on both sides and indented with an \r
- additional margin on both sides of 1~pica.}\r
-\end{figure}\r
-\r
-\noindent Callouts should be 9-point Helvetica, non-boldface type. \r
-Initially capitalize only the first word of section titles and first-, \r
-second-, and third-order headings.\r
-\r
-FIRST-ORDER HEADINGS. (For example, {\large \bf 1. Introduction}) \r
-should be Times 12-point boldface, initially capitalized, flush left, \r
-with one blank line before, and one blank line after.\r
-\r
-SECOND-ORDER HEADINGS. (For example, {\elvbf 1.1. Database elements}) \r
-should be Times 11-point boldface, initially capitalized, flush left, \r
-with one blank line before, and one after. If you require a third-order \r
-heading (we discourage it), use 10-point Times, boldface, initially \r
-capitalized, flush left, preceded by one blank line, followed by a period \r
-and your text on the same line.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Footnotes}\r
-\r
-Please use footnotes sparingly%\r
-\footnote\r
- {%\r
- Or, better still, try to avoid footnotes altogether. To help your \r
- readers, avoid using footnotes altogether and include necessary \r
- peripheral observations in the text (within parentheses, if you \r
- prefer, as in this sentence).\r
- }\r
-and place them at the bottom of the column on the page on which they are \r
-referenced. Use Times 8-point type, single-spaced.\r
-\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{References}\r
-\r
-List and number all bibliographical references in 9-point Times, \r
-single-spaced, at the end of your paper. When referenced in the text, \r
-enclose the citation number in square brackets, for example~\cite{ex1}. \r
-Where appropriate, include the name(s) of editors of referenced books.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Illustrations, graphs, and photographs}\r
-\r
-All graphics should be centered. Your artwork must be in place in the \r
-article (preferably printed as part of the text rather than pasted up). \r
-If you are using photographs and are able to have halftones made at a \r
-print shop, use a 100- or 110-line screen. If you must use plain photos, \r
-they must be pasted onto your manuscript. Use rubber cement to affix the \r
-images in place. Black and white, clear, glossy-finish photos are \r
-preferable to color. Supply the best quality photographs and \r
-illustrations possible. Penciled lines and very fine lines do not \r
-reproduce well. Remember, the quality of the book cannot be better than \r
-the originals provided. Do NOT use tape on your pages!\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Color}\r
-\r
-The use of color on interior pages (that is, pages other\r
-than the cover) is prohibitively expensive. We publish interior pages in \r
-color only when it is specifically requested and budgeted for by the \r
-conference organizers. DO NOT SUBMIT COLOR IMAGES IN YOUR \r
-PAPERS UNLESS SPECIFICALLY INSTRUCTED TO DO SO.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Symbols}\r
-\r
-If your word processor or typewriter cannot produce Greek letters, \r
-mathematical symbols, or other graphical elements, please use \r
-pressure-sensitive (self-adhesive) rub-on symbols or letters (available \r
-in most stationery stores, art stores, or graphics shops).\r
-\r
-%------------------------------------------------------------------------ \r
-\SubSection{Copyright forms}\r
-\r
-You must include your signed IEEE copyright release form when you submit \r
-your finished paper. We MUST have this form before your paper can be \r
-published in the proceedings.\r
-\r
-%------------------------------------------------------------------------- \r
-\SubSection{Conclusions}\r
-\r
-Please direct any questions to the production editor in charge of these \r
-proceedings at the IEEE Computer Society Press: Phone (714) 821-8380, or \r
-Fax (714) 761-1784.\r
-\r
-%------------------------------------------------------------------------- \r
-\nocite{ex1,ex2}\r
-\bibliographystyle{latex8}\r
-\bibliography{latex8}\r
-\r
-\end{document}\r
-\r
+++ /dev/null
-\documentclass[times, 10pt,twocolumn, draft]{article}
-\pagestyle{headings}
-%\usepackage{graphicx}
-\usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
-%\usepackage{hyperref}
-%\usepackage{picins}
-\usepackage{latex8}
-\usepackage{times}
-
-\pagestyle{empty}
-
-
-\newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
-\newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
-\newcommand{\pair}[2]{<\!#1,#2\!>}
-\newcommand{\canonical}{\bot}
-\newcommand{\R}{~\mathscr{R}~}
-\newcommand{\N}{\,\mathbb{N}\,}
-\newcommand{\B}{\,\mathbb{B}\,}
-\newcommand{\NT}{\,\mathbb{N}\,}
-\newcommand{\NH}{\,\mathbb{N}\,}
-\renewcommand{\star}{\ast}
-\renewcommand{\vec}{\overrightarrow}
-\newcommand{\one}{{\bf 1}}
-\newcommand{\mult}{\cdot}
-\newcommand{\ind}{Ind(X)}
-\newcommand{\indP}{Ind(\vec{P}~|~X)}
-\newcommand{\Xind}{\ensuremath{X_{ind}}}
-\newcommand{\XindP}{\ensuremath{X_{ind}}}
-\renewcommand{\|}{\ensuremath{\quad | \quad}}
-\newcommand{\triUP}{\ensuremath{\Delta}}
-\newcommand{\triDOWN}{\ensuremath{\nabla}}
-\newcommand{\Rx}{\ensuremath{R_X}}
-
-\newtheorem{thm}{Theorem}[subsection]
-
-\title{Modified Realizability and Inductive Types}
-\author{...}
-
-
-\begin{document}
-\maketitle
-\thispagestyle{empty}
-
-\begin{abstract}
-In 1959, Kreisel introduced a notion of ``modified'' realizability to
-provide an alternative technique to G\"odel functional (dialectica)
-interpretation for establishing the connection between Peano Arihtmetic
-and System T. While the dialectica interpretation has been widely
-studied in the literature, Kreisel's technique, although remarkably
-simpler,has apparently been almost neglected (with the only exception
-of Troelstra). In this paper we give a modern presentation of the technique,
-and generalize it to arbitrary inductive types in a first order setting.
-This is part of a larger program, advocating the study
-of logical systems with primitive inductive types starting form
-weak, predicative logical frameworks and adding little by little small
-bits of logical power.
-
-\end{abstract}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{Introduction}
-The characterization of the provable recursive functions of
-Peano Arithmetic as the terms of system T is a well known
-result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge
-that the functional interpretation of the Dialectica paper
-is not among the major achievements of the author (see e.g. \cite{Girard87}),
-the result has been extensively investigated and there is a wide
-literature on the
-topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
-and the bibliography therein).
-
-A different, more neglected, but for many respects much more
-direct relation between Peano (or Heyting) Arithmetics and
-G\"odel System T is provided
-by the so called {\em modified realizability}. Modified realizability
-was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
-a bit of effort to recognize it in the few lines of paragraph 3.52 -
-and later in \cite{Kreisel62} under the name of generalized realizability.
-The name of modified realizability seems to be due to Troelstra
-\cite{Troelstra}
-- who contested Kreisel's name but unfortunately failed in proposing
-a valid alternative; we shall reluctantly adopt this latter name
-to avoid further confusion. Modified realizability is a typed variant of
-realizability, essentially providing interpretations
-of $HA^{\omega}$ into itself: each theorem is realized by a typed function
-of system T, that also gives the actual computational content extracted
-from the proof.
-In spite of the simplicity and the elegance of the proof, it is extremely
-difficult to find a modern discussion of this result; the most recent
-exposition we are aware of is in the encyclopedic work by
-Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago.
-Even modern introductory books
-to Type Theory and Proof Theory devoting much space to system T
-such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
-illuminating result. Both the previous textbooks
-prefer to focus on higher order arithmetics and its relation with
-Girard's System $F$ \cite{Girard86}, but the technical complexity and
-the didactical value of the two proofs is not comparable: when you
-prove that the Induction Principle is realized by the recursor $R$
-of system $T$ you catch a sudden gleam of understanding in the
-students eyes; usually, the same does not happen when you show, say,
-that the ``forgetful'' interpretation of the higher order predicate defining
-the natural numbers is the system $F$ encoding
-$\forall X.(X\to X) \to X \to X$ of $\N$.
-Moreover, after a first period of enthusiasm, the impredicative
-encoding of inductive types in Logical Frameworks has shown several
-problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
-solved by assuming inductive types as a primitive logical notion
-(leading e.g. form the Calculus of Constructions to the Calculus
-of Inductive Constructions - CIC). Even the extraction algorithm of
-CIC, strictly based on realizability principles, and in a first time
-still oriented towards System F \cite{Paulin87,Paulin89} has been
-recently rewritten \cite{Letouzey04}
-to take advantage of concrete types and pattern matching of ML-like
-languages. Unfortunately, systems like the Calculus of Inductive
-Constructions are so complex, from the logical point of view, to
-substantially prevent a really neat theoretical exposition (at present,
-it does not
-even exists a truly complete consistency proofs covering all aspects
-of such systems); moreover, not everybody may be interested in all the features
-offered by these frameworks, from polymorphism to types depending on
-proofs. Our program is to restart the analysis of logical systems with
-primitive inductive types in a smooth way, starting form first order
-logic and adding little by little small bits of logical power.
-This paper is the first step in this direction.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{G\"odel system T}
-We shall use a variant of system T with three atomic types $\N$ (natural
-numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
-type constructors $\times$ (product) and $\to$ (arrow type).
-
-The terms of the language comprise the usual simply typed lambda terms
-with explicit pairs, plus the following additional constants:
-\begin{itemize}
-\item $*:\one$,
-\item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$
-\item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
-\end{itemize}
-Redexes comprise $\beta$-reduction, projections,
-and type specific reductions as reported in table \ref{tab:tredex}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.34\textwidth}r}
- $\lambda x:U.M ~ N \leadsto M[N/x]$ & $(\beta)$ \\
- $fst \pair{M}{N} \leadsto M$ & $(\pi_1)$ \\
- $snd \pair{M}{N} \leadsto N$ & $(\pi_2)$ \\
- $D~M~N~ true \leadsto M$ & $(D_{true})$ \\
- $D~M~N~false \leadsto N$ & $(D_{false})$ \\
- $R~M~F~ 0 \leadsto M$ & $(R_0)$ \\
- $R~M~F~(S~n) \leadsto F~n~(R~M~F~n)$ & $(R_S)$ \\
- $M \leadsto * ~~~~ $ for any M of type $\one$ & $(*)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:tredex}Reduction rules for System T}
-\end{table}
-
-Note that using the well known isomorpshims
-$\one \to A \cong A$, $A \to \one \cong \one$
-and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
-we may always get rid of $\one$ (apart the trivial case).
-The terminal object does not play a major role in our treatment, but
-it allows to extract better algorithms. In particular we use it
-to realize atomic proposition, and stripping out the terminal object using
-the above isomorphisms gives a simple way of just keeping the truly
-informative part of the algorithms.
-
-\Section{Heyting's arithmetics}
-
-{\bf Axioms}
-
-\begin{itemize}
-\item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
-\item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
-\item $ex\_intro: \forall x.(P \to \exists x.P)$
-\item $fst: P \land Q \to P$
-\item $snd: P \land Q \to Q$
-\item $conj: P \to Q \to P \land Q$
-\item $false\_ind: \bot \to Q$
-\item $discriminate:\forall x.0 = S(x) \to \bot$
-\item $injS: \forall x,y.S(x) = S(y) \to x=y$
-\item $plus\_O:\forall x.x+0=x$
-\item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
-\item $times\_O:\forall x.x\mult0=0$
-\item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$
-\end{itemize}
-
-\noindent
-{\bf Inference Rules}
-
-say that ax:AX refers to the previous Axioms list...
-%\begin{table}[!h]
-%\hrule\vspace{0.1cm}
-%\begin{tabular}{p{0.34\textwidth}r}
-
- $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
- $$ \Gamma \vdash ax : AX~~~ (Const)$$
- $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
- $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
- {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
- $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
- (\forall_i)$$
- $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
- ~~~ (\forall_e)$$
-
-%\end{tabular}\vspace{0.1cm}
-%\hrule
-%\caption{\label{tab:HArules}Inference rules}
-%\end{table}{lr}
-
-%\[
-% (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
-% {\Gamma \vdash \pair{M}{N} : A \land B}
-%\hspace{2cm}
-% (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
-%\hspace{2cm}
-% (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
-%\]
-
-
-%\[
-% (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
-% (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
-%{\Gamma \vdash Q}
-%\]
-
-\Section{Extraction}
-
-The formulae to types translation function $\sem{\cdot}$, see table
-\ref{tab:formulae2types}, takes in input formulae in HA and returns
-types in T. In table \ref{tab:structproof} we the proofs to terms
-function for structured proofs. Axiom translation is reported in table
-\ref{tab:axioms}. In table \ref{tab:canonical} we define how the
-canoniac element is formed.
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.21\textwidth}p{0.21\textwidth}}
- $\sem{A} = \one$ if A is atomic &
- $\sem{A \land B} = \sem{A}\times \sem{B}$ \\
- $\sem{A \to B} = \sem{A}\to \sem{B}$ &
- $\sem{\forall x:\N.P} = \N \to \sem{P}$ \\
- $\sem{\exists x:\N.P} = \N \times \sem{P}$ &
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:formulae2types}Formulae to types translation}
-\end{table}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.20\textwidth}p{0.20\textwidth}}
- $\semT{M N} = \semT{M} \semT{N}$ &
- $\semT{M t} = \semT{M} \semT{t}$ \\
- \multicolumn{2}{l}{$\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$} \\
- \multicolumn{2}{l}{$\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$}
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:structproof}Structured proofs}
-\end{table}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{l}%{0.47\textwidth}p{0.47\textwidth}}
- $\sem{fst} = \pi_1$\\
- $\sem{snd} = \pi_2$\\
- $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$\\
- $\sem{false\_ind} = \canonical_{\sem{Q}}$\\
- $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$\\
- $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\
- $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$\\
- $\sem{nat\_ind} = R$ \\
- $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$ \\
- $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ \\
- $\sem{ex\_ind} = \lambda f:(\N \to \sem{P} \to \sem{Q}).$\\
- $\qquad\lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:axioms}Axioms translation}
-\end{table}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{l}%p{0.23\textwidth}p{0.23\textwidth}}
- $\canonical_\one = \lambda x:\one.x$ \\
- $\canonical_N = \lambda x:\one.0$ \\
- $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U}
- x}{\canonical_{V} x}$ \\
- $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:canonical}Canonical element}
-\end{table}
-
-
-\Section{Realizability}
-The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
-$P$ is a closed formula.
-In particular:
-\begin{itemize}
-\item $\neg (\star \R \bot)$
-\item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
-\item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
-\item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
-\item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
-\item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
-\end{itemize}
-%We need to generalize the notion of realizability to sequents.
-%Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
-%$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff
-%forall natural numbers $n_1, \ldots, n_m$,
-%if forall $i \in {1,\ldots,n}$
-%$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
-%$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
-%
-\noindent
-We need to generalize the notion of realizability to sequents.\\
-Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
-$\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
-$b_1:B_1, \ldots, b_n:B_n$.\\
-We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
-$$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R
-\forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
-Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
-so we can use the previous definition of realizability on it.
-
-\noindent
-We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
-
-\begin{itemize}
-\item $nat\_ind$.
- We must prove that the recursion schema $R$ realizes the induction principle.
- To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
- $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
- \,n) \R P(\underline{n})$.\\
- We proceed by induction on n.\\
- If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
- Suppose by induction that
- $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
- still holds for $n+1$. By definition
- $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
- and since $f \R \forall x.(P(x) \to P(S(x)))$,
- $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
-
-\item $ex\_ind$.
- We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
- \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
- to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
- $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
- $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
- $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
- then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
- affects only $P$).\\
- Expanding the definition of $\underline{ex\_ind}$, $fst$
- and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
- since $g_p \R P[\underline{n_p}/x]$.
-
-\item $ex\_intro$.
- We must prove that
- $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
- that leads to prove that for each n
- $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
- Evaluating the substitution we have
- $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
- Again by definition of $\R$ we have to prove that given a
- $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
- Expanding the definition of $\underline{ex\_intro}$ we have
- $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
-
-\item $fst$.
- We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
- that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
- $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
- So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
- with $P$.
-
-\item $snd$. The same for $fst$.
-
-\item $conj$.
- We have to prove that
- $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
- Following the definition of $\R$ we have to show that
- for each $m \R P$ and for each $n \R Q$ then
- $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
- This is the same of $\pair{m}{n} \R P \land Q$ that is verified since
- $m \R P$ and $n \R Q$.
-
-
-\item $false\_ind$.
- We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
- Trivial, since there is no $m \R \bot$.
-
-\item $discriminate$.
- Since there is no $n$ such that $0 = S n$ is true... \\
- $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
-
-\item $injS$.
- We have to prove that for each $n_1$ and $n_2$\\
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R
- (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
- We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
- $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
- natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
- $* \R n_1=n_2$.
-
-\item $plus\_O$.
- Since in the standard model for natural numbers $0$ is the neutral element
- for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
-
-\item $plus\_S$.
- In the standard model of natural numbers the addition of two numbers is the
- operation of counting the second starting from the first. So
- $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
-
-\item $times\_O$.
- Since in the standard model for natural numbers $0$ is the absorbing element
- for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
-
-\item $times\_S$.
- In the standard model of natural numbers the multiplications of two
- numbers is the operation of adding the first to himself a number of times
- equal to the second number. So
- $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
-
-\end{itemize}
-
-
-\noindent
-{\bf example}\\
-Let us prove the following principle of well founded induction:
-\[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
-In the following proof we shall make use of proof-terms, since we finally
-wish to extract the computational content; we leave to reader the easy
-check that the proof object describes the usual and natural proof
-of the statement.
-
-We assume to have already proved the following lemmas (having trivial
-realizers):\\
-\[L : \forall p, q.p < q \to q \le 0 \to \bot\]
-\[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
-Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
-We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
-For $n=0$, we get a proof of $P ~q$ by
-\begin{eqnarray}
-B & \equiv & \lambda q.\lambda h_0:q \le 0. h ~q~ \nonumber\\
-& & \quad (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \nonumber
-\end{eqnarray}
-In the inductive case, we must prove that, for any $n$,
-\[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
-Assume $h_1: \forall q. q \le n \to P q$ and
-$h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
-If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
-$h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
-In conclusion, the proof of the
-inductive case is
-\begin{eqnarray}
-I & \equiv & \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. \nonumber\\
- & & \quad h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2))
- \nonumber
-\end{eqnarray}
-(where $h$ is free in I).
-The full proof is
-\begin{eqnarray}
-& \lambda h:\forall m.(\forall p. p < m\to P~p)\to P~m.\lambda m. &\nonumber\\
-& \quad nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) & \nonumber
-\end{eqnarray}
-
-where $le\_n$ is a proof that $\forall n. n \le n$, and the free $P$ in the definition of $nat_{ind}$ is instantiated with $\forall m.m \le m \to P~m$.\\
-Form the previous proof,after stripping terminal objects,
-and a bit of eta-contraction to make
-the term more readable, we extract the following term (types are omitted):
-
-\[R' \equiv \lambda f.\lambda m.
-R~ (\lambda n.f ~n~ (\lambda q.*))~
-(\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
-
-The intuition of this operator is the following: supose to
-have a recursive definition $h q = F[h]$ where $q:\N$ and
-$F[h]: A$. This defines a functional
-$f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
-(morally) $h$ is the fixpoint of $f$. For instance,
-in the case of the fibonacci function, $f$ is
-\begin{eqnarray}
-fibo & \equiv & \lambda q. \lambda g. if~ q = 0~then~ 1~ else \nonumber\\
-& & \quad if~ q = 1~ then~ 1~ else ~ g (q-1)+g (q-2) \nonumber
-\end{eqnarray}
-
-So $f$ build a new
-approximation of $h$ from the previous approximation $h$ taken
-as input. $R'$ precisely computes the mth-approximation starting
-from a dummy function $(\lambda q.*_A)$. Alternatively,
-you may look at $g$ as the ``history'' (curse of values) of $h$
-for all values less or equal to $q$; then $f$ extend $g$ to
-$q+1$.
-
-Let's compute for example
-\begin{eqnarray}
-R'~fibo~2 & \leadsto &
- R~ (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
-& \leadsto &
- (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
- 2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
- 2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
- 2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- (\lambda q.fibo ~q~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
- )2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- (\lambda q.fibo ~q~
- (\lambda n.fibo ~n~ (\lambda q.*)))2
- \nonumber\\
-& \leadsto &
- fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
-& \leadsto &
- (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
- (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
-& \leadsto &
- fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
- fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
-& \leadsto &
- 1 + 1 \nonumber
-\end{eqnarray}
-Note that the second argument of $fibo$ is always a method to calculate all the prvious values of $fibo$. DA CAPIRE (per me) come mai $\lambda n$ non viene usata...
-CAPITA CON csc:
-
-n non serve perche' c'e' una relazione logica di n con q,
-in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
-e quindi posso usare come history $< n$ una history $< q$.
-il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
-
-se si spiega come array viene decente... forse. lunedi' provo a scrivere
-meglio.
-
-\Section{Inductive types}
-The notation we will use is similar to the one used in
-\cite{Werner} and \cite{Paulin89} but we prefer
-giving a label to each constructor and use that label instead of the
-longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
-We adopt the vector notation to make things more readable.
-$\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
-be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
-name to the first $m$ and assert $n>0$). If the vector notation is
-used inside an arrow type it has a slightly different meaning,
-$A \to \vec{B} \to C$ is a shortcut for
-$A \to B_1 \to \ldots \to B_n \to C$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Extensions to the logic framework}
-To talk about arbitrary inductive types (and not hard coded natural numbers) we
-have to extend a bit our framework.
-
-First we admit quantification over inductive types $T$, thus $\forall x:T.A$
-and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
-definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
-$\sem{\exists x:T.P} = T \times \sem{P}$.
-
-For each inductive type we will describe the formation rules and the
-corresponding induction principle schema.
-
-Symmetrically we have to extend System T with arbitrary inductive types and
-we will see how theyr recursors are defined in the following sections.
-
-The definition of $\R$ is modified substituting each occurrence of $\N$ with
-a generic inductive type $T$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Type definition}
-$$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
-$$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
-In the second case we mean $T \neq X$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Induction principle}
-The induction principle for an inductive type $X$ and a predicate $Q$
-is a constant with the following type
-$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
-$\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
-constructor of X, and $c:C(X)$) and is defined by recursion as follows:
-\begin{eqnarray}
-\triUP\{X, c\} & = & Q(c) \nonumber\\
-\triUP\{T \to C(X), c\} & = &
- \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
-\triUP\{X \to C(X), c\} & = &
- \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
-\end{eqnarray}
-
-%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Recursor}
-%\SubSubSection{Type}
-The type of the recursor $\Rx$ on an inductive type $X$ is
-$$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
-$\square$ is defined by recursion on the constructor type $C(X)$.
-\begin{eqnarray}
-\square\{X\} & = & \alpha \nonumber \\
-\square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
-\square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
-\end{eqnarray}
-%\SubSubSection{Reduction rules}
-We say that
-$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
-\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
-$\triDOWN$ takes a constructor type $C(X)$, a term $f$
-(of type $\square\{C(X)\}$) and is defined by recursion as follows:
-\begin{eqnarray}
-\triDOWN\{X, f, \} & = & f\nonumber \\
-\triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
- \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
-\triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
- \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
- \vec{m}\}\nonumber
-\end{eqnarray}
-We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
-can omit $\vec{m}$ since it is an empty sequence.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Realizability of the induction principle}
-Once we have inductive types and their induction principle we want to show that
-the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
-$\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
-
-\begin{thm}$\Rx : \sem{\Xind}$\end{thm}
-\begin{proof}
-We have to compare the definition of $\square$ and $\triUP$
-since they play the same role in constructing respectively the types of
-$\Rx$ and
-$\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
-function to each right side of the $\triUP$ definition we obtain
-exactly $\square$. The last two elements of the arrows $\Rx$ and
-$\Xind$ are again the same up to $\sem{\cdot}$.
-\end{proof}
-
-\begin{thm}$\Rx\R \Xind$\end{thm}
-\begin{proof}
-To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
-of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
-have to prove that for each $t:X$
-$$\Rx~\vec{f}~t \R Q(t)$$
-\noindent
-We proceed by induction on the structure of $t$.
-\\
-The base case is when the
-type of the head constructor of $t$ has no recursive arguments (i.e. the type
-is generated using only the first two rules $C(X)$), so
-$(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
-realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
-case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
-Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
-\\
-In the induction step we have as induction hypothesis that for each recursive
-argument $t_i$ of the head constructor $c_i$, $r_i\equiv
-\Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
-$f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
-then all the recursive one. In general they can be mixed and the proof is
-exactly the same but the notation is really heavier). We know by hypothesis
-that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
-t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
-Q(c_i~\vec{m}~\vec{t})$.
-\end{proof}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{Strong normalization of extended system T}
-Strong normalization for system T is a well know result\cite{GLT}
-that can be easily extended to System T with this kind of inductive
-types. The first thing we have to do is to extend the definition of
-neutral term to the terms not of the form $<u,v>$, $\lambda x.u$,
-$c_i~\vec{m}$.
-
-In conformity with the demonstration we are extending we call $\nu(t)$
-the length of the longest reduction path from $t$ and $\ell(t)$ the
-number of symbols in the normal form of $t$.
-
-For an inductive type $\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$
-we have to prove that for each $i$,
-given a proper sequence of reducible arguments $\vec{m}$ and $\vec{f}$,
-$(c_i~\vec{m})$ and $\Rx~\vec{f}~(c_i~\vec{m})$ are reducible.
-
-First the simple case of constructors. If the constructor $c_i$ takes
-no arguments then it is already in normal form. If it takes
-$m_1,\ldots,m_n$ reducible arguments, then $\nu(c_i~\vec{m}) = max \{m_1,
-\ldots,m_n\}$ and so $c_i~\vec{m}$ is strongly nomalizable thus
-reducible for the definition of reducibility for base types.
-
-To show that $\Rx~\vec{f}~(c_i~\vec{m})$ is reducible we can use
-(\textbf{CR 3}) that states that if $t$ is neutral and every $t'$ obtained by
-executing one redex of $t$ is reducible, then $t$ is reducible.
-
-Now we have to show that each term that can be obtained by a
-reduction step is reducible. We can procede induction on
-$\Sigma\nu(f_i) + \nu(c_i~\vec{m}) +
-\ell(c_i~\vec{m})$ since we know by hypothesis that $\vec{f}$ and
-$(c_i~\vec{m})$ are reducible and consequently strongly normalizing.
-\\
-The base case is when $c_i$ takes no arguments and $\vec{f}$ are
-normal. In this case the only redex we can compute is
-$$\Rx~\vec{f}~c_i~\leadsto~f_i$$ that is reducible by hypothesis.
-\\
-The interesting inductive case is when $\vec{m}$ and $\vec{f}$ are
-normal, so the only reduction step we can execute is
-$$\Rx~\vec{f}~(c_i~\vec{m})~\leadsto~f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$
-where $\vec{n}$ are the recursive arguments of $c_i$ (here we wrote
-the recursive calls as the last parameters of $f_i$ just to lighten
-notation). Since $\ell(n_j)$ is less than $\ell(c_i~\vec{m})$ for
-every $j$ we can apply the inductive hypothesis and state that
-$\Rx~\vec{f}~n_j$ is reducible. Then by definition of reducibility of
-the arrow types and by the hypothesis that $f_i$ and $\vec{m}$ are
-reducible, we obtain that $$f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$ is
-reducible.
-\\
-All other cases, when we execute a redex in $\vec{m}$ or $\vec{f}$,
-are straightforward applications of the induction hypothesis.
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{Improving inductive types}
-It is possible to parametrise inductive types over other inductive types
-without much difficulties since the type $T$ in $C(X)$ is free. Both the
-recursor and the induction principle are schemas, parametric over $T$.
-
-Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
-fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
-
-Credo anche che quantificare su eventuali variabili di tipo non cambi niente
-visto che non abbiamo funzioni.
-
-Se ammettiamo che i tipi dipendano da termini di tipo induttivo
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\bibliographystyle{latex8}
-%\bibliography{latex8}
-
-\begin{thebibliography}{}
-\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
-Foundations of Computing, Cambrdidge University press, 1991.
-\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
-years later. Theoretical Computer Science 45, 1986.
-\bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
-Bibliopolis, Napoli, 1987.
-\bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
-Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
-Press, 1989.
-\bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
-des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
-\bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
-1990.
-\bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
-Lambda-calculus, Cambridge University Press, 1986.
-\bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
-by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
-\bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
-in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
-Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
-\bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
-number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
-\bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
-constructive functionals of finite type. In. A.Heyting ed.
-{\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
- \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic
-predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
-\bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle
-certifi\'ee; l'extraction
-de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
-Paris XI-Orsay, 2004.
-\bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
-Bibliopolis, Napoli, 1984.
-\bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
-Constructions. Ph.D. Thesis, Universit\'e de
-Paris 7, 1987.
-\bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs
-from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual
-ACM Symposium on
-Principles of Programming Languages, Austin, January, ACML Press 1989.
-\bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
-Wissenschaften 225, Springer Verlag, Berlin, 1977.
-\bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of
-Intuitionistic
-Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
-Berlin, 1973.
-\bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
-Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
-Press, 1996.
-\bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
-Ph.D.Thesis, Universit\'e de Paris 7, 1994.
-
-
-\end{thebibliography}
-
-\end{document}
-
projects / helm.git / commitdiff