; TeX output 1996.03.06:1228 s o 0 G G dcr1728Theh'L G G dctt1728semantic-pacykage!",
cmsy10 86e dcr1200PweterlMllerNeergaard ] L dctt1200turtle@diku.dkhttp://www.diku.dk/students/turtle%vV Marcwhl6,1996-bލ "!l dcbx0900Abstract_ o$ dcr0900Thispac
dcbx10001WSym>bQolsmڬ2`I 2WInferenceRulesI3 3T
ranslationDiagrams+C4` 4SomeNotesabQouttheFiles t6̍I Lc K"ȜI &&oi
dctt1000semantic "
dcr1000isaLf'h dcr0700A zTUY&E9X2
b>
cmmi10"+M/-packqageeasy I inghthewritingofnotationofsemanI tics!andcompilers.׀T*ouseittheI leDsemantic.styshouldbGeplaced,I so'thatLfA zTUY&E9Xcan ndit. InyourI doGcument!preambleyoushouldincludeI \usepackage{semantic}X InVthefollowingIwilldescribGetheI use?ofthedierentpartsofOsemantic:I symbGols,inferencerulesandtranslaI tionOMdiagrams.`ThereisalsoasectionI describingtheinstallationandgivingI a
shortintroGductiontothetwo lesI semantic.dtxU andsemantic.ins.X LikedQmostothercomputer-programs,I Im#havemkprovidedthispackqagewithsevI eralAbugs,N},whichyieldsI CW[ [h*y
dcit1000commandVi.A(]] ahenvir}/onment ɸi y.$If}youneedtodescribGemorethanonekindofevqalI uations,e.g. bGothE!andE ^ O! cmsy7}ܹ,youcanprovideanoptionalargumentimmediatelyI after2\comprespGectively\eval.AsanexampleadenotationalruleforasequenI ciliasingU oftwoU commandssE ICW[ [C1?;C2]] {+I and=>,
whichisavqailableinbGothmathematicsandtext.ZBytypinga*or+afterI ->U or=>yougetthestarred*handplussedversions:q!^,)^,!^ٓR cmr7+ and)^+.X InT6theinferencesymbols-environmentT6thevqastma 0jorityofLfA zTUY&E9X-commandsI workṡnormally*.ItishowevernotpGossibletoensure,athatthesymbGols|,a-andI =works100%likeoutsidetheenvironment^1|2,Գandforinstance\cline{::: -:::}I cannotEbGeusedinthisenvironmentE(ithoweverEworksifitispartofacommandI de nedU outsidetheenvironment).I & ff r E !i-:0][ dcr06001KInside6theenÒvironment61a dctt0800|,N-and=arede nedasmacros.0Thesemacrosexamensthenext cÒharacter3andifitis-or=,KG>and>resp
dccc1000TrZue+`s
>0)^0 ; ^0Q`while?E9dosF<)^00sSw fe (q`while?E9dosF<)^00 It(2)U :<#C]ڵ`E
)Fhalse*b w fe u
(`while?E9dosF<)퍑LU and𨍍荒 εp,MU !^p^09,M^0 ; εp^09,M^0#Y!U p^00 r,M^00 JFw fe Qp (Op,MU !^p^00 r,M^00 TU K cmsy8!-:wqAa cmr61i2 fe F4E (p,MU !^p,MP^TU!-:wq2%LU areU easilysetusing\inference.qThesyntaxis31b \inference[5 cmsy9hname i J]{hline 1*i \\\N45" cmmi9:::=B\\Nhline ; cmmi6n 7i }{hc$onclusion .i1}31I where9n0soyoualsocantypGeaxioms.hpEachlineconsitsofpremisessepGerated I byU &:b hpr$emise 1*i *~&:::
ʦ&hpr$emise miI NotethatmcanalsobGezerowhichisusedwhentypingaxioms.Theoptional I nameU issettotherightoftheinference.X The rulesissetsotheline ushwiththecenterofsmalllettersinthesurroundI ing~text.VInthisway~secondaryconditionsornames(likethe rstexampleabGove)I can.bGewritteninthesurroundingtext.@ItalsomakesitpossibletosettherulesI inU atablelikeshownherewiththelastexample: jwR^ T*ransitiveU (1):荒 p,MU !^p^09,M^0 ; p^09,M^0#Y!U p^00 r,M^00 lw fe Qp (Op,MU !^p^00 r,M^0044^ T*ransitiveU (2): l2 fe F4E (p,MU !^p,M \vX AnU inferencerulecanunproblematiclybGenestedwithinanother,like:-N<#`n 9) fe F4E (p,MU !^p,M =.xL!-:wq2 p,MU !^p^09,M^0fw fe (;p,MU !^p^09,M^0 byxL!-:wq1:6p^09,M'U !p^00 r,M^00_
)w fe% (qEp,MU !^p^00 r,M^00 {TU!-:wq1X The"appGearanceoftheinferencesrulescanpartlybecontrolledbythefollowing$n\setpremisesend\setpremisesspace
\setnamespaceI lengths:ȍ<#"= Kpremisesend Í < u
cmex10z 31 Z}| 31 Z{ premise"=premisesSpace Í z 31
}| 31
{ 'premise <w fe ( (2`conclusion$Pnamespace Í )dz 31
}| 31
{ GTUnamenI Thelengthsarechangedusingthethreecommands\setnamespace{hlength Ui"Yx},I \setpremisesend{hlength Ui"Yx}[og\setpremisesspace{hlength Ui}.hlength Ui.:!canbGeI giveninbGothabsoluteunitslikeptandcmandinrelativeunitslikeemandI ex.xThe defaultvqaluesare:1 33133& fe s2bemforpremisesspace, 3& fe s4
emforpremisesendog J331J33& fe s2ObemNfornamespace.
Notethatthelengthsc}/annotbGealteredusingtheordinaryI LfA zTUY&E9X-commandsU \setlengthand\addtolength.X Besides9thattheappGearanceofinferencerulesislikefractionsinmath:(AmongI other7Nthingsthepremiseswillnormal lybGeatsameheightabove7NthebaselineandI there isaminimumdistancefromthelinetothebGottomofthepremises..TheI informationU tosettheruleslikefractionistakenfromthecurrentmathfont. (3 !P s o dI 8*=
manfntUF:etcћkM dcsl0900expressionistobAeI ev|yaluatedinaen#3#4\predicateend{%kr$#1N\vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S#4$}
i I ThenUtheinference(bAorro]vY)
J Ss-=0D`s>v7{q 0n cmsy50Y)
J Ss-=00 ֟I fe ՟ ؝ r9DӍ`NTl(s)>v7{q0Y)
J Ss-=00:saeTlRgI can$bAeaccomplishedb{v}s'&D|-$s$=>{v'}s''}kr{DN|-Tl($s$)=>{v'}s''}i I Please$notethattheinferencesymbols-en&examened,Xeandifitis\end,semanticconcludesthatthepremisedo,himplementationDplanguage iky} b \interpreter{hsour$ce i ,himplemenationAlanguage ih}b \compiler{hsour$ce i ,hmachine i)d,htar$get +i e}b \machine{hmachine i)d}I TheZargumentscanbGeaeitherastringdescribingthelanguage(pleasedonotuse I a3=macroatthestartofthestring)oroneofthefourcommands. However3=theI combinations)givingnomeaningareexcludedlikeimplementingainterpreteronI aU program,whichyieldtheerrormessage: fP!NPackagesemanticError:Aprogramcannotbeatthebottom. u`SeeNthesemanticpackagedocumentationforexplanation. u`Type rHNforimmediatehelp.zq...X WhenZyouareusingacommandasanargumentsemanticwillcopythelan I guage4fromthenestedcommandandautomaticlyplacethetwo4 guresinpropGorI tion toeachother.YdInthiswaybigtranslationdiagramscaneasilybGedrawn.YdTheI hole&constructionshouldbGeplacedusingaf\putcommand,'wherether}/eferenceI p}/oint\isithecenterofthebGottomofthe gurecorrespondingtotheoutermostI command.TI+/think+gafewexamples(withthereferencepGointmarkedby+gr
+g)willI clarifyU someofthesepGoint:U 32 fd 32 fd LΟ ( fe LΟ ( fe *S @TL' r 32 fd LΟ fe LΟ fe32 L LΟ Ή fe32LLΟ Ή fe 32 fe *P 32 fd P 32 fd 6 32 fd " 32 fd LΟ feTLΟ fe"LΟ fe6LΟ fe՚' !*CT 32 fd hLΟ feTLΟ fe32TLήTLΟ Ή fe32hLhLΟ Ή fe^ 32 fe [*P[*MB*M" 32 fd " T& T0 , )*M)*M *C rI isU obtainedbythecommands b \begin{picture}(220,75)(0,-35) fP\put(10,0){\interpreter{S,L'}}fP\put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}b \end{picture}I Notejfromthesecondexample,oJthatwhen\compilerisusedasimplementation I language-argument3itisbyconventionattributedtotherightofthe gure. mItI iséalsoworthmentioningthatthereisnostrictdemandonwhichcommandyouI shoulduchoGoseastheoutermost,ie.thesecondexamplecouldalsobewritten(withI aU changeinthecoGordinatesto\putduetothenewreferencepoint)as b \put(160,-20){\compiler{\program{P,C},\machine{M},\program{P,M}}} (5 E s o I starting'ointhemiddleinsteadofusingaleft-to-right-approachin'factitwill I often6bGeeasiesttostartinthemiddleasthisgivestheleastnestingmakingitI easierU toendtheargumentsattherightpGosition.X ThoughusingnestingitisinsomerarecasesadequatetousedierentlanguageI symbGols̔onthetwosidesofthelineoftouch.CE.g.whendescribingbGootstrappringI the VpGoorU-codeimplementationcanbesymbolizedbyAU^ ,)KwhichstillisexecutedI onRaU-machine.iThiscanbGedonebyprovidingthesymbGol-commandwithanI optional#argumentimmediatelyafterthecommandname.InthiswaythebGootI strapping:Z 32 fd P 32 fd 32 fd ׀ 32 fd LΟ fe LΟ fe LΟ fe LΟ fe՚ ܀ ! 32 fd P 32 fd 32 fd 32 fd LΟ fe LΟ fe LΟ fe LΟ fe՚ ! @TML *U @TML @TML 32 fd P 32 fd 32 fd 32 fd LΟ fe;LΟ fe LΟ fe LΟ fe՚ ! 32 fd P 32 fd 32 fd ׀ 32 fd LΟ fe LΟ fe LΟ fe LΟ fe՚ ܀ ! @TML *U @TML @TML 32 fd P 32 fd O 32 fd ; 32 fd LΟ femLΟ fe;LΟ feOLΟ fe՚@ !'@TML[*UB*U)*U 32 fd T
T *U,
*U^ , *U^ ׀ 32 fd ׀ T ۀ T *U, ۀ*U^ I isU typGed b \compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ y\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}X Whencalculatingthedimensionsofthepicture-environmentitisgoGodto I knowU thedimensionsofthe gures,whichisgiveninunitsof\unitlength:$8 I compiler:q80*40I interpreter:q20*40 machine:q20*17.1 program:q20*40!֍I 4` SomeG\NotesabpouttheFiles~I semanticisdistributedinthetwo lessemantic.dtxandsemantic.ins.I semantic.dtxꐹisthemostimpGortantasitcontainsalltheessentialsusersguide,I coGdeanddocumentationofthecodewhilesemantic.insisusedonlytoguideI @#-%5
dcss1000@doGcstripU ingeneratingsemantic.styfromsemantic.dtx.X T*o2get[ [and]]usedin\comp,6\evaland\exesemantictriestoloadtheI packqage@bbGoldwrittenby23A.|Jeffrey.ZIfthisisnotinstalledonyoursystem, theI symbGolsyaresimulatedbydrawingtogethertosharps.ߡIywillhoweverrecommendI thatU youget@bbGoldfromyournearestCT*AN-archive.X InadditiontotheusersguideyoukqanalsogetthefullydoGcumentedcoGde.@Y*ouI willRWhoweveronlyneedthisifyouwillsneakinhowIRVimplementedthemacrosorI changeM somepartofthepackqage.nY*oushouldstartbyeditingsemantic.dtxandI makeU thetwolines(nearline1545)b \OnlyDescription8%NMaketoacommenttogetthedocumentation b \DisableCrossrefs+%NRemovecommentiftheindexisreadyorif I inU toacommentandremove%fromthebGeginingofthetwonextlines:b %\CodelineIndex W%NMakeaindexofthecommandusageb %\RecordChanges W%NMakethechangeshistory (6 TӠ s o I ThenyyoushouldrunLfA zTUY&E9Xtwiceontheedited letogetacorrecttableof I contents.qThenU yougeneratetheindexandchangehistoryusingmakeindex: b makeindexN-sgind.istsemantic b makeindexN-sgglo.ist-osemantic.glssemantic.glo I AndU atlastthedoGcumentationisreadyforprintingafteranotherrunofLfA zTUY&E9X.X semantic.dtx;isdesignedtobGeusedwith@docand@docstrip.IItthereforeconI sistspofthepackqagecoGdebutmostofallofalotofcommentscontaningtheusersI guideandthedoGcumentationofthecode.=WhenTUY&E9Xisrunnedonsemantic.ins,I @doGcisusedtoremoveallthesecommentsandtheresultiswritteninthepackI age- lesemantic.sty.bWhenyoumaketheusersguidebyrunningLfA zTUY&E9XonI semantic.dtx,f2LfA zTUY&E9Xa rstskipsabGout650linesofcomments(containingtheI sourceoftheusersguide)bGeforeitgetstothelinesnormallymakingupthepackI age- le.4
Thenfollows850linesofintermixedcommentsandcoGdede ningthecomI mandsinthepackqage.mAtlastLfA zTUY&E9Xcomestoaline\documentclass{ltxdoc}I (@ltxdoGcisLfA zTUY&E9X2"*='sstandardclassfordocumenting).AfteracoupleofpackI agesloadingOandsomecommandde nitionitreaches\begin{document}andI \docinput{semantic.dtx}.7ThismakesLfA zTUY&E9X'sreadingoversemantic.dtxonceI moreU butthistimeskippingthe%-charsinthe rstcolumn.
?OL_7* q q dcr2074cI A!", q
cmsy10A
]tAtelastthebGorrowingformalstu:IY*ouaencouragedtocopy*,use,delete]tetc.thepackqage(semantic.dtxandsemantic.ins)asmuchasyourheartI desiresaslongasyoupassitonincomplete(ie.notonlysemantic.sty).FY*ouI are?welcometosneakinthecoGdeandgetinspiration(A littlewarninghowever:I this2ismy rstbunchofrealTUY&E9X-coGde!).fY*oushouldjustremembGer:2c`K
G19951996I PћkM dcsl09009? dcr05008*=
manfnt7* q q dcr20745 cmsy945" cmmi92\g>
dccc10001a dctt08000][ dcr0600,Cs cmtt8+
dcbx1000$qk ff ff dcbx1440##| ff ff dcr1440"r dcti0900!l dcbx0900 dcr0900 C dcr0800 L dctt1200 q% cmsy6 K cmsy8; cmmi62 cmmi8Aa cmr6e dcr1200!",
cmsy10'L G G dctt17280 G G dcr1728 "
dcr1000
!",
cmsy10 O! cmsy7 0n cmsy5
b>
cmmi10K`y
cmr10ٓR cmr7<
lcircle10O
line10 u
cmex10 pC