Thanks:  0

Thread: How can we apply the functions?

1. Hey!!

Let $\text{Val} = \{0, 1\}^8$, $\text{Adr} = \{0, 1\}^{32}$ and $\text{Mem} = \text{Val}^{\text{Adr}}$.

The addition modulo $2^8$ of two numbers in binary system of length $8$, is given by the mapping:
$$\text{add}_{\text{Val}} : \text{Val}\times \text{Val}\rightarrow \text{Val} \\ (u,v) \mapsto \text{bin}_8 ((\text{Num}_2(u)+\text{Num}_2(v))\mod 2^8)$$

The addition modulo $2^{32}$ of two numbers in binary system of length $32$ and $8$, is given by the mapping:
$$\text{add}_{\text{Adr}} : \text{Adr}\times \text{Val}\rightarrow \text{Adr} \\ (a,v) \mapsto \text{bin}_{32} ((\text{Num}_2(a)+\text{Num}_2(v))\mod 2^{32})$$

A queue is a data structure with the operations „enqueue“, „dequeue“ and „first“.

In our memory model a queue can be represented with at most $2^8$ values by an address. The address and the next field save an pointer at the beginning and the end of the queue. The pointer gives the address relative to the basic address +2.

The mappings init_queue, is_empty, enqueue, dequeue and first are defined as follows:

For each memory $m \in \text{Mem}$, each address $a \in \text{Adr}$ and each value $v \in \text{Val}$, the init_queue(m, a) initializes a queue at $a$ in $m$, is_empty(m, a) checks if the queue at $a$ in $m$ is empty or not, enqueue(m, a, v) places the value $v$ in the queue at $a$ in $m$, dequeue(m, a) takes the oldest value from the queue at $a$ in $m$ and first(m, a) gives the oldest value of the queue at $a$ in $m$.

Let $m\in \text{Mem}$ and $a = \text{bin}_{32}(0)$. I want to compute the value of

first(dequeue(enqueue(enqueue(init_queue(m, a), a, 00101111), a, 00001100), a), a)

First the most inner function is init_queue(m, a). This initializes a queue at $a$ in $m$.

Then we have to compute the mapping enqueue(init_queue(m, a), a, 00101111).

For that we have to compute the $a'=\text{add}_{\text{Adr}}(a,1)$ and $a^{\star}=\text{add}_{\text{Adr}}(a,\text{bin}_8(2))$. How can we do that? I haven't really understood the function $\text{add}$...

Originally Posted by mathmari
For that we have to compute the $a'=\text{add}_{\text{Adr}}(a,1)$ and $a^{\star}=\text{add}_{\text{Adr}}(a,\text{bin}_8(2))$. How can we do that? I haven't really understood the function $\text{add}$...
We have that $a'=\text{add}_{\text{Adr}}(a,1)=\text{bin}_{32}(1)$ and $a^{\star}=\text{add}_{\text{Adr}}(a,\text{bin}_8(2))=\text{bin}_{32}(2)$, right?

I want to define inductively, using only $\text{add}_{\text{Val}}$, is_empty, dequeue and first, a function sum: Mem × Adr â†’ Val such that for each memory m âˆˆ Mem and each address a âˆˆ Adr it holds that sum(m, a) is in the binary system the sum modulo $2^8$ of all values, expressed in binary system of numbers, in the queue at a in m, where the empty sum is 0.
Does this mean that $\text{sum}(m,a)=\text{bin}_8( (m+a) \mod 2^8)$ ?