diff options
author | Karl Berry <karl@freefriends.org> | 2019-02-17 23:02:19 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2019-02-17 23:02:19 +0000 |
commit | 9337ead45078f53688180eb292f26766703110d9 (patch) | |
tree | a1927cdffdcf1016b3d884f39e48558b9f2c8438 /Master/texmf-dist/doc | |
parent | 8c3bfc326ff7064c4b80a6b4c7fc2053aa4672cc (diff) |
rec-thy (17feb19)
git-svn-id: svn://tug.org/texlive/trunk@50047 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc')
-rw-r--r-- | Master/texmf-dist/doc/latex/rec-thy/rec-thy.pdf | bin | 114232 -> 178442 bytes | |||
-rw-r--r-- | Master/texmf-dist/doc/latex/rec-thy/rec-thy.tex | 129 |
2 files changed, 97 insertions, 32 deletions
diff --git a/Master/texmf-dist/doc/latex/rec-thy/rec-thy.pdf b/Master/texmf-dist/doc/latex/rec-thy/rec-thy.pdf Binary files differindex f16d2aa585c..beb678f7008 100644 --- a/Master/texmf-dist/doc/latex/rec-thy/rec-thy.pdf +++ b/Master/texmf-dist/doc/latex/rec-thy/rec-thy.pdf diff --git a/Master/texmf-dist/doc/latex/rec-thy/rec-thy.tex b/Master/texmf-dist/doc/latex/rec-thy/rec-thy.tex index a5e256e8ad0..8fb6f3cbf21 100644 --- a/Master/texmf-dist/doc/latex/rec-thy/rec-thy.tex +++ b/Master/texmf-dist/doc/latex/rec-thy/rec-thy.tex @@ -53,7 +53,9 @@ \usepackage{multirow} \usepackage{booktabs} \usepackage{xtab} -\usepackage{rec-thy} + +\usepackage[suppPriorityTrees]{rec-thy} +\usepackage{suffix} \usepackage{metalogo} @@ -112,6 +114,33 @@ Include the package in your document by placing \verb=\usepackage{rec-thy}= into Significant use is made in this package of optional arguments delimited either by square brackets or parenthesis. Users of the package should take care to wrap arguments that may themselves include brackets or parenthesis in braces. For example \verb=\REset(\REset(X){e}){i}= should be fixed to \verb=\REset({\REset(X){e}}){i}=. +\section{Alternate Symbols} +While the symbols used by default in the package are suggested for adoption to achieve greater consistency users may wish to specify their own symbols and options have been provided to enable this. The following parameters may be specified. + +\begin{itemize} + \item[modulescr] Sets the script used to typeset the \verb=\module= command. Default is mathcal. + \item[reqscr] Sets the script used to typeset requirements. Default is mathscr. + \item[pfcasefont] Sets the script used to typeset Case in the cases helper. + \item[emptystr] Sets the empty string symbol + \item[concatsym] Sets the concat symbol. + \item[cdeltasym] Sets the symbol used to denote computably \( \Delta \) formulas. Default is \( \prescript{\mathcal{C}}{}{\Delta} \). + \item[cpisym] Same for \( \Pi \) formulas. Default is \( \prescript{\mathcal{C}}{}{\Pi} \). + \item[csigmasym] Same for \( \Sigma \) formulas. Default is \( \prescript{\mathcal{C}}{}{\Sigma} \). + \item[recfnlsym] Sets the symbol used for recursive functionals. Default is \( \Phi \). + \item[recfsym] Sets the symbol used for recursive functions. Default is \( \phi \). + \item[usesym] Sets the symbol used for the use operator. Default is \( \symbffrak{u} \) where this is printed using \verb=\symbfrak= if unicode-math is loaded and with \verb=\mathfrak= otherwise. + \item[ballsymb] Sets the symbol used for the ball command. Default is \( \mathscr{B} \). +\end{itemize} + +As an example of how to use these commands consider the following code changing the ball symbol to \( \mathbf{B} \). + +\begin{verbatim} +\def\myballsymb{\mathbf{B}} + +\usepackage[suppPriorityTrees, ballsymb=myballsymb]{rec-thy} +\end{verbatim} + + \section{Commands} A few general conventions are usually followed in the commands. Whenever an operator can be used as a binary operator (as in \( X \union Y \)) and as an operation on some collection \( \Union_{i \in \omega} X_i \) the binary operator will begin with a lowercase letter \verb=\union= and the operation on the collection will begin with a capital letter \verb=\Union=. If the first letter is already capitalized then the second letter is used instead. @@ -122,21 +151,28 @@ Unless indicated otherwise all macros are to be used inside math mode. Indented \subsection{Priority Trees} -Note the commands in this section double as suggestions for standardized notation. +Note the commands in this section double as suggestions for standardized notation. \begin{xtabular}{l | l | l}\toprule - \verb=\PriorityTree= & \( \PriorityTree \) & Truepath. \\ \midrule + \verb=\PriorityTree= & \( \PriorityTree \) & Priority Tree \\ \midrule \verb=\tpath= & \( \tpath \) & Truepath. \\ \midrule \verb=\tpath[s]= & \( \tpath[s] \) & Approximate Truepath. \\ \midrule \verb=\xi \leftof \eta = & \( \xi \leftof \eta \) & The left of relation for priority tree arguments \\ \midrule - \verb=\Astages{\xi}= & \( \Astages{\xi} \) & Set of stages at which \( \xi \) is active. \\ \midrule - \verb=\Vstages{\xi}= & \( \Vstages{\xi} \) & Stages where \( \xi \subfun \tpath[s] \) even if links skip \( \xi \). \\ \midrule - \verb=\reqof{\xi}= & \( \reqof{\xi} \) & Requirement implemented by a node \( \xi \). \\ \midrule + \verb=\module{R}[X]{i,j}= & \module{R}{i,j} & Module in tree construction (superscript optional arg) \\ \midrule \verb=\ball[X]{y}{s}= & \( \ball[X]{y}{s} \) & Location of ball \( y\) (headed to \( X \)) at \( s \)\\ \midrule \verb=\ball{y}{s}= & \( \ball{y}{s} \) & Location of ball \( y\) at \( s \)\\ \bottomrule \end{xtabular} \\ +There are a few additional commands relating to priority trees which are less frequently used and require passing the option \verb=suppPriorityTrees= to the package to use. These commands exist in a kind of limbo and will probably be removed in some future edition of the package absent popular demand and feedback for better notation. + +\begin{xtabular}{l | l | l}\toprule + \verb=\Astages{\xi}= & \( \Astages{\xi} \) & Set of stages at which \( \xi \) is active. \\ \midrule + \verb=\Vstages{\xi}= & \( \Vstages{\xi} \) & Stages where \( \xi \subfun \tpath[s] \) even if links skip \( \xi \). \\ \midrule + \verb=\reqof{\xi}= & \( \reqof{\xi} \) & Requirement implemented by a node \( \xi \). \\ \bottomrule +\end{xtabular} + + \subsection{Computations} To disable these commands pass the option \verb=nocomputations=. \\ To specify an alternative symbol for either recursive functionals or recursive functions pass \verb!recfnlsym=macroname! or \verb!recfsym=macroname!. For instance, to use \( \psi \) for recursive functions and \( \Psi \) for recursive functionals pass the options \verb!recfsym=psi, recfnlsym=Psi!. @@ -146,10 +182,10 @@ To disable these commands pass the option \verb=nocomputations=. \\ To specify \verb=\recf[s]{e}= & \( \recf[s]{e} \) & \\[6pt] \verb=\recf{e}(x)= & \( \recf{e}(x) \) & \\[6pt] \verb=\recf[s]{e}(x)= & \( \recf[s]{e}(x) \) & \\[6pt] - \verb=\recf{e}[Y]= & \( \recf{e}[Y] \) & \\[6pt] - \verb=\recf[s]{e}[Y]= & \( \recf[s]{e}[Y] \) & \\[6pt] - \verb=\recf{e}[Y](x)= & \( \recf[s]{e}[Y](x) \) & \\[6pt] - \verb=\recf[s]{e}[Y](x)= & \( \recf[s]{e}[Y](x) \) & \\[6pt] + \verb=\recf(Y){e}= & \( \recf(Y){e} \) & \\[6pt] + \verb=\recf[s](Y){e}= & \( \recf[s](Y){e} \) & \\[6pt] + \verb=\recf(Y){e}(x)= & \( \recf(Y){e}(x) \) & \\[6pt] + \verb=\recf[s](Y){e}(x)= & \( \recf[s](Y){e}(x) \) & \\[6pt] \verb=\recfnl{e}{Y}{x}= & \( \recfnl{e}{Y}{x} \) &\multirow{4}{*}{Computable functionals} \\[6pt] \verb=\recfnl[s]{e}{Y}{x}= & \( \recfnl[s]{e}{Y}{x} \) & \\[6pt] \verb=\recfnl{e}{Y}{}= & \( \recfnl{e}{Y}{} \) & \\[6pt] @@ -195,14 +231,19 @@ To disable these commands pass the option \verb=nodegrees=. \\ \tab \verb=X \Teq Y= & & \\ \midrule \verb=X \nTequiv Y= & \multirow{2}{*}{\( X \nTequiv Y \)} & \multirow{2}{*}{Turing inequivalence} \\ \tab \verb=X \nTeq Y= & & \\ \midrule - \verb=X \Tlneq Y= & \( X \Tlneq Y \) & \\ \midrule - \verb=X \Tleq Y= & \( X \Tleq Y \) & \\ \midrule - \verb=X \Tgneq Y= & \( X \Tgneq Y \) & \\ \midrule - \verb=X \Tgeq Y= & \( X \Tgeq Y \) & \\ \midrule - \verb=X \Tgtr Y= & \( X \Tgtr Y \) & \\ \midrule - \verb=X \Tless Y= & \( X \Tless Y \) & \\ \midrule - \verb=X \nTleq Y= & \( X \nTleq Y \) & \\ \midrule - \verb=X \nTgeq Y= & \( X \nTgeq Y \) & \\ \midrule + \verb=X \Tlneq Y= & \( X \Tlneq Y \) & \\ \midrule + \verb=X \Tleq Y= & \( X \Tleq Y \) & \\ \midrule + \verb=X \Tgneq Y= & \( X \Tgneq Y \) & \\ \midrule + \verb=X \Tgeq Y= & \( X \Tgeq Y \) & \\ \midrule + \verb=X \Tgtr Y= & \( X \Tgtr Y \) & \\ \midrule + \verb=X \Tless Y= & \( X \Tless Y \) & \\ \midrule + \verb=X \nTleq Y= & \( X \nTleq Y \) & \\ \midrule + \verb=X \nTgeq Y= & \( X \nTgeq Y \) & \\ \midrule + \verb=X \Tincompat Y= & \multirow{2}{*}{\( X \Tincompat Y \)} & Turing incompatibility \\ + \tab \verb=X \Tincomp Y= & & \\ \midrule + \verb=X \Tcompat Y= & & \multirow{3}{*}{\( X \Tcompat Y \)} \\ + \tab \verb=X \nTincomp Y= & & \\ + \tab \verb=X \nTincompat Y= & & \\ \midrule \verb=\Tdeg{d} \Tdegjoin \Tdeg{d'}= & \( \Tdeg{d} \Tdegjoin \Tdeg{d'} \) & Join of degrees\\ \midrule \verb=\Tdeg{d} \Tdegmeet \Tdeg{d'}= & \multirow{2}{*}{\( \Tdeg{d} \Tdegmeet \Tdeg{d'} \)} & \multirow{2}{*}{Meet of degrees (when defined)} \\ \tab \verb=\Tdeg{d} \Tmeet \Tdeg{d'}= & & \\ \midrule @@ -228,13 +269,13 @@ Math mode is not required for \verb=\req{R}{e\}= \begin{tabular}{l | l | l}\toprule \verb=\req{R}{e}= & \( \req{R}{e} \) & \multirow{3}{*}{Requirement } \\ \midrule -\verb=\req[\nu]{R}{e\}= & \req[\nu]{R}{e} & \\ \midrule +\verb=\req{R}[\nu]{e\}= & \req{R}[\nu]{e} & \\ \midrule \verb=\req*{R}{e\}= & \req{R}{e} & \multirow{3}{*}{Requirement without hyperlinks} \\ \midrule -\verb=\req*[\nu]{R}{e\}= & \req[\nu]{R}{e} & \\ \midrule +\verb=\req*{R}[\nu]{e\}= & \req{R}[\nu]{e} & \\ \midrule \bottomrule \end{tabular} \\ -We also introduce the following two enviornments for introducing requirements. The requirement enviornment is used as follows +We also introduce the following environments for introducing requirements. The requirement environment is used as follows \begin{lstlisting}[breaklines] \begin{requirement}{\req{R^{*}}{r,j}} @@ -248,7 +289,7 @@ Giving output \recfnl{r}{B}{} = \REset{j} \implies \exists[k] \left( \Upsilon^{j}_k(C \Tplus \REset{j}) = B) \lor \REset{j} \Tleq \Tzero \right) \end{requirement} -The require environment merges the \verb=\req[\nu]{R}{e\}= command directly into the environment arguments. It also creates an automatic label which makes use of the 1st and 2nd arguments but assumes the third argument contains only indexes whose names are subject to change. Unless \verb=nohyperreqs= is passed the \verb=\req[\nu]{R}{e\}= automatically links to the defining require enviornment. +The require environment merges the \verb=\req[\nu]{R}{e\}= command directly into the environment arguments. It also creates an automatic label which makes use of the 1st and 2nd arguments but assumes the third argument contains only indexes whose names are subject to change. Unless \verb=nohyperreqs= is passed the \verb=\req[\nu]{R}{e\}= automatically links to the defining require environment. \begin{lstlisting}[breaklines] \begin{require}{R}{i} @@ -262,6 +303,22 @@ The require environment merges the \verb=\req[\nu]{R}{e\}= command directly into \recfnl{i}{B}{} = \REset{i} \implies \exists[k] \left( \Upsilon^{i}_k(C \Tplus \REset{i}) = B) \lor \REset{j} \Tleq \Tzero \right) \end{require} +To list multiple requirements at once without introducing unnecessary spaces we also introduce the requirements environment which can be used as follows. Note that one may \textit{not} end the final line with a linebreak or an undesired tag will appear. + +\begin{lstlisting}[breaklines] +\begin{requirements} +\require{P}[A]{e} A \neq \recfnl{i}{}{} \\ +\require{P}[B]{e} B \neq \recfnl{i}{}{} \\ +\require{R}{i,\hat{i},j,\hat{j}} \recfnl{i}{A}{} = \hat{A} \land \recfnl{\hat{i}}{\hat{A}}{} = A \land \recfnl{j}{B}{} = \hat{B} \land \recfnl{\hat{j}}{\hat{B}}{} = B \implies \Gamma(\hat{A} \symdiff \hat{B}) = A \Tplus B +\end{requirements} +\end{lstlisting} + +\begin{requirements} +\require{P}[A]{e} A \neq \recfnl{i}{}{} \\ +\require{P}[B]{e} B \neq \recfnl{i}{}{} \\ +\require{R}{i,\hat{i},j,\hat{j}} \recfnl{i}{A}{} = \hat{A} \land \recfnl{\hat{i}}{\hat{A}}{} = A \land \recfnl{j}{B}{} = \hat{B} \land \recfnl{\hat{j}}{\hat{B}}{} = B \implies \Gamma(\hat{A} \symdiff \hat{B}) = A \Tplus B +\end{requirements} + @@ -273,10 +330,6 @@ To disable these commands pass the option \verb=nomath=. \\ \verb=\iffdef= & \( \iffdef \) & Definitional equivalence\\ \midrule \verb=\aut= & \( \aut \) & Automorphisms of some structure\\ \midrule \verb=\Ord= & \( \Ord \) & Set of ordinals\\\midrule - \verb=x \meet y= & \( x \meet y \) & \multirow{2}{*}{Meet operation} \\[6pt] - \verb=\Meet_{i\in \omega} x_i= & \( \Meet_{i\in \omega} x_i \) & \\ \midrule - \verb=x \join y= & \(x \join y \) & \multirow{2}{*}{Join operation} \\[6pt] - \verb=\Join_{i\in \omega} x_i= & \( \Join_{i\in \omega} x_i \) & \\ \midrule \verb=\abs{x}= & \( \abs{x} \) & Absolute value\\ \midrule \verb=\dom= & \( \dom \) & Domain \\ \midrule \verb=\rng= & \( \rng \) & Range\\ \midrule @@ -289,10 +342,21 @@ To disable these commands pass the option \verb=nomath=. \\ \tab \verb=f \compose g= & &\\ \midrule \verb=\( \ensuretext{blah} \)= & \multirow{2}{*}{\( \ensuretext{blah} \)}& \multirow{2}{*}{Types argument in text mode} \\ \tab \verb=\ensuretext{blah}= & & \\ - \bottomrule \end{tabular} \\ \newpage + +\subsection{Operators} +Misc operators used in logic and computability. To disable these commands pass the option \verb=nooperators=.\\ + +\begin{tabular}{l | l | l}\toprule +\verb=x \meet y= & \( x \meet y \) & \multirow{2}{*}{Meet operation} \\[6pt] + \verb=\Meet_{i\in \omega} x_i= & \( \Meet_{i\in \omega} x_i \) & \\ \midrule + \verb=x \join y= & \(x \join y \) & \multirow{2}{*}{Join operation} \\[6pt] + \verb=\Join_{i\in \omega} x_i= & \( \Join_{i\in \omega} x_i \) & \\ \midrule + \verb=x \xor y= & \( x \xor y \) & \\ \bottomrule +\end{tabular} \\ + \subsection{Set Notation} To disable these commands pass the option \verb=nosets=.\\ @@ -300,7 +364,6 @@ Note that \verb=\Cross= and \verb=\cross= overwrite the existing commands saving \begin{tabular}{l | l | l}\toprule \verb=\set{(x,y)}{x > y}= & \( \set{(x,y)}{x > y} \) & \multirow{2}{*}{Set notation} \\[6pt] - \verb=\set{(x,y)}{}= & \( \set{(x,y)}{} \) & \\ \midrule \verb=\set{(x,y)}= & \( \set{(x,y)} \) & \\ \midrule \verb=\card{X}= & \( \card{X} \) & Cardinality \\ \midrule \verb=X \union Y= & \( X \union Y \) & \multirow{2}{*}{Union} \\[6pt] @@ -314,9 +377,9 @@ Note that \verb=\Cross= and \verb=\cross= overwrite the existing commands saving \verb=x \nin A= & \( x \nin A \) & not an element\\ \midrule \verb=\setcmp{X}= & \( \setcmp{X} \) & Set compliment\\\midrule \verb=X \setdiff Y= & \( X \setdiff Y \) & Set difference \\ \midrule - \verb=X \symdiff Y= & \( X \symdiff Y \) & Symmetric difference \\ \midrule - \verb=\interior X= & \( \interior X \) & Interior \\ \midrule - \verb=\closure X= & \( \closure X \) & Closure \\ \midrule + \verb=X \symdiff Y= & \( X \symdiff Y \) & Symmetric difference \\ \bottomrule + % \verb=\interior X= & \( \interior X \) & Interior \\ \midrule + % \verb=\closure X= & \( \clos X \) & Closure \\ \midrule \bottomrule \end{tabular} \\ @@ -420,7 +483,7 @@ To specify an alternative symbol for the empty string pass \verb!emptystr=macron To disable these commands pass the option \verb=nosubfuns=.\\ \begin{tabular}{l | l | l}\toprule - \verb=f \subfun g= & \( f \subfun g \) & \multirow{8}{*}{Varities of the function extension relation} \\ \midrule + \verb=f \subfun g= & \( f \subfun g \) & Varieties of the function extension relation \\ \midrule \verb=f \supfun g= & \( f \supfun g \) & \\ \midrule \verb=f \nsubfun g= & \( f \nsubfun g \) & \\ \midrule \verb=f \nsupfun g= & \( f \nsupfun g \) & \\ \midrule @@ -616,6 +679,8 @@ Finally to enable the mrref helper macros pass the option \verb=mrref=.\\ These \section{Release Notes} \begin{itemize} + \item[3.01] 02/17/2019 - Fixed \verb=\RE= \verb=\CE= \verb=\Re= and \verb=\Ce= for the various capitalized versions. Fixed weird bug with \verb=\recfnl= no longer working based on let. Removed \verb=\interior= and \\verb=\closure= as not really appropriate commands for the package and having bugs. Also fixed package to have correct version. + \item[3.0] 02/16/2019 - Added requirements environment for multiple requirements. Changed the \verb=\req= and \verb=\require= commands to take their optional argument after the first mandatory arguments as well as before. Added the commands \verb=\module= and \verb=\modof= and \verb=\xor=. Improved the corner quotes. Added \verb=\leftofeq=, \verb=\rightof=, \verb=\rightofeq=. Added \verb=\RE=, \verb=\CE=, \verb=\Ce=, \verb=\Re= and \verb=\Tincompat=, \verb=\Tincomp=, \verb=\Tcompat=. Changed the way strings are symbolized and coded. Fixed suffix commands to work with unicode-math. Also added \verb=\require*= inside \verb=\requirements=. Added \verb=\nleftofeq=, \verb=\nrightof=, \verb=\nrightofeq=, \verb=\nleftof=. The commands \verb=\ancestor=, \verb=\descendant= etc... \verb=\reqof=, \verb=\Astages= and \verb=\Vstages=now require the option suppPriorityTrees be passed to the class to use and should be viewed as depreciated. Fixed the options system so different symbols can be correctly passed to the class. Changed the way \verb=\recf= works to comply with the usual syntax. \item[2.4.3] 11/29/2018 - Rendered compatible with beamer by removing enumitem requirement if beamer is loaded. \item[2.4.2] 11/29/2018 - Fixed horrible bugs introduced in last version and fixed many symbols to work even in pdflatex mode. Also have everything compiling again. \item[2.4.1] 2/14/2018 - Moved to using xparse to define the case macros and several other macros to allow nested brackets for optional arguments. Added the recf command and cleaned up some option processing. Also worked around the mathtools/unicode-math font bug described \href{https://tex.stackexchange.com/questions/335164/incompatibility-with-mathtools-and-unicode-math-in-xelatex/335177}{here} |