I have this program written in haskell : enter image description here

I have to prove that: $(\forall a \in \mathbb{N})[!D_V [h](a) \Rightarrow log_2 (D_V[h](a) )\equiv 2 (mod$ $ 10) ]$.

The predicate $P_2$ for the $g$ function is obvious : $P_2(f,g) \equiv (\forall x,y \in \mathbb{N})[!g(x,y) \Rightarrow g(x,y)\backsimeq xy]$.

But the predicate for the function $f$ which would give me authomaticaly the one for $h$ I have no idea what it should be.

Any ideas and help in solving this problem is welcomed :)


  • $D_V[h]$: denotational semantics with passing by value of the function $f$.
  • $!F(x)$ means that $F$ is defined at point $x$.
  • $F(x) \backsimeq V$ means has the value $V$ at the point $x$ or is undefined.
  • 2
    $\begingroup$ Please explain your notations. What is $D_V(a)$? What are $!$, $\equiv$ and $\backsimeq$? Also, please post the Haskell code as text. $\endgroup$ Jan 11 '16 at 15:40
  • 1
    $\begingroup$ From context, I gather that $\equiv$ is equality in the semantic domain (i.e. equality in $\mathbb{N}$)? And what's $P_2$? (You seem to use $P_2$ as a concept, rather than defining a particular notation.) $\endgroup$ Jan 11 '16 at 17:18

The function $f$ computes the recurrence relation $$ f(x) = \begin{cases} 4 & x \leq 1, \\ f(x-1)^2 f(x-2)^4 & x > 1. \end{cases} $$ Taking $\ell = \log_2 \circ f$, we get $$ \ell(x) = \begin{cases} 2 & x \leq 1, \\ 2\ell(x-1) + 4\ell(x-2) & x > 1. \end{cases} $$ Now, modulo 10 we have $$ 2 \cdot 2 + 4 \cdot 2 = 12 \equiv 2 \pmod{10}. $$ An easy proof by induction then shows that $\ell(x) \equiv 2 \pmod{10}$ for all $x$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.