Arxana 2017

Joseph Corneli & Raymond Puzio Copyright (C) 2005-2017 Joseph Corneli <holtzermann17@gmail.com>
Copyright (C) 2010-2017 Raymond Puzio <rspuzio@planetmath.info>
transferred to the public domain.
(Last revised: December 30, 2020)
Abstract

A tool for building hackable semantic hypertext platforms. An overview and link to our source code repository is at http://arxana.net.

1 Introduction

Note 1.1 (What is “Arxana”?).

Arxana is the name of a “next generation” hypertext system that emphasizes annotation. Every object in this system is annotatable. Because of this, our first name for the program “the scholium system”, but “Arxana” better reflects our aim: to explore the mysterious world of links, attachments, correspondences, and side-effects. This edition of the program relies entirely on Emacs for storage and display, and integrates a backend storage mechanism devised by Ray Puzio, and frontend interactions from earlier prototypes by Joe Corneli, and (in Section 5.2) a new application to modelling mathematical dialogues jointly developed by both authors. Previous versions contain often excessive but sometimes interesting discussion of ideas for future work. Such discussion has been kept to a minimum here.

Note 1.2 (Using the program).

If you are looking at the source version of this document in Emacs, evaluate the following s-expression (type C-x C-e with the cursor positioned just after its final parenthesis). This prepares the Emacs environment for interactive use. (The code that achieves this is in Appendix A.)

(save-excursion
  (let ((beg (search-forward "\\begin{verbatim}"))
        (end (progn (search-forward "\\end{verbatim}")
                    (match-beginning 0))))
    (eval-region beg end)
    (lit-process)))

If you are looking at this in a PDF or printout, you will see that the document has a “literate” style. That is, it can be read as text, not just as code. In Section 4, we define functions that allow the user to read and revise the contents of this document as hypertext.

2 Backend

Note 2.1 (Overview of the backend).

This backend is a Higher Order NEtwork Yarnknotter or HONEY for short. It stores a network of quintuplets of the form (uid label source sink . content). One such quintuplet is called a nema. The structure of an individual nema is as follows: The uid is a numeric identifier that is unique on a network basis. The label is an (optional) string that corresponds uniquely to the uid. The source is the nema (identified by uid) to the “left” of our quintuplet, and the sink is the uid to the “right” of our quintuplet. One or both may be 0, and in case both are, the nema is understood to be a node. Lastly, the nema’s content can be any Lisp object -- including another nema in the same network or another network.11 1 TODO: (Check this last statement…)

2.1 Preliminaries

Note 2.2 (Some preliminaries).

We define several simple preliminary functions that we use later on.

Note 2.3 (Required packages).

We use the Common Lisp compatibility functions.

(require ’cl)
Note 2.4 (On ‘filter’).

This is a useful utility to filter elements of a list satisfying a condition. Returns the subset of stuff which satisfies the predicate pred.

(defun filter (pred stuff)
  (let ((ans nil))
    (dolist (item stuff (reverse ans))
      (if (funcall pred item)
            (setq ans (cons item ans))
        nil))))
(filter ’(lambda (x) (= (% x 2) 1)) ’(1 2 3 4 5 6 7))
=> (1 3 5 7)
Note 2.5 (On ‘intersection’).

Set-theoretic intersection operation. More general than the version coming from the ‘cl’ package.

(defun intersection (&rest arg)
  (cond ((null arg) nil)
        ((null (cdr arg)) (car arg))
        (t (let ((ans nil))
             (dolist (elmt (car arg) ans)
               (let ((remainder (cdr arg)))
                 (while (and remainder
                             (member elmt (car remainder)))
                   (setq remainder (cdr remainder))
                   (when (null remainder)
                     (setq ans (cons elmt ans))))))))))
(intersection ’(a b c d e f g h j)
              ’(a b h j k)
              ’(b d g h j k))
=> (j h b)
Note 2.6 (On ‘mapply’).

Map and apply rolled into one.

(defun mapply (f l)
  (if (member nil l) nil
    (cons (apply f (mapcar ’car l))
          (mapply f (mapcar ’cdr l)))))
(mapply ’+ ’((1 2) (3 4)))
 => (4 6)
Note 2.7 (On ‘sublis’).

Substitute objects in a list.

(defun sublis (sub lis)
  (cond
   ((null lis) nil)
   ((assoc lis sub) (cadr (assoc lis sub)))
   ((atom lis) lis)
   (t (cons (sublis sub (car lis))
            (sublis sub (cdr lis))))))

2.2 Core definitions

Note 2.8 (HONEY set up).

These variables are needed for a coherent set-up.22 2 TODO: Explain what they will do.

(defvar plexus-registry ’(0 nil))
(defvar current-plexus nil)
Note 2.9 (The ‘add-plexus’ function).

We use this create a new plexus for storage. It defines a counter (beginning at 1), together with several hash tables that allow efficient access to the plexus’ contents: an article table, forward links, backward links, forward labels, and backward labels. Additionally, it defines a ‘‘ground’’ and ‘‘type’’ nodes.33 3 TODO: Explain these things in more detail.44 4 TODO: NB. it could be useful to maintain a registry available networks, by analogy with Emacs’s ‘buffer-list’, which I think could be done if we use ‘cl-defstruct’ below instead of ‘list’, and set up the constructor suitably (info "(cl) Structures").

(defun add-plexus ()
  "Create a new plexus."
  (let ((newbie (list ’*plexus*
                      1                               ; nema counter
                      (make-hash-table :test ’equal)  ; nema table
                      (make-hash-table :test ’equal)  ; forward links
                      (make-hash-table :test ’equal)  ; backward links
                      (make-hash-table :test ’equal)  ; forward labels
                      (make-hash-table :test ’equal)  ; backward labels
                      (car plexus-registry))))
    ;; Define ground and type nodes.
    (puthash 0 ’(0 0) (nth 2 newbie))
    (puthash 1 ’(0 0) (nth 2 newbie))
    (puthash 0 ’((0 . 0) (1 . 0)) (nth 3 newbie))
    (puthash 0 ’((0 . 0) (1 . 0)) (nth 4 newbie))
    (puthash 0 ’"ground" (nth 5 newbie))
    (puthash ’"ground" 0 (nth 6 newbie))
    (puthash 1 ’"type" (nth 5 newbie))
    (puthash ’"type" 1 (nth 6 newbie))
    ;; Register the new object and return it.
    (setq plexus-registry
          (append
           ‘(,(+ (car plexus-registry) 1)
             ,newbie)
           (cdr plexus-registry)))
    newbie))
Note 2.10 (The “remove-plexus” function).

When we’re done with our plexus, we should tidy up after ourselves.

(defun remove-plexus (plex)
  "Remove a plexus."
  ;; Wipe out the hash tables
  (dotimes (i 5)
    (clrhash (nth (+ i 2) plex)))
  ;; Remove the entry from the registry.
  (setq plexus-registry
        (cons
         (car plexus-registry)
         (delete
          (assoc (nth 7 plex)
                 (cdr plexus-registry))
          (cdr plexus-registry)))))
(defun show-plexus-registry ()
  plexus-registry)
Note 2.11 (Network selection).

We can work with several networks, only one of which is “current” at any given time.

(defun set-current-plexus (plex)
  "Examine a different plexus instead."
  (setq current-plexus plex))

(defmacro with-current-plexus (plex &rest expr)
  (declare (debug (&rest form)))
  (append ‘(let ((current-plexus ,plex))) expr))

(defun show-current-plexus ()
  "Return the plexus currently being examined."
  current-plexus)
Note 2.12 (On ‘next-unique-id’).

Increment the identifier that tells us how many nemas are in our network.

(defun next-unique-id ()
  "Produce a yet unused unique identifier."
  (1+ (cadr current-plexus)))
Note 2.13 (On ‘reset-plexus’).

Reset article counter and hash tables. Redefine “ground” and “article-type”.

(defun reset-plexus ()
  "Reset the database to its initial configuration."
  ; Reset nema counter and hash tables.
  (setcar (cdr current-plexus) 1)
  (dotimes (n 5)
    (clrhash (nth (+ n 2) current-plexus)))
  ;; Define ground and nema-type.
  (puthash 0 ’(0 0) (nth 2 current-plexus))
  (puthash 1 ’(0 0) (nth 2 current-plexus))
  (puthash 0 ’((0 . 0) (1 . 0)) (nth 3 current-plexus))
  (puthash 0 ’((0 . 0) (1 . 0)) (nth 4 current-plexus))
  (puthash 0 ’"ground" (nth 5 current-plexus))
  (puthash ’"ground" 0 (nth 6 current-plexus))
  (puthash 1 ’"type" (nth 5 current-plexus))
  (puthash ’"type" 1 (nth 6 current-plexus))
  nil)

2.3 Individual Operations

Note 2.14 (On ‘add-nema’).

Add record to article table. Add record to list of forward links of source. Add record to list of backward links of sink. Return the id of the new article.55 5 TODO: Should we add an alias ‘add-triple’ for this function, to make it more clear that our middle/frontend is not implementation specific?

(defun add-nema (src txt snk)
  "Enter a new nema to the database."
  (let ((uid (next-unique-id)))
    ;; Add record to nema table.
    (puthash uid
             ‘(,src ,snk . ,txt)
             (nth 2 current-plexus))
    ;; Add record to list of forward links of source.
    (puthash src
             (cons ‘(,uid . ,snk)
                   (gethash src (nth 3 current-plexus) nil))
             (nth 3 current-plexus))
    ;; Add record to list of backward links of sink.
    (puthash snk
             (cons
              ‘(,uid . ,src)
              (gethash snk (nth 4 current-plexus) nil))
             (nth 4 current-plexus))
    ;; Update the counter for long-term storage
    (setcar (cdr current-plexus) uid)
    ;; Return the id of the new nema.
    uid))
Note 2.15 (Retrieving elements of a nema).

These functions exist to get the relevant components of a nema, given its uid.

(defun get-content (uid)
  "Return the content of the nema."
  (cddr (gethash uid (nth 2 current-plexus))))

(defun get-source (uid)
  "Return the source of the nema."
  (car (gethash uid (nth 2 current-plexus))))

(defun get-sink (uid)
  "Return the sink of the nema."
  (cadr (gethash uid (nth 2 current-plexus))))

(defun get-triple (uid)
  (list (get-source uid)
        (get-content uid)
        (get-sink uid)))
Note 2.16 (On ‘update-content’).

old source old sink new content

(defun update-content (uid txt)
  "Replace the content of the nema."
  (puthash uid
              (let ((x (gethash uid (nth 2 current-plexus))))
                     ‘(,(car x)    ; old source
                              ,(cadr x) . ; old sink
                                     ,txt))      ; new content
                 (nth 2 current-plexus)))
Note 2.17 (On ‘update-source’).

Extract current source. Extract current sink. Extract current content. Update the entry in the article table. Remove the entry with the old source in the forward link table. If that is the only entry filed under old-src, remove it from table. Add an entry with the new source in the forward link table. Update the entry in the backward link table.

(defun update-source (uid new-src)
  "Replace the source of the nema."
  (let* ((x (gethash uid (nth 2 current-plexus)))
         (old-src (car x))   ; extract current source
         (old-snk (cadr x))  ; extract current sink
         (old-txt (cddr x))) ; extract current content
    ;; Update the entry in the nema table.
    (puthash uid
             ‘(,new-src ,old-snk . ,old-txt)
             (nth 2 current-plexus))
    ;; Remove the entry with the old source in the
    ;; forward link table.  If that is the only entry
    ;; filed under old-src, remove it from table.
    (let ((y (delete ‘(,uid . ,old-snk)
                     (gethash old-src
                              (nth 3 current-plexus)
                              nil))))
      (if y
          (puthash old-src y (nth 3 current-plexus))
        (remhash old-src (nth 3 current-plexus))))
    ;; Add an entry with the new source in the
    ;; forward link table.
    (puthash new-src
             (cons ‘(,uid . ,old-snk)
                   (gethash old-src (nth 3 current-plexus) nil))
             (nth 3 current-plexus))
    ;; Update the entry in the backward link table.
    (puthash old-snk
             (cons ‘(,uid . ,new-src)
                   (delete ‘(,uid . ,old-src)
                           (gethash old-src
                                    (nth 4 current-plexus)
                                    nil)))
             (nth 4 current-plexus))))
Note 2.18 (On ‘update-sink’).

Extract current source. Extract current sink. Extract current content. Update the entry in the article table. Remove the entry with the old sink in the backward link table. If that is the only entry filed under old-src, remove it from table. Add an entry with the new source in the backward link table. Update the entry in the forward link table.

(defun update-sink (uid new-snk)
  "Change the sink of the nema."
  (let* ((x (gethash uid (nth 2 current-plexus)))
          (old-src (car x))   ; extract current source
           (old-snk (cadr x))  ; extract current sink
            (old-txt (cddr x))) ; extract current content
    ; Update the entry in the nema table.
    (puthash uid
             ‘(,old-src ,new-snk . ,old-txt)
             (nth 2 current-plexus))
    ;; Remove the entry with the old sink in the
    ;; backward link table.  If that is the only entry
    ;; filed under old-src, remove it from table.
    (let ((y (delete ‘(,uid . ,old-src)
                     (gethash old-snk
                              (nth 4 current-plexus)
                              nil))))
      (if y
          (puthash old-snk y (nth 4 current-plexus))
        (remhash old-snk (nth 4 current-plexus))))
    ;; Add an entry with the new source in the
    ;; backward link table.
    (puthash new-snk
             (cons ‘(,uid . ,old-src)
                   (gethash old-snk
                            (nth 4 current-plexus)
                            nil))
             (nth 4 current-plexus))
    ;; Update the entry in the forward link table.
    (puthash old-src
             (cons ‘(,uid . ,new-snk)
                   (delete ‘(,uid . ,old-snk)
                           (gethash old-src
                                    (nth 3 current-plexus)
                                    nil)))
             (nth 3 current-plexus))))
Note 2.19 (On ‘remove-nema’).

Remove forward link created by article. Remove backward link created by article. Remove record from article table.

(defun remove-nema (uid)
  "Remove this nema from the database."
  (let ((old-src (car (gethash uid (nth 2 current-plexus))))
        (old-snk (cadr (gethash uid (nth 2 current-plexus)))))
  ;; Remove forward link created by nema.
  (let ((new-fwd (delete ‘(,uid . ,old-snk)
                          (gethash old-src (nth 3 current-plexus)))))
    (if new-fwd
        (puthash old-src new-fwd (nth 3 current-plexus))
      (remhash old-src (nth 3 current-plexus))))
  ;; Remove backward link created by nema.
  (let ((new-bkw (delete ‘(,uid . ,old-src)
                          (gethash old-snk (nth 4 current-plexus)))))
    (if new-bkw
        (puthash old-snk new-bkw (nth 4 current-plexus))
      (remhash old-snk (nth 4 current-plexus))))
  ;; Remove record from nema table.
  (remhash uid (nth 2 current-plexus))))
Note 2.20 (Functions for gathering links).

Links are stored on triples alongside other elements.

(defun get-forward-links (uid)
  "Return all links having given object as source."
  (mapcar ’car (gethash uid (nth 3 current-plexus))))

(defun get-backward-links (uid)
  "Return all links having given object as sink."
  (mapcar ’car (gethash uid (nth 4 current-plexus))))
Note 2.21 (On ‘label-nema’).

Nemas can be given a unique human-readable label in addition to their numeric uid.

(defun label-nema (uid label)
  "Assign the label to the given object."
  (puthash uid label (nth 5 current-plexus))
  (puthash label uid (nth 6 current-plexus)))
Note 2.22 (Label to uid and uid to label lookup).

These functions allow the exchange of uid and label.

(defun label2uid (label)
  "Return the unique identifier corresponding to a label."
  (gethash label (nth 6 current-plexus) nil))

(defun uid2label (uid)
  "Return the label associated to a unique identifier."
  (gethash uid (nth 5 current-plexus) nil))

2.4 Bulk Operations

Note 2.23 (On ‘download-en-masse’).

Unpack triplets, obtain labels if they exist. Write data in the network to a list, and return.

(defun download-en-masse ()
  "Produce a representation of the database as quintuples."
  (let ((plex nil))
    (maphash (lambda (uid tplt)
               ;; Unpack triplet.
               (let ((src (car tplt))
                     (snk (nth 1 tplt))
                     (txt (nthcdr 2 tplt)))
                 ;; Obtain label if exists.
                 (setq lbl (gethash uid
                                    (nth 5 current-plexus)
                                    nil))
                 ;; Write data to list.
                 (setq plex (cons ‘(,uid ,lbl ,src ,snk . ,txt)
                                 plex))))
             (nth 2 current-plexus))
    ;; Return list of data.
    (reverse plex)))
Note 2.24 (On ‘upload-en-masse’).

Unpack quintuplets. Plug into tables. Bump up article counter as needed.

(defun upload-en-masse (plex)
  "Load a representation of a database as quintuples into memory."
  (dolist (qplt plex t)
    ; unpack quintuplet
    (let ((uid (car qplt))
            (lbl (nth 1 qplt))
              (src (nth 2 qplt))
                (snk (nth 3 qplt))
                  (txt (nthcdr 4 qplt)))
      ; plug into tables
      (puthash uid
                      ‘(,src ,snk . ,txt)
                             (nth 2 current-plexus))
      (puthash src
                      (cons ‘(,uid . ,snk)
                                 (gethash src (nth 3 current-plexus) nil))
                             (nth 3 current-plexus))
      (puthash snk
                      (cons
                       ‘(,uid . ,src)
                       (gethash snk (nth 4 current-plexus) nil))
                             (nth 4 current-plexus))
      (when lbl
          (progn
                (puthash uid lbl (nth 5 current-plexus))
                    (puthash lbl uid (nth 6 current-plexus))))
      ; Bump up nema counter if needed.
      (when (> uid (cadr current-plexus))
             (setcar (cdr current-plexus) uid)))))
Note 2.25 (On ‘add-en-masse’).

Given several articles, add all of them at once.

(defun add-en-masse (plex)
  "Add multiple nemata given as list of quartuplets."
  (mapcar (lambda (qplt)
            (let ((uid (next-unique-id)))
              (add-nema (nth 1 plex)
                        (nthcar 2 plex)
                        (nth 2 plex))
              (label-nema uid (car qplt))))
          plex))

2.5 Query

Note 2.26 (Overview of search and query functionality).

We first describe several elementary functions for accessing elements of the network. We then describe a robust search pipeline and show how it is implemented.

Note 2.27 (Various lookup functions).

These functions allow testing and lookup of various elements of a net.

(defun uid-p (uid)
  "Is this a valid uid?"
  (let ((z ’(())))
    (not (eq z (gethash uid (nth 2 current-plexus) z)))))

(defun uid-list ()
  "List of all valid uid’s."
  (maphash (lambda (key val) key)
           (nth 2 current-plexus)))

(defun ground-p (uid)
  "Is this nema the ground?"
  (= uid 0))

(defun source-p (x y)
  "Is the former nema the sink of the latter?"
  (equal x (get-source y)))

(defun sink-p (x y)
  "Is the former nema the sink of the latter?"
  (equal x (get-sink y)))

(defun links-from (x y)
  "Return all links from nema x to nema y."
  (filter ’(lambda (z) (source-p x z))
            (get-backward-links y)))

(defun links-p (x y)
  "Does nema x link to nema y?"
  (when (member x (mapcar
                      ’get-source
                      (get-backward-links y)))
    t))

(defun triple-p (x y z)
  "Do the three items form a triplet?"
  (and (source-p y x)
       (sink-p y z)))

(defun plexus-p (x)
  "Is this object a plexus?"
  (let ((ans t))
    (setq ans (and ans
                      (equal (car x) "*plexus*")))
    (setq ans (and ans
                      (integrp (cadr x))))
    (dotimes (n 5)
          (setq ans (and ans (hash-table-p
                                    (nth (+ n 2) x)))))
    ans))

2.6 Iteration

Note 2.28 (Iterating over a plexus).

These functions allow users to run loops over a plexus without having to delve into its internal structure.66 6 TODO: I forget whether the use of ‘apply’ here is good form.

(defmacro do-plexus (var res body)
  ‘((maphash (lambda (,var val) ,body)
             (nth 2 current-plexus))
    ,res))

;; This maps over the keys; func should be
;; defined appropriately.
(defun map-plexus (func)
  (let ((ans nil))
    (maphash
     (lambda (key val)
       (push (apply func (list key)) ans))
     (nth 2 current-plexus))
    ans))

(defun filter-plexus (pred)
  (let ((ans nil))
    (maphash
     (lambda (key val)
       (when (apply pred (list key))
         (push key ans)))
       (nth 2 current-plexus))
     ans))
Note 2.29 (Filtering convenience functions).

Several convenience functions for filtering the plexus can be defined. They give lists of uids, which can be expanded using get-triple.

(defun nemas-given-beginning (node)
  "Get triples outbound from the given NODE."
  (filter-plexus
   (lambda (x) (when (equal (get-source x)
                            node)
                 (list node
                       (get-content x)
                       (get-sink x))))))

(defun nemas-given-end (node)
  "Get triples inbound into NODE."
  (filter-plexus
   (lambda (x) (when (equal (get-sink x)
                            node)
                 (list (get-source x)
                       (get-content x)
                       node)))))

(defun nemas-given-middle (edge)
  "Get the triples that run along EDGE."
  (filter-plexus
   (lambda (x) (when (equal (get-content x)
                            edge)
                 (list (get-source x)
                       edge
                       (get-sink x))))))

(defun nemas-given-middle-and-end (edge node)
  "Get the triples that run along EDGE into NODE."
  (filter-plexus
   (lambda (x) (when (and
                      (equal (get-content x)
                             edge)
                      (equal (get-sink x)
                             node))
                 (list (get-source x)
                       edge
                       node)))))

(defun nemas-given-beginning-and-middle (node edge)
  "Get the triples that run from NODE along EDGE."
  (filter-plexus
   (lambda (x) (when (and
                      (equal (get-source x)
                             node)
                      (equal (get-content x)
                             edge))
                 (list node
                       edge
                       (get-sink x))))))

(defun nemas-given-beginning-and-end (node1 node2)
  "Get the triples that run from NODE1 to NODE2."
  (filter-plexus
   (lambda (x) (when (and
                      (equal (get-source x)
                             node1)
                      (equal (get-sink x)
                             node2))
                 (list node1
                       (get-content x)
                       node2)))))

(defun nemas-exact-match (node1 edge node2)
  "Get the triples that run from NODE1 along EDGE to
NODE2."
  (filter-plexus
   (lambda (x) (when (and
                      (equal (get-source x)
                             node1)
                      (equal (get-content x)
                             edge)
                      (equal (get-sink x)
                             node2))
                 (list node1
                       edge
                       node2)))))
Note 2.30 (Additional elementary functions for node access).

These functions give access to the various parts of a node.77 7 TODO: Note: since ‘article-list’ is not defined, should these functions be deleted? Or should they be rewritten to access ‘current-plexus’?

(defun get-src (n)
  (car (nth 0 (cdr (assoc n (cdr article-list))))))

(defun get-flk (n)
  (cdr (nth 0 (cdr (assoc n (cdr article-list))))))

(defun get-txt (n)
  (nth 1 (cdr (assoc n (cdr article-list)))))

(defun get-snk (n)
  (car (nth 2 (cdr (assoc n (cdr article-list))))))

(defun get-blk (n)
  (cdr (nth 2 (cdr (assoc n (cdr article-list))))))

(defun get-ids nil
  (mapcar (quote car) (cdr article-list)))

(defun get-gnd nil 0)
Note 2.31 (On ‘search-cond’).

Surround the search within dolist loops on free variables. Wrap no further when finished.88 8 TODO: Upgrade this to concatenate the results together. Also maybe allow options to add headers or to only loop over unique tuplets.99 9 TODO: Explain; how does this differ from the function defined at Note 2.40?

(defmacro search-cond (vars prop)
  "Find all n-tuplets satisfying a condition"
  (let ((foo ’(lambda (vars cmnd)
                (if vars
                    Wrap in a loop.
                    ‘(dolist (,(car vars) uids)
                       ,(funcall foo (cdr vars) cmnd))
                    cmnd))))
    (funcall foo vars prop)))
Note 2.32 (Overview of the search pipeline).

We will implement the search as a pipeline which gradually transforms the query into a series of expressions which produce the sought-after result, then evaluate those expressions.

A search query designates predicates apply to the nodes and the network relationships that apply to them. The network relationships function as wildcards.

The basic model of the data is triplets that point to other triplets. The following query asks for a funny link from a big blue object to a small green link pointing outwards from the big blue object.

(((a blue big) (b funny) (c green small)
  ((b src a) (b snk c) (c src a))

The first step of processing is to put the quaerenda in some order so that each item links up with at least one previous item:

(scheduler
 ’((b funny)
   (c green small))
 ’((b src a)
   (b snk c)
   (c src a))
 ’((a blue big)))
=>
((c (green small) ((b snk c) (c src a)))
 (b (funny) ((b src a)))
 (a blue big))

Note that the order is reversed due to technicalities of implementing ‘scheduler’ — that is to say, a is first and does not link to any other variable, b is next and links to only a, whilst c is last and links to both a and b. At the same time, we have also rearranged things so that the links to previous items to which a given object are listed alongside that object. The next step is to replace the links with the commands which generate a list of such objects:

((c (green small) ((b snk c) (c src a)))
 (b (funny) ((b src a)))
 (a blue big))
=>
((c (green small)
    (intersection (list (get-snk b)) (get-forward-links a)))
 (b (funny)
    (intersection (get-backward-links a)))
 (a blue big))

This is done using the function ‘tplts2cmd’, e.g.

(tplts2cmd ’c  ’((b snk c) (c src a)))
=>
(intersection (list (get-snk b)) (get-forward-links a))

Subsequently, we filter over the predicates:

((c (filter ’(lambda (c) (and (green c) (small c)))
    (intersection (list (get-snk b))
  (get-forward-links))))
 (b (filter ’(lambda (b) (and (funny b)))
    (intersection (get-backward-links a)))))

This is done with the command ‘add-filt’:

(add-filt ’c
  ’(green small)
  ’((b snk c) (c src a)))
=>
(c (filter (quote (lambda (c) (and (green c) (small c))))
   (intersection (list (get-snk b))
 (get-forward-links a))))

This routine calls up the previously described routine ‘tplts2cmd’ to take care of the third argument. The last entry, (a blue big) gets processed a little differently because we don’t as yet have anything to filter over; instead, we generate the initial list by looping over the current network:

(a (let ((ans nil))
     (donet ’node
    (when (and (blue (get-content node))
       (big (get-content node)))
      (setq ans (cons node ans))))
     ans))

This is done by invoking ‘first2cmd’:

(first2cmd ’(blue big))
=>
(let ((ans nil))
  (donet (quote node)
 (when (and (blue (get-content node))
    (big (get-content node)))
 (setq ans (cons node ans))))
 ans)

And putting this all together:

(query2cmd
 ’((c (green small) ((b snk c) (c src a)))
   (b (funny) ((b src a)))
   (a blue big)))
=>
((c (filter (quote (lambda (c) (and (green c) (small c))))
    (intersection (list (get-snk b))
  (get-forward-links a))))
 (b (filter (quote (lambda (b) (and (funny b))))
    (intersection (get-forward-links a))))
 (a (let ((ans nil))
      (donet (quote node)
     (when (and (blue (get-content node))
(big (get-content node)))
       (setq ans (cons node ans))))
      ans)))

To carry out these instructions in the correct order and generate a set of variable assignments, we employ the ‘matcher’ function. Combining this last layer, we have the complete pipeline:

(matcher nil
 (query2cmd
  (scheduler
   ’((b funny)
     (c green small))
   ’((b src a)
     (b snk c)
     (c src a))
   ’((a blue big)))))

This combination of operations is combined into the ‘search’ function, which can be called as follows:

(search
 ’(((a blue big)
    (b funny)
    (c green small))
   ((b src a)
    (b snk c)
    (c src a))))

Having described what the functions are supposed to do and how they work together, we now proceed to implement them.

Note 2.33 (On ‘scheduler’).

The scheduler function takes a list search query and rearranges it into an order suitable for computing the answer to that query. Specifically, a search query is a pair of lists — the first list consists of lists whose heads are names of variables and whose tails are predicates which the values of the variables should satisfy and the second list consists of triples indicating the relations between the values of the variables. Its arguments are:

  • new-nodes, a list of items of the form (node &rest property);

  • links, a list of triplets;

  • sched is a list whose items consist of triplets of the form
    (node (&rest property) (&rest link)).

A recursive function to find linked nodes. If done, return answer. New nodes yet to be examined. Element of remaining-nodes currently under consideration. List of links between candidate and old-nodes. List of nodes already scheduled. Loop through new nodes until find one linked to an old node. Look at the next possible node. Find the old nodes linking to the candidate node and record the answer in “ties”. Pick out the triplets whose first element is the node under consideration and whose third element is already on the list or vice-versa. Recursively add the rest of the nodes.

(defun scheduler (new-nodes links sched)
  (if (null new-nodes)
      sched
    (let ((remaining-nodes new-nodes)
          (candidate nil)
          (ties nil)
          (old-nodes (mapcar ’car sched)))
      (while (null ties)
        (setq candidate (car remaining-nodes))
        (setq remaining-nodes (cdr remaining-nodes))
        (setq ties
              (filter ’(lambda (x)
                         (or
                          (and (eq (first x) (car candidate))
                               (member (third x) old-nodes))
                          (and (member (first x) old-nodes)
                               (eq (third x) (car candidate)))))
                      links)))
      (scheduler (remove candidate new-nodes)
                 links
                 (cons (list (car candidate)
                             (cdr candidate)
                             ties)
                       sched)))))
Note 2.34 (On ‘tplts2cmd’).

1010 10 TODO: Explain.

(defun tplts2cmd (var tplts)
  (cons ’intersection
        (mapcar
         #’(lambda (tplt)
             (cond ((and (eq (third tplt) var)
                         (eq (second tplt) ’src))
                    ‘(get-flk ,(first tplt)))
                   ((and (eq (third tplt) var)
                         (eq (second tplt) ’snk))
                    ‘(get-blk ,(first tplt)))
                   ((and (eq (first tplt) var)
                         (eq (second tplt) ’src))
                    ‘(list (get-src ,(third tplt))))
                   ((and (eq (first tplt) var)
                         (eq (second tplt) ’snk))
                    ‘(list (get-snk ,(third tplt))))
                   (t nil)))
         tplts)))
Note 2.35 (On ‘add-filt’).

1111 11 TODO: Explain.

(defun add-filt (var preds tplts)
  ‘(,var
    (filter
     #’(lambda (,var)
         ,(cons ’and
                (mapcar
                 #’(lambda (pred)
                     (list pred
                           (list ’get-txt var)))
                 preds)))
     ,(tplts2cmd var tplts))))
Note 2.36 (On ‘first2cmd’).

1212 12 TODO: Explain.

(defun first2cmd (preds)
  ‘(let ((ans nil))
     (dolist (node (get-ids) ans)
       (when
           ,(cons ’and
                  (mapcar
                   #’(lambda (pred)
                       (cons pred ’((get-txt node))))
                   preds))
         (setq ans (cons node ans))))))
Note 2.37 (On ‘query2cmd’).

1313 13 TODO: Explain.

(defun query2cmd (query)
  (let ((backwards (reverse query)))
    (reverse
     (cons
      (list (caar backwards)
            (first2cmd (cdar backwards)))
      (mapcar
       #’(lambda (x)
           (add-filt (first x) (second x) (third x)))
       (cdr backwards))))))
Note 2.38 (On ‘matcher’).

1414 14 TODO: Explain.

(defun matcher (assgmt reqmts)
  (if (null reqmts) (list assgmt)
    (apply ’append
           (mapcar
            #’(lambda (x)
                (matcher (cons (list (caar reqmts) x)
                               assgmt)
                         (cdr reqmts)))
            (apply ’intersection
                   (eval ‘(let ,assgmt
                            (mapcar ’eval
                                    (cdar reqmts)))))))))
Note 2.39 (How matcher works).

Here are some examples unrelated to what comes up in searching triplets which illustrate how matcher works:

(matcher ’((x 1)) ’((y (list 1 3))
                    (z (list (+ x y) (- y x)))))
=>
(((z 2) (y 1) (x 1))
 ((z 0) (y 1) (x 1))
 ((z 4) (y 3) (x 1))
 ((z 2) (y 3) (x 1)))

(matcher nil ’((x (list 1))
               (y (list 1 3))
               (z (list (+ x y) (- y x)))))
=>
(((z 2) (y 1) (x 1))
 ((z 0) (y 1) (x 1))
 ((z 4) (y 3) (x 1))
 ((z 2) (y 3) (x 1)))
Note 2.40 (On ‘search’).

1515 15 TODO: Explain; how does this differ from the macro defined at Note 2.31?

(defun search (query)
  (matcher nil
           (reverse
            (query2cmd
             (scheduler
              (cdar query)
              (cadr query)
              (list (caar query)))))))

2.7 Scholium programming

Note 2.41 (Scholium programming).

The next several functions allow us to store and retrieve code from inside of the network.

Note 2.42 (On ‘node-fun’).

1616 16 TODO: Explain. Produce a list of commands to produce temporary bindings. Produce a list of commands to reset function values.

(defun node-fun (node get-code get-links)
  (let ((code  (funcall get-code node))
        (links (funcall get-links node)))
    (list
     ’lambda
     (car code)
     (cons
      ’prog1
      (cons
       (append
        ’(progn)
        (mapcar #’(lambda (x)
                    ‘(fset ’,(car x)
                           (node-fun ,(cdr x)
                                     ’,get-code
                                     ’,get-links)))
                links)
        (cdr code))
       (mapcar #’(lambda (x)
                   (if (fboundp (car x))
                       ‘(fset ’,(car x)
                              ’,(symbol-function (car x)))
                     ‘(fmakunbound ’,(car x))))
               links))))))
Note 2.43 (On ‘tangle-module’).

Recursively replace the chunks to recover executable code.1717 17 TODO: Explain.

(defun tangle-module (node get-cont ins-links)
  (insert-chunk
   (funcall get-cont node)
   (mapcar #’(lambda (x)
               (cons (car x)
                     (tangle-module (cdr x)
                                    get-cont
                                    ins-links)))
           (funcall ins-links node))))
Note 2.44 (On ‘insert-chunk’).

Given a node and an association list of replacement texts, insert the chunks at the appropriate places.

(defun insert-chunk (body chunks)
  (cond ((null body) nil)
        ((null chunks) body)
        ((equal (car body) ’*insert*)
         (cdr (assoc (cadr body) chunks)))
        (t (cons (insert-chunk (car body) chunks)
                 (insert-chunk (cdr body) chunks)))))
Note 2.45 (Functions for rewriting nemas).

Several functions for rewriting nemas.1818 18 TODO: How does this stuff relate to what’s going on in the vicinity of Note 2.18?

(defun set-src (n x)
  (if (equal n 0)
      0
    (progn (let ((old-backlink
                  (nth 1 (assoc (get-src n)
                                (cdr article-list)))))
             (setcdr old-backlink
                     (delete n (cdr old-backlink))))
           (let ((new-backlink
                  ‘(nth 1 (assoc x (cdr article-list)))))
             (setcdr new-backlink (cons n (cdr new-backlink))))
           (setcar (nth 1 (assoc n (cdr article-list))) x))))

(defun set-txt (n x)
  (setcar (cdr (cdr (assoc n (cdr article-list)))) x))

(defun set-snk (n x)
  (if (equal n 0)
      0
    (progn (let ((old-backlink
                  (nth 3 (assoc (get-snk n)
                                (cdr article-list)))))
             (setcdr old-backlink
                     (delete n (cdr old-backlink))))
           (let ((new-backlink
                  (nth 3 (assoc x (cdr article-list)))))
             (setcdr new-backlink (cons n (cdr new-backlink))))
           (setcar (nth 3 (assoc n (cdr article-list))) x))))

(defun ins-nod (src txt snk)
  (progn (setcdr article-list
                 (cons (list (car article-list)
                             (list src)
                             txt
                             (list snk))
                       (cdr article-list)))
         (let ((backlink
                (nth 3 (assoc snk (cdr article-list)))))
           (setcdr backlink (cons (car article-list)
                                  (cdr backlink))))
         (let ((backlink
                (nth 1 (assoc src (cdr article-list)))))
           (setcdr backlink (cons (car article-list)
                                  (cdr backlink))))
         (- (setcar article-list (+ 1 (car article-list))) 1)))

(defun del-nod (n)
  (if (or (equal n 0)
          (get-blk n)
          (get-flk n))
      nil
    (progn (let ((old-backlink
                  (nth 3 (assoc (get-snk n)
                                (cdr article-list)))))
             (setcdr old-backlink
                     (delete n (cdr old-backlink))))
           (let ((old-backlink
                  (nth 1 (assoc (get-src n)
                                (cdr article-list)))))
             (setcdr old-backlink
                     (delete n (cdr old-backlink))))
           (setcdr article-list
                   (delete (assoc n (cdr article-list))
                           (cdr article-list)))
            t)))

2.8 Initialization

Note 2.46 (Initialize with a new network).

For now, we just create one network to import things into. Additional networks can be added later (see Section 5).

(set-current-plexus (add-plexus))

3 An example middleënd

Note 3.1 (A middleënd for managing collections of articles).

This middleënd is a set of functions that add triples into the backend. At this stage we basically ignore details of storage, and rely on the convenience functions defined above as the backend’s API. In principle it would be possible to swap out the backend for another storage mechanism. We will give an example later on that uses more of the LISP-specific aspects of the backend implementation.1919 19 TODO: Let’s try to be a bit more concrete about this, especially in Section 5.2. In this example, rather than talking about nemas and networks, we will talk about articles and scholia. These objects are things that user will want to access, create, and manipulate. However, we will deal with functions for user interaction (input, display, and editing) in Section 4, not here. Like the backend, the middleënd could also be swapped out in applications where a different kind of data is modelled. And in fact, we come to some examples of other mid-level interfaces in Section 5.

3.1 Database interaction

Note 3.2 (The ‘article’ function).

You can use this function to create an article with a given name and contents. You can optionally put it in a list by specifying the heading that it is under. (If this is used multiple times with the same heading, that just becomes a cone over the contents.)

(defun article (name contents &optional heading)
  (let ((coordinates (add-nema name
                               "has content"
                               contents)))
    (when heading (add-nema coordinates "in" heading))
    coordinates))
Note 3.3 (The ‘scholium’ function).

You can use this function to link annotations to objects. As with the ‘article’ function, you can optionally categorize the connection under a given heading (cf. Note 3.2).

(defun scholium (beginning link end &optional heading)
  (let ((coordinates (add-nema beginning
                               link
                               end)))
    (when heading (add-nema coordinates "in" heading))
    coordinates))
Note 3.4 (Uses of coordinates).

It is convenient to do further immediate processing of the object we’ve created while we still have ahold of the coordinates returned by ‘add-nema’ (e.g., for importing code that is adjacent to the article, see Note 4.3).

Note 3.5 (On ‘get-article’).

Get the contents of the article named ‘name’. We assume that there is only one such article for now.

(defun get-article (name)
  (get-sink
   (first
    (nemas-given-beginning-and-middle
     (first
      (nemas-given-beginning-and-end
       name "arxana-merge.tex"))
     "has content"))))
Note 3.6 (On ‘get-names’).

This function simply gets the names of articles that have names -- in other words, every triple built around the ‘‘has content’’ relation.2020 20 TODO: This seems to work but are both map operations needed?

(defun get-names (&optional heading)
  (mapcar #’get-source
   (mapcar #’get-source (nemas-given-middle "has content"))))

4 An example frontend

Note 4.1 (Overview of the frontend).

The frontend provides a demonstration of Arxana’s functionality that is directly accessible to the user. Specifically, it is used to import LaTeX documents into a network structure. They can then be edited, remixed, saved, browsed, and exported.2121 21 TODO: Some of this functionality still needs to be merged in or written!

4.1 Importing LaTeX documents

Note 4.2 (Importing sketch).

The code in this section imports a document, represented as a collection of (sub-)sections and notes. It gathers the sections, sub-sections, and notes recursively and records their content in a tree whose nodes are places and whose links express the “component-of” relation described in Note LABEL:order-of-order.

This representation lets us see the geometric, hierarchical, structure of the document we’ve imported. It exemplifies a general principle, that geometric data should be represented by relationships between places, not direct relationships between strings. This is because ‘‘the same’’ string often appears in ‘‘different’’ places in any given document (e.g. a paper’s many sub-sections titled ‘‘Introduction’’ will not all have the same content).2222 22 TODO: Do we need to relax this?

What goes into the places is in some sense arbitrary. The key is that whatever is in or attached to these places must tell us everything we need to know about the part of the document associated with that place (e.g., in the case of a note, its title and contents). That’s over and above the structural links which say how the places relate to one another. Finally, all of these places and structural links will be added to a heading that represents the document as a whole.

A natural convention we’ll use is to put the name of any document component that’s associated with a given place into that place, and add all other information as annotations.2323 23 TODO: Does this contradict what is said above about Introductions?

Following our usual coding convention, functions are introduced below “from the bottom up.”

Note 4.3 (On ‘import-code-continuations’).

This function will run within the scope of ‘import-notes’. In fact, it is meant to run right after a Note itself has been scanned. The job of this function is to turn the series of Lisp chunks or other code snippets that follow a given note into a scholium attached to that note. Each separate snippet becomes its own annotation. The ‘‘conditional regexps’’ form used here only works with Emacs version 23 or higher.2424 24 TODO: Note the use of an edge-pointing-to-an-edge for categorization; is this a good style?

;; coords don’t exist anymore, now we use uids
(defun import-code-continuations (coords)
  (let ((possible-environments
         "\\(?1:elisp\\|idea\\|common\\)"))
    (while (looking-at
            (concat "\n*?\\\\begin{"
                    possible-environments
                    "}"))
      (let* ((beg (match-end 0))
             (environment (match-string 1))
             (end (progn (search-forward-regexp
                          (concat "\\\\end{"
                                  environment
                                  "}"))
                         (match-beginning 0)))
             (content (buffer-substring-no-properties
                       beg
                       end)))
        (scholium (scholium coords
                            "has attachment"
                            content)
                  "has type"
                  environment)))))
Note 4.4 (On ‘import-notes’).

We’re going to make the daring assumption that the ‘‘textual’’ portions of incoming LaTeX documents are contained in ‘‘Notes’’. That assumption is true, at least, for the current document. The function takes a buffer position ‘end’ that denotes the end of the current section. The function returns the count of the number of notes imported, so that ‘import-within’ knows where to start counting this section’s non-note children.2525 25 TODO: Would this same function work to import all notes from a buffer without examining its sectioning structure? Not quite, but close! (Could be a fun exercise to fix this.)

(defun import-notes (end)
  (let ((index 0))
    (while (re-search-forward (concat "\\\\begin{notate}"
                                      "{\\([^}\n]*\\)}"
                                      "\\( +\\\\label{\\)?"
                                      "\\([^}\n]*\\)?")
                              end t)
      (let* ((name
              (match-string-no-properties 1))
             (tag (match-string-no-properties 3))
             (beg
              (progn (next-line 1)
                     (line-beginning-position)))
             (end
              (progn (search-forward-regexp
                      "\\\\end{notate}")
                     (match-beginning 0)))
             ;; get the uid for our new nema
             (coords (add-nema name "in" buffername)))
        (scholium coords
                  "has content"
                  (buffer-substring-no-properties
                   beg end))
        (setq index (1+ index))
        ;; current-parent is in scope inside import-within
        (scholium current-parent
                  index
                  coords
                  buffername)
        (import-code-continuations coords)))
    index))
Note 4.5 (On ‘import-within’).

Recurse through levels of sectioning in a document to import LaTeX code. Children that are notes are attached to the hierarchical structure by the subroutine ‘import-notes’, called by this function. Sections are attached directly by ‘import-within’. We observe that a note “has content” whereas a section does not.

Incidentally, when looking for the end of an importing level, ‘nil’ is an OK result: that describes the case when we have reached the last section at this level and there is no subsequent section at a higher level.

(defun import-within (levels)
  (let ((this-level (car levels))
        (next-level (car (cdr levels))) answer)
    (while (re-search-forward
            (concat
             "^\\\\" this-level "{\\([^}\n]*\\)}"
             "\\( +\\\\label{\\)?"
             "\\([^}\n]*\\)?")
            level-end t)
      (let* ((name (match-string-no-properties 1))
             (at (add-nema name "in" buffername))
             (level-end
              (or (save-excursion
                    (search-forward-regexp
                     (concat "^\\\\" this-level "{.*")
                     level-end t))
                  level-end))
             (notes-end
              (if next-level
                  (or (progn (point)
                             (save-excursion
                               (search-forward-regexp
                                (concat "^\\\\"
                                        next-level "{.*")
                                level-end t)))
                      level-end)
                level-end))
             (index (let ((current-parent at))
                      (import-notes notes-end)))
             (subsections (let ((current-parent at))
                            (import-within (cdr levels)))))
        (while subsections
          (let ((coords (car subsections)))
            (setq index (1+ index))
            (scholium at
                      index
                      coords
                      buffername)
            (setq subsections (cdr subsections))))
        (setq answer (cons at answer))))
    (reverse answer)))
Note 4.6 (On ‘import-buffer’).

This function imports a LaTeX document, taking care of the high-level, non-recursive, aspects of this operation. It imports frontmatter (everything up to the first \begin{section}), but assumes “backmatter” is trivial, and does not attempt to import it. The imported material is classified as a “document” with the same name as the imported buffer.

Links to sections will be made under the ‘‘heading’’ of this document.2626 26 TODO: The sectioning levels should maybe be scholia attached to root-coords, but for some reason that wasn’t working so well – investigate later – maybe it just wasn’t good to run after running ‘import-within’.

(defun import-buffer (&optional buffername)
  (save-excursion
    (set-buffer (get-buffer (or buffername
                                (current-buffer))))
    (goto-char (point-min))
    (search-forward-regexp "\\\\begin{document}")
    (search-forward-regexp "\\\\section")
    (goto-char (match-beginning 0))
    (scholium buffername "is a" "document")
    (scholium buffername
              "has frontmatter"
              (buffer-substring-no-properties
               (point-min)
               (point))
              buffername)
    (let* ((root-coords (add-nema buffername "in" buffername))
           (levels
            ’("section" "subsection" "subsubsection"))
           (current-parent buffername)
           (level-end nil)
           (sections (import-within levels))
           (index 0))
      (while sections
        (let ((coords (car sections)))
          (setq index (1+ index))
          (scholium root-coords
                    index
                    coords
                    buffername))
        (setq sections (cdr sections))))))
Note 4.7 (On ‘autoimport-arxana’).

This just calls ‘import-buffer’, and imports this document into the system.

(defun autoimport-arxana ()
  (interactive)
  (import-buffer "arxana-merge.tex"))

4.2 Browsing database contents

Note 4.8 (Browsing sketch).

This section facilitates browsing of documents represented with structures like those created in Section 4.1, and sets the ground for browsing other sorts of contents (e.g. collections of tasks, as in Section 5.1).

In order to facilitate general browsing, it is not enough to simply use ‘get-article’ (Note 3.5) and ‘get-names’ (Note 3.6), although these functions provide our defaults. We must provide the means to find and display different things differently – for example, a section’s table of contents will typically be displayed differently from its actual contents.

Indeed, the ability to display and select elements of document sections (Note 4.14) is basically the core browsing deliverable. In the process we develop a re-usable article selector (Note 4.10; cf. Note 5.9). This in turn relies on a flexible function for displaying different kinds of articles (Note 4.9).

Note 4.9 (On ‘display-article’).

This function takes in the name of the article to display. Furthermore, it takes optional arguments ‘retriever’ and ‘formatter’, which tell it how to look up and/or format the information for display, respectively.

Thus, either we make some statement up front (choosing our ‘formatter’ based on what we already know about the article), or we decide what to display after making some investigation of information attached to the article, some of which may be retrieved and displayed (this requires that we specify a suitable ‘retriever’ and a complementary ‘formatter’).

For example, the major mode in which to display the article’s contents could be stored as a scholium attached to the article; or we might maintain some information about “areas” of the database that would tell us up front what which mode is associated with the current area. (The default is to simply insert the data with no markup whatsoever.)

Observe that this works when no heading argument is given, because in that case ‘get-article’ looks for all place pseudonyms. (But of course that won’t work well when we have multiple theories containing things with the same names, so we should get used to using the heading argument.)

(The business about requiring the data to be a sequence before engaging in further formatting is, of course, just a matter of expediency for making things work with the current dataset.)

(defun display-article
  (name &optional heading retriever formatter)
  (interactive "Mname: ")
  (let* ((data (if retriever
                   (funcall retriever name heading)
                 (get-article name))))
    (when (and data (sequencep data))
      (save-excursion
        (if formatter
            (funcall formatter data heading)
          (pop-to-buffer (get-buffer-create
                          "*Arxana Display*"))
          (delete-region (point-min) (point-max))
          (insert "NAME: " name "\n\n")
          (insert data)
          (goto-char (point-min)))))))
Note 4.10 (An interactive article selector).

The function ‘get-names’ (Note 3.6) and similar functions can give us a collection of articles. The next few functions provide an interactive functionality for moving through this collection to find the article we want to look at.

We define a “display style” that the article selector uses to determine how to display various articles. These display styles are specified by text properties attached to each option the selector provides. Similarly, when we’re working within a given heading, the relevant heading is also specified as a text property.

At selection time, these text properties are checked to determine which information to pass along to ‘display-article’.

(defvar display-style ’((nil . (nil nil))))

(defun thing-name-at-point ()
  (buffer-substring-no-properties
   (line-beginning-position)
   (line-end-position)))

(defun get-display-type ()
  (get-text-property (line-beginning-position)
                     ’arxana-display-type))

(defun get-relevant-heading ()
  (get-text-property (line-beginning-position)
                     ’arxana-relevant-heading))

(defun arxana-list-select ()
  (interactive)
  (apply ’display-article
         (thing-name-at-point)
         (get-relevant-heading)
         (cdr (assoc (get-display-type)
                     display-style))))

(define-derived-mode arxana-list-mode fundamental-mode
  "arxana-list" "Arxana List Mode.

\\{arxana-list-mode-map}")

(define-key arxana-list-mode-map (kbd "RET")
            ’arxana-list-select)
Note 4.11 (On ‘pick-a-name’).

Here ‘generate’ is the name of a function to call to generate a list of items to display, and ‘format’ is a function to put these items (including any mark-up) into the buffer from which individiual items can then be selected.

One simple way to get a list of names to display would be to reuse a list that we had already produced (this would save querying the database each time). We could, in fact, store a history list of lists of names that had been displayed previously (cf. Note 4.19).

We’ll eventually want versions of ‘generate’ that provide various useful views into the data, e.g., listing all of the elements of a given section (Note 4.14).

Finding all the elements that match a given search term, whether that’s just normal text search or some kind of structured search would be worthwhile too. Upgrading the display to e.g. color-code listed elements according to their type would be another nice feature to add.

(defun pick-a-name (&optional generate format heading)
  (interactive)
  (let ((items (if generate
                   (funcall generate)
                 (reverse (get-names heading)))))
    (when items
      (set-buffer (get-buffer-create "*Arxana Articles*"))
      (toggle-read-only -1)
      (delete-region (point-min)
                     (point-max))
      (if format
          (funcall format items)
        (mapc (lambda (item) (insert item "\n")) items))
      (toggle-read-only t)
      (arxana-list-mode)
      (goto-char (point-min))
      (pop-to-buffer (get-buffer "*Arxana Articles*")))))
Note 4.12 (On ‘get-section-contents’).

This function is used by ‘display-section’ (Note 4.14) to ‘pick-a-name’ as a generator for the table of contents of the section with the given name under the given heading.

This function first finds the triples that begin with the name of the section, then checks to see which of these represent structural information about that document. It also looks at the items found at via these links to see if they are sections or notes (‘‘noteness’’ is determined by them having content). The links are then sorted by their middles (which show the numerical order in which the components have in the section we’re examining). After this ordering information has been used for sorting, it is deleted, and we’re left with just a list of names in the appropriate order, together with an indication of their noteness.2727 27 TODO: The initial import strategy used in the latest round (as of July 12 2017) doesn’t seem to make the same assumptions about order of sections and their contents that are made in this function.

(defun get-section-contents (name heading)
  (let (contents)
    (dolist (triple (mapcar #’get-triple
                            (nemas-given-beginning
                             ;; ???
                             name)))
      (when (get-triple
             ;; hopefully assuming uniqueness
             ;; doesn’t defeat the purpose
             (first
              (nemas-exact-match
               (car triple) "in" heading)))
        (let* ((number (print-middle triple))
               (site (isolate-end triple))
               (noteness
                (when (get-triple
                       (nemas-given-beginning-and-middle
                        site "has content"))
                  t)))
          (setq contents
                (cons (list number
                            (print-system-object
                             (place-contents site))
                            noteness)
                      contents)))))
    (mapcar ’cdr
            (sort contents
                  (lambda (component1 component2)
                    (< (parse-integer (car component1))
                       (parse-integer (car component2))))))))
Note 4.13 (On ‘format-section-contents’).

A formatter for document contents, used by ‘display-document’ (Note 4.15) as input for ‘pick-a-name’ (Note 4.11).

Instead of just printing the items one by one, like the default formatter in ‘pick-a-name’ does, this version adds appropriate text properties, which we determine based the second component of of ‘items’ to format.

(defun format-section-contents (items heading)
  ;; just replicating the default and building on that.
  (mapc (lambda (item)
          (insert (car item))
          (let* ((beg (line-beginning-position))
                 (end (1+ beg)))
            (unless (second item)
              (put-text-property beg end
                                 ’arxana-display-type
                                 ’section))
            (put-text-property beg end
                               ’arxana-relevant-heading
                               heading))
          (insert "\n"))
        items))
Note 4.14 (On ‘display-section’).

When browsing a document, if you select a section, you should display a list of that section’s constituent elements, be they notes or subsections. The question comes up: when you go to display something, how do you know whether you’re looking at the name of a section, or the name of an article?

When you get the section’s contents out of the database (Note 4.12)

(defun display-section (name heading)
  (interactive (list (read-string
                      (concat
                       "name (default "
                       (buffer-name)
                       "): ")
                      nil nil (buffer-name))))
  ;; should this pop to the Articles window?
  (pick-a-name ‘(lambda ()
                  (get-section-contents
                   ,name ,heading))
               ‘(lambda (items)
                  (format-section-contents
                   items ,heading))))

(add-to-list ’display-style
             ’(section . (display-section
                          nil)))
Note 4.15 (On ‘display-document’).

This file shows the top-level table of contents of a document. (Most typically, a list of all of that document’s major sections.) In order to do this, we must find the triples that are begin at the node representing this document and that are in the heading of this document. This boils down to treating the document’s root as if it was a section and using the function ‘display-section’ (Note 4.14).2828 28 TODO: Assuming that the name comes from the current buffer is perhaps a bit odd.

(defun display-document (name)
  (interactive (list (read-string
                      (concat
                       "name (default "
                       (buffer-name) "): ")
                      nil nil (buffer-name))))
  (display-section name name))
Note 4.16 (Work with ‘heading’ argument).

We should make sure that if we know the heading we’re working with (e.g. the name of the document we’re browsing) that this information gets communicated in the background of the user interaction with the article selector.

Note 4.17 (Selecting from a hierarchical display).

A fancier “article selector” would be able to display several sections with nice indenting to show their hierarchical order.

Note 4.18 (Browser history tricks).

I want to put together (or put back together) something similar to the multihistoried browser that I had going in the previous version of Arxana and my Emacs/Lynx-based web browser, Nero2929 29 http://metameso.org/~joe/nero.el. The basic features are: (1) forward, back, and up inside the structure of a given document; (2) switch between tabs. More advanced features might include: (3) forward and back globally across all tabs; (4) explicit understanding of paths that loop.

These sorts of features are independent of the exact details of what’s printed to the screen each time something is displayed. So, for instance, you could flip between section manifests a la Note 4.14, or between hierarchical displays a la Note 4.17, or some combination; the key thing is just to keep track in some sensible way of whatever’s been displayed!

Note 4.19 (Local storage for browsing purposes).

Right now, in order to browse the contents of the database, you need to query the database every time. It might be handy to offer the option to cache names of things locally, and only sync with the database from time to time. Indeed, the same principle could apply in various places; however, it may also be somewhat complicated to set up. Using two systems for storage, one local and one permanent, is certainly more heavy-duty than just using one permanent storage system and the local temporary display. However, one thing in favor of local storage systems is that that’s what I used in the the previous prototype of Arxana – so some code already exists for local storage! (Caching the list of names we just made a selection from would be one simple expedient, see Note 4.11.)

Note 4.20 (Hang onto absolute references).

Since ‘get-article’ (Note 3.5) translates strings into their “place pseudonyms”, we may want to hang onto those pseudonyms, because they are, in fact, the absolute references to the objects we end up working with. In particular, they should probably go into the text-property background of the article selector, so it will know right away what to select!

4.3 Exporting LaTeX documents*

Note 4.21 (Roundtripping).

The easiest test is: can we import a document into the system and then export it again, and find it unchanged?

Note 4.22 (Data format).

We should be able to stably import and export a document, as well as export any modifications to the document that were generated within Arxana. This means that the exporting functions will have to read the data format that the importing functions use, and that any functions that edit document contents (or structure) will also have to use the same format. Furthermore, browsing functions will have to be somewhat aware of this format. So, this is a good time to ask – did we use a good format?

4.4 Editing database contents*

Note 4.23 (Roundtripping, with changes).

Here, we should import a document into the system and then make some simple changes, and after exporting, check with diff to make sure the changes are correct.

Note 4.24 (Re-importing).

One nice feature would be a function to “re-import” a document that has changed outside of the system, and make changes in the system’s version whereever changes appeared in the source version.

Note 4.25 (Editing document structure).

The way we have things set up currently, it is one thing to make a change to a document’s textual components, and another to change its structure. Both types of changes must, of course, be supported.

5 Applications

5.1 Managing tasks

Note 5.1 (What are tasks?).

Each task tends to have a name, a description, a collection of prerequisite tasks, a description of other material dependencies, a status, some justification of that status, a creation date, and an estimated time of completion. There might actually be several “estimated times of completion”, since the estimate would tend to improve over time. To really understand a task, one should keep track of revisions like this.

Note 5.2 (On ‘store-task-data’).

Here, we’re just filling in a frame. Since “filling in a frame” seems like the sort of operation that might happen over and over again in different contexts, to save space, it would probably be nice to have a macro (or similar) that would do a more general version of what this function does.

(defun store-task-data
  (name description prereqs materials status
        justification submitted eta)
  (add-nema name "is a" "task")
  (add-nema name "description" description)
  (add-nema name "prereqs" prereqs)
  (add-nema name "materials" materials)
  (add-nema name "status" status)
  (add-nema name "status justification" justification)
  (add-nema name "date submitted" submitted)
  (add-nema name "estimated time of completion" eta))
Note 5.3 (On ‘generate-task-data’).

This is a simple function to create a new task matching the description above.

(defun generate-task-data ()
  (interactive)
  (let ((name (read-string "Name: "))
        (description (read-string "Description: "))
        (prereqs (read-string
                  "Task(s) this task depends on: "))
        (materials (read-string "Material dependencies: "))
        (status (completing-read
                 "Status (tabled, in progress, completed):
                 " ’("tabled" "in progress" "completed")))
        (justification (read-string "Why this status? "))
        (submitted
         (read-string
          (concat "Date submitted (default "
                  (substring (current-time-string) 0 10)
                  "): ")
          nil nil (substring (current-time-string) 0 10)))
        (eta
         (read-string "Estimated date of completion:")))
    (store-task-data name description prereqs materials
                     status
                     justification submitted eta)))
Note 5.4 (Possible enhancements to ‘generate-task-data’).

In order to make this function very nice, it would be good to allow “completing read” over known tasks when filling in the prerequisites. Indeed, it might be especially nice to offer a type of completing read that is similar in some sense to the tab-completion you get when completing a file name, i.e., quickly completing certain sub-strings of the final string (in this case, these substrings would correspond to task areas we are progressively zooming down into).

As for the task description, rather than forcing the user to type the description into the minibuffer, it might be nice to pop up a separate buffer instead (a la the Emacs/w3m textarea). If we had a list of all the known tasks, we could offer completing-read over the names of existing tasks to generate the list of ‘prereqs’. It might be nice to systematize date data, so we could more easily e.g. sort and display task info “by date”. (Perhaps we should be working with predefined database types for dates and so on.)

Also, before storing the task, it might be nice to offer the user the chance to review the data they entered.

Note 5.5 (On ‘get-filler’).

Just a wrapper for ‘nemas-given-beginning-and-middle’. (Maybe we should add ‘heading’ as an optional argument here.)

(defun get-filler (frame slot)
  (third (first
          (print-triples
           (mapcar #’get-triple
                   (nemas-given-beginning-and-middle frame
                                                     slot))))))
Note 5.6 (On ‘get-task’).

Uses ‘get-filler’ (Note 5.5) to assemble the elements of a task’s frame.

(defun get-task (name)
  (when (triple-exact-match name "is a" "task")
    (list (get-filler name "description")
          (get-filler name "prereqs")
          (get-filler name "materials")
          (get-filler name "status")
          (get-filler name "status justification")
          (get-filler name "date submitted")
          (get-filler name
                      "estimated time of completion"))))
Note 5.7 (On ‘review-task’).

This is a function to review a task by name.

(defun review-task (name)
  (interactive "MName: ")
  (let ((task-data (get-task name)))
    (if task-data
        (display-task task-data)
      (message "No data."))))

(defun display-task (data)
  (save-excursion
    (pop-to-buffer (get-buffer-create
                    "*Arxana Display*"))
    (delete-region (point-min) (point-max))
    (insert "NAME: " name "\n\n")
    (insert "DESCRIPTION: " (first data) "\n\n")
    (insert "TASKS THIS TASK DEPENDS ON: "
            (second data) "\n\n")
    (insert "MATERIAL DEPENDENCIES: "
            (third data) "\n\n")
    (insert "STATUS: " (fourth data) "\n\n")
    (insert "WHY THIS STATUS?: " (fifth data) "\n\n")
    (insert "DATE SUBMITTED:" (sixth data) "\n\n")
    (insert "ESTIMATED TIME OF COMPLETION: "
            (seventh data) "\n\n")
    (goto-char (point-min))
    (fill-individual-paragraphs (point-min) (point-max))))
Note 5.8 (Possible enhancements to ‘review-task’).

Breaking this down into a function to select the task and another function to display the task would be nice. Maybe we should have a generic function for selecting any object “by name”, and then special-purpose functions for displaying objects with different properties.

Using text properties, we could set up a “field-editing mode” that would enable you to select a particular field and edit it independently of the others. Another more complex editing mode would know which fields the user had edited, and would store all edits back to the database properly. See Section 4.4 for more on editing.

Note 5.9 (Browsing tasks).

The function ‘pick-a-name’ (Note 4.11) takes two functions, one that finds the names to choose from, and the other that says how to present these names. We can therefore build ‘pick-a-task’ on top of ‘pick-a-name’.

(defun get-tasks ()
  (mapcar #’first
          (print-triples
           (mapcar #’get-triple
                   (nemas-given-middle-and-end "is a" "task")
                   t))))

(defun pick-a-task ()
  (interactive)
  (pick-a-name
   ’get-tasks
   (lambda (items)
     (mapc (lambda (item)
             (let ((pos (line-beginning-position)))
               (insert item)
               (put-text-property pos (1+ pos)
                                  ’arxana-display-type
                                  ’task)
               (insert "\n"))) items))))

(add-to-list ’display-style
             ’(task . (get-task display-task)))
Note 5.10 (Working with theories).

Presumably, like other related functions, ‘get-tasks’ should take a heading argument.

Note 5.11 (Check display style).

Check if this works, and make style consistent between this usage and earlier usage.

Note 5.12 (Example tasks).

It might be fun to add some tasks associated with improving Arxana, just to show that it can be done… maybe along with a small importer to show how importing something without a whole lot of structure can be easy.

Note 5.13 (Org mode integration).

The “default” task manager on Emacs is Org mode. It would be good to provide integration between Org mode and Arxana. This is one of the first things that Emacs people ask about when they hear about Arxana.

5.2 “Modelling mathematics the way it is really done”

Note 5.14 (Demonstration of an application to modelling mathematics).

In a paper for the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design (FARM 2017), we talk about how Arxana can be applied to model mathematical proofs. A rather advanced form of “mathematical knowledge management” is proposed, that integrates dialogue, heuristics, and that ultimately moves in the direction of an AI system. In this section, we will walk through this application.

The basic idea here is to write an interpreter that will read s-expressions and convert them into triples in the backend. So we will need a function that reads s-exps into some designated storage. The s-expressions are constrained to follow the grammar defined for the Inference Anchoring Theory + Content (IATC) language. The primatives of this language are described below. The number of arguments is indicated in the variable name. (1.5 means that it takes one and, optionally, two arguments.)

We will create a new plexus to store this content.

(add-plexus)

;; (with-current-plexus (second plexus-registry)
;;                      (add-nema "this" "is a" "test"))

(defvar iatc-performatives-2   ’(Define))
(defvar iatc-performatives-1.5 ’(Assert Agree Challenge Retract))
(defvar iatc-performatives-1   ’(Suggest Judge Query))
(defvar iatc-performatives-A   ’(QueryE))

(defvar iatc-intermediate-2    ’(implies strategy auxiliary analogy
                                 implements generalises wlog
                                 has_property instance_of
                                 indep_of))
(defvar iatc-intermediate-1.5  ’(easy))
(defvar iatc-intermediate-1    ’(not goal plausible beautiful useful
                                 heuristic))
(defvar iatc-intermediate-A    ’(conjunction and))
(defvar iatc-intermediate-1A   ’(case_split))

(defvar iatc-content-2         ’(used_in sub_prop reform instantiates
                                 expands sums))
(defvar iatc-content-1         ’(extensional_set))

(defvar iatc-verbs (append iatc-performatives-2
                           iatc-performatives-1.5
                           iatc-performatives-1
                           iatc-performatives-A
                           iatc-intermediate-2
                           iatc-intermediate-1.5
                           iatc-intermediate-1
                           iatc-intermediate-A
                           iatc-intermediate-1A iatc-content-2
                           iatc-content-1))

(defvar iatc-imported-matcher
  (concat (regexp-opt (mapcar #’symbol-name iatc-verbs)) "[0-9]*"))
Note 5.15 (Second attempt).

This code is based on the simpler idea of printing parent-child relationships.3030 30 https://stackoverflow.com/a/45772888/821010 But it is a bit more complicated, partly because we need different behaviour in the different cases outlined above.

It would be nice, and, actually, necessary, to have “multiple” return values, per the example below. The reason we need these return values is that new structure is developed relative to existing graph structure.

The function works recursively. It will always turn the top-level verb into a nema and return it. It will also create one or more nemas along the way (behaviour depends on the specific verb).

We also want to build up a structure that mirrors the tree that was put in, but that shows how the elements of that structure have been mapped into the graph.

;; utility function
(defun get-verbs (tree)
  (let ((head (car tree))
        (tail (cdr tree)))
    (append
     (if (consp head)
         (get-verbs head)
       (list head))
     (let (acc)
       (while tail
         (setq child (car tail)
               tail (cdr tail))
         ;; we are only interested in recursing to add’l
         ;; function applications
         (when (consp child)
           (setq acc (append (get-verbs child) acc))))
       acc))))

; (get-verbs ’(a (b (c 1 2)) 8 9 (d (e 1 2 3) (g 4 5))))

;; This function will takes in a tree that indicates a given subgraph,
;; marks up the subgraph with a cone (unless one exists already) and
;; return a handle to the cone.
;;
;; Note that the cone itself can be stored as a list of nemas.
;;
;; The natural extension would take a forest, find all of the cones,
;; and merge them.
(defun sexp-to-cone-contents (tree &optional entailed-nemas)
  (with-current-plexus
   (second plexus-registry)
   ;; we have to parse input in much the same way as done by
   ;; ‘read-tree’.  This is because both *named* nodes and
   ;; *additional* entailed structure will be (e.g., edges).  But this
   ;; time, instead of creating any new structure, we just put the
   ;; entailed items in our grab-bag
   (let* (;; verb to handle - it may correspond to a nema
          (verb (car tree))
          ;; as a nema, if such exists.
          ;; (is it OK to retrieve by label?)
          (atom (label2uid verb)))
     ;;
     (when atom (push atom entailed-nemas))
     (cond
      ((string= (symbol-name verb) "and")
       ;; there will be edges pointing to any children; we grab the edges here
       (dolist (child (cdr tree))
         (push (:id (nemas-exact-match atom
                                       nil
                                       (label2uid child)))
               entailed-nemas))
       (sexp-to-cone-contents child entailed-nemas))
      ((string= (symbol-name verb) "implies")
       ;; an *implies* node gets two associated edges:
       ;; one pointing to its antecedent and one pointing to its
       ;; consequent
       (let ((antecedent (first (cdr tree)))
             (consequent (second (cdr tree))))
         (push (:id (nemas-exact-match atom
                                       "antecedent"
                                       (label2uid child)))
               entailed-nemas)
         (push (:id (nemas-exact-match atom
                                       "consequent"
                                       (label2uid child)))
               entailed-nemas)))
      (t
       ;; default behaviour covers these verbs:
       ;; - and (multiple clauses; included above to illustrate)
       ;; - analogy (do we need to check that it only has 2 terms?)
       (dolist (child (cdr tree))
         (push (:id (nemas-exact-match atom
                                       nil
                                       (label2uid child)))
               entailed-nemas))))
     entailed-nemas)))

;; simulate "multi-value return"
(defun read-tree (tree)
  (second (highlight-tree tree)))

;; recursively chase through the tree, import it, and mark it up
(defun highlight-tree (tree &optional highlights)
  (with-current-plexus
   (second plexus-registry)
   ;; Cases:
   ;; (1):IATC - create an internal identifier for it.
   ;; (2):already-imported IATC - don’t import it again, just refer to it
   ;; (3):string - if we want to deal with this separately, just create a schematic node
   ;; (4):generic hcode or other LISP - push form into a node as contents
   (cond
    ;; (1):IATC
    ;; we need to import the tree ->
    ((member (car tree) iatc-verbs)
     (let* ((verb (car tree))                   ; verb to import
            (symb (gensym (symbol-name verb)))  ; as a symbol
            (atom (add-nema 0 symb 0))          ; as a nema
                                                ; *this will be 1st return value*
            (label (label-nema atom symb))      ; we give it a handle
            (type (add-nema symb "type" verb))) ; we annotate it with a type
       (cond
        ((string= (symbol-name verb) "and")
         ;; Connect each of the children, which we process here
         (dolist (child (cdr tree))
           (add-nema atom
                     nil
                     (if (consp child)
                         (first (highlight-tree child))
                       child))))
        ((string= (symbol-name verb) "implies")
         ;; an *implies* node gets two associated edges:
         ;; one pointing to its antecedent and one pointing to its
         ;; consequent
         (let ((antecedent (first (cdr tree)))
               (consequent (second (cdr tree))))
           (add-nema atom
                     "antecedent"
                     (if (consp antecedent)
                         (first (highlight-tree antecedent))
                       antecedent))
           (add-nema atom
                     "consequent"
                     (if (consp consequent)
                         (first (highlight-tree consequent))
                       consequent))))
        (t
         ;; default behaviour covers these verbs:
         ;; - and (multiple clauses; included above to illustrate)
         ;; - analogy (do we need to check that it only has 2 terms?)
         (dolist (child (cdr tree))
           (add-nema atom
                     nil
                     (if (consp child)
                         (first (highlight-tree child))
                       child)))))
       ;; we replace the verb with its new symbol as a handle
       (rplaca tree symb)
       (list atom tree)))
    ;; (2):already-imported IATC, as indicated by the verb’s form
    ((string-match iatc-imported-matcher (symbol-name verb))
     ;; the s-exp rooted on this verb is representative of a
     ;; subgraph that has already been imported.  We convert it
     ;; to a cone over the subgraph, and return that.
     )
    ;; (3):string
    ((stringp (car tree))
     ;; just add it.
     ;; This is a terminal node so no more recursion here.
     (list (add-nema 0 (car tree) 0) nil)
     )
    ;; (4):generic hcode
    (t
     )
    )))
Note 5.16 (Example: describing and querying a simple analogy).

The first example proposes a superficially simple analogy. Note that while it builds up a structure in the backend, the interpreter returns some convenient handles for the contents that are entered.

(with-current-plexus (second plexus-registry)
                     (reset-plexus))

(setq
 %1-implies
 (read-tree ’(Assert (implies (and "G finite group"
                                   "H subgroup of G"
                                   "[G : H] finite")
                              "G not equal to union of ghg^-1"))))
;=> %1-implies

(setq
 %2-analogy
 (read-tree
  ‘(Assert (analogy
            ,(cadr %1-implies)
            (implies (and "G infinite group"
                          "H subgroup of G"
                          "[G : H] finite")
                     "G not equal to union of ghg^-1")))))
;=> %2-analogy

(setq %3-question ‘(Question ,(car (cddadr %2-implies))))
;=> %3-question
Note 5.17 (A challenge problem).

The second example is a full solution to a challenge problem.

;; What is the 500th digit of (sqrt(3)+sqrt(2))^2012?

(Assert
 "goal"
 "compute 500th digit of (sqrt(3)+sqrt(2))^2012")

;; Even this...

(Assert (exists (strategy "goal"
                          "strategy X")))

(Assert (has_property "strategy X"
                      "HAL"))

;; For now...

(Suggest (strategy goal
                   "simplify and compute"))

;; Furthermore...

(Suggest (strategy goal
                   "this should be straightforward
                    once we find the trick"))

;; Can we do...

(Assert
 (analogy
  "compute 500th digit of (sqrt(2)+sqrt(3))^2012"
  "compute 500th digit of (x+y)^2012"))

(Assert
 (analogy
  "compute 500th digit of (sqrt(2)+sqrt(3))^2012"
  "compute 500th digit of e^2012"))

(Assert
 (analogy
  "compute 500th digit of (sqrt(2)+sqrt(3))^2012"
  "compute 500th digit of r^2012,
   where r is a rational with small denominator"))

(Assert
 (has_property
  "compute 500th digit of r^2012,
   where r is a rational with small denominator"
  "we can really compute this"))

(Assert
 (has_evidence
  "we can really compute this"
  "e.g. 500th digit of (1/10)^2012 is 0"))

;; How about small...

(Suggest (strategy goal
                   "the trick might be: it
                    is close to something
                    we can compute"))

;; mth digit of...

(Suggest (auxilliary
          "generalise"
          "general form of the problem:
           mth digit of (sqrt(3)+sqrt(2))^n"))

;; (sqrt(3)+sqrt(2))^2

(Suggest (auxilliary
          "specialise"
          "(sqrt(3)+sqrt(2))^2"))

(Assert (instantiates
         "(sqrt(3)+sqrt(2))^2"
         "general form of the problem:
           mth digit of (sqrt(3)+sqrt(2))^n"))

(Assert (has_property
         "(sqrt(3)+sqrt(2))^2"
         "we can really compute this"))

;; 2 + 2 sqrt(2) sqrt(3) + 3

(Assert (expands
         "(sqrt(3)+sqrt(2))^2"
         "2 + 2 sqrt(3) sqrt(2) + 3"))

;; (sqrt(3)+sqrt(2))^2 + (sqrt(3)-sqrt(2))^2 = 10

(Suggest (strategy "eliminate cross terms"))

(Assert (expands "(sqrt(3)+sqrt(2))^2 + (sqrt(3)-sqrt(2))^2"
                 "2 + 2 sqrt(2) sqrt(3) + 3
                + 2 - 2 sqrt(2) sqrt(3) + 3"))

(Assert (sums "2 + 2 sqrt(2) sqrt(3) + 3
             + 2 - 2 sqrt(2) sqrt(3) + 3"
              "10"))

;; (sqrt(3)+sqrt(2))^2012 + (sqrt(3)-sqrt(2))^2012 is an integer

(Suggest (strategy "binomial theorem"))

(Assert (generalises "binomial theorem"
                     "eliminate cross terms"))

(Assert (sums "(sqrt(3)+sqrt(2))^2012 + (sqrt(3)-sqrt(2))^2012"
              "some integer"))

;; And (sqrt(3)-sqrt(2))^2012 is a very small number

(Assert (contains_as_summand
        "(sqrt(2)+sqrt(3))^2012+(sqrt(3)-sqrt(2))^2012"
        "(sqrt(3)-sqrt(2))^2012"))

(Assert (has_property "(sqrt(3)-sqrt(2))^2012"
                      "is small"))

(Assert (implements #SUBGRAPH
                    "the trick might be: it
                     is close to something
                     we can compute"))

(Suggest (strategy "numbers that are very close
                    to integers have \"9\"
                    in many places of their
                    decimal expansion"))

;; We need to check...

(Assert "sqrt(3)-sqrt(2)<1/2")
(Assert "0<a<b<1 => a^N < b^N")
(Assert "(1/2)^2012 = ((1/2)^4)^503")
(Assert "(1/2)^4 = 1/16")
(Assert "1/16 < .1")
(Assert ".1^503 has 502 0’s
         in its decimal expansion")
(Assert "an integer minus something with
         at least 502 0’s in its decimal
         expansion has at least 503 9’s
         in its decimal expansion")

(Assert (implies #SUBGRAPH2
                 "(sqrt(2)+sqrt(3))^2012
                  = (sqrt(2)+sqrt(3))^2012
                    +(sqrt(2)+sqrt(3))^2012
                    -(sqrt(2)-sqrt(3))^2012
                  has at least 503 9’s in its
                  decimal expansion"))

(Assert (has_specialisation
           "(sqrt(2)+sqrt(3))^2012
                  = (sqrt(2)+sqrt(3))^2012
                    +(sqrt(2)+sqrt(3))^2012
                    -(sqrt(2)-sqrt(3))^2012
                  has at least 503 9’s in its
                  decimal expansion"
           "(sqrt(2)+sqrt(3))^2012 has 500
            9s in its decimal expansion"))

(Assert "(sqrt(2)+sqrt(3))^2012 has 500
         9s in its decimal expansion")

6 Conclusion

Note 6.1 (Ending and beginning again).

This is the end of this Arxana demo system. Contributions that support the development of the Arxana project are welcome.

Appendix A Appendix: A simple literate programming system

Note A.1 (The literate programming system used in this paper).

This code defines functions that grab all the Lisp portions of this document, and evaluates the Emacs Lisp sections. It requires that the LaTeX be written in a certain consistent way. The function assumes that this document is the current buffer.

(defvar lit-code-beginning-regexp
  "^\\\\begin{elisp}")

(defvar lit-code-end-regexp
  "^\\\\end{elisp}")

(defvar lit-count 0)

(defun lit-eval ()
  (interactive)
  (lit-process ’eval))

(defun lit-process (&optional code)
  (interactive)
  (setq lit-count (1+ lit-count))
  (save-excursion
    (let ((to-buffer (concat "*Lit Code " (int-to-string
                                            lit-count)"*"))
          (from-buffer (buffer-name (current-buffer))))
      (set-buffer (get-buffer-create to-buffer))
      (erase-buffer)
      (set-buffer (get-buffer-create from-buffer))
      (goto-char (point-min))
      (while (re-search-forward
              lit-code-beginning-regexp nil t)
        (let* ((beg (match-end 0))
               (end (save-excursion
                      (search-forward-regexp
                       lit-code-end-regexp nil t)
                      (match-beginning 0)))
               (match (buffer-substring beg end)))
          (save-excursion
            (set-buffer to-buffer)
            (insert match))))
      (case code
       (’eval
        (set-buffer to-buffer)
        (eval-buffer)
        ;; (kill-buffer (current-buffer))
        )
       (t
        (switch-to-buffer to-buffer))))))
Note A.2 (A literate style).

Ideally, each function will have its own Note to introduce it, and will not be called before it has been defined. I sometimes make an exception to this rule, for example, functions used to form recursions may appear with no further introduction, and may be called before they are defined.

Index