788 lines
26 KiB
TeX
Executable File
788 lines
26 KiB
TeX
Executable File
\usepackage{float}
|
|
\usepackage{color}
|
|
\usepackage{xspace_spezial}
|
|
%\usepackage{amsmath}
|
|
%\usepackage{amssymb}
|
|
\usepackage{alltt}
|
|
\usepackage{fancybox}
|
|
\usepackage{stmaryrd}
|
|
\usepackage{verbatim}
|
|
\usepackage{epsfig}
|
|
%\usepackage{multicol}
|
|
\usepackage{longtable}
|
|
\newlength{\textwid}
|
|
\setlength{\textwid}{\textwidth}
|
|
\addtolength{\textwid}{-4ex}
|
|
\newlength{\textfighei}
|
|
\setlength{\textfighei}{\textheight}
|
|
\addtolength{\textfighei}{-10ex}
|
|
\DeclareSymbolFont{blackboard}{OT1}{bbm}{m}{sl}
|
|
\DeclareMathSymbol{\IR}{0}{blackboard}{"52}
|
|
\DeclareMathSymbol{\IN}{0}{blackboard}{"4E}
|
|
\DeclareMathSymbol{\IF}{0}{blackboard}{"46}
|
|
\DeclareMathSymbol{\IP}{0}{blackboard}{"50}
|
|
\DeclareMathSymbol{\IK}{0}{blackboard}{"4D}
|
|
\DeclareMathSymbol{\IZ}{0}{blackboard}{"5A}
|
|
\DeclareMathSymbol{\IQ}{0}{blackboard}{"51}
|
|
\DeclareMathSymbol{\IC}{0}{blackboard}{"43}
|
|
\parindent 0mm
|
|
\renewcommand{\unlhd}{<}
|
|
%\renewcommand{\lhd}{<\!\!|}
|
|
%\renewcommand{\rhd}{|\!\!>}
|
|
%\definecolor{blue}{rgb}{0,0,1}
|
|
%\definecolor{red}{rgb}{1,0,0}
|
|
%\definecolor{green}{rgb}{0,1,0.3}
|
|
%\definecolor{bluered}{rgb}{1,0,1}
|
|
%\definecolor{bluegreen}{rgb}{1,0.3,0}
|
|
%\newcommand{\black}[1]{\textcolor{black}{#1}}
|
|
%\newcommand{\red}[1]{\textcolor{red}{#1}}
|
|
%\newcommand{\blue}[1]{\textcolor{blue}{#1}}
|
|
%\newcommand{\green}[1]{\textcolor{green}{#1}}
|
|
%\newcommand{\bluered}[1]{\textcolor{bluered}{#1}}
|
|
%\newcommand{\bluegreen}[1]{\textcolor{bluegreen}{#1}}
|
|
\reversemarginpar
|
|
%\newcommand{\commentary}[1]{\marginpar[\tiny #1]{\tiny #1}}
|
|
%\newcommand{\commentaryforKlaeren}[1]{\marginpar[\tiny #1]{\tiny #1}}
|
|
\newcommand{\commentary}[1]{}
|
|
\newcommand{\commentaryforKlaeren}[1]{}
|
|
%\newcommand{\commentaryN}[1]{\marginpar[\tiny #1]{\tiny #1}}
|
|
\newcommand{\commentaryN}[1]{}
|
|
\newcommand{\subsec}[1]{\textbf{\medskip\\\large #1\medskip}}
|
|
%
|
|
% figure - Einstellungen
|
|
%
|
|
\def\textfraction{0}
|
|
\def\topfraction{1}
|
|
\def\bottomfraction{1}
|
|
\def\floatpagefraction{0}
|
|
\renewcommand{\floatpagefraction}{0.9}
|
|
%\def\dbltopfraction{1}
|
|
%\def\dblfloatpagefraction{1.0}
|
|
\newcommand{\indexentry}[2]{\item[] #1 \dotfill #2\qquad\qquad\vspace{-0.8em}}
|
|
\newcommand{\sub}{\textrm{\,$\sqsubseteq$\,}\xspace}
|
|
\newcommand{\nsub}{\text{\,$\not\sqsubseteq$\,}\xspace}
|
|
\newcommand{\ecap}{\mbox{$\,\sqcap\,$}}
|
|
\newcommand{\ecup}{\mbox{$\,\sqcup\,$}}
|
|
\newcommand{\pre}{\mbox{$\,\preceq\,$}}
|
|
\newcommand{\botam}{{\{\, \bot,\ \amalg \,\}}\xspace}
|
|
|
|
%
|
|
% Substitutions
|
|
%
|
|
\newcommand{\subst}{\textrm{$\expbf{subst}{\normaltset}$}}
|
|
|
|
%
|
|
% Signaturen
|
|
%
|
|
\def\einf#1#2{\mbox{$(#1,~#2)$}\xspace}
|
|
\newcommand{\sig}{\einf{\normalbtermset}{\Theta}}
|
|
\def\typesig{\einf{\simpletype}{TC}}
|
|
\newcommand{\einsig}{\einf{\normaltermset}{F}\xspace}
|
|
\newcommand{\msig}{\einsig}
|
|
\newcommand{\mssig}{\einf{\equivtermset}{F_{ms}}\xspace}
|
|
\newcommand{\ossig}{\einf{\normaltset, \sub}{F_{os}}\xspace}
|
|
\def\einfm#1#2{\langle #1,\ #2 \rangle}
|
|
\def\pos#1#2{\einf{#1,\ \sqsubseteq}{#2}}
|
|
\def\posm#1#2{\pos{#1}{#2}}
|
|
\def\posSO#1{\pos{#1}{F}}
|
|
\def\posSIG#1{\pos{S}{#1}}
|
|
\newcommand{\posig}{\pos{S}{\Sigma}}
|
|
\newcommand{\overposig}{\pos{\overline{S}}{\overline{\Sigma}}}
|
|
\def\fsf#1#2#3{\mbox{$#1^{(#2,#3)}$}\xspace}
|
|
\def\Sigmaa#1#2{\fsf{F}{#1}{#2}\xspace}
|
|
\newcommand{\Sigmaws}{\Sigmaa{w}{s}}
|
|
\newcommand{\Sigmawt}{\Sigmaa{w}{\theta}}
|
|
\def\mathrmtt#1{\mbox{\rm \texttt{#1}}}
|
|
\def\set#1{\{\,#1 \,\}}
|
|
\newcommand{\termset}[3]{\textrm{$\exp{#1_{#2}}{#3}$}\xspace}
|
|
\newcommand{\normaltset}{\termset{T}{\Theta}{TV}}
|
|
\newcommand{\normaltermset}{\termset{T}{\Theta}{TV}}
|
|
\newcommand{\simpletype}{\textrm{$\expsf{SType$_{\mathit{TS}}$}{BTV}$}\xspace}
|
|
\newcommand{\QMextends}[1]{\textrm{\tt ?\,extends}\,#1}
|
|
\newcommand{\QMextendsabbr}[1]{\textrm{\tt ?\,ext.}\,#1}
|
|
\newcommand{\QMsuper}[1]{\textrm{\tt ?\,super}\,#1}
|
|
\newcommand{\alltype}{\textrm{$\expsf{Type$_{\mathit{TS}}$}{BTV}$}\xspace}
|
|
\newcommand{\lambdatype}[2]{\textrm{$\#\, #1 \, (#2)$}}
|
|
\newcommand{\funtype}[3]{\textrm{\exptype{{\texttt{Fun}}\textit{#1}}{$#2 , #3$}}}
|
|
\newcommand{\funtypett}[3]{\textrm{\exptype{{\texttt{Fun}}\texttt{#1}}{$\mathtt{#2} , \mathtt{#3}$}}}
|
|
\newcommand{\functiontype}[2]{\textrm{\exptype{{{\texttt{Function}}}}{$#1,#2$}}}
|
|
\newcommand{\functiontypett}[2]{\textrm{\exptype{{\texttt{Function}}}{$\mathtt{#1} , \mathtt{#2}$}}}
|
|
\newcommand{\funtypestar}[3]{\textrm{\exptype{\texttt{Fun#1}\$\$}{$#2$,$ #3$}}}
|
|
\newcommand{\funtypestarsmall}[3]{\textrm{\exptype{\small\texttt{Fun#1}\$\$}{$#2, #3$}}}
|
|
\newcommand{\funtypestartt}[3]{\textrm{\exptype{{\texttt{Fun}}\texttt{#1\$\$}}{$\mathtt{#2} $,\linebreak[0]$\mathtt{#3}$}}}
|
|
%\newcommand{\funtypestartt}[3]{\textrm{\exptype{{\rm \texttt{Fun}}\texttt{#1}$*$}{$\mathtt{#2} , \mathtt{#3}$}}}
|
|
\newcommand{\funtypettsmall}[3]{\exptype{\smallmathtt{Fun{#1}}}{\smallmathtt{#2} ,\smallmathtt{#3}}}
|
|
\newcommand{\funtypestarttsmall}[3]{\exptype{\smallmathtt{Fun{#1}*}}{\mbox{\smallmathtt{#2},}\smallmathtt{#3}}}
|
|
\newcommand{\lambdatypett}[2]{\lambdatype{\mathtt{#1}}{\mathtt{#2}}}
|
|
\newcommand{\extsimpletype}{\textrm{$\expsf{ExtSType$_{\mathit{TS}}$}{BTV}$}\xspace}
|
|
\newcommand{\normalbtermset}{\termset{T}{TC}{BTV}}
|
|
\newcommand{\equivtermset}{\textrm{$\exp{T_{\Theta_{\sim}}}{TV}$}\xspace}
|
|
\newcommand{\equiva}[1]{[#1]_{\sim}}
|
|
\newcommand{\popoSIG}[1]{\einf{\normaltset,~\sqsubseteq}{#1}}
|
|
\newcommand{\poposig}{\popoSIG{F}}
|
|
%\newcommand{\poss}{polymorphically order-sorted signature\xspace}
|
|
%\newcommand{\posa}{polymorphically order-sorted algebra\xspace}
|
|
\newcommand{\polyosalg}{\textrm{\rm \textbf{PolyOSAlg}$_{\SigO}$}}
|
|
\newcommand{\polyalg}{\textrm{\rm \textbf{PolyAlg}$_{\SigM}$}}
|
|
\newcommand{\SigO}{\textrm{$\Sigma_{\textit{os}}$}\xspace}
|
|
\newcommand{\FuO}{\textrm{$F$}\xspace}
|
|
\newcommand{\SigM}{\textrm{$\Sigma_{\textit{ms}}$}\xspace}
|
|
\newcommand{\FuM}{\textrm{$F$}\xspace}
|
|
\newcommand{\Sig}{\textrm{$\Sigma$}\xspace}
|
|
\newcommand{\SigE}{\textrm{$\Sigma_{\textit{ext}}$}\xspace}
|
|
\newcommand{\objprogram}{\textrm{$<\Sig, \, E>$}\xspace}
|
|
|
|
%
|
|
% Algebren
|
|
%
|
|
\let\oldsqsubseteq=\sqsubseteq
|
|
\renewcommand{\sqsubseteq}{\leq}
|
|
\def\alg#1#2{\textrm{{\rm (}$#1;#2${\rm )}}\xspace}
|
|
\def\algm#1#2{(#1;#2)}
|
|
\def\algME#1{\alg{#1}{\alpha}}
|
|
\def\algABB#1{\alg{A}{#1}}
|
|
\def\algebra{\alg{A}{\alpha}}
|
|
\def\termalg{\mbox{$\algm{T_{\text{\rm posig}}}{\iota}$}}
|
|
\def\termalgm#1{\algm{T_{\text{#1}}}{\iota_{\text{#1}}}}
|
|
\def\OStermsetvar#1{\textrm{$T_{\SigO}#1$}\xspace}
|
|
\def\OStermset{\OStermsetvar{(V)}}
|
|
\def\OStset{\OStermsetvar{}\xspace}
|
|
\def\OStermsettypevar#1#2{\textrm{$T^{#1}_{\SigO}#2$}\xspace}
|
|
\def\OStermsettype#1{\OStermsettypevar{#1}{(V)}}
|
|
\def\ops{\exp{Ops}{A}}
|
|
\def\exp#1#2{#1(\,#2\,)\xspace}
|
|
%\def\exptt#1#2{\exp{\text{\tt #1}}{\text{\tt #2}}}
|
|
%\def\exptt#1#2{\exp{\texttt{#1}}{\texttt{#2}}}
|
|
\def\exptt#1#2{\exp{\mbox{$\mathtt{#1}$}}{\mbox{$\mathtt{#2}$}}}
|
|
\def\expsyn#1#2{\exp{\syn{#1}}{\syn{#2}}}
|
|
\def\expbf#1#2{\exp{\textbf{#1}}{#2}}
|
|
\def\expsf#1#2{\exp{\textsf{#1}}{#2}}
|
|
\newcommand{\exptype}[2]{\mathtt{#1 \texttt{<} #2 \texttt{>} }}
|
|
|
|
\def\exptypett#1#2{\texttt{#1<#2>}\xspace}
|
|
%\def\exptypett#1#2{\mathtt{#1}\mathrm{{\tt <}}\mathtt{#2}\mathrm{{\tt >}}\xspace}
|
|
\def\smalltt#1{\texttt{\small #1}}
|
|
\def\smallmathtt#1{\textrm{\small $\tt #1$}}
|
|
\def\term{\textrm{$\exp{f}{t_1, \ \ldots \ ,t_n}$}\xspace}
|
|
\def\hverbandm#1#2{\textrm{$(#1,~#2)$}}
|
|
\def\partord#1#2{\hverbandm{#1}{#2}\xspace}
|
|
\def\eval#1{eval_{\left<#1\right>}\xspace}
|
|
\def\evalA{$\eval{\algm{A}{\alpha}}$\xspace}
|
|
\def\la#1#2{\mbox{$\lambda#1.#2$}\xspace}
|
|
\def\set#1{\{\, #1 \,\}}
|
|
|
|
\newcommand{\inletters}[1]{
|
|
\ifx\the
|
|
first
|
|
\fi}
|
|
|
|
%\newcommand{\olsub}{\textrm{$\, \ol{\sqsubseteq} \,$}\xspace}
|
|
\newcommand{\olsub}{\textrm{$\, \leq^\ast \,$}\xspace}
|
|
\newcommand{\lessdotQM}{\textrm{$\,\lessdot_?\,$}}
|
|
\newcommand{\olsubneq}{\textrm{$\, \lneq^\ast \,$}\xspace}
|
|
\newcommand{\olsubprime}{\textrm{$\, \ol{\sqsubseteq}' \,$}\xspace}
|
|
\newcommand{\nolsub}{\textrm{$\, \not\sqsubseteq^* \,$}\xspace}
|
|
\newcommand{\hverband}{\partord{S}{\sqsubseteq}\xspace}
|
|
\newcommand{\qverband}{\partord{\exp{\ol{T}_{\Theta}}{V}}{\olsub}}
|
|
\newcommand{\cloqverband}{\partord{\exp{T_{\Theta}}{V}}{\olsub}}
|
|
\newcommand{\hord}{\mbox{$(S,~\sqsubseteq)$}\xspace}
|
|
\def\einschr#1{|_{#1}}
|
|
\def\uppereinschr#1{|^{#1}}
|
|
\def\lowereinschr#1{_{#1}\!|}
|
|
%\newcommand{\lsem}{[\hspace*{-0.3ex}[}
|
|
%\newcommand{\rsem}{]\hspace*{-0.3ex}]}
|
|
\newcommand{\lsem}{\llbracket\hspace{.5ex}}
|
|
\newcommand{\rsem}{\hspace{.5ex}\rrbracket}
|
|
\newcommand{\lsemm}{\lsem}
|
|
\newcommand{\rsemm}{\rsem}
|
|
\newcommand{\semantic}[1]{\lsem #1 \rsem\xspace}
|
|
\newcommand{\ol}[1]{\overline{#1}}
|
|
\newcommand{\ul}[1]{\underline{#1}}
|
|
\newcommand{\dps}{\displaystyle}
|
|
\newcommand{\sema}[3]{{\cal #1}_{#2}\semantic{#3}}
|
|
\newcommand{\sem}[2]{\sema{#1}{}{#2}\xspace}
|
|
|
|
% TI for FGJ wildcards
|
|
\newcommand\rulename[1]{\textup{\textsc{(#1)}}}
|
|
\newcommand{\generalizeRule}{General}
|
|
\newcommand{\generics}[1]{\ensuremath{\mathtt{\texttt{<} {#1} \texttt{>} }}}
|
|
\newcommand{\expr}[1]{\texttt{#1}}
|
|
\newcommand{\lessdotCC}{\ensuremath{\lessdot^{\texttt{c}}}}
|
|
|
|
\newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
|
|
\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
|
|
|
|
\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}}}
|
|
\newcommand{\wildcardEnv}{\ensuremath{\mathbb{W}}}
|
|
\newcommand{\wildcard}[3]{\ensuremath{\mathtt{#1 : [#3 .. #2]}}}
|
|
\newcommand{\wcNtype}[2]{\exists #1 .\ntype{#2}}
|
|
\newcommand{\wctype}[3]{\exists #1 .\exptype{#2}{#3}}
|
|
\newcommand{\wtype}[1]{\mathit{#1}}
|
|
\newcommand{\ntype}[1]{\mathtt{#1}}
|
|
|
|
\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
|
|
|
|
%
|
|
% Programming languages
|
|
%
|
|
|
|
\newcommand{\haskell}{\textsf{Haskell}\xspace}
|
|
\newcommand{\gofer}{\textsf{Gofer}\xspace}
|
|
\newcommand{\objp}{\mbox{\textsf{OBJ--P}}\xspace}
|
|
%\newcommand{\java}{\mbox{\textsf{G--JAVA}}\xspace}
|
|
\newcommand{\javafive}{\mbox{\textsf{Java 5}}\xspace}
|
|
\newcommand{\java}{\mbox{\textsf{Java}}\xspace}
|
|
\newcommand{\javaseven}{\mbox{\textsf{Java 7}}\xspace}
|
|
\newcommand{\javaeight}{\mbox{\textsf{Java 8}}\xspace}
|
|
\newcommand{\javaten}{\mbox{\textsf{Java 10}}\xspace}
|
|
\newcommand{\javatx}{\mbox{\textsf{Java-TX}}\xspace}
|
|
\newcommand{\javafx}{\mbox{\textsf{JavaFX}}\xspace}
|
|
\newcommand{\javalam}{\mbox{\textsf{Java}$_\lambda$}\xspace}
|
|
\newcommand{\javabyte}{\mbox{\textsf{Java Byte Code}}\xspace}
|
|
\newcommand{\jvm}{\mbox{\textsf{JVM}}\xspace}
|
|
%\newcommand{\oldjava}{\mbox{\textsf{JAVA}}\xspace}
|
|
\newcommand{\oldjava}{\mbox{\textsf{Java}}\xspace}
|
|
\newcommand{\pizza}{\mbox{\textsf{PIZZA}}\xspace}
|
|
\newcommand{\gj}{\mbox{\textsf{GJ}}\xspace}
|
|
\newcommand{\sml}{\mbox{\textsf{SML}}\xspace}
|
|
\newcommand{\ocaml}{\textsf{OCAML}}
|
|
\newcommand{\obj}{\mbox{\textsf{OBJ--3}}\xspace}
|
|
\newcommand{\objtwo}{\mbox{\textsf{OBJ--2}}\xspace}
|
|
\newcommand{\scala}{\mbox{\textsf{Scala}}\xspace}
|
|
|
|
\def\pot#1{{\cal P}(\, #1 \,)\xspace}
|
|
\def\partf{\overset{\text{\tiny part}}{\longrightarrow}\xspace}
|
|
%
|
|
% Deduktionssystem
|
|
%
|
|
\newcommand{\byrule}[1]{\raisebox{1.5ex}[0ex][0ex]{{{\rm [{\bf \small #1}]}}}}
|
|
\newcommand{\byruleok}[1]{\raisebox{1.5ex}[0ex][0ex]{{{\rm \small #1}}}}
|
|
\newcommand{\byrulewb}[1]{\raisebox{2.5ex}[0ex][0ex]{{{\rm [{\bf \small #1}]}}}}
|
|
\newcommand{\byruleokwb}[1]{\raisebox{2.5ex}[0ex][0ex]{{{\rm \small #1}}}}
|
|
\newcommand{\byrulesli}[1]{\raisebox{3.0ex}[0ex][0ex]{{{\rm [{\bf \small #1}]}}}}
|
|
\newcommand{\inter}[1]{\bigwedge \hspace{-.55em} \bigwedge_{#1}}
|
|
|
|
%
|
|
% ARRAY WITH ARGUMENTS
|
|
%
|
|
\newcommand{\sarray}[2]{\begin{array}[t]{#1} #2 \end{array}}
|
|
\newcommand{\sarrayt}[2]{\begin{array}[t]{#1} #2 \end{array}}
|
|
\newcommand{\sarrayb}[2]{\begin{array}[b]{#1} #2 \end{array}}
|
|
\newcommand{\sarrayc}[2]{\begin{array}[c]{#1} #2 \end{array}}
|
|
\newcommand{\sarrayo}[2]{\begin{array}{#1} #2 \end{array}}
|
|
|
|
%
|
|
% INFERENCE RULES
|
|
%
|
|
\newcommand{\byrulenew}[1]{\raisebox{2.1ex}[0ex][0ex]{{{\rm [{\bf \small #1}]}}}}
|
|
\newcommand{\postcond}[1]{\raisebox{2.1ex}[0ex][0ex]{#1}}
|
|
\newcommand{\lef}[1]{\multicolumn{1}{@{}l}{#1}}
|
|
\newcommand{\ri}[1]{\multicolumn{1}{r@{}}{#1}}
|
|
\newcommand{\ce}[1]{\multicolumn{1}{c}{#1}}
|
|
\newcommand{\axiom}[2]{\textrm{[}\textbf{\small #1}\textrm{]} & \lef{#2}}
|
|
\newcommand{\irule}[4]{&\multicolumn{1}{@{}l@{}}{\bf [#1]}\\ & \sarray{c}{#2}\vspace{1ex}\\\cline{2-2}
|
|
\vspace{-2ex}\\ %\byrulenew{#1}
|
|
& \sarray{c}{#3} & \postcond{$#4$}
|
|
}
|
|
\newenvironment{irules}{$\begin{array}{@{}l@{}c@{}l@{}}}{\end{array}$}
|
|
|
|
%
|
|
% Kategorien
|
|
%
|
|
\newcommand{\funs}[1]{\mbox{$F^S_{ERR}$(\, #1 \,)}\xspace}
|
|
\newcommand{\funa}[1]{\mbox{$F^A_{ERR}$(\, #1 \,)}\xspace}
|
|
\newcommand{\funh}[1]{\mbox{$F^H_{ERR}(\, #1 \,)$}\xspace}
|
|
|
|
%
|
|
% Typherleitungen
|
|
%
|
|
%\let\oldrhd=\rhd
|
|
%\newcommand{\rder}{\hspace*{0.5ex} \rhd_{\textrm{\tiny $\Sig$}} \hspace{0.5ex}}
|
|
\newcommand{\rder}{\hspace*{0.5ex} \rhd \hspace{0.5ex}}
|
|
%\newcommand{\lder}{\hspace*{0.5ex} \lhd_{\textrm{\tiny $\Sig$}} \hspace*{0.5ex}}
|
|
\newcommand{\lder}{\hspace*{0.5ex} \lhd \hspace*{0.5ex}}
|
|
\newcommand{\rderStmt}{\hspace*{0.5ex} \rhd_{Stmt} \hspace*{0.5ex}}
|
|
\newcommand{\rderExpr}{\hspace*{0.5ex} \rhd_{Expr} \hspace*{0.5ex}}
|
|
\newcommand{\rderIdent}{\hspace*{0.5ex} \rhd_{Id} \hspace*{0.5ex}}
|
|
|
|
\let\oldblacktriangleright=\blacktriangleright
|
|
%\newcommand{\fder}{\hspace*{1ex} \textrm{$\blacktriangleright_{\textsl{\tiny \hspace{-1ex}\Sig}}$}}
|
|
\newcommand{\fder}{\hspace*{1ex} \textrm{$\blacktriangleright$}}
|
|
|
|
\newcommand{\newtheo}[3]{\newtheorem{#1}[defhalbordnung]{#2}
|
|
\begin{#1} {\rm #3} \label{#1} \end{#1}}
|
|
\newcommand{\der}[2]{\mbox{$#1 \rhd\ #2$}\xspace}
|
|
\newcommand{\derl}[2]{#1 \lhd_{\textrm{\tiny $\Sig$}} #2\xspace}
|
|
\newcommand{\derr}[2]{#1 \rhd_{\textrm{\tiny \hspace{-1ex}$\Sig$}} #2\xspace}
|
|
\newcommand{\derf}[3]{( \, #1, \, #2 \, ) \fder #3\xspace}
|
|
|
|
\newcommand{\deri}[1]{\der{A}{K}{#1}\xspace}
|
|
\newcommand{\derif}[1]{\derf{A}{K}{D}{#1}\xspace}
|
|
\newcommand{\arity}[3]{\textrm{$\alpha^{(#1,#2)}_{#3}$}\xspace}
|
|
\newcommand{\coarity}[2]{\textrm{$\beta^{(#1,#2)}$}\xspace}
|
|
\newcommand{\sodaprg}{\textrm{$(\,\textsl{csig},\ D\,)$\xspace}}
|
|
|
|
%
|
|
% Typen
|
|
%
|
|
%\newcommand{\typ}[3]{\textrm{$ #1 \times \ldots \times #2 \rightarrow #3$}\xspace}
|
|
\newcommand{\typ}[3]{\textrm{$( #1 \ldo #2) \rightarrow #3$}\xspace}
|
|
\newcommand{\syn}[1]{{\rm \texttt{\small #1}}}
|
|
\newcommand{\sigmatyp}{\typ{\sigma_1}{\sigma_n}{\sigma}\xspace}
|
|
\newcommand{\sigmadef}{\mbox{$\sigma_1 \times \ldots \times \sigma_n$}\xspace}
|
|
\newcommand{\tautyp}{\typ{\tau_1}{\tau_n}{\tau}\xspace}
|
|
\newcommand{\tautypsup}[1]{\typ{\tau^{#1}_1}{\tau^{#1}_n}{\tau^{#1}}\xspace}
|
|
\newcommand{\taudef}{\mbox{$\tau_1 \times \ldots \times \tau_n$}\xspace}
|
|
\newcommand{\thetatyp}{\typ{\theta_1}{\theta_n}{\theta_0}\xspace}
|
|
\newcommand{\typea}{\text{$\text{TYPE}_T(\,S,\ V\,)$}\xspace}
|
|
\newcommand{\ptype}{\expsf{Type}{\normaltset}\xspace}
|
|
\newcommand{\ptypea}{\text{$\text{TYPE}_T(\,\Theta,\ V\,)$}\xspace}
|
|
\newcommand{\types}{\text{$\text{TYPE}_s(\,S,\ \Gamma\,)$}\xspace}
|
|
\newcommand{\extends}[1]{{}_{?}#1}
|
|
\newcommand{\super}[1]{{}^{?}#1}
|
|
|
|
\newcommand{\epsbox}[2]{
|
|
%\begin{center}
|
|
\setlength{\fboxsep}{4mm}
|
|
\fbox{\epsfxsize=#1 \epsfbox{#2}}
|
|
%\end{center}
|
|
}
|
|
|
|
\newcommand{\epsxybox}[3]{
|
|
\begin{minipage}[t]{#1}
|
|
\setlength{\fboxsep}{4mm}
|
|
\fbox{\epsfysize=#2 \epsfbox{#3}}
|
|
\end{minipage}}
|
|
|
|
\newenvironment{program}{\begin{alltt}\small}
|
|
{\normalsize\end{alltt}\vspace*{-1em}}
|
|
\floatstyle{plain}
|
|
\newfloat{soda}{htp}{lop}
|
|
\floatname{soda}{SODA-Program}
|
|
|
|
%\sodaprog
|
|
% 1. width
|
|
% 2. figure
|
|
% 3. file
|
|
\newcommand{\sodaprog}[3]{
|
|
\begin{figure}%[#2]
|
|
%\begin{center}
|
|
\begin{Sbox}
|
|
\begin{minipage}{#1}
|
|
\small
|
|
\begin{alltt}
|
|
\verbatiminput{#3.soda}
|
|
\end{alltt}
|
|
\normalsize
|
|
\end{minipage}
|
|
\end{Sbox}
|
|
\setlength{\fboxsep}{2mm}
|
|
\fbox{\TheSbox}
|
|
%\end{center}
|
|
\caption{SODA module \texttt{#3}}
|
|
\label{fig:#3}
|
|
\end{figure}
|
|
}
|
|
|
|
%
|
|
% Theorem
|
|
%
|
|
\newcommand{\QED}{\rule{1.1ex}{1.1ex}}
|
|
%\newenvironment{proof}{\par \bigskip \noindent {\bf Proof:}
|
|
% }{\mbox{ } \hfill \QED \par \smallskip}
|
|
%\newenvironment{remark}{\par \bigskip \noindent {\bf Remark}
|
|
% }{\par \smallskip}
|
|
%\newtheorem{definition}{Definition}[chapter]
|
|
%\newtheorem{example}[definition]{Example}
|
|
%\newtheorem{theorem}[definition]{Theorem}
|
|
%\newtheorem{corollary}[definition]{Corollary}
|
|
%\newtheorem{lemma}[definition]{Lemma}
|
|
%\newtheorem{algorithm}[definition]{Algorithm}
|
|
%\newenvironment{abstract}{\small \begin{center} {\bf Abstract}\\[2ex]
|
|
%\begin{minipage}{0.85\textwidth}}{\end{minipage} \end{center}}
|
|
\newenvironment{Zusammenfassung}{\small \begin{center} {\bf Zusammenfassung}\\[2ex]
|
|
\begin{minipage}{0.85\textwidth}}{\end{minipage} \end{center}}
|
|
\newlength{\level}
|
|
\newlength{\wid}
|
|
|
|
|
|
%\newcommand{\thelb}{
|
|
\def\notunlhd{\mathrel{\unlhd\!\!\!\!\!\mid}}
|
|
\def\In#1#2{#1 \! \in \! #2}
|
|
\def\Leq#1#2#3{#1 \! \leqslant \! #2 \! \leqslant \! #3}
|
|
\def\Lequ#1#2#3{#1 \leqslant #2 \leqslant #3}
|
|
\newcommand{\ma}[1]{\text{``}#1\text{''}\xspace}
|
|
\newcommand{\ttm}[1]{\mbox{\tt #1}\xspace}
|
|
\newcommand{\ret}[2]{\ttm{r}^{\ttm{\footnotesize #1}}_{\ttm{\footnotesize #2}}\xspace}
|
|
\newcommand{\retm}[2]{\ttm{r}^{#1}_{#2}\xspace}
|
|
\newcommand{\re}[2]{\displaystyle r^{#1}_{#2}\xspace}
|
|
\newlength{\qwert}
|
|
%\newcommand{\htext}[1]{\settowidth{\qwert}{#1} \addtolength{\qwert}{-0.65ex} \hspace*{\qwert}}
|
|
\newcommand{\htext}[1]{\settowidth{\qwert}{#1} \hspace*{\qwert}}
|
|
\newcommand{\leng}[1]{\settowidth{\qwert}{#1} \qwert}
|
|
\newcommand{\ldo}{, \ldots , }
|
|
\newcommand{\tvar}[1]{\textit{$\mathtt{#1}$}\xspace}
|
|
|
|
%
|
|
% Algorithmus
|
|
%
|
|
\newcommand{\nll}{\newline\hspace*{\level}}
|
|
\newcommand{\nlevel}{\addtolength{\level}{0.4cm}}
|
|
\newcommand{\llevel}{\addtolength{\level}{-0.4cm}}
|
|
\newcommand{\ifc}[1]{\textbf{if} \nlevel #1 \llevel}
|
|
\newcommand{\elsifc}[1]{\textbf{elsif} \nlevel #1 \llevel}
|
|
\newcommand{\foreachc}[2]{\textbf{foreach} #1 \nlevel #2 \llevel}
|
|
\newcommand{\thenc}[1]{\textbf{then} \nlevel #1 \llevel}
|
|
\newcommand{\ifthenc}[2]{\textbf{if} #1 \textbf{then} \nlevel #2 \llevel}
|
|
\newcommand{\elsec}[1]{\textbf{else} \nlevel #1 \llevel}
|
|
\newcommand{\eifc}{\textbf{endif}\\}
|
|
\newcommand{\casec}[2]{\fbox{\textbf{case} #1}\ \nlevel \nlevel #2 \llevel \llevel}
|
|
\newcommand{\letc}[2]{\textbf{let} \nlevel \\ #1 = \nlevel #2 \llevel \llevel}
|
|
\newcommand{\letbf}[1]{\textbf{let} \nlevel \\ #1 \llevel}
|
|
\newcommand{\inc}[1]{\textbf{in} \nlevel #1 \llevel \nopagebreak\\ \textbf{end}}
|
|
\newcommand{\lam}[2]{\textbf{fn } #1 \textrm{$\, \Rightarrow \,$} #2}
|
|
\newcommand{\inputc}[1]{\nll \textbf{Input:} \nlevel #1 \llevel}
|
|
\newcommand{\outputc}[1]{\nll \textbf{Output:} \nlevel #1 \llevel}
|
|
%\newcommand{\letforeachc}[3]{\textbf{let-foreach} \nlevel #1:\\ \ul{#2} = \nlevel #3 \llevel \llevel}
|
|
\newcommand{\letforeachc}[3]{\textbf{let-foreach} \nlevel #1:\\ #2 = \nlevel #3 \llevel \llevel}
|
|
%\newcommand{\letuc}[2]{\textbf{let} \nlevel \\ \ul{#1} = \nlevel #2 \llevel \llevel}
|
|
\newcommand{\letuc}[2]{\textbf{let} \nlevel \\ #1 = \nlevel #2 \llevel \llevel}
|
|
%\newcommand{\letu}[2]{\nlevel\\ \ul{#1} = \nlevel #2 \llevel\llevel}
|
|
\newcommand{\letu}[2]{\nlevel\\ #1 = \nlevel #2 \llevel\llevel}
|
|
\newcommand{\letnc}[2]{\nlevel\\ #1 = \nlevel #2 \llevel\llevel}
|
|
\newcommand{\misc}[1]{\nlevel\\ #1 \llevel}
|
|
\newcommand{\least}{\textrm{$\top$}\xspace}
|
|
\newenvironment{algocommands}{
|
|
\setlength{\level}{2mm}
|
|
\renewcommand{\\}{\nll}
|
|
\noindent
|
|
}{\renewcommand{\\}{\newline}
|
|
\vspace{1ex}
|
|
}
|
|
\newenvironment{algo}{\begin{algorithm} \rm %\mbox{}\\
|
|
\begin{algocommands}
|
|
}{\end{algocommands}
|
|
\end{algorithm}
|
|
}
|
|
|
|
\newenvironment{boxedalgo}{
|
|
\begin{Sbox}
|
|
\begin{minipage}{\textwid}
|
|
\begin{algo}
|
|
}{\end{algo}
|
|
\end{minipage}
|
|
\end{Sbox}
|
|
\fbox{\TheSbox}
|
|
}
|
|
|
|
%\newcommand{\red}[1]{\textcolor{red}{#1}}
|
|
%\newcommand{\blue}[1]{\textcolor{blue}{#1}}
|
|
%\newcommand{\green}[1]{\textcolor{green}{#1}}
|
|
%\newcommand{\bluered}[1]{\textcolor{bluered}{#1}}
|
|
%\newcommand{\bluegreen}[1]{\textcolor{bluegreen}{#1}}
|
|
\newcommand{\tabularfield}[1]{
|
|
\begin{tabular}{@{}l@{}}
|
|
#1
|
|
\end{tabular}
|
|
}
|
|
|
|
\newenvironment{Liste}{\begin{list}{\textbf{--}}{\setlength{\parsep}{0pt
|
|
plus0.0ex} \setlength{\itemsep}{0pt} \item[]}}{\end{list}}
|
|
|
|
\newenvironment{Listenullparsep}{\begin{list}{\textbf{--}}{
|
|
%\setlength{\topsep}{-5ex}
|
|
\setlength{\topsep}{0ex}
|
|
%\setlength{\parsep}{0pt plus1ex}
|
|
\setlength{\parsep}{0pt}
|
|
\setlength{\labelwidth}{2ex}
|
|
\setlength{\itemsep}{0pt}
|
|
\setlength{\leftmargin}{\labelsep +\labelwidth}
|
|
}}{\normalsize \end{list}}
|
|
|
|
|
|
%\landscapeonly
|
|
%\portraitonly
|
|
%\slidewidth9.7in
|
|
%\slideheight8.2in
|
|
%\slideframewidth0in
|
|
%\slideframesep0in
|
|
\newcounter{begriffnr}
|
|
\setcounter{begriffnr}{1}
|
|
\newcommand{\nextbegriff}[1]{\thebegriffnr. #1 \addtocounter{begriffnr}{1}}
|
|
|
|
\newcommand{\bflarge}[1]{\textbf{\large #1}}
|
|
\newcommand{\portraitslidey}[3]{
|
|
\begin{slide*}
|
|
\section*{#1}
|
|
\medskip
|
|
\begin{center}
|
|
\epsfysize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
\end{slide*}}
|
|
\newcommand{\portraitslidex}[3]{
|
|
\begin{slide*}
|
|
\section*{#1}
|
|
\medskip
|
|
\begin{center}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
\end{slide*}}
|
|
\newcommand{\landscapeslidex}[3]{
|
|
\landscapeslide{#1}{
|
|
\begin{center}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
}
|
|
}
|
|
\newcommand{\landscapeslidexoffset}[3]{
|
|
\landscapeslide{#1}{
|
|
\vspace*{-0.5cm}
|
|
\begin{center}
|
|
\hspace*{-2cm}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
}
|
|
}
|
|
\newcommand{\landscapeslidexlabel}[4]{
|
|
\begin{slide}
|
|
\section*{#1}
|
|
\medskip
|
|
\begin{center}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
#4
|
|
\end{slide}}
|
|
\newcommand{\landscapeslidexcomment}[4]{
|
|
\begin{slide}
|
|
\section*{#1}
|
|
\medskip
|
|
\begin{center}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
\comment{#4}
|
|
\end{slide}}
|
|
\newcommand{\landscapeslidexsubsub}[3]{
|
|
\begin{slide}
|
|
\subsubsection{#1}
|
|
\medskip
|
|
\begin{center}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
\end{slide}}
|
|
|
|
\newcommand{\landscapeslidextocsuboffset}[3]{
|
|
\landscapeslidetocsub{#1}{
|
|
\vspace*{-0.5cm}
|
|
\begin{center}
|
|
\hspace*{-2cm}
|
|
\epsfxsize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
}
|
|
}
|
|
\newcommand{\landscapeslidexoTnormal}[2]{
|
|
\begin{frame}
|
|
\begin{center}
|
|
\begin{minipage}[t]{#1}
|
|
%\vspace*{-5truecm}
|
|
%\vspace*{-2truecm}
|
|
\epsfxsize#1
|
|
%\hspace*{-5truecm}
|
|
%\hspace*{-3truecm}
|
|
\epsfbox{#2}
|
|
\end{minipage}
|
|
\end{center}
|
|
\end{frame}}
|
|
\newcommand{\landscapeslidexoT}[2]{\landscapeslidexoTXY{0cm}{0cm}{#1}{#2}}
|
|
\newcommand{\landscapeslidexoTXY}[4]{
|
|
\begin{frame}
|
|
\begin{center}
|
|
\begin{minipage}[t]{\textwidth}
|
|
\hspace*{#1}
|
|
\vspace*{#2}
|
|
\epsfxsize#3
|
|
\epsfbox{#4}
|
|
\end{minipage}
|
|
\end{center}
|
|
\end{frame}}
|
|
\newcommand{\landscapeslidexoTcomment}[3]{
|
|
\begin{slide}
|
|
\begin{center}
|
|
\begin{minipage}[t]{\slidewidth}
|
|
%\vspace*{-5truecm}
|
|
\vspace*{-2truecm}
|
|
\epsfxsize#1
|
|
%\hspace*{-5truecm}
|
|
\hspace*{-3truecm}
|
|
\epsfbox{#2}
|
|
\end{minipage}
|
|
\end{center}
|
|
\comment{#3}
|
|
\end{slide}}
|
|
\newcommand{\landscapeslidexoTlabel}[3]{
|
|
\begin{slide}
|
|
\begin{center}
|
|
\begin{minipage}[t]{\slidewidth}
|
|
%\vspace*{-5truecm}
|
|
\vspace*{-2truecm}
|
|
\epsfxsize#1
|
|
%\hspace*{-5truecm}
|
|
\hspace*{-3truecm}
|
|
\epsfbox{#2}
|
|
\end{minipage}
|
|
\end{center}
|
|
#3
|
|
\end{slide}}
|
|
\newcommand{\landscapeslideyoT}[2]{
|
|
\begin{slide}
|
|
\begin{center}
|
|
\begin{minipage}[t]{\slidewidth}
|
|
%\vspace*{-5truecm}
|
|
\vspace*{-3truecm}
|
|
\epsfysize#1
|
|
\hspace*{3truecm}
|
|
\epsfbox{#2}
|
|
\end{minipage}
|
|
\end{center}
|
|
\end{slide}}
|
|
\newcommand{\landscapeslidey}[3]{
|
|
\begin{slide}
|
|
\section*{#1}
|
|
\medskip
|
|
\begin{center}
|
|
\epsfysize#2
|
|
\epsfbox{#3}
|
|
\end{center}
|
|
\end{slide}}
|
|
|
|
%\newcommand{\landscapeslide}[2]{
|
|
% \begin{slide}
|
|
% \section*{#1}
|
|
% \medskip
|
|
|
|
% #2
|
|
% \end{slide}}
|
|
|
|
\newcommand{\landscapeslide}[2]{
|
|
\frame{
|
|
\frametitle{#1}
|
|
#2
|
|
}
|
|
}
|
|
|
|
\newcommand{\landscapeslidetocsub}[2]{
|
|
\subsection{#1}
|
|
\landscapeslide{#1}{#2}
|
|
}
|
|
\newcommand{\landscapeslidetocsubsub}[2]{
|
|
\begin{slide}
|
|
\subsubsection{#1}
|
|
\medskip
|
|
|
|
#2
|
|
\end{slide}}
|
|
|
|
\newcommand{\landscapeslidetoc}[3]{
|
|
\section{#1}
|
|
\landscapeslide{#2}{#3}
|
|
}
|
|
\newcommand{\landscapeslidetoctitle}[2]{
|
|
\landscapeslidetoc{#1}{#1}{#2}
|
|
}
|
|
\newenvironment{landscapeslideenv}[1]{
|
|
\begin{frame}
|
|
\frametitle{#1}
|
|
}
|
|
{\end{frame}}
|
|
|
|
\def\landscapesl#1{
|
|
\begin{slide}
|
|
\section*{#1}
|
|
\medskip}
|
|
|
|
%1.Breite links
|
|
%2.Inhalt links
|
|
%3.Breite oben rechts
|
|
%4.Inhalt oben rechts
|
|
%5. Inhaly Folie
|
|
\newcommand{\landscapeslideObenBild}[5]{
|
|
\begin{frame}
|
|
\frametitle{#2}
|
|
\begin{minipage}[b]{#1}
|
|
#5
|
|
\end{minipage}
|
|
\hfill
|
|
\parbox[b][\textheight-1cm]{#3}{
|
|
%\begin{minipage}[b]{#3}
|
|
\setlength{\epsfxsize}{#3}
|
|
\epsfbox{#4}
|
|
%\end{minipage}
|
|
\vfill
|
|
}
|
|
%#5
|
|
\end{frame}}
|
|
|
|
\newcommand{\portraitslide}[2]{
|
|
\begin{slide*}
|
|
\section*{#1}
|
|
\medskip
|
|
#2
|
|
\end{slide*}}
|
|
|
|
\definecolor{black}{rgb}{0,0,0}
|
|
\definecolor{blue}{rgb}{0,0,1}
|
|
\definecolor{blueA}{rgb}{0.2,0,0.4}
|
|
\definecolor{blueB}{rgb}{0.2,0,0.6}
|
|
\definecolor{blueC}{rgb}{0.2,0,0.8}
|
|
\definecolor{blueD}{rgb}{0.2,0,1.0}
|
|
\definecolor{blueE}{rgb}{0,0,0.8}
|
|
\definecolor{red}{rgb}{1,0,0}
|
|
\definecolor{redA}{rgb}{0.6,0,0.2}
|
|
\definecolor{green}{rgb}{0,1,0.3}
|
|
\definecolor{greenA}{rgb}{0.2,0.6,0}
|
|
\definecolor{greenB}{rgb}{0.2,0.6,0.2}
|
|
\definecolor{greenC}{rgb}{0.2,0.6,0.4}
|
|
\definecolor{bluered}{rgb}{1,0,1}
|
|
\definecolor{blueredB}{rgb}{0.4,0,0.6}
|
|
\definecolor{blueredC}{rgb}{0.4,0,1}
|
|
\definecolor{blueredD}{rgb}{0.6,0,1}
|
|
\definecolor{bluegreen}{rgb}{0.8,0.5,0}
|
|
\definecolor{yellow}{rgb}{1,1,0}
|
|
\definecolor{yellowA}{rgb}{1,0.8,0}
|
|
\definecolor{yellowB}{rgb}{1,0.6,0}
|
|
\definecolor{yellowC}{rgb}{1,0.4,0}
|
|
\definecolor{gray}{rgb}{0.662,0.662,0.662}
|
|
\definecolor{grayA}{rgb}{0.9,0.9,0.9}
|
|
\newcommand{\black}[1]{\textcolor{black}{#1}}
|
|
\newcommand{\red}[1]{\textcolor{red}{#1}}
|
|
\newcommand{\DHBWred}[1]{\textcolor{DHBWrot}{#1}}
|
|
\newcommand{\redA}[1]{\textcolor{redA}{#1}}
|
|
\newcommand{\blue}[1]{\textcolor{blue}{#1}}
|
|
\newcommand{\blueA}[1]{\textcolor{blueA}{#1}}
|
|
\newcommand{\blueB}[1]{\textcolor{blueB}{#1}}
|
|
\newcommand{\blueC}[1]{\textcolor{blueC}{#1}}
|
|
\newcommand{\blueD}[1]{\textcolor{blueD}{#1}}
|
|
\newcommand{\blueE}[1]{\textcolor{blueE}{#1}}
|
|
\newcommand{\green}[1]{\textcolor{green}{#1}}
|
|
\newcommand{\bluered}[1]{\textcolor{bluered}{#1}}
|
|
\newcommand{\blueredB}[1]{\textcolor{blueredB}{#1}}
|
|
\newcommand{\blueredC}[1]{\textcolor{blueredC}{#1}}
|
|
\newcommand{\blueredD}[1]{\textcolor{blueredD}{#1}}
|
|
\newcommand{\bluegreen}[1]{\textcolor{bluegreen}{#1}}
|
|
\newcommand{\greenA}[1]{\textcolor{greenA}{#1}}
|
|
\newcommand{\greenB}[1]{\textcolor{greenB}{#1}}
|
|
\newcommand{\greenC}[1]{\textcolor{greenC}{#1}}
|
|
\newcommand{\yellow}[1]{\textcolor{yellow}{#1}}
|
|
\newcommand{\yellowA}[1]{\textcolor{yellowA}{#1}}
|
|
\newcommand{\yellowB}[1]{\textcolor{yellowB}{#1}}
|
|
\newcommand{\yellowC}[1]{\textcolor{yellowC}{#1}}
|
|
\newcommand{\gray}[1]{\textcolor{gray}{#1}}
|
|
\newcommand{\grayA}[1]{\textcolor{grayA}{#1}}
|