latex/honey-pure.tex

   1
   2 \documentclass{article}
   3 \input{arxana-header.tex}
   4
   5 \begin{document}
   6 \title{Pure Honey}
   7
   8 \author{Joseph Corneli \& Raymond Puzio\thanks{Copyright (C) 2017
   9     Joseph Corneli {\tt <holtzermann17@gmail.com>}\newline
  10     Copyright (C) 2017 Raymond Puzio {\tt <rsp@planetmath.info>}}}
  11 \date{Last revised: \today}
  12
  13 \maketitle
  14
  15 \abstract{This is a reference implementation of arxana backend
  16   primitives as described in the honey spec.}
  17
  18 \tableofcontents
  19
  20 \section{Introduction}
  21
  22 \begin{notate}{What we are doing?}
  23   Here we present a purely functional implementation of nemata and
  24   plexi as s-expressions.  To make everything explict, we pass the
  25   plexus as an argument to to our functions and, in the case of
  26   functions that can modify it, get the plexus back in the output.
  27
  28   In order to make for a reader-friendly exposition we will develop
  29   our code incrementally.  Since it is meant primarily to illustrate
  30   principles, the first version of the code presented here will
  31   hopelessly clunky and inefficient.  In successive versions, we will
  32   make various opimizations and improvements until we arrive at a more
  33   practical implementation.
  34 \end{notate}
  35
  36 \begin{notate}{Theoretical definition}
  37   We begin with a theoretical definition of a plexus as quintuplet $(U,
  38   G, H, T, C)$ where
  39
  40   \begin{itemize}
  41   \item $U$ is a (finite) set of identifiers
  42   \item $G$ is a distinguished element of $U$. (the ground)
  43   \item $H$ and $T$ are functions from $U$ to $U$ (head and tail)
  44   \item $C$ is a function from $U$ to a content set $S$
  45   \end{itemize}
  46
  47   subject to the conditions that $H(G) = T(G) = G$.
  48
  49   By using the canonical isomorphism between a set of functions with a
  50   common domain and a single function from the same domain to the
  51   product of their codomains, we may rewrite the definition as a
  52   triplet $(U, G, N)$ where $N$ is a function from $U$ to $H \times T
  53   \times C$.  The graph of $N$ consists of a set of quartiplets, which
  54   we call nemata.
  55
  56   For the purpose of implementing this structure in LISP, we will take
  57   the identifiers which lie in $U$ to be natural numbers, take $G$ to
  58   be 0, and take the content set $S$ to be the set of LISP lists.  We
  59   will represent a nema by cons'ing an element $x$ of $U$ and the
  60   corresponding values $H(x)$ and $T(x)$ onto $C(x)$.  Since we fixed
  61   the value of $G$ once and for all, we don't have to restate it, so a
  62   plexus will be represented as a list whose \verb|car| is $U$ and
  63   whose \verb|cdr| is the association list of nemata.
  64 \end{notate}
  65
  66 \section{Version 0}
  67
  68 \begin{notate}{About version 0}
  69   The honey primitives can be described as mathematical functions on
  70   the structure described above.  We will now write down these
  71   functions explicitly and translate the mathematical notation into
  72   LISP to produce the initial version.
  73 \end{notate}
  74
  75 \subsection{Utility routines}
  76
  77 \begin{notate}{Why utilities?}
  78   Before starting, we need to defun a few simple utility functions.
  79   Adhering to the highest standards of purity, we write them
  80   recursively and immutably.
  81 \end{notate}
  82
  83 \begin{notate}{On `next-available-number'}
  84   The first function takes a set of integers and a starting number
  85   finds the smallest integer which is not in the list but above the
  86   starting point.  This will be used to generate identifiers when
  87   adding new nemata.
  88 \end{notate}
  89 \begin{elisp}
  90 (defun next-available-number (ids start)
  91   (if (member start ids)
  92       (next-available-number ids (+ start 1))
  93     start))
  94 \end{elisp}
  95
  96 \begin{notate}{On `filter'}
  97   Select out the elements of the list which satisfy the predicate.
  98 \end{notate}
  99 \begin{elisp}
 100 (defun filter (prd lis)
 101   (if (consp lis)
 102       (if (funcall prd (car lis))
 103           (cons (car lis)
 104                 (filter prd (cdr lis)))
 105         (filter prd (cdr lis)))
 106     nil))
 107 \end{elisp}
 108
 109 \begin{notate}{On `cons*'}
 110   Convenience function which \verb|cons|'es a whole bunch of stuff in
 111   front of a list.  This could just as well be done as
 112   \verb(append (list ... ))\verb but since we will be doing this
 113   fairly often, it tidies up the code to give it a name.
 114 \end{notate}
 115 \begin{elisp}
 116 (defun cons* (&rest args)
 117   (if (cdr args)
 118       (cons (car args)
 119             (apply 'cons* (cdr args)))
 120     (car args)))
 121 \end{elisp}
 122
 123 \subsection{Individual Operations}
 124
 125 \begin{notate}{On `add-nema'}
 126   Formally, we may define $\mathrm{add-nema} : \mathbf{Plex} \times
 127   \mathbb{N} \times \mathbb{N} \times S \to \mathbf{Plex}$ as
 128   $((U, G, H, T, C), h, t, c) \mapsto (U' G' H' T' C')$
 129   where
 130   \begin{align*}
 131     U' &= \{0\} \sqcup U \\
 132     G' &= \mathrm{in}_2 (G) \\
 133     H' \circ \mathrm{in}_2 &= H, &  H'(\mathrm{in}_1(0)) &= h \\
 134     T' \circ \mathrm{in}_2 &= T, &  T'(\mathrm{in}_1(0)) &= t \\
 135     C' \circ \mathrm{in}_2 &= C, &  C'(\mathrm{in}_1(0)) &= c  .
 136   \end{align*}
 137   We will implement the coproduct with a singleton by picking a number
 138   which is not in $U$ and consing it on to $U$.  Then $\mathrm{in}_2$
 139   is just restriction of $U'$ to $U$ so all we need to do is add a
 140   nema.
 141 \end{notate}
 142 \begin{elisp}
 143 (defun pure-add-nema-v0 (plex src txt snk)
 144   (let ((next (next-available-number (car plex) 1)))
 145     (cons*
 146      ;; Start with U',
 147      (cons next (car plex))
 148      ;; then the the new nema
 149      (cons* next src snk txt)))
 150   ;; and end with the old nemata.
 151   (cdr plex))))
 152 \end{elisp}
 153
 154 \begin{notate}{On `remove-nema'}
 155   Formally, we may define
 156   \begin{align*}
 157     \mathtt{remove{\mhyphen}nema} : \prod_{p
 158     \colon \mathbf{Plex}} \mathrm{pr}_1 (p) \setminus \{ \mathrm{pr}_2
 159     (p) \} &\to \mathbf{Plex} \\
 160     ((U, G, H, T, C), n) &\mapsto (U', G, H
 161     |_{U'}, T |_{U'}, C |_{U'})
 162   \end{align*}
 163   where $U' = U \setminus \{n\}$.
 164 \end{notate}
 165 \begin{elisp}
 166 (defun pure-remove-nema-v0 (plex nema)
 167   (cons
 168    (remove nema (car plex))
 169    (remove (assoc nema (cdr plex))
 170            (cdr plex))))
 171 \end{elisp}
 172
 173 \begin{notate}{On `get-src', `get-sink' and `get-content'}
 174   Formally, we have
 175   \begin{align*}
 176     \mathrm{get-source} \colon
 177       \prod_{p \colon \mathbf{Plex}} \mathrm{pr}_1(p) &\to \mathbb{N} \\
 178     ((U, G, H, T, C), n) &\mapsto H(n) \\
 179     \mathrm{get-sink} \colon
 180       \prod_{p \colon \mathbf{Plex}} \mathrm{pr}_1(p) &\to \mathbb{N} \\
 181     ((U, G, H, T, C), n) &\mapsto T(n) \\
 182     \mathrm{get-content} \colon
 183        \prod_{p \colon \mathbf{Plex}} \mathrm{pr}_1(p) &\to S \\
 184     ((U, G, H, T, C), n) &\mapsto C(n)
 185   \end{align*}
 186 Woo-hoo, dependent types!!
 187 \end{notate}
 188 \begin{elisp}
 189 (defun pure-get-source-v0 (plex nema)
 190   (nthcdr 1 (assoc nema (cdr plex))))
 191
 192 (defun pure-get-sink-v0 (plex nema)
 193   (nthcdr 2 (assoc nema (cdr plex))))
 194
 195 (defun pure-get-content-v0 (plex nema)
 196   (nthcdr 3 (assoc nema (cdr plex))))
 197 \end{elisp}
 198
 199 \begin{notate}{On `get-forward-links' and `get-backward-links'}
 200   Formally,
 201   \begin{align*}
 202     \mathrm{get-forward-links} \colon
 203       \prod_{p : \mathbf{Plex}} \mathrm{pr}_1(p) &\to
 204       \mathcal{P}(\mathbb{Z}) \\
 205     ((U, G, H, T, C), n) &\mapsto H^{-1} (n) \\
 206     \mathrm{get-backward-links} :
 207       \prod_{p : \mathbf{Plex}} \mathrm{pr}_1(p) &\to
 208       \mathcal{P}(\mathbb{Z}) \\
 209   ((U, G, H, T, C) n) &\mapsto T^{-1} (n) .
 210   \end{align*}
 211 \end{notate}
 212 \begin{elisp}
 213 (defun pure-get-forward-links-v0 (plex nema)
 214   (mapcar 'car
 215           (filter (lambda (x) (equal x (nth 1 nema)))
 216                   (cdr plex))))
 217
 218 (defun pure-get-backward-links-v0 (plex nema)
 219   (mapcar 'car
 220           (filter (lambda (x) (equal x (nth 2 nema)))
 221                   (cdr plex))))
 222 \end{elisp}
 223
 224 \begin{notate}{On `update-source', `update-sink', and
 225     `update-content'}
 226   Formally, we have the following:
 227   \begin{align*}
 228     \mathtt{update-source} :
 229     \prod_{p : \mathbf{Plex}}
 230       \mathrm{pr}_1(p) \times \mathrm{pr}_1(p)
 231       &\to \mathbf{Plex} \\
 232     ((U, G, H, T, C), n, m) &\mapsto (U, G, H', T, C)
 233   \end{align*}
 234   where $H'(k) = H(k)$ when $k \neq n$ and $H'(n) = m$.
 235   \begin{align*}
 236     \mathtt{update-sink} :
 237     \prod_{p : \mathbf{Plex}}
 238       \mathrm{pr}_1(p) \times \mathrm{pr}_1(p)
 239       &\to \mathbf{Plex} \\
 240     ((U, G, H, T, C), n, m) &\mapsto (U, G, H, T', C)
 241   \end{align*}
 242   where $T'(k) = T(k)$ when $k \neq n$ and $T'(n) = m$.
 243     \begin{align*}
 244     \mathtt{update-source} :
 245     \prod_{p : \mathbf{Plex}}
 246       \mathrm{pr}_1(p) \times S
 247       &\to \mathbf{Plex} \\
 248     ((U, G, H, T, C), n, m) &\mapsto (U, G, H, T, C')
 249   \end{align*}
 250   where $C'(k) = C(k)$ when $k \neq n$ and $C'(n) = m$.
 251 \end{notate}
 252
 253 \begin{elisp}
 254 (defun update-source (plex nema new-src)
 255   (let ((changer (assoc nema (cdr plex))))
 256     (cons*
 257      ;; U
 258      (car plex)
 259      ;; The nema with an updated source.
 260      (cons*
 261       (nth 0 changer)
 262       new-src
 263       (nth 2 changer)
 264       (nthcdr 2 changer))
 265      ;; The rest of the nemata which remain unchanged.
 266      (remove changer (cdr plex)))))
 267
 268 (defun update-sink (plex nema new-snk)
 269   (let ((changer (assoc nema (cdr plex))))
 270     (cons*
 271      ;; U
 272      (car plex)
 273      ;; The nema with an updated sink.
 274      (cons*
 275       (nth 0 changer)
 276       (nth 1 changer)
 277       new-snk
 278       (nthcdr 2 changer))
 279      ;; The rest of the nemata which remain unchanged.
 280      (remove changer (cdr plex)))))
 281
 282 (defun update-content (plex nema txt)
 283   (let ((changer (assoc nema (cdr plex))))
 284     (cons*
 285      ;; U
 286      (car plex)
 287      ;; The nema with a updated content.
 288      (cons*
 289       (nth 0 changer)
 290       (nth 1 changer)
 291       (nth 2 changer)
 292       txt)
 293      ;; The rest of the nemata which remain unchanged.
 294      (remove changer (cdr plex)))))
 295 \end{elisp}
 296
 297 \end{document}