MHB How can we apply the functions?

[mathmari]

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:

View attachment 6265

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}$... (Wondering)

 

[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}$... (Wondering)

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?

 

[mathmari]

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)$ ? (Wondering)