Changeset 3557 for Papers


Ignore:
Timestamp:
Apr 24, 2015, 1:31:35 PM (4 years ago)
Author:
mulligan
Message:

bit more on bitvectortrie

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2015/boender-jar-2015.tex

    r3555 r3557  
    241241A central design decision in our formalisation is the choice of how to encode memory.
    242242The MCS-51 has various memory spaces and registers that can be addressed with bytes and words.
    243 \begin{lstlisting}
    244 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] :=
    245   Leaf: A -> BitVectorTrie A O
    246 | Node: $\forall$n: nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
    247 | Stub: $\forall$n: nat. BitVectorTrie A n.
    248 \end{lstlisting}
     243Using a complete associative map to capture an entire memory space, including large swathes of uninitialised data, would be incredibly inefficient and make any proof incredibly difficult due to the strain placed on Matita.
     244However, using a na\"ive data structured like an association-list to encode memory would lead to inefficiencies when stepping through the semantics of a machine code program inside Matita.
     245We therefore use an indexed type, \texttt{BitVectorTrie}, to efficiently represent a memory space that may have `holes' of uninitialised or unspecified data:
     246\begin{lstlisting}
     247inductive BitVectorTrie (A: Type[0]): $\mathbb{N}$ $\rightarrow$ Type[0] :=
     248  Leaf: A $\rightarrow$ BitVectorTrie A O
     249| Node: $\forall$n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
     250| Stub: $\forall$n. BitVectorTrie A n.
     251\end{lstlisting}
     252The $\mathbb{N}$ index of the \texttt{BitVectorTrie} family records the maximum length of any path to stored data through the tree.
     253For a dependently-typed encoding of a trie data structure, the \texttt{Leaf} and \texttt{Node} constructors are standard.
     254The novelty of \texttt{BitVectorTrie} lies in the \texttt{Stub} constructor, which intuitively represents a `hole' in the tree, and can appear
    249255
    250256% Trie data structure and use of dependent types
Note: See TracChangeset for help on using the changeset viewer.