clean

[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 2017 workshop at the International Conference on
Functional Programming to take place at Oxford this Autumn, we will be
making a presentation on 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.

** Glossary of keywords

- 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.

** 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 Fare'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.

** 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.

*** What is on offer in this approach

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 link.

* 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 
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


* Task tree

** 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 =togetherly.el=.

** Progress on paper

*** 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...
- ...

*** 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 Feigenbaum (Sam and Pam)
- 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]]).
- AI textbook in wiki.

*** TODO Initial non-working pseudocode prototype

Here 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.

*** TODO Basic working version

*** 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.

* 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 formally verified.

** Further afield

/We're probably better off pruning these out of the final paper, but some topics of interest can be noted here./

- One interesting project within the DAG paradigm is the
  [[https://github.com/ipfs/ipfs/blob/master/papers/ipfs-cap2pfs/ipfs-p2p-file-system.pdf][InterPlanetary File System]] (IPFS).

* Future work

- I think it is probably not realistic to get the clojure.spec
  type-based work running *in addition* to the scholium-based
  stuff, but the topics seem related.  In particular, the
  objects that we would describe using clojure.spec are somehow
  the "C" in IAT+C.  So, we could have a think about how
  structural relationships between objects and propositions (per
  Gabi's description of IAT+C) might relate to the clojure.spec
  stuff.  I think would be appropriate to have a few pages of
  ``future work'' describing these issues.

* References                                                       :noexport:

# bibliography items are rendered
# with the following command

\printbibliography


* Annex

Tasks, timeline, and other things we don't need to include in the
final report.

** Timeline

Note: this could be more nicely organized using the org agenda.

** Week 17th April
*** Science March on Saturday
** Week 24th April
*** Met: Tuesday 25th April
*** DONE Joe get this document under version control
** Week 1 May
*** Meet Monday 1 May (note: this is a Bank Holiday in the UK)
** Week 8 May
*** Meet Saturday May 13
** Week 15 May
*** *outline* of talk May 16th
** Week 22 May
*** *Present* 23/24th May at [[http://dream.inf.ed.ac.uk/events/ciao-2017/][CIAO 2017]].                                :TALK:
*** *Submit* 26th May                                              :DEADLINE:

** Completed tasks

*** DONE Figure out what to do and record it in this document.         :meta:
*** DONE Set up collaborative editing for files.
*** WONTFIX Some way to share images (e.g. whiteboard in BBB or screenshare or...)
*** DONE Debug Togetherly
*** DONE make =visible-mode= on by default in this buffer

#+BEGIN_COMMENT
The following is for controlling Togetherly and Org mode.  This might
not be necessary if line 454 of togetherly.el is commented
out/changed.  Also, it isn't actually evaluated.  How to fix?
#+END_COMMENT

#+BEGIN_SRC emacs-lisp
(defun execute-startup-block ()
  (interactive)
  (show-all))
#+END_SRC

# Local Variables:
# eval: (+ 1 1)
# End: