<commit_before>\newpage
\section{Exercises}
%if False
\begin{code}
import DSLsofMath.FunExp
import DSLsofMath.Simplify
\end{code}
%endif

\begin{exercise}\label{exc:homomorphisms}
\textbf{Homomorphisms.}
Consider the following definitions:
\begin{spec}
  -- |h : A -> B| is a homomorphism from |Op : A->A->A| to |op : B->B->B|
  H2(h,Op,op)  =  Forall x (Forall y (h(Op x y) == op (h x) (h y)))
  -- |h : A -> B| is a homomorphism from |F : A -> A| to |f : B -> B|
  H1(h,F,f)    =  Forall x (h(F x) == f (h x))
  -- |h : A -> B| is a homomorphism from |E : A| to |e : B|
  H0(h,E,e)    =  h E == e
\end{spec}

Prove or disprove the following claims:
\begin{itemize}
\item |H2((2*),(+),(+))|
\item |H2((2*),(*),(*))|
\item |H2(exp,(+),(*))|
\item |H2(eval',(:+:),(+))|
\item |H1(sqrt,(4*),(2*))|
\item |Exists f (H1(f,(2*).(1+),(1+).(2*)))|
  % |Exists f (Forall x (f.(2*).(1+) == (1+).(2*).f))|
  % |Exists f (Forall x (f (2*(1+x)) == 1+2*(f x)))|
  % |Exists f (Forall x (f (2*(1+x)) == 1+2*(f x)))|
  % Assume f = const c
  % |c == 1+2*c|
  % |-1 == c|
  % So, yes, there exists such a function, and |const (-1)| is an example.
\end{itemize}

\end{exercise}


%TODO (by DaHe): One or more exercises on "characterize the homomorphisms from
% X to Y"

\begin{exercise}
  Complete the numeric instance declarations for |FunExp|.
\end{exercise}

\begin{exercise}
  Complete the instance declarations for |Dup REAL|, deriving them
  from the homomorphism requirement for |applyFD| (in
  \refSec{sec:apply}).
\end{exercise}

\begin{exercise}
  We now have three different ways of computing the derivative of a
  function such as |f x = sin x + exp (exp x)| at a given point, say
  |x = pi|.
  \begin{enumerate}

    \item Find |e :: FunExp| such that |eval e = f| and use |eval'|.

    \item Find an expression of type |FD REAL| and use |apply|.

    \item Apply |f| directly to the appropriate |(x, x')| and use |snd|.

\end{enumerate}

  Do you get the same result?
\end{exercise}



\begin{exercise}
  \fromExam{2017-08-22}

  In Exercise~\ref{exc:e1_semiring} we looked at the datatype |SR v|
  for the language of semiring expressions.
  %
  We will now use some of the concepts discussed in this chapter to
  expand on this language.

  \begin{enumerate}

    \item Define a type class |SemiRing| that corresponds to the semiring
      structure.

    \item Define a |SemiRing| instance for the datatype |SR v| that you
      defined in exercise 1.3.

    \item Find two other instances of the |SemiRing| class.

    \item Specialise the evaluator that you defined in
      Exercise~\ref{exc:e1_semiring} to the two |SemiRing| instances
      defined above.
      %
      Take three semiring expressions of type |SR String|, give the
      appropriate assignments and compute the results of evaluating,
      in each case, the three expressions.

  \end{enumerate}
\end{exercise}

\begin{exercise}
  Show that arithmetic modulo |n| satisfies the semiring laws (it is
  even a ring).
%
  In more details: show that |Zn = {0,1,...,n-1}| with |plus x y = mod (x+y)
  n| and |times x y = mod (x*y) n| forms a semiring.
%

  With |h x = mod x n|, show that |h| is a homomorphism from |ZZ| to
  |Zn|.
\end{exercise}

\begin{exercise}
  \fromExam{2016-03-15}

  In Exercise~\ref{exc:e1_lattice}, we looked a datatype for the language of lattice
  expressions. We will now use some of the concepts discussed in this chapter to
  expand on this language.

  \begin{enumerate}

    \item Define a type class |Lattice| that corresponds to the lattice
      structure.

    \item Define a |Lattice| instance for the datatype for lattice expressions
      that you defined in 1.4.1.

    \item Find two other instances of the |Lattice| class.

    \item Specialise the evaluator you defined in exercise 1.4.2 to the two<commit_msg>fix refs<commit_after>\newpage
\section{Exercises}
%if False
\begin{code}
import DSLsofMath.FunExp
import DSLsofMath.Simplify
\end{code}
%endif

\begin{exercise}\label{exc:homomorphisms}
\textbf{Homomorphisms.}
Consider the following definitions:
\begin{spec}
  -- |h : A -> B| is a homomorphism from |Op : A->A->A| to |op : B->B->B|
  H2(h,Op,op)  =  Forall x (Forall y (h(Op x y) == op (h x) (h y)))
  -- |h : A -> B| is a homomorphism from |F : A -> A| to |f : B -> B|
  H1(h,F,f)    =  Forall x (h(F x) == f (h x))
  -- |h : A -> B| is a homomorphism from |E : A| to |e : B|
  H0(h,E,e)    =  h E == e
\end{spec}

Prove or disprove the following claims:
\begin{itemize}
\item |H2((2*),(+),(+))|
\item |H2((2*),(*),(*))|
\item |H2(exp,(+),(*))|
\item |H2(eval',(:+:),(+))|
\item |H1(sqrt,(4*),(2*))|
\item |Exists f (H1(f,(2*).(1+),(1+).(2*)))|
  % |Exists f (Forall x (f.(2*).(1+) == (1+).(2*).f))|
  % |Exists f (Forall x (f (2*(1+x)) == 1+2*(f x)))|
  % |Exists f (Forall x (f (2*(1+x)) == 1+2*(f x)))|
  % Assume f = const c
  % |c == 1+2*c|
  % |-1 == c|
  % So, yes, there exists such a function, and |const (-1)| is an example.
\end{itemize}

\end{exercise}


%TODO (by DaHe): One or more exercises on "characterize the homomorphisms from
% X to Y"

\begin{exercise}
  Complete the numeric instance declarations for |FunExp|.
\end{exercise}

\begin{exercise}
  Complete the instance declarations for |Dup REAL|, deriving them
  from the homomorphism requirement for |applyFD| (in
  \refSec{sec:apply}).
\end{exercise}

\begin{exercise}
  We now have three different ways of computing the derivative of a
  function such as |f x = sin x + exp (exp x)| at a given point, say
  |x = pi|.
  \begin{enumerate}

    \item Find |e :: FunExp| such that |eval e = f| and use |eval'|.

    \item Find an expression of type |FD REAL| and use |apply|.

    \item Apply |f| directly to the appropriate |(x, x')| and use |snd|.

\end{enumerate}

  Do you get the same result?
\end{exercise}



\begin{exercise}
  \fromExam{2017-08-22}

  In Exercise~\ref{exc:e1_semiring} we looked at the datatype |SR v|
  for the language of semiring expressions.
  %
  We will now use some of the concepts discussed in this chapter to
  expand on this language.

  \begin{enumerate}

    \item Define a type class |SemiRing| that corresponds to the semiring
      structure.

    \item Define a |SemiRing| instance for the datatype |SR v| that you
      defined in exercise 1.3.

    \item Find two other instances of the |SemiRing| class.

    \item Specialise the evaluator that you defined in
      Exercise~\ref{exc:e1_semiring} to the two |SemiRing| instances
      defined above.
      %
      Take three semiring expressions of type |SR String|, give the
      appropriate assignments and compute the results of evaluating,
      in each case, the three expressions.

  \end{enumerate}
\end{exercise}

\begin{exercise}
  Show that arithmetic modulo |n| satisfies the semiring laws (it is
  even a ring).
%
  In more details: show that |Zn = {0,1,...,n-1}| with |plus x y = mod (x+y)
  n| and |times x y = mod (x*y) n| forms a semiring.
%

  With |h x = mod x n|, show that |h| is a homomorphism from |ZZ| to
  |Zn|.
\end{exercise}

\begin{exercise}
  \fromExam{2016-03-15}

  In \cref{exc:e1_lattice}, we looked a datatype for the language of lattice
  expressions. We will now use some of the concepts discussed in this chapter to
  expand on this language.

  \begin{enumerate}

    \item Define a type class |Lattice| that corresponds to the lattice
      structure.

    \item Define a |Lattice| instance for the datatype for lattice expressions
      that you defined in \cref{exc:e1_lattice}.

    \item Find two other instances of the |Lattice| class.

    \item Specialise the evaluator you defined in \cref{exc:e1_lattice} to the two
{'fraction_non_alphanumeric': 0.1441453214845792, 'fraction_numerical': 0.01594354417145844, 'mean_word_length': 3.230514096185738, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3565125', 'n_tokens_mistral': 2849, 'n_tokens_neox': 2694, 'n_words': 1031}