# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1311027878 -7200
# Node ID 11c55592ac3349faef9765237aa3e19de7fd0ae9
# Parent  becb48258245290aae6e63f83339fbd4f731f15b
First draft of ex9.

diff -r becb48258245 -r 11c55592ac33 tex/theory1_ex9.tex
--- a/tex/theory1_ex9.tex	Mon Jul 18 20:17:25 2011 +0200
+++ b/tex/theory1_ex9.tex	Tue Jul 19 00:24:38 2011 +0200
@@ -23,14 +23,16 @@
 
 \section*{Exercise 9.1.3}
 \begin{align*}
-ADT_{bool} = &(\Sigma_{bool}, \E)\\
+ADT\, bool = &(\Sigma_{bool}, \E)\\
 \Sigma_{bool} = &\{true^{(0)}, false^{(0)}, not^{(1)}, and^{(2)}, or^{(2)}\}\\
 \E = &\{true \approx not(false),\\
-& false \approx not(true),\\
-& not(not(x)) \approx x\\
-& and(x, y) \approx not(or(not(x), not(y))),\\
-& or(x, y) \approx not(and(not(x), not(y)))\}\\
+& not(not(x)) \approx x,\\
+& or(x, false) \approx x,\\
+& or(x, true) \approx true,\\
+& and(x, y) \approx not(or(not(x), not(y)))\}\\
 \end{align*}
+Remarks: $false \approx not(true)$ follows from $true \approx not(false)$ and $not(not(x)) \approx x$.\\
+$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)))$.
 
 \section*{Exercise 9.1.4}
 \begin{align*}
@@ -43,4 +45,21 @@
 \J(or)(x, y) &= max(x, y)\\
 \end{align*}
 
+\section*{Exercise 9.2}
+\begin{align*}
+ADT\, Stack = &(\Sigma_{Stack}, \E)\\
+\Sigma_{Stack} = &\{new^{(0)}, true^{(0)}, false^{(0)}, pop^{(1)}, top^{(1)}, isEmpty^{(1)}, push^{(2)}\}\\
+& new: Stack\\
+& true: bool\\
+& false: bool\\
+& pop: Stack \to Stack\\
+& top: Stack \to A\\
+& isEmpty: Stack \to bool\\
+& push: Stack \times A \to Stack\\
+\E = &\{isEmpty(new) \approx true,\\
+& isEmpty(push(S, x)) \approx false,\\
+& top(push(S, x)) \approx x,\\
+& pop(push(S, x)) \approx S\}\\
+\end{align*}
+The ADT $Stack$ has only one constructor $new$.
 \end{document}