documentation changes

[arxana.git] / org / arxana-redux.org

#+TITLE:     Arxana Redux
#+AUTHOR:    Joe Corneli, Raymond Puzio
#+EMAIL:     contact@planetmath.org
#+DATE:      April 15, 2017 for Friday, 26 May, 2017 deadline
#+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
#+KEYWORDS: arxana, hypertext, inference anchoring
#+LANGUAGE: en
#+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
#+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
#+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
#+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport
#+LINK_UP:
#+LINK_HOME:
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
#+BIBLIOGRAPHY: arxana-redux-refs plain
#+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex}
#+LATEX_HEADER: \addbibresource{arxana-redux-refs}
#+STARTUP: showeverything

* Overview (Introduction)

For the Scheme and FARM 2017 workshops at the International Conference
on Functional Programming (/ICFP/) to take place at Oxford this
September, we plan to make presentations about /Arxana/ and math
texts.  We plan to get some version of Arxana working, then use it to
mark up some mathematical text along the lines of /IAT/ and then come
up with a demo which shows what such a /scholiumific representation/
is good for.  We will draw on /CD/ theory to move /IAT/ style
representations into a computable form.

We have written a 12 page paper for the FARM workshop that describes
our ideas in more detail.  It can be found here:
http://metameso.org/ar/farm-2017.pdf

Further information on the project and ongoing development can be
found below.

** Glossary of keywords

- ICFP :: the International Conference on Functional Programming is an
 annual academic conference in the field of computer science
 sponsored by the ACM SIGPLAN, the Association for Computing
 Machinery's Special Interest Group on programming languages.
 Previous publications in the conference series touch on
 things like /A functional programmer's guide to homotopy type theory/,
 /Program synthesis: opportunities for the next decade/,
 /Lem: reusable engineering of real-world semantics/ [Lem stands for "[[http://www.cl.cam.ac.uk/~pes20/lem/][Lightweight executable mathematics]]"],
 /Functional programming with structured graphs/,
 /Painless programming combining reduction and search: design principles for embedding decision procedures in high-level languages/,
 /Using camlp4 for presenting dynamic mathematics on the web: DynaMoW, an OCaml language extension for the run-time generation of mathematical contents and their presentation on the web/,
 /TeachScheme!: a checkpoint/,
 /A functional I/O system or, fun for freshman kids/ and
 /Commutative monads, diagrams and knots/
 (i.e., a selection of papers from the proceedings over
 the last 10 years that mention "mathematics" or
 something similar; hopefully at least a few of them
 are relevant).  We plan to submit to the
 [[http://www.schemeworkshop.org/][Scheme and Functional Programming]] workshop,
 though perhaps we might also want to have a look
 at the [[http://functional-art.org/2017/cfp.html][Functional Art, Music, Modelling and Design]]
 workshop in case it proves to be a better fit.

- IAT :: Inference Anchoring Theory was devised by Budzynska et
     al \cite{budzynska2014model} to model the logical structure
     of dialogical arguments.  This has since been adapted to
     model mathematical arguments \cite{corneli2017qand}.  The
     primary features of this adaptation are: (1) to introduce
     more explicit relationships between pieces of mathematical
     content; and (2) to advance a range of ``predicates'' that
     relate mathematical propositions.  These predicates
     describe inferential structure, judgements of validity or
     usefulness, and reasoning tactics.

- scholium :: A scholium is a word for a marginal annotation or
     scholarly, explanatory, remark. Corneli and Krowne proposed
     a "scholia-based document model" \cite{corneli2005scholia}
     for "commons-based peer production," that is, the kind of
     collaborative online knowledge-building that happens on
     sites like Wikipedia or in online forums
     \cite{benkler2002coase}, or in other digital libraries
     broadly construed \cite{krowne2003building}.  The proposal
     is that online text resources grow ``by attaching.''  One
     familiar class of examples is provided by revision control
     systems, e.g., Git, which builds a network history of
     changes to documents in a directed acyclic graph (DAG).

- Arxana :: Arxana is the name given to a series of prototype
     implementations of the scholium-based document model with
     an Emacs front-end.  Arxana is inspired in part by Ted
     Nelson's Xanadu™ project, which was the first effort to
     work with ``hypertext'' per se
     \cite{nelson1981literary}. We have been specifically
     interested in applications within mathematics, which has
     given Arxana a unique flavour.  In particular, we propose
     to use a scholium model to model the logic of proofs, not
     just to represent mathematical texts for reading.

- CD :: Conceptual Dependence was introduced as a tool for
     understanding natural language \cite{schank1972conceptual}. It
     is also used to represent knowledge about actions
     \cite{lytinen1992conceptual,sowa2008conceptual}.  The basis of
     the theory is a set of /primitives/ which describe basic types
     of actions such as "PTRANS — transfer of location" or "MBUILD
     — construction of a thought or new information". Each
     primitive comes with a set of /slots/ which accept objects of
     certain types. By filling in the slots of a primitive, one
     obtains the most elementary form of a /conceptual dependency
     graph/. By combining such basic graphs, one can build up more
     complicated CD graphs which describe actions in greater
     detail.

** Plan of our ICFP workshop contributions

We used these bullet points as our main outline for the paper, though
the sections have since been given shorter titles.  An early outline
of the paper can be found in http://metameso.org/ar/farm-2017.org.

- Unlike a classical proof which consists of mathematical statements
  and deductions, informal mathematical language is more general, and
  the reasoning involved may be abductive, inductive, or heuristic.

- The presentation here will describe a strategy we have been
  developing for representing mathematical dialogues and other
  informal texts.

- A publication appearing in "Artificial Intelligence" this month
  describes the high-level features of informal mathematics, and
  helped inspire this project.

- Our latest efforts produce more detailed models mathematical
  arguments.

- A graphical formalism and a corresponding prototype implementation
  will be described.

- Applications include modelling collaborative proof dialogues and
  discursive Q&A, as well as more traditional proofs.

- /In our planned next steps we plan to bring in explicit type-theoretic representations of mathematical objects within a service-oriented architecture./

 - [Scheme branch]
  - LISP stuff, implementation, search and programming, hypergraphs
  - pattern matching (like grep), but now since we're doing LISP, and LISP functions are cells -- parsing and grep might fit into this (compare "Graph Grammars" and clojure.spec regexps)
  - /think about what our ≈five slides would be/
  - CDs

 - [FARM branch]
  - mob programming
  - music from corneli, pease, stefanou survey ("Chapter 6")
  - prior art: board games, story stuff

** Statement of the research problem

The kinds of structures that are described by ``IAT+Content''
are still more or less graphs.  However, to work with
mathematics we need to be able to talk about /hypergraphs/.  For
example, if we say ``In September 1993, an error was found in
Wiles's proposed proof of Fermat's Last Theorem'' we would like
to point to the entire proposed proof as an object.  Similarly,
we would like to be able to draw a connection between this 1993
proposal with the corrected version published in 1995.

As we will see (*I should think! -JC*), even a proof itself is
more conveniently represented by hypergraph structures.  In
particular, some of the ``predicates'' are really generative
functions.  Indeed, some of them are ``heuristics'' which take
some work to specify.

Another feature of our representation is that hypergraphs can be
placed inside nodes and links of other hypergraphs.  This allows
one to organize ther representation by levels of generality.  For
instance, at the highest level, there might be the structure of
statements and proofs of theorems.  At thje next level, there
would be the individual propositions and the argument structure.
At the lowest level, there would be the grammatical structure of
the propositions.  Having a way of ``coarse-graining'' the
representation is important in order to have it be managable and
allow users to zoom in and out of the map to find the appropriate
level of detail.   This is related to Faré's categorical theory
of levels of a computer system [add citation].

One effect of this is that the markup we are devising is
``progressive'' in the sense that we can describe heuristics with
nodes without fully formalising them.  A corresponding user feature is
to be able to fold things at many levels.  This is important because
the diagrams get quite large.

*** Proofs and prologues

In several of our examples, such as the Gowers problem and Artin's
book, on sees a structure in which a proof or calculation is preceded
by a kind of prologue in which the author describes motivation and
strategy.  Unlike the proof proper which consists of mathematical
statements and deductions, the language here is more general and
the reasoning may be abductive, inductive, or heuristic.

We would like to have a representation for these sorts of prologues
and indicate how they connect with the proof which they introduce
as well as the rest of the text.  A challenge here is that the
texts in question can allude and refer to all sorts of referents
including themselves at a high level of abstraction and require
a certain amount of common sense to be understood.

Since the issues that arise here are similar to those which arise in
undestanding and representing natural language stories, we should be
able to adapt techniques such as conceptual dependency relation or
goals and themes to a mathematical context.

*** Registers of mathematical discourse

The natural language which occurs in mathematical texts comes in
several different types.  Since these types differ in their
vocabulary, manner of reasoning, subject matter, and degree of
literality, it simplifies the study of the subject to distinguish
these types and examine them individually.

**** The formal register
One type of mathematical language is what we may call the
/formal register/.  This is the type of language which is used to state
mathematical propositions.  For example, "Every natural number can be
expressed as the sum of four squares." or "In every triangle, the sum
of the angles equals two right angles."  In this register, vocabulary
is interpreted in a certain technical fashion and the reasoning is
purely deductive.  Semantically, such statements are assumed to be
equivalent to symbolic expressions in formal logic (in whatever formal
system one is working).  For the examples, the following would be
formal equivalents:
\begin{align*}
  &(\forall n \in \mathbb{N}) (\exists a, b, c, d \in \mathbb{N})
     n = a^2 + b^2 + c^2 + d^2 \\
  &(\forall \Delta abc \in \mathrm{triangle})
     \angle abc + \angle bca + \angle cab = 2 * \perp
\end{align*}
Indeed, in mathematical writing, such statements in natural language
and their formal equivalents both appear and may even be combined
within a single sentence, such as "Whenever $(x, y)$ lies inside the
region, we have $x^2 + y^4 < 12$."

This register of discourse has been studied by de Bruijn, Ranta, Mohan
and others and there exist parsers which can translate between natural
language and formal expressions.  Once we have formal representations,
we can reason about them using tools from Frege and others.

While there is much work to be done towards developing a formal linguistic
theory of mathematics, at least some basic principles are understood and have
been illustrated with example programs so, for the purpose of this project,
we shall take this subject as given and allow ourselves to introduce
formal restatements of propositions without worrying about how the
translation might be accomplished.

**** The expository register
Another type of mathematical language is what we will call the
/expository register/.  This is the sublanguage which is used to
express how and why one is interested in a particular formal statement
and describe mathematical reasoning.  Examples of such language
include:

+ It is easy to see that our theory is complete if we assume the
  descending chain condition.

+ A more elegant way of proving theorem 5 is by induction on the
  degree; however, we chose to present the current proof because it
  makes it clear that the result depends upon the factorizibility
  condition.

+ Is it possible to prove that any point and any line will do?

+ Can we do this for $x+yx+y$? For $e$? Rationals with small denominator?

The expository register has several salient features which work together:

# Expanded a bit more in http://metameso.org/cgi-bin/current.pl/Two_years_later
# terms - put examples

- Mathematical content (Universe of discourse) :: The main focus of this type of discusses are mathematical objects and mathematical propositions (which may exist in analogy with physical objects or psychological states).  These are used to convey *narratives* of how one or more actors navigate their way through mathematical hyperreality.  Formal mathematics models the objects in this universe of discourse and their relationships, but the discourse itself is not necessarily formal.

- Metamathematical reasoning :: It is metamathematical, discussing not only with objects and propositions, but also inference and proofs.  For instance, in the first example *"It is easy to see that our theory is complete if we assume the
  descending chain condition"* says something about the proof of a statement.  Likewise, it indicates types of proofs and proof strategies.  It is however,
not a purely formal statement.  It relies on the next feature:

- Heuristic value judgements :: Whereas the formal register only has deductive reasoning of the strictest sort, in the expository register we also have *inductive* and *abductive* reasoning as well as reasoning by analogy, heuristics, and looser forms of approximate and plausible reasoning.  Concomittantly, the truth judgements made go beyond the truth values of formal logic to vaguer assertions such as "this proof is elegant" or "this statement sounds likely to be false".  This is closer to what one has in non-mathetical discourse.  These sorts of assertions influence the choice of actions and strategies.

*** Related fields

In order to build a computational theory of the expository register,
we will draw upon several well-studied topics in AI which deal with
situations that have common features, namely the block world, board
games, and story comprehension.

| /Level/               | *Block World*     | *Board Games*         | *Story Comprehension* |
|-----------------------+-------------------+-----------------------+-----------------------|
| universe of discourse | blocks on a table | game pieces on board  | everyday life         |
| reasoning             | instructions      | rules & strategy      | analogy               |
| value                 | consistency?      | prediction of winning | costs and benefits    |
| role of disagreement  | none              | multiple strategies   | ethical dilemmas      |

In a mathematical setting, thespects are modelled in "IATC" or
"Inference Anchoring Theory + Content" \cite{martin2017bootstrapping,corneli2017towards}.

In a Lakatos setting disagreement is the primary engine that drives discovery.

** Suitability of venue

As we will also see, it is not just incidental that our work is
implemented in LISP.  Actually, the kind of hypergraph programs
we use are a ``natural'' extension of the basic LISP data model.

Emacs (and Org mode) are suitable for interacting with other
programming languages and long-running processes, e.g., MAXIMA.
(Also see preiterature on heuristics in LISP from Lenat.)

*** What is on offer in this approach

Kinematics vs dynamics.

Purely formal logic written as graph subsitution - example.

One thing we have here is links that contain code.

Another thing hypergraphs give us is links to links - of course
we can also think about higher-dimensional versions of the same,
but links to links is the main thing.

* Guide to files in our git repository <<short-docs>>
** org
*** arxana-redux.org
*This file -- a guide to our work in progress.*
*** robotone-opensets.org
Walk through a simple proof ROBOTONE proof from \cite{Ganesalingam2016} and mark it up in IATC.
*** mpm.org
Walk through parts of a MiniPolymath proof and mark it up in IATC.
*** scheme-2017.org
Our submitted abstract for Scheme 2017 lightning talk.
*** gowers2012.org
Walk through a simple proof from Gowers and mark it up in IATC.
*** ciao-talk.org
Slides on "Reasoning about mathematics with graphical programs" presented Tuesday 23 May, 2017 at "CIAO 25 AB 70" in Edinburgh.
*** farm-2017.org
Preliminary outline of our FARM 2017 submission.
** elisp
*** binom-demo.el
*** bootstart.el
*** clyde.el
*** honey.el
All of the code for low-layer HONEY functionality.
*** prelim.el
*** sch-prog-demo.el
*** sch-prog.el
*** simple-ui.el
*** search-expanded.el
This contains meso-layer search functionality built on top of HONEY.
*** tarot.el
Used for building arxana.net.  Could be expanded to produce adaptive text (e.g., narrative tarot readings); see \cite{veale2017dejavu} for an illustration of how.
** latex
*** arxana-reboot.tex <<arxana2010>>
This is the 2010-era version of Arxana.  Unlike its predecessor [[arxana2005]], this uses Common Lisp and
MySQL for storage, so setup is more complicated.  In principle some other external datastore could
be used, i.e., a [[https://en.wikipedia.org/wiki/Graph_database][graph database]] like [[https://en.wikipedia.org/wiki/Neo4j][Neo4j]] or a hypergraph database like [[http://hypergraphdb.org/][HypergraphDB]] or [[https://github.com/opencog/atomspace][AtomSpace]],
the latter being especially quite close to what we're working on, since they make use
of "Atoms" which are similar to our "nemas", and since they have Scheme bindings for their
database operations.
*** honey-demo.tex
Exposition of the "Higher Order NEsted Yarnknotter" (HONEY) system.  Some of this text went into our paper for FARM 2017.
*** sbdm4cbpp.tex <<arxana2005>>
This is the 2005-era version of Arxana.  It runs entirely in Emacs, using a hash table for storage.
A version of the software was demoed in Atlanta at the Free Culture and the Digital Library Symposium, in connection with
\cite{corneli2005scholia}.  It was largely replaced by [[arxana2010]], though this version still has some features that the
later version lacked.
*** sch-prog.png
A figure to illustrate code embedded inside of networks; used in the FARM paper.
** and elsewhere
*** In our web directory
*** On the old AsteroidMeta wiki
*** On Overleaf
* Infrastructure

This file is in versioned storage in the "mob" branch of our arxana
repo; instructions to access are here:
http://repo.or.cz/w/arxana.git/blob_plain/d187e244a8eb7d2208f1fe98db1ef895c6cd4a36:/README.mob

A working copy of this repository is checked out at
=/home/shared-folder/arxana-redux/arxana/= on the Linode.

And a "scratch" copy of the file has been copied to:
=/home/shared-folder/arxana-redux/arxana-redux.org=

This can be edited in live sessions using floobits.

*Note* Due to buggy behavior of togetherly, we've since decided to
switch to Floobits for live editing sessions, via:

=M-x floobits-join-workspace RET https://floobits.com/holtzermann17/arxana RET=

* Extensions to the core of IATC

** IAT + CD

By itself, IAT is useful for describing *what* takes place in a
mathematical discourse, but not so useful for figuring out *why*
and *how* (viz., kinematics and dynamics).  To address these issues,
we will augment it with the framework of /conceptual dependency theory/ (CD),
which has been used for such purposes in the context of machine understanding of stories
\cite{leon2011computational}.

# also a chapter in the AI Handbook.

The main ingredient of CD is a set of *primitives* which describe
types of actions.  Ususally, these consist of various physical and
mental operations but, for the purpose at hand, we will take them to
be the *performatives* of IAT.

We will have two classes of objects: the participants in the dialogue
and mathematical propositions.  

*** TODO We should figure out what the inferences between basic assertions (I/R, I/E, etc.) would look like here. (e.g. fig. 7 of Lytinen)

- links between basic CD's
 - e.g., joe communicated the IP address to ray, by talking, so that ray could get on the server

** Goals

In order to figure out why and how actions take place, CD theory
introduces procedural knowledge in the form of scripts, MOPs, TOPs,
goals, and plans.  For our purposes, goals and plans will be used.

This relates to the meta items of the spec.  Maybe we should expand
the goal item using some sort of ontology like that of Schank and
Ableson.

** Parsing

A simple example from \cite{lytinen1992conceptual} schematizes the
sentence "John gave Mary a book" as an s-expression.

#+BEGIN_SRC lisp
(atrans actor  (person name john)
        object (phys-obj type book)
        recip  (person name mary))
#+END_SRC

** Possible "warm up" example

"Adjoints exist and are unique." - See Halmos.

#+BEGIN_SRC lisp
(defn adjoint-of-a-bounded-linear-operator-on-a-hilbert-space
  (X Y A Astar)
  (hilbert-space X)
  (hilbert-space Y)
  (bounded-linear-operator A X Y)
  (and (map Astar Y X)
       (forall x :in X :st
               (forall y :in Y :st
                       (eq (inner-product :on Y :of (A x) y)
                           (inner-product :on X :of x (Astar y)))))))

(defproof
  adjoint-of-a-bounded-linear-operator-on-a-hilbert-space:fact:
  adjoints-exist-and-are-unique (A X Y)
  (hilbert-space X)
  (hilbert-space Y)
  (bounded-linear-operator A X Y)
  (bind phi (map phi X Y :takes x
                 :to (inner-product :on Y :of (A x) y)))
  ;; We need to show that phi is linear, but that’s ‘easy’
  (shows (linear phi)
         (linear A)
         (properties-of-inner-product))
  ;; The lemma allows us to spawn a reasonable target
  (obtain v :st
          (unique v :in X :st
                  (forall u :in X :st (eq (varphi u)
                                          (inner-product :in X :of u v))))
          (uniquely-represent-a-linear-functional-by-an-inner-product
           X phi))
  (bind Astar (map Astar Y X :takes w :to v))
  ;; Finally, assert that the Astar so constructed is the adjoint
  (assert (adjoint-of-a-bounded-linear-operator-on-a-hilbert-space X Y
                                                                   A Astar)))
#+END_SRC

** Arxana

*** Basic features

The basis of Arxana is higher-order nested semantic networks.  By
``higher order'', it is meant that links can point to other links.  By
``nested'', it is meant that the nodes which make up a network may
contain other networks, which themselves may have nodes containing yet
other networks, etc., ad nauseam or ad infinitum, whichever comes
first.  In addition, all the links are bidirectional and no
fundamental distinction is made between links and nodes.  This
sophistication makes the package suitable as a platform to construct
knowledge bases for such advanced applications as hyperreal
dictionaries.

For convenience and flexibility, this package has been designed in a
modular and extensible fashion.  The basic functionality is provided
by a back-end which manages the data of the network.  In the
implementation described here, this data is stored in hash tables, but
one could instead have it stored in, say, a relational database or a
file system by writing a suitable back-end and using that instead.
For higher-level access to the data is mediated by means of a handful
of primitive commands and, as long as these commands behave similarly,
it does not matter to the end user how they are implemented or how the
data is represented internally.

Since these primitive command are, well, primitive, restricting
oneself to them would be quite a tedious way to interact with the
knowledge base except for basic maintenance operations.  Thus, on top
of the built-in layer, one would normally add a layer or two of
application packages which accomplish more sophisticated tasks such as
rendering documents or updating links en masse or implement different
types of documents as semantic nets.  In the interests of integrity of
the knowledge base and modularity with respect to its representation,
these routines should not access the underlying databases directly but
call upon the primitive access functions to do their bidding.  In a
finished application, one might even have several layers, say a middle
end which implements layered services upon the database and a
front-end which provides a user-friendly interface to these services.

The basic unit from which we will construct our networks is called an
``article''.  Articles are data objects which serve to encode both
links and nodes and are characterized by the following components:

- Identifier
- Source
- Sink
- Content

Each article has a unique identifier which the computer assigns to it
when it is entered into the database.  This identifier is used by the
access functions to refer to the article for subsequent operations.
Since talking about, say, article 12 pointing to article 5 is not
intuitive for most users, the system also has a mechanism for
assigning names to articles so that one could instead, say, refer to
``walrus'' pointing to ``mammal'' instead.

Source and sink are pointers to other articles and content is a place
in which to store a lisp object, which might be some text, or an
expression, or maybe a number or maybe something else depending on
what intends to represent with one's network and how one intends to
use it.  In particular, the content of an article can even be another
network constructed out of more articles.

In order to provide a foundation for building up networks, there is a
special article ``ground'' which serves as a foundation.  It is the
zero object of our system; its source and sink is itself and its
content is nil.  To enter an article which is meant as a node, we set
its source and its sink to ground.  We can also set the source to
ground and sink to a non-ground article or vice-versa; this provides a
means for creating ``stickies'' which attach directly to articles, a
construction for which we shall find use from time to time.

This system of articles each of which point to two other articles and
a ground article is similar to the cons cells of lisp, but expands the
paradigm in two important ways --- the cells carry content and the
links are bidirectional.  These differences allow the system under
consideration to accomplish things which would not be feasible with
plain old s-expressions.

Bidirectional linking means that the links are stored and accessed in
a manner which makes it no more costly to find and traverse links in
the backwards than the forward direction.  This is what makes it
practical to make links as mentioned above and done explicitly below.

Storing content in articles is what allows us to construct nodes.
While, in lisp, =(cons nil nil)= is certainly valid, it's not
terribly useful since it doesn't carry much information.  However,
when we can attach information to a cell, then each such object is
able to serve as a distinct carrier of information and can be quite
useful.  In the case of links, this room for extra information can be
used to do things like, say, specify what part of a story is being
considered in a link to a comment on a story.

*** Hypergraph search

- Search item consists of a hypergraph whose articles contain predicates.

- Given such a query hypergraph and any other hypergraph, which we
  will consider as a database, a match consists of a mapping of
  hypergraphs from the query to the database such that, for every
  article in the query, the predicate it contains is true of the
  contents of the corresponding database article.

- The predicate can be any lisp function.  Within reason, of course
  --- we want it to say something sensible and relevant when applied
  to database content.  If we have a type system in place, this would
  be a good place to deploy it.

- Since lisp functions can be recursive and nested, the above fact,
  especially when combined with the text-as-program feature, allows
  for a high level of expressivity and complexity.

- By modelling various structures as hypergraphs, we can search for
  instances of them.

- If we implement typing via a special node "type" and as links of
  type "type", we can search for items by type.

- If we implement subcollections as cones (essentially the same idea)
  we can restrict searches to subcollections.

- If we represent logical inferences as matching subhypergraphs, this
  can check or find proofs.

- If we represent production rules as hypergraph patterns, we can
  parse and become experts.

- cf. graph grammars.

- This also smells like generalized elements and presheaf categories.

- What would a relational version a la kanren looked like?

*** Text as program

We can also treat content of articles as executable programs.  This by
itself is unteresting since, in lisp, code is data and the content
happens to be data so, of course it might be code.  What makes it
worthy of attention is that we can also specify bindings of symbols
scholiumifically.

Since there are many ways to specify such links but we do not want to
prejudice any one of them over any other, we ask that the user
provides a function which, given a node, produces an association list
of symbols and their values.  Similarly, in the interest of
generality, we allow the user to specify a function which extracts the
code contained in a node.  As we shall see, there are circumstances
under which one would not want the code to simply be the text
contained in a given node.

The main function which implements this functionality is ~node-fun~.
This function takes as input a node, a function to retrieve links and
a function to retrieve code.  As output, it produces a lambda
expression which is the retrived code wrapped inside a let statement
which provides the environment.  Furthermore, the wrapper code is
written in such a way that evaluation of symbol values does not happen
at the time ~node-fun~ runs, but is delayed until that symbol is
evaluated.  This feature makes possible recursion since, given a
function which directly or indirectly calls itsef, unwinding the
recursive calls will not be done at once leading to an explosion but
will proceed on a need-to know basis.

One important use of this facility in the scholium based document
model is handling clusions.  The basic feature of clusions is that,
rather than simply looking at the text of a node, one instead
generates a text from that node by processing that text in its
network context.  A classical example would be one where the text
contains link anchors which mean "copy this portion of the texts from
some other node".  In this case the processing would consist of
looking up those references and inserting the portions in the
appropriate places (i.e. quasiquotation).  Furthermore, due to
possibility of recursion described above, it is possible that the
texts cited might themselves be in need of similar assembly.  To be
sure, in such situations, there is a danger of infinite regress
crashing the system but, in the spirit of lisp, we have opted to
preserve expressivity rather than try to implement some safeguard or
another which would limit the what could be said in one way or
another.  The essence of clusion is replacing ~value~ with ~(value)~.

Another use of being able to run scholium-based documents as documents
is /annotative programming/, which is a style of programming in which
programs take the form of hypertext and dependencies are indicated by
links.  Other languages which supprort this style are Kurzweil's Flare
and Nelson's ZigZag.

* Task tree
** Progress on preparing the work for public consumption

*** DONE Corpus/Examples: Hand-drawn diagrams in IAT+C

/We are allowed to submit an appendix without a size limit, so if we don't have room for all of the diagrams in the paper, we could put them in the appendix./

- Minipolymath, treated by Gabi in the Transactions on Social Computing paper, pdf available from https://www.overleaf.com/read/jyhzpqsythzq
- Our randomly selected MathOverflow discussion (from Q&A article)
- Gowers 2012 trick problem, http://metameso.org/ar/gowers-example.pdf
- Also there's Schuam's Abstract Algebra exercise 337, a diagram is shown on arxana.net.
 - Redone using IATC: http://metameso.org/ar/schuams-example.pdf
- An example from the Ganesalingam and Gowers paper: http://metameso.org/ar/robotone-example.pdf
- Galois theory. Emil Artin's book.
- Euclid algorithm
- possibly an example from metamath or coq or whatever to show that we can model that stuff as discourse...
- ...

*** DONE Other Background

**** Items we've worked on before

Over the years as we've worked on Arxana, we have generated all sorts
of files.  Here are descriptions and locations of some of them which
are relevant to the current project.

Many of these are stored in =/home/shared-folder/public_html/=, and
accessible on the web at [[http://metameso.org/ar/]].

***** Research notes

- "nemas" document:  http://metameso.org/ar/metamathematics.pdf
- Joe's thesis Appendix B: http://metameso.org/ar/thesis-appendix-b.pdf
- Metamathematics preprint: http://metameso.org/ar/mathematical-semantics.pdf
- hcode function spec: http://metameso.org/ar/hcode.pdf
- Lakatos game spec: http://metameso.org/ar/lakatos-flowchart.pdf

***** Wiki

- [[http://metameso.org/cgi-bin/current.pl?action=browse;oldid=Arxana;id=A_scholium-based_document_model][A scholium-based document model]] is the wiki homepage for Arxana and has several relevant discussions.
- [[http://metameso.org/cgi-bin/current.pl/Two_years_later][Two years later]] collects many of the mathematical themes in
  overview
- [[http://metameso.org/cgi-bin/current.pl/samples_of_formal_mathematical_writing][samples of formal mathematical writing]] is a small collection
  of statements in mathematical language (leaving out ``the part
  in between dollar signs'')

***** Website

- [[http://arxana.net][arxana.net]] has links to source code from various prototypes
 - It also has a small gallery of hand-drawn diagrams

**** And other things elsewhere:

- /Handbook of artificial intelligence/ by Barr and Feigenbaum describes *SAM* and *PAM*, the /Script Applier Mechanism/ and /Plan Applier Mechanism/ by Schank and Abelson et al., on page 306 et seq. \cite{barr1981handbook}
- Winograd, Natural language and stories --- MIT AI Technical Report 235, February 1971 with the title "Procedures as a Representation for Data in a Computer Program for Understanding Natural Language" ([[http://hci.stanford.edu/winograd/shrdlu/AITR-235.pdf][link]])
 - Could we reuse this stuff for the "narrative"
 - How do we know how to read the text and transform it into IATC?
 - An example is Gowers's "total stuckness": how do we turn that into code?
- Conceptual dependency representation - from "Deep Blue" website ([[https://deepblue.lib.umich.edu/bitstream/handle/2027.42/30278/0000679.pdf?sequence=1][link]]).
 - Schank's MARGIE system is described on page 300 /et seq./ of \cite{barr1981handbook}.
- AI textbook in wiki.

*** DONE Initial non-working pseudocode prototype

It makes sense to at least try and transcribe the main examples in
some "pseudocode", inspired by IATC and hcode, which we can then
refine into a working version later.

**** Initial transcription

As per the headline, these don't currently *do* anything.

- http://metameso.org/ar/mpm3.html
- http://metameso.org/ar/gowers2012.html
- http://metameso.org/ar/robotone-opensets.html

**** More detailed transcription

In our FARM paper we have analysed some of the Gowers paper in more
depth.

*** TODO Complete a short summary documentation
The section [[short-docs]] here is a start.
*** TODO Clean up namespaces of functions
*** TODO Write an IATCD evaluator
*** TODO connect frontend for interaction and backend for storage
Backend storage could be a database or something else
*** TODO find the generic inteface layer and put it in its own file
*** TODO Having assembled a buffer from distributed storage, put things back where they came from :UI:
*** TODO Write some simple user language and an interface that generates triplets/quintuplets
*** TODO Basic working version
What this means is "Demo the system walking through the steps of a
proof like GCP or MPM."
*** TODO Fuzzy search to retrieve loose matches and analogies
*** TODO Demo with APM-Xi content
Show interface with types
*** TODO Demo with APM prelim problems
*** TODO Public demoable version
Could go to the BCS contest on *September 1, 2017* if we're ready.
*** TODO Write up applications to mathematics
Possibly for IJCAI/ECAI.
Papers due *January 2018*?
To take place *July 13-19, 2018*
http://www.chessprogress.com/IJCAI-2018/calls/
*** TODO logic programming like in Reasoned Schemer but with hypergraphs
Possibly submit to [[http://conf.researchr.org/home/icfp-2018][ICFP]]. Papers due *Fri 16 Mar 2018*.
Event to take place in St. Louis, Missouri, United States, to take place *late September*.
*** TODO Can the system come up with answers to new, basic, questions?

- Inspired by Nuamah et al's geography examples
- Simple comparisons, like, how does this concept relate to that concept?  We informally talk about this as ``analogy'' between concepts.  But...

*** TODO Foldable views (like in Org mode) so that people can browse proofs

- This may come after the May submission
- Folding and unfolding the definitions of terms in something like an APM context is relevant example.  Just `unpacking' terms.

** Future work
*** Immediate upcoming
**** Emacs NYC July 10th
**** Include in Big Proof talk same week
*** Formal proof
**** Demo the system walking through the steps of a proof like GCP or MPM.
**** Refine both representations and reasoning aspects.
**** Integrate external computer algebra / proof checking systems.
*** Embodiment and cognitive science
**** Build on CD theory to reason about embodied intuitions in geometric problems, integrate with Lakoff and Núñez's conceptual metaphors \cite{kaliszyk2014developing-misc}.
*** Linguistics and NLP
**** Integrate parsers to generate IATC+CD automatically.
**** Use these models to seed statistical machine learning, e.g., expanding on the work of Kaliszyk et al who ascertained the frequency of various schematic usages like ``let $X$ be a $Y$'' in a specific corpus of proofs.
*** Machine learning
**** Integrate with knowledge bases of mathematical terms and frequency data (as above).
**** Model Stack Exchange dialogues, in parallel with the work done  on Reddit discussions \cite{zhang2017characterizing}.
**** Build a system with multiple agents that ``converse with each other to sharpen their wits'' \cite{heretical-theory}.

* Related work

** In a mathematics context

- ``Lakatos-style Collaborative Mathematics through Dialectical,
  Structured and Abstract Argumentation'' shows how it is possible to
  ``formalize'' the informal logic proposed by Lakatos
  \cite{pease2017lakatos}.
- [[http://www.emis.de/monographs/Trzeciak/biglist.html][Mathematical English Usage - a Dictionary]] (Jerzy Trzeciak)
- [[https://case.edu/artsci/math/wells/pub/html/abouthbk.html][The Handbook of Mathematical Discourse]] (Charles Wells)
- [[http://universaar.uni-saarland.de/monographien/volltexte/2015/111/pdf/wolska_mathematicalProofs_komplett_e.pdf][Students'language in computer-assisted tutoring of mathematical proofs]] (Magdalena A. Wolska)

** Does what we're doing relate in any way to other formal proof checkers?

- Default answer: no, because people have build large repositories of formal math (Mizar, Coq, metamath, etc.).  These other projects don't make a serious effort to deal with mathematical text.  TeX is in one place, and logic is in another place.

 - There's another paper by Josef Urban et al. that is the exception that proves the rule \cite{kaliszyk2014developing} (see also the poster that accompanied this paper \cite{kaliszyk2014developing-misc})

- There's also a generative program by Ganesalingam and Gowers thath meshes natural language and formal mathematical reasoning.

- With these examples in mind, we assert that what we are doing can be combined with proof checkers synergistically.  For instance, one could attach scholia to the statements in an IAT representation which contain formalized representations of the content, and scholia which indicate that certain statements have been 
* The core language

Here we'll describe the structures coming from several different
places, e.g., Gabi, Lakatos, etc.

** Content (=structure=)                                               :GRAY:
*** object $O$ is =used_in= proposition $P$
**** Example: ``The Caley graph of group \(G\)'' has sub-object $G$
*** proposition $Q$ is a =sub-proposition= of proposition $P$
**** Example: ``$P$ is difficult to prove'' has sub-proposition $P$
*** proposition $R$ is a =reformed= version of proposition $P$
**** Example: ``Every $x$ is a \(P\)'' might be reformed to ``Some $x$ is a \(P\)''
*** property $p$ is as the =extensional_set= of all objects with property $p$
**** Example: the set $\mathcal{P}$ of primes is the extension of the predicate $\mathit{prime}$.
*** $O$ =instantiates= some class $C$
**** Comment: This is not quite syntactic sugar for =has_property=!
If we have a class of items $C$ we want to be able say that $x$ is a
member of $C$.  In principle, we could write $x$ =has_property= $C$.
But I think there are cases where we would want to
distinguish between, e.g.,
$2$ =has_property= prime, and $prime(2)$ =instantiates=
$prime(x)$.  This =instantiates= operation is a natural extension of
backquote; so e.g., we could write the true statement
$prime(4)$ =instantiates= $prime(x)$, even though $prime(4)$ is false.
**** Comment: Perhaps we need a further distinction between objects and 'schemas'
So we might write =has_property(member_of(x,primes))= to talk about
class membership.  Presumably (except in Russell paradox situations)
this is the same as =has_property(x,prime)=, or whatever.
*** $s$ =expands= $y$
**** Comment: This is something that a computer algebra system like MAXIMA could confirm
*** $s$ =sums= $y$
**** Comment: This is something that a computer algebra system like MAXIMA could confirm
*** $s$ =contains as summand= $t$
**** Comment: This is more specific than the =used in= relation
This relation is interesting, for example, in the case of sums like
$s+t$ where $t$ is, or might be, ``small''.  Note that there
would be similar ways to talk about any algebraic or
syntactic relation (e.g., multiplicand or integrand or whatever).
In my opinion this is better than having one general-purpose 'structural'
relation that loses the distinction between all of these.  However,
generalising in this way does open a can of worms for addressing.
I.e. do we need XPATH or something like that for indexing into
something deeply nested?
*** $M$ =generalises= $m$
**** Comment: Here, content relationships between methods.
Does this work?  Instead of talking about content relationships 'at
the content level' we are now interested in assertions like
"binomial theorem" =generalises= "eliminate cross terms",
where both of the quoted concepts are heuristics, not 'predicates'
*** Proposition vs Object vs Binder vs Inference rule?
Note that there are different kinds of `content'.  If for example I
say `\(0<a<b<1 \Rightarrow a^N < b^N\)', then this is more than just a
proposition, but something that can be used as a ``binder''; i.e., if
I fill in specific values of $a$ and $b$ (and, optionally, $N$) I know
the property holds for them.  At the same time, this sort of "binder"
is presumably also a *theorem* that has been proved.  This is,
additionally, similar to an *inference rule* since it allows us to move
from one statement to another, schematically (see discussion above
about "instantiates").  Anyway, this isn't yet about another kind of
structural relation, but it does suggest that we should be a bit
careful about how we think about content.
** inferential structure (=rel=)                                       :PINK:
*** =stronger= (s,t)
*** =not= (s)
*** =conjunction= (s,t)
*** =has_property= (o,p)
**** Comment: It seems useful in some case to be able to say that a 'method' or heuristic has a property
E.g. =has_property(strategyx, HAL)=
**** Comment: has_property should probably 'emit' the property as a side-effect
This way we can more easily see which is the object and which is the property.
It seems that thing that has a property may also be a 'proposition',
or, at least, a bit of 'object code' (like: "compute XYZ").
Furthermore, at least in this case, the 'property' might be a heuristic
or method (like "we actually know how to compute this").
*** =instance_of= (o,m)
*** =independent_of= (o,d)
*** =case_split= (s, {si}.i)
*** =wlog= (s,t)
** reasoning tactics; ``meta''/guiding (=meta=)                        :BLUE:
*** =goal= (s)
*** =strategy= (s,m)
**** Note: use method $m$ to prove $s$
**** Comment: perhaps this should be =strategy= (m [, s ]) so that s is optional
This is because, just for graphical simplicity, we might assume that
the statement that we want to prove is known in advance (e.g., it is
the statement of the problem).

This is the style at the beginning of gowers-example.pdf
**** Comment: how to show that a suggestion 'has been implemented'?
We might need some other form of 'certificate' for that.
E.g., it would say =implements(BLOB OF CODE,strategyx)=.
*** =auxiliary= (s,a)
*** =analogy= (s,t)
**** Comment: analogies between statements are different from auxiliaries to prove
Introducing some set of 'analogies' in a way sets us up for
'inductive' reasoning across a class of examples.  What do they all
have in common?  Which one is the most suitable?  Etc.
** heuristics and value judgements (=value=)                          :GREEN:
*** =easy= (s,t)
*** =plausible= (s)
*** =beautiful= (s)
*** =useful= (s)
*** =heuristic= (x)
**** Comment: It seems that we will have several layers of 'guidance'
Many of them will be neither value judgements nor metamathematical tags
like =strategy=, =goal=, or =auxiliary=.  Rather, the heuristics may be
used at an even higher level to produce or to implement these.  So,
for example, the heuristic might be what a =strategy= concretely
suggests.  It's also true that a given =auxiliary= might need a
heuristic "header", that explains /why/ this auxiliary problem has
been suggested.  Similar to a =strategy= the heuristic might look
for something that 'satisfies' or 'implements' the heuristics.
In some cases we've looked at, this 'satisficing' object will appear
directly as the argument of the heuristic, hence =heuristic(x)=.
For example: =specialise(THE PROBLEM, (sqrt(2)+sqrt(3))^2)=.
Incidentally, this particular example is only meaningful in connection
with *another* heuristic that has told us how to *generalise* the
problem, i.e., that has turned a static expression into something
with a variable in it.
** Performatives (=perf=)                                            :YELLOW:
*** =Agree= (s [, a ])
**** Note: optional argument $a$ is a justification for $s$
*** =Assert= (s [, a ])
**** Note: optional argument $a$ is support for $s$
**** Comment: It seems like we might want to be able to assert a 'graph structure'
Here is an example from early in gowers-example.pdf
#+BEGIN_SRC c
Assert(exists(strategy(PROBLEM, strategyx))
       AND has_property(strategyx,HAL))
#+END_SRC
*** =Challenge= (s [, c ])
**** Note: $c$ is a counter-argument or counter-example to $s$
*** =Define= (o,p)
**** Note: object with name $o$ satisfies property $p$
*** =Judge= (s)
**** Note: takes a =value= argument
*** =Query= (s)
*** =QueryE= ({pi(X)}.i)
**** Note: Asks for the class of objects  for which all of the properties pi hold
*** =Retract= (s [, a ])
**** Note: can only be made by someone who asserted $s$; $a$ is an optional reason
*** =Suggest= (s)
**** Note: Takes a =meta= argument