\documentclass[a4paper, 10pt, pagesize, smallheadings]{article}  

\usepackage{graphicx}

%\usepackage[latin1]{inputenc}

\usepackage{amsmath, amsthm, amssymb}

\usepackage{typearea}

\usepackage{algorithm}

\usepackage{algorithmic}

\usepackage{fullpage}

\usepackage{mathtools}

\usepackage[all]{xy}

\title{Theory I, Sheet 9 Solution}

\author{Eugen Sawin}

\renewcommand{\familydefault}{\sfdefault}

\newcommand{\Pos}{\mathcal{P}os}

\newcommand{\E}{\mathcal{E}}

\newcommand{\D}{\mathcal{D}}

\newcommand{\J}{\mathcal{J}}

\include{pythonlisting}

\pagestyle{empty}

\begin{document}

\maketitle

\section*{Exercise 9.1.3}

\begin{align*}

ADT\, bool = &(\Sigma_{bool}, \E)\\

\Sigma_{bool} = &\{true^{(0)}, false^{(0)}, not^{(1)}, and^{(2)}, or^{(2)}\}\\

\E = &\{true \approx not(false),\\

& 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*}

\D_{bool} &= (M, \J)\\

M &= \{0, 1\}\\

\J(true) &= 1\\

\J(false) &= 0\\

\J(not)(x) &= 1 - x\\

\J(and)(x, y) &= min(x, y)\\

\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}