Prove an arithmetic property of a partial recursive function
-
03-11-2019 - |
Frage
I have this program written in haskell :
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 :)
Notations:
- $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.
Keine korrekte Lösung
Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit cs.stackexchange