sawine@13: \documentclass[a4paper, 10pt, pagesize, smallheadings]{article}  
sawine@13: \usepackage{graphicx}
sawine@13: %\usepackage[latin1]{inputenc}
sawine@13: \usepackage{amsmath, amsthm, amssymb}
sawine@13: \usepackage{typearea}
sawine@13: \usepackage{algorithm}
sawine@13: \usepackage{algorithmic}
sawine@13: \usepackage{fullpage}
sawine@13: \usepackage{mathtools}
sawine@13: \usepackage[all]{xy}
sawine@13: \title{Theory I, Sheet 9 Solution}
sawine@13: \author{Eugen Sawin}
sawine@13: \renewcommand{\familydefault}{\sfdefault}
sawine@13: \newcommand{\Pos}{\mathcal{P}os}
sawine@13: \newcommand{\E}{\mathcal{E}}
sawine@13: \newcommand{\D}{\mathcal{D}}
sawine@13: \newcommand{\J}{\mathcal{J}}
sawine@13: \include{pythonlisting}
sawine@13: 
sawine@13: \pagestyle{empty}
sawine@13: \begin{document}
sawine@13: \maketitle
sawine@13: 
sawine@13: \section*{Exercise 9.1.3}
sawine@13: \begin{align*}
sawine@14: ADT\, bool = &(\Sigma_{bool}, \E)\\
sawine@13: \Sigma_{bool} = &\{true^{(0)}, false^{(0)}, not^{(1)}, and^{(2)}, or^{(2)}\}\\
sawine@13: \E = &\{true \approx not(false),\\
sawine@14: & not(not(x)) \approx x,\\
sawine@14: & or(x, false) \approx x,\\
sawine@14: & or(x, true) \approx true,\\
sawine@14: & and(x, y) \approx not(or(not(x), not(y)))\}\\
sawine@13: \end{align*}
sawine@14: Remarks: $false \approx not(true)$ follows from $true \approx not(false)$ and $not(not(x)) \approx x$.\\
sawine@14: $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)))$.
sawine@13: 
sawine@13: \section*{Exercise 9.1.4}
sawine@13: \begin{align*}
sawine@13: \D_{bool} &= (M, \J)\\
sawine@13: M &= \{0, 1\}\\
sawine@13: \J(true) &= 1\\
sawine@13: \J(false) &= 0\\
sawine@13: \J(not)(x) &= 1 - x\\
sawine@13: \J(and)(x, y) &= min(x, y)\\
sawine@13: \J(or)(x, y) &= max(x, y)\\
sawine@13: \end{align*}
sawine@13: 
sawine@14: \section*{Exercise 9.2}
sawine@14: \begin{align*}
sawine@15: ADT\, Stack(A) = &(\Sigma_{Stack}, \E)\\
sawine@14: \Sigma_{Stack} = &\{new^{(0)}, true^{(0)}, false^{(0)}, pop^{(1)}, top^{(1)}, isEmpty^{(1)}, push^{(2)}\}\\
sawine@14: & new: Stack\\
sawine@14: & true: bool\\
sawine@14: & false: bool\\
sawine@14: & pop: Stack \to Stack\\
sawine@14: & top: Stack \to A\\
sawine@14: & isEmpty: Stack \to bool\\
sawine@14: & push: Stack \times A \to Stack\\
sawine@14: \E = &\{isEmpty(new) \approx true,\\
sawine@14: & isEmpty(push(S, x)) \approx false,\\
sawine@14: & top(push(S, x)) \approx x,\\
sawine@14: & pop(push(S, x)) \approx S\}\\
sawine@14: \end{align*}
sawine@14: The ADT $Stack$ has only one constructor $new$.
sawine@13: \end{document}