\documentclass[12pt]{article}
\usepackage{amsfonts}

\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\renewcommand{\and}{\wedge}
\renewcommand{\or}{\vee}
\newcommand{\impl}{\Rightarrow}
\newcommand{\lequiv}{\Leftrightarrow} %equivalence as logical connective
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
%\equiv is already defined for === semantic equivalence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}
\newcommand{\true}{{\mathbb{T}}}
\newcommand{\false}{{\mathbb{F}}}


\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2007.
Homework 6, given Dec 6, due Dec 13.}

\bigskip

\noindent
1.
Design a ``pattern program'' for computing the reverse of a list, starting
from the properties of the function when applied to the empty list and to
a list formed by appending an element to a list.

\bigskip

\noindent
2. Transform this program in a functional program and study its behaviour
on a list with three elements.

\bigskip

\noindent
3. Use the associativity of concatenation of lists in order to transform the
trace obtained above into a list of pairs.

\bigskip

\noindent
4. Design a tail recursive auxiliary function which can be used to compute the
reverse of a list.

\bigskip

\noindent
Hint: the process is similar to the design and the transformation of the
function which computes the sum of the first $n$ numbers, which was studied
in the lecture.

\end{document}
