First draft of ex9.
1.1 --- a/tex/theory1_ex9.tex Mon Jul 18 20:17:25 2011 +0200
1.2 +++ b/tex/theory1_ex9.tex Tue Jul 19 00:24:38 2011 +0200
1.3 @@ -23,14 +23,16 @@
1.4
1.5 \section*{Exercise 9.1.3}
1.6 \begin{align*}
1.7 -ADT_{bool} = &(\Sigma_{bool}, \E)\\
1.8 +ADT\, bool = &(\Sigma_{bool}, \E)\\
1.9 \Sigma_{bool} = &\{true^{(0)}, false^{(0)}, not^{(1)}, and^{(2)}, or^{(2)}\}\\
1.10 \E = &\{true \approx not(false),\\
1.11 -& false \approx not(true),\\
1.12 -& not(not(x)) \approx x\\
1.13 -& and(x, y) \approx not(or(not(x), not(y))),\\
1.14 -& or(x, y) \approx not(and(not(x), not(y)))\}\\
1.15 +& not(not(x)) \approx x,\\
1.16 +& or(x, false) \approx x,\\
1.17 +& or(x, true) \approx true,\\
1.18 +& and(x, y) \approx not(or(not(x), not(y)))\}\\
1.19 \end{align*}
1.20 +Remarks: $false \approx not(true)$ follows from $true \approx not(false)$ and $not(not(x)) \approx x$.\\
1.21 +$or(x, y) \approx not(and(not(x), not(y)))$ follows from $not(not(x)) \approx x$ and $and(x, y) \approx not(or(not(x), not(y)))$.
1.22
1.23 \section*{Exercise 9.1.4}
1.24 \begin{align*}
1.25 @@ -43,4 +45,21 @@
1.26 \J(or)(x, y) &= max(x, y)\\
1.27 \end{align*}
1.28
1.29 +\section*{Exercise 9.2}
1.30 +\begin{align*}
1.31 +ADT\, Stack = &(\Sigma_{Stack}, \E)\\
1.32 +\Sigma_{Stack} = &\{new^{(0)}, true^{(0)}, false^{(0)}, pop^{(1)}, top^{(1)}, isEmpty^{(1)}, push^{(2)}\}\\
1.33 +& new: Stack\\
1.34 +& true: bool\\
1.35 +& false: bool\\
1.36 +& pop: Stack \to Stack\\
1.37 +& top: Stack \to A\\
1.38 +& isEmpty: Stack \to bool\\
1.39 +& push: Stack \times A \to Stack\\
1.40 +\E = &\{isEmpty(new) \approx true,\\
1.41 +& isEmpty(push(S, x)) \approx false,\\
1.42 +& top(push(S, x)) \approx x,\\
1.43 +& pop(push(S, x)) \approx S\}\\
1.44 +\end{align*}
1.45 +The ADT $Stack$ has only one constructor $new$.
1.46 \end{document}