Skip to content

Commit

Permalink
Documentation: Removes unnecessary enumitem package in stepper specs (#…
Browse files Browse the repository at this point in the history 
…1574)

* bumping version

* removing unnecessary enumitem package
  • Loading branch information
@martin-henz
martin-henz authored Mar 5, 2024
1 parent fa17dc7 commit 2b0992d
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 65 deletions.
79 changes: 15 additions & 64 deletions docs/specs/source_2_stepper_rules.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ \subsection*{Programs}
\sEntry{Program-intro}{In a sequence of statements, we can always reduce the
first one that isn't a value statement.}
\gentzen{
\sVar{statement} \rightarrow \sVar{statement}'
\sVar{statement} \Rightarrow \sVar{statement}'
}{
[\sVar{value}\sKw{;}]\sKw{ }\sVar{statement}\ldots \Rightarrow
[\sVar{value}\sKw{;}]\sKw{ }\sVar{statement}'\ldots
Expand Down Expand Up @@ -376,7 +376,7 @@ \subsection*{Expresssions: Blocks}
return \sVar{return-expression};
\sVar{statement}$\ldots$\}
}
\rightarrow
\Rightarrow
\sCode{
\{return \sVar{return-expression}; \sVar{statement}$\ldots$\}
}
Expand All @@ -402,7 +402,7 @@ \subsection*{Expresssions: Blocks}
\gentzen{}{
\sKw{\{} \sKw{return } \sVar{value} \sKw{; }
\sVar{statement\ldots} \sKw{\}}
\rightarrow
\Rightarrow
\sVar{value}
}

Expand Down Expand Up @@ -746,11 +746,10 @@ \section*{Substitution}
}
\]

\pagebreak
\textbf{Function declaration}: All occurrences of $x$ in the body of a function are substituted with $e_x$ under given circumstances.
\begin{enumerate}[label=\large\protect\textcircled{\small\arabic*}]
\begin{enumerate}
\item Function declaration where $x$ has the same name as a parameter.
\end{enumerate}

\[
\frac{
\exists \, i \in \{1, \cdots, n\} \text{ s.t. } x \ = \ x_i
Expand All @@ -760,49 +759,32 @@ \section*{Substitution}
\textbf{\texttt{function}}\ \textit{name} \ \textbf{\texttt{(}}\ x_1 \ldots x_n \ \textbf{\texttt{)}}\ \textit{block}
}
\]
\vspace{3mm}
\begin{enumerate}[label=\large\protect\textcircled{\small\arabic*}, start=2]
\item Function declaration where $x$ does not have the same name as a parameter.
\begin{enumerate}[label=(\,\roman*\,)]
\begin{enumerate}
\item No parameter of the function occurs free in $e_x$.
\end{enumerate}
\end{enumerate}
\[
\frac{
\forall \, i \in \{1, \cdots, n\} \text{ s.t. } x \ \neq \ x_i \text{, } \ \forall \, j \in \{1, \cdots, n\} \text{ s.t. } x_j \text{ does not occur free in $e_x$}
}{
\substack{\substack{\displaystyle{(\textbf{\texttt{function}}\ \textit{name} \ \textbf{\texttt{(}}\ x_1 \ldots x_n \ \textbf{\texttt{)}}\ \textit{block})[x := e_x]} \vspace{1.5mm} \\ \vspace{0.5mm} \displaystyle{=}} \\ \displaystyle{ \textbf{\texttt{function}}\ \textit{name} \ \textbf{\texttt{(}}\ x_1 \ldots x_n \ \textbf{\texttt{)}}\ \textit{block}[x := e_x]}}
}
\]
\vspace{3mm}
\begin{enumerate}
\item[]
\begin{enumerate}[label=(\,\roman*\,), start=2]
\item A parameter of the function occurs free in $e_x$.
\end{enumerate}
\end{enumerate}
\[
\frac{
\forall \, i \in \{1, \cdots, n\} \text{ s.t. } x \ \neq \ x_i \text{, } \ \exists \, j \in \{1, \cdots, n\} \text{ s.t. } x_j \text{ occurs free in $e_x$}
}{
\substack{\substack{\displaystyle{(\textbf{\texttt{function}}\ \textit{name} \ \textbf{\texttt{(}}\ x_1 \ldots x_j \ldots x_n \ \textbf{\texttt{)}}\ \textit{block})[x := e_x]} \vspace{1.5mm} \\ \vspace{0.5mm} \displaystyle{=}} \\ \displaystyle{(\textbf{\texttt{function}}\ \textit{name} \ \textbf{\texttt{(}}\ x_1 \ldots y \ldots x_n \ \textbf{\texttt{)}}\ \textit{block}[x_j := y])[x := e_x]}}
}
\]

\begin{enumerate}
\item[]
\begin{enumerate}[label=\roman*., start=2]
\item[]
\vspace{3mm}
Substitution is applied to the whole expression again as to recursively detect and rename all parameters of the function declaration that clash with variables that occur free in $e_x$, at which point (\,i\,) takes place. Note that the name $y$ is not declared in, nor occurs in \textit{block} and $e_x$.
\end{enumerate}
\end{enumerate}
\end{enumerate}

\vspace{10mm}
\textbf{Lambda expression}: All occurrences of $x$ in the body of a lambda expression are substituted with $e_x$ under given circumstances.
\begin{enumerate}[label=\large\protect\textcircled{\small\arabic*}]
\begin{enumerate}
\item Lambda expression where $x$ has the same name as a parameter.
\end{enumerate}
\[
\frac{
\exists \, i \in \{1, \cdots, n\} \text{ s.t. } x \ = \ x_i
Expand All @@ -812,13 +794,9 @@ \section*{Substitution}
\textbf{\texttt{(}}\ x_1 \ldots x_n \ \textbf{\texttt{)}}\ \textbf{\texttt{=>}}\ \textit{block}
}
\]
\vspace{3mm}
\begin{enumerate}[label=\large\protect\textcircled{\small\arabic*}, start=2]
\item Lambda expression where $x$ does not have the same name as a parameter.
\begin{enumerate}[label=(\,\roman*\,)]
\begin{enumerate}
\item No parameter of the lambda expression occurs free in $e_x$.
\end{enumerate}
\end{enumerate}
\[
\frac{
\forall \, i \in \{1, \cdots, n\} \text{ s.t. } x \ \neq \ x_i \text{, } \ \forall \, j \in \{1, \cdots, n\} \text{ s.t. } x_j \text{ does not occur free in $e_x$}
Expand All @@ -828,13 +806,7 @@ \section*{Substitution}
\textbf{\texttt{(}}\ x_1 \ldots x_n \ \textbf{\texttt{)}}\ \textbf{\texttt{=>}}\ \textit{block}[x := e_x]
}
\]
\vspace{3mm}
\begin{enumerate}
\item[]
\begin{enumerate}[label=(\,\roman*\,), start=2]
\item A parameter of the lambda expression occurs free in $e_x$.
\end{enumerate}
\end{enumerate}
\[
\frac{
\forall \, i \in \{1, \cdots, n\} \text{ s.t. } x \ \neq \ x_i \text{, } \ \exists \, j \in \{1, \cdots, n\} \text{ s.t. } x_j \text{ occurs free in $e_x$}
Expand All @@ -844,20 +816,14 @@ \section*{Substitution}
(\textbf{\texttt{(}}\ x_1 \ldots y \ldots x_n \ \textbf{\texttt{)}}\ \textbf{\texttt{=>}}\ \textit{block}[x_j := y])[x := e_x]
}
\]
\begin{enumerate}
\item[]
\begin{enumerate}[label=\roman*., start=2]
\item[]
\vspace{3mm}
Substitution is applied to the whole expression again as to recursively detect and rename all parameters of the lambda expression that clash with variables that occur free in $e_x$, at which point (\,i\,) takes place. Note that the name $y$ is not declared in, nor occurs in \textit{block} and $e_x$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
\end{enumerate}

\pagebreak
\textbf{Block expression}: All occurrences of $x$ in the statements of a block expression are substituted with $e_x$ under given circumstances.
\begin{enumerate}[label=\large\protect\textcircled{\small\arabic*}]
\begin{enumerate}
\item Block expression in which $x$ is declared.
\end{enumerate}
\[
\frac{
x \text{ is declared in \textit{block}}
Expand All @@ -867,13 +833,9 @@ \section*{Substitution}
\textit{block}
}
\]
\vspace{3mm}
\begin{enumerate}[label=\large\protect\textcircled{\small\arabic*}, start=2]
\item Block expression in which $x$ is not declared.
\begin{enumerate}[label=(\,\roman*\,)]
\begin{enumerate}
\item No names declared in the block occurs free in $e_x$.
\end{enumerate}
\end{enumerate}
\[
\frac{
x \text{ is not declared in \textit{block}}\text{, } \ \textit{name} \text{ declared in \textit{block} does not occur free in } e_x
Expand All @@ -883,13 +845,7 @@ \section*{Substitution}
[\textit{block}[0][x := e_x] \text{, } \ldots \text{, } \textit{block}[n][x := e_x]]
}
\]
\vspace{3mm}
\begin{enumerate}
\item[]
\begin{enumerate}[label=(\,\roman*\,), start=2]
\item A name declared in the block occurs free in $e_x$.
\end{enumerate}
\end{enumerate}
\[
\frac{
x \text{ is not declared in \textit{block}}\text{, } \ \textit{name} \text{ declared in \textit{block} occurs free in } e_x
Expand All @@ -899,14 +855,9 @@ \section*{Substitution}
[\textit{block}[0][\textit{name} := y] \text{, } \ldots \text{, } \textit{block}[n][\textit{name} := y]][x := e_x]
}
\]
\begin{enumerate}
\item[]
\begin{enumerate}[label=\roman*., start=2]
\item[]
\vspace{3mm}
Substitution is applied to the whole expression again as to recursively detect and rename all declared names of the block expression that clash with variables that occur free in $e_x$, at which point (\,i\,) takes place. Note that the name $y$ is not declared in, nor occurs in \textit{block} and $e_x$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
\end{enumerate}

\vspace{10mm}
\textbf{Variable declaration}: All occurrences of $x$ in the declarators of a variable declaration are substituted with $e_x$.
Expand Down
1 change: 0 additions & 1 deletion docs/specs/source_header.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@
\usepackage{latexsym}
\usepackage{mathtools}
\usepackage{amsmath,amssymb}
\usepackage{enumitem}

\usepackage[T1]{fontenc}

Expand Down

0 comments on commit 2b0992d

Please sign in to comment.