I do not want the LaTeX-commands in the index This is borrowed from the standard package “doc.dtx”

I also exclude the commands used to generate the index

The semantic-package^{∗}

Peter Møller Neergaard

   turtle@diku.dk   http://www.diku.dk/students/turtle

December 30, 1997

Abstract This package provides commands that eases the notation of semantics and compilers in your documents. The notation implemented is primarily that used in Introduction to the Semantics for Programming Languages teached at the Department of Computer Science at the University of Copenhagen in fall ’95.

Table of contents in two columns — borrowed from the standard package of “doc.dtx”

We have to reset (bug in L^{A}TEX)

Contents

1 Symbols 3

2 Inference Rules 4 3 Translation Diagrams 5

4 Some Notes about the Files 7

semantic is a L^{A}TEX 2ε-package easying the writing of notation of semantics and compilers. To use it the file semantic.sty should be placed, so that L^{A}TEX can find it. In your document preamble you should include

\usepackage{semantic}

In the following I will describe the use of the different parts of semantic: symbols, inference rules and translation diagrams. There is also a section describing the installation and giving a short introduction to the two files

semantic.dtx and semantic.ins.

Like most other computer-programs, I have provided this package with several bugs, insuffiencies and inconsistencies. These should be regarded as features of the package. To increase the excitement of using the package these features appear in—even to me— unpredictable places. If they however get to annoying and seriously reduce your satisfaction with semantic then please notify me. You could also drop me a note, if you would like to be informed, when I update semantic.

In continuation of this I will espcially draw your attention to two troublesome areas: the syntax and the documentation. When laying down the syntax I have tried to satisfy to contrary considerations: to use the wellknown L^{A}TEX-syntax and to give a syntax, that is easy typed and read. This has lead to some compromises, which most probaply satisfy neither. And being dane and therefore not native english-speaking it is even harder than normal to express clearly in the documentation, what my intention was. Any feedback would therefore be greatly appreciated.

∗This file has version 1.2α and is dated 1996/01/31

A last—and compulsary—part is a special thanks to Jesper Groth Løhr, who has been β-tester of several versions leading to many improvements. and Kai Neegård, who read and commented the documentation.

1 Symbols

\eval To support writing denotational semantics the commands \comp and \eval \comp are provided to describe the evaluation of programs respectively expressions.

They have the same syntax: \comp{⟨command⟩}{⟨environment⟩}, which yields C[[⟨command ⟩]]⟨environment⟩. If you need to describe more than one kind of evaluations, e.g. both E and E^{∗}, you can provide an optional argument immediately after \comp respectively \eval. As an example a denotational rule for a sequenciliasing of two commands

C[[C1 ; C2]]d = d′ if C[[C1]]d = d′′ and C[[C2]]d′′ = d′

can be typed

     \[
       \comp{C1 ; C2}{d} = \mathtt{d'} \quad
        \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and
                   $\comp{C2}{d''} = \mathtt{d'}$}
     \]

\evalsymbol As shown above you can get the evaluationsymbol in it self. This is done by \compsymbol \compsymbol respectively \evalsymbol. These commands can also be supplied

with an optional argument, e.g. \evalsymbol[*] to get E^{∗}. \exe The result of executing a program on a machine with som data can be de-

scribed using \exe, which has the syntax \exe{⟨program⟩}[⟨machine⟩]{⟨data⟩}, where the ⟨machine⟩ as indicated is optional. The third Futumara projection cogen = [[spec]](spec.spec) can using the \exe-command be written

$\mathtt{cogen} = \exe{spec}{spec.spec}$. Or you can give an explicit ma-
chine L: $\mathtt{cogen} = \exe{spec}[L]{spec.spec}$ and you will then get
cogen = [[spec]]^{L}(spec.spec)

inferencesymbols When writing inference rules, proofs etc. the symbols ⊢, ⊧, → and ⇒ are often used extensively. Normally they are only available in mathematics ($…$) and you therefore need to key in lengthy and cumbersome com-

mands. In the inferencesymbol-environment (\begin{inferencesymbols} . . .

\end{inferencesymbols}) these symbols are provided as “ligatures” of |-, |=, -> and =>, which is available in both mathematics and text. By typing a * or + after -> or => you get the “starred” and “plussed” versions: →^{∗}, ⇒^{∗}, →^{+} and ⇒^{+}.

In the inferencesymbols-environment the vast majority of L^{A}TEX-commands works normally. It is however not possible to ensure, that the symbols |, - and = works 100% like outside the environment^{1}, and for instance \cline{…-…} cannot be used in this environment (it however works if it is part of a command defined outside the environment).

2 Inference Rules

\inference Inference rules like

It(1) : ρ ⊢ E ⇒ True ρ ⊢ s ⇒ ρ′ ρ′ ⊢ while E do s ⇒ ρ′′ ρ-while $E$ do $s$=>\rho''\} It(2) : \frac{ρ ⊢ E ⇒ False}{ρ ⊢ while E do s ⇒ ρ} and ^{→_{1}^{∗}} ^{→_{2}^{∗}}

are easily set using \inference. The syntax is

\inference[⟨name⟩]{⟨line_{1}⟩ \\ … \\ ⟨line_{n}⟩}{⟨conclusion⟩}

where n ≥ 0 so you also can type axioms. Each line consits of premises seperated by &:

⟨premise_{1}⟩&…&⟨premise_{m}⟩

Note that m can also be zero which is used when typing axioms. The optional name is set to the right of the inference.

The rules is set so the line flush with the center of small letters in the surrounding text. In this way secondary conditions or names (like the first example above) can be written in the surrounding text. It also makes it possible to set the rules in a table like shown here with the last example:

Transitive (1): p,M →^{∗} p′,M′ ; p′,M′ → p′′,M′′ ; p,M →^{∗} p′′,M′′
Transitive (2): \overline{p,M →^{∗} p,M}

An inference rule can unproblematicly be nested within another, like:

\frac{\overline{p,M →^{∗} p,M} ^{→_{2}^{∗}} p,M →^{∗} p′,M′}{p,M →^{∗} p′,M′} ^{→_{1}^{∗}} p′,M’ → p′′,M′′

p,M →^{∗} p′′,M′′ →_{1}^{∗}

\setpremisesend The appearance of the inferences rules can partly be controlled by the following

\setpremisesspace
\setnamespace

lengths:

\frac{^{premisesend} premise ^{premisesSpace}premise}{conclusion} ^{^{namespace}name}

The lengths are changed using the three commands \setnamespace{⟨length⟩},

\setpremisesend{⟨length⟩} og \setpremisesspace{⟨length⟩}. ⟨length⟩ can be

given in both absolute units like pt and cm and in relative units like em and ex. The default values are: 1\frac{1}{2}em for premisesspace, \frac{3}{4}em for premisesend og \frac{1}{2}em for namespace. Note that the lengths cannot be altered using the ordinary L^{A}TEX-

1Inside the environment |, - and = are defined as macros. These macros examens the next character and if it is - or =, > and > respectively, the command for the ligature, e.g. $\vdash$ for |- is returned. Otherwise the characters from outside the environment is returned (both the character and catcode).

commands \setlength and \addtolength.

Besides that the appearance of inference rules is like fractions in math: Among other things the premises will normally be at same height above the baseline and there is a minimum distance from the line to the bottom of the premises. The information to set the rules like fraction is taken from the current math font.

This description is only for TeXnichians and it it therefore written in a smaller fotn. The dangorous bend is designed to span two lines Fetching the font informa-

tion from the math font and the evaluation (in case they are defined in relative units) of the lengths mentioned above is done just before the individual rule is set. This is demonstrated by the following construction (which admittedly is not very useful):

Conclusion

tiny

Conclusion

footnotesize

Conclusion

normalsize

Conclusion

Large

Note that as going from the top to the bottom, the eaves are getting bigger and the names come farer from the line below.

\predicate To set up a single predicate (a premise or conclusion) the singleargument command

\predicate is used. This allows a finer control of the formatting. As an example alle premises and conclusions can be set in mathematics mode by the command:

     \renewcommand{\prediate}[1]{$ #1 $}

semantic only uses \predicate on a premise, when it does not contain a nested

\inference.^{2} So though the declaration above has been given, \inference would never be executed in math mode, nor if you wrote:

     \inference{\inference. . .}{. . .}
\predicatebegin  The default definition of \predicate is \predicatebegin #1\predicateend, where
\predicateend

\predicatebegin and \predicateend is defined to be empty. The setting of premises and conlusions in math could therefore also be obtained by

     \renewcommand{\predicatebegin}{$}
     \renewcommand{\predicateend}{$}

My motivation however for introducing \predicatebegin and \predicateend was

to use TEX’s patternmatching on macro arguments to do even more sophisticated formatting by redefining \predicatebegin. If for example every expression is to be evaluated in a environment giving a value, and you would like to set all the environments values in mathematics and the expressions in typewriter-font, then this could be eased by the definition:

     \def\predicatebegin#1|-#2=>#3#4\predicateend{%
       $#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}

Then the inference (borrowed from M. Hennessy, The Semantics of Programming Languages)

\frac{D ⊢ s ⇒^{v}_{S} s′ D ⊢ s ⇒^{v′}_{S} s′′}{D ⊢ Tl(s) ⇒^{v′}_{S} s′′}  ^{TlR}

can be accomplished by

2What semantic precisely does is to append the tokens \inference \end to the code of a premise, when it has isolated it. semantic then uses TEX’s pattern matching to search this new list of tokens for an appearance of the token \inference. When this is found the following token is examened, and if it is \end, semantic concludes that the premise does not contain a nested inference rule

     \inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}
       {D |- Tl($s$) =>{v'} s''}

Please note that the inferencesymbols-environment has not been used above. TeXnichian

mod OFF

3 Translation Diagrams

\compiler To draw translation diagrams describing the result of using one or more compilers,

\interpreter
\program
\machine

interpreters etc., semantic has commands for the diagrams:

       [figure: P; L; {S \atop L}; ^{→ S         T M}; M]

The commands should only be used in a picture-environemnt and are respectively

\program{⟨program⟩,⟨implementation language⟩} \interpreter{⟨source⟩,⟨implemenation language⟩} \compiler{⟨source⟩,⟨machine⟩,⟨target⟩}

     \machine{⟨machine⟩}

The arguments can be a either a string describing the language (please do not use a macro at the start of the string) or one of the four commands. However the combinations giving no meaning are excluded—like implementing a interpreter on a program, which yield the errormessage:

      ! Package semantic Error: A program cannot be at the bottom .
         See the semantic package documentation for explanation.
         Type  H <return>  for immediate help.
          ...

When you are using a command as an argument semantic will copy the language from the nested command and automaticly place the two figures in proportion to each other. In this way big translation diagrams can easily be drawn. The hole construction should be placed using af \put command, where the reference point is the center of the bottom of the figure corresponding to the outermost command. I think a few examples (with the reference point marked by ) will clarify some of these point:

              [figure: {S \atop L'}; P; →; C; P; M; M; M; M; C]

is obtained by the commands

     \begin{picture}(220,75)(0,-35)
      \put(10,0){\interpreter{S,L'}}
      \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}
     \end{picture}

Note from the second example, that when \compiler is used as “implementation language”-argument it is by convention attributed to the right of the figure. It is also worth mentioning that there is no strict demand on which command you should choose as the outermost, ie. the second example could also be written (with a change in the coordinates to \put due to the new reference point) as

     \put(160,-20){\compiler{\program{P,C},\machine{M},\program{P,M}}}

starting off in the middle instead of using a “left-to-right”-approach—in fact it will often be easiest to start in the middle as this gives the least nesting making it easier to end the arguments at the right position.

Though using nesting it is in some rare cases adequate to use different language symbols on the two sides of the line of touch. E.g. when describing bootstrappring the poor U-code implementation can be symbolized by U^{−}, which still is executed on a U-machine. This can be done by providing the symbol-command with an optional argument immediately after the commandname. In this way the bootstrapping:

              [figure: →; ^{→ ML        U ML}; ML; →; ^{→ ML        U ML}; ML; ^{→ ML        U U}; U; U; U^{−}; U^{−}; U; U^{−}]

is typed

     \compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{
          \compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}

When calculating the dimensions of the picture-environment it is good to know the dimensions of the figures, which is given in units of \unitlength:

compiler: 80*40 interpreter: 20*40 machine: 20*17.1 program: 20*40

4 Some Notes about the Files

semantic is distributed in the two files semantic.dtx and semantic.ins.

semantic.dtx is the most important as it contains all the essentials—users guide, code and documentation of the code—while semantic.ins is used only to guide docstrip in generating semantic.sty from semantic.dtx.

To get [[ and ]] used in \comp, \eval and \exe semantic tries to load the package bbold written by A. Jeffrey. If this is not installed on your system, the symbols are simulated by drawing together to sharps. I will however recommend that you get bbold from your nearest CTAN-archive.

In addition to the users guide you kan also get the fully documented code. You will however only need this if you will sneak in how I implemented the macros or change some part of the package. You should start by editing semantic.dtx and make the two lines (near line 1545)

     \OnlyDescription    % Make to a comment to get the documentation
     \DisableCrossrefs   % Remove comment if the index is ready or if

in to a comment and remove % from the begining of the two next lines:

     %\CodelineIndex      % Make a index of the command usage
     %\RecordChanges      % Make the changes history

Then you should run L^{A}TEX twice on the edited file to get a correct table of contents. Then you generate the index and change history using makeindex:

     makeindex -s gind.ist semantic
     makeindex -s gglo.ist -o semantic.gls semantic.glo

And at last the documentation is ready for printing after another run of L^{A}TEX.

semantic.dtx is designed to be used with doc and docstrip. It therefore consists of the packagecode but most of all of a lot of comments contaning the users guide and the documentation of the code. When TEX is runned on semantic.ins, doc is used to remove all these comments and the result is written in the package-file semantic.sty. When you make the users guide by running L^{A}TEX on semantic.dtx, L^{A}TEX first skips about 650 lines of comments (containing the source of the users guide) before it gets to the lines normally making up the package-file. Then follows 850 lines of intermixed comments and code defining the commands in the package. At last L^{A}TEX comes to a line \documentclass{ltxdoc} (ltxdoc is L^{A}TEX 2ε’s standard class for documenting). After a couple of packagesloading and some command definition it reaches \begin{document} and

\docinput{semantic.dtx}. This makes L^{A}TEX’s reading over semantic.dtx once

more but this time skipping the %-chars in the first column.

\begin{matrix}c \\ ◯ \end{matrix} At last the borrowing formal stuff: You a encouraged to copy, use, delete

etc. the package (semantic.dtx and semantic.ins) as much as your heart desires as long as you pass it on in complete (ie. not only semantic.sty). You are welcome to sneak in the code and get inspiration (A little warning however: this is my first bunch of real TEX-code!). You should just remember: \begin{matrix}c \\ ◯ \end{matrix}1995–1996

Peter Møller Neergaard