Merge branch 'mob'

[arxana.git] / org / farm-2017.org

#+TITLE:     Functional models of mathematical reasoning
#+AUTHOR:    Joseph Corneli and Raymond Puzio
#+EMAIL:     contact@planetmath.org
#+DATE:      May 27, 2017 for Thursday 1 June, 2017 deadline
#+DESCRIPTION: Outline and draft of 12 page paper on math text analysis for FARM workshop at ICFP 2017
#+KEYWORDS: arxana, hypertext, inference anchoring theory
#+LANGUAGE: en
#+OPTIONS: H:3 num:nil 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: farm-refs plain
#+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex}
#+LATEX_HEADER: \addbibresource{farm-refs}
#+STARTUP: showeverything


#+BEGIN_QUOTE
Functional Programming has emerged as a mainstream software
development paradigm, and its artistic and creative use is booming. A
growing number of software toolkits, frameworks and environments for
art, music and design now employ functional programming languages and
techniques. FARM is a forum for exploration and critical evaluation of
these developments, for example to consider potential benefits of
greater consistency, tersity, and closer mapping to a problem domain.

FARM encourages submissions from across art, craft and design,
including textiles, visual art, *music*, 3D sculpture, animation, GUIs,
video *games*, 3D printing and architectural models, choreography,
*poetry*, and even VLSI layouts, GPU configurations, or
*mechanical engineering designs*.  *Theoretical foundations*, *language design*,
*implementation issues*, and *applications* in industry or the arts are
all within the scope of the workshop.  The language used need not be
purely functional (“mostly functional” is fine), and may be manifested
as a domain specific language or tool.  Moreover, submissions focusing
on questions or issues about the use of functional programming are
within the scope.
#+END_QUOTE

* 0 Introduction

#+BEGIN_QUOTE
``To get to the moon, we needed crashes and endless fiddling.'' Gabriel and Goldman, "Mob Software: The Erotic Life of Code" \cite{gabriel2000mob}
#+END_QUOTE

** 0.1 CONTEXT OF APPLICATION
- modelling mathematical dialogues, people don't just write their things in metamath, ghilbert, HOL, etc.
- mathematical text contains argumentation and narrative in addition to logic and calculations
- if you /were/ using a formal system, there's approximately one way to write it down; in normal text there are lots of different expository choices you can make.  A popular book or an article.
** 0.2 FORCES
- push to make everything formal (QED, Tarski, LCF)
- push to make everything understandable (Alexander).  Halmos has a book on exposition, e.g. "How to write mathematics" essay.  Thurston "Proof and Progress".
** 0.3 PROBLEM
- because each different user will have a different "way in", depending on their background knowledge, we need to intelligently use our expository choices, e.g., so we can tailor a given formal content to a given reader.
- how to get behind the scenes to see why things work the way they do, or why they fail?; adding more intuition is another thing besides more clarity: building bridges from the way people think to the new question.  We often think in terms of diagrams!  Peirce said: "all mathematical reasoning is diagrammatic."  How can a computer be useful in such a circumstance?
** 0.4 SOLUTION (STRATEGY)
- thought: what we need is a computer system that's based on diagrammatic reasoning
- focus on expressivity
- focus on representing process
- formalization and efficiency are important, but will be left for later or forked off to something else.
- diagrammatic reasoning and functional programming go hand in hand
** 0.5 RATIONALE
- objective: understand mathematics as people do it (literary criticism, rhetoric, argumentation)
- objective: learn from these methods to build new mathematical texts, towards math AI!
- build on intuitive diagrams
- build on the idea of parsing natural language (complementary to Mohan's work; graph grammars?)
** 0.6 RESOLUTION of FORCES
- philosophical: bridging 'two cultures' (proof checkers and artists/designers/hackers).  Cf. Gowers's "two cultures"
- outcome: sharing diagrams with people who can use them
- potential: draw new diagrams?

* 1 THEORETICAL FOUNDATIONS Informal mathematical language is more general, and  the reasoning involved may be abductive, inductive, or heuristic. :RAY:

Even though a mathematical result and its proof involve strict logic,
the process of formulating, motivating proving and explaining go
beyond strict formality. (Pierce, Lautman)

# ** <<1.1>> 1.1 Examples of actual texts (different registers)

# *** TODO Pull up examples from real texts.

# - E.g. Artin's Galois theory book
# - E.g. Gowers's "Eventually this is something a computer can solve"

# ** <<1.2>> 1.2 A formal language doesn't do anything with this ("Proofs and Prologues")

# - (Conclusion from inductive reasoning in 1.1.)

# ** Text

Since our purpose is to understand mathematical reasoning as practiced
by mathematicians, we will begin by studying examples of mathematical
texts.  We would like to characterize the use of language
gramatically and rhetorically, describe the logic and argumentation
structures used so as to develop our formalism for representing
mathematical knowledge in an informed matter.  For the purposes of
illustration, we will examine four short texts:

- *MPM* :: Mini-polymath 3, threads 3, 11, and 14 - selected portions
           of a collaborative online effort to solve a problem from
           the 2011 International Mathematics Olympiad.[fn::
           https://polymathprojects.org/2011/07/19/minipolymath3-project-2011-imo/]

- *GCP* :: Timothy Gowers's - What is the 500th digit of
           $(\sqrt{2}+\sqrt{3})^{2012}$? from his Maxwell Institute
           Lecture "Modelling the mathematical discovery process"

- *AGT* :: Section II.H, ``Normal Extensions'' of ``Galois Theory'' by
           Emil Artin.

- *HHS* :: Section 22, ``Adjoints'' of ``Introduction to Hilbert
           Space'' by P. R. Halmos.

One of the first features which leaps to the eye when reading these
texts is that much of the text is written in a fashion which employs a
precise technical vocabulary, logical idioms, and symbolic notation to
state mathematical propositions.  We will refer to this as the /formal
register/ of mathematical discourse.  Here are two typical instances
from our sample texts:

- If, conversely, $\varphi$ is a bounded linear functional, then
  there exists a unique operator $A$ such that $\varphi (x,y) = (Ax,
  y)$ for all $x$ and $y$.  (HHS, statement of theorem 1)

- The intermediate field $B$ is a normal extension of $F$ if and only
  if the subgroup $G_B$ is a normal subgroup of $G$. (AGT, statement
  of theorem 16)

Semantically, such statements are assumed to be equivalent to symbolic
expressions in formal logic (in whatever formal system one is
working).  For the examples above, the following might be formal
equivalents:
\begin{align*}
  &\varphi \in \mathrm{BLF} \Rightarrow (\exists ! A) (\forall x,y)
  \varphi (x,y) = (Ax,y) \\
  &\mathrm{norm\_ext} (B, F) \Leftrightarrow \mathrm{norm\_subgp} (G_B,
  G)
\end{align*}

While statements in the formal register are an important part of
mathematical writing, a text consisting only of formal statements
would be frustrating to read because, while it might contain all the
technical information, it would offer no guidance to the reader as to
where the statements came from, why they are interesting, and how to
go about understanding them.[fn:lamport-reviewer:Lamport \cite[p.~20]{lamport2012write21st} quotes a referee who had read one of his structured proofs (see Section [[2.3][2.3, below]]): "The proofs ... are lengthy, and are presented in a style which I find very tedious. I think the readers ... are going to be more interested in understanding the techniques and how they can apply them, than they will be in reading the formal proofs. A problem with the proofs is that they do not clearly distinguish the trivial manipulations from the nontrivial or surprising parts. ... My feeling is that informal proof sketches ... to explain the crucial ideas in each result would be more appropriate."] To offer this
guidance, a mathematical text will also contain expository statements
such as the following:

+ We begin the proper business of this section by showing that the
  connection between linear transformations and bilinear functionals
  goes quite deeper than these superficial remarks. (HHS, first
  paragraph)

+ We come now to a theorem known as the /Fundamental Theorem of Galois
  Theory/ which gives the relation between the structure of a
  splitting field and its group of automorphisms.  (AGT, right before
  statement of theorem 16)

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

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

The /expository register/ has several salient features which work
together and which distinguish it from the formal register.

While the subject matter of expository statements is also mathematical
objects and propositions, the language is not only descriptive, but
also narrative and argumentative.  For instance, the phrases ``we
begin'' and ``we come now'' in the first two examples are indicative
of a narrative structure; the former serves to introduce and motivate
the theory of adjoint operators in terms of a few observations and the
latter motivates the theorem by describing its purpose in general
terms.  The third example is argumentative, asking whether an earlier
proposal might be generalizable.

Whereas in formal logic, only the strictest deductive reasoning is
allowed, mathematical exposition also makes use of inductive and
abductive reasoning, and even looser reasoning by analogy.  For
instance, the fourth example illustrates an inductive mode of
reasoning in which the questioner is looking for a general result of
which the problem posed would be a special case.  In the first
example, an analogy is being set up between the remarks which precede
that statement and the propositions which follow it.

A related point is that, whereas formal statements only make use of
the truth values and predicates of formal logic, the expository
register also makes use of looser judgements of plausibility and
heuristics.  For instance, in the first example, the adjectives
``superficial'' and ``deeper'' appear.  Terms such as these are not
formally definable but refer to approximate notions which inform
heuristic choices.

Allowing such loose notions and non-deductive reasoning serves an
important purpose because, quite often, the exact deduction of some
result might be lengthy and/or opaque.  When that happens, it is
helpful to the reader to augment the formal reasoning with informal
reasoning which is shorter and easier to understand.  Moreover, it
not infrequently happens that such informal reasoning can serve to
guide the construction of a formal proof, as in GCP and MPM.

Finally, the expository register is metamathematical, discussing not
only objects and propositions, but also inference and proofs.  For
instance, the third example asks about the provability of a
statement.  Furthermore, this is not just strict metamathematics, but
also may involve approximate and heuristic elements.  In particular,
when setting out to prove a theorem, one may first assess different
possible proof strategies using heuristic notions such as difficult
vesrus easy or by making analogies with techniques used to
successfully prove similar results.

In this essay, our main focus will be to construct a theory of
mathematical exposition which will account for the features noted
above and provide a semantics for utterances in the expository
register which can be implemented and queried algorithmically.  Our
focus here will be on the representation and what can be done with it
as opposed to parsing natural language.  This is a matter of
specialization, not of trivializing the latter.  We also note that
there has been progress by Mohan in parsing the formal register and
will later note that there exist natural language parsers for related
AI problems in order to suggest that it is plausible that one could
build a parser.

** Urban explorer metaphor

As a way of illustrating the formal and expository registers, we offer
the following analogy.  Instead of mathematical objects and
propositions, consider locations and buildings in a city.  Instead of
inferences, roads and paths and, instead of theoroes, neighborhoods
and districts.

Now consider guides to that city.  A basic feature of a guide is
description --- ``The exchange building is built of red brick and has
a gabled roof''; ``The memorial fountain is made of white marble and
has a stream of water coming out of the lion's mouth into an octagonal
basin filled with goldfish.''  This corresponds to the formal
register.  The most utilitarian form of a guidance is a list of
directions --- ``Go straight three blocks, turn left, go another two
blocks.  In the middle of the third block, there will be a building
with yellow clapboard siding.''  This kind of statement corresponds to
formal mathematical proofs.

However, there is much more to city guides than just straightforward
descriptions and directions.  They may contain value judgements ---
``For a more scenic view, take this detour''; ``To avoid nasty taxi
traffic, go under the intersection through the tunnel.''  While a
straightforward set of directions might suffice for a business person
passing through town, for someone with more leisure a single route or
tree-like transportation map may be dissatisfying since that person
would like to learn about all the different ways around together with
their historical, cultural, and aesthetic associations.  A newcomer
might appreciate a book which not only says what there is and how to
get there, but also provides a higher level guidance as to what are
some prominant landmarks and important sites and have things laid out
in some order that makes it possible to assimilate information
gradually rather than be barraged with everything at once.  Three
comrades going out for a night together might start out by having a
debate on which way to go is the best, weighing different concerns
such as travel time versus convenience.  This is like the expository
register.

Since a city is not a tree \cite{alexander1964city}, any guide to it
which lays things out in a straightforward tree-like fashion will
necessarily leave things out and be of limited use.  Likewise, for
math, in order to go beyond the superficial, we will want some more
rhizomatic sort of description which enables one to wander along a
dérive along quirky winding roads.

* 2 LANGUAGE DESIGN The presentation here will describe a strategy we have been developing for representing mathematical dialogues and other informal texts. :JOE:

Bundy has argued that finding the right representation is the key to
successful reasoning \cite[p.~16]{Bundy20130194}.  Since we cannot
simply build on formal theorem proving for our current purposes, we
need to look further afield for foundations.  We are concerned in
particular with building representations \emph{of} reasoning
\cite{corneli2017towards}.  This helps guide our search for useful
paradigms.  McCarthy \cite{mccarthy2008well} posited several high-level
features of a "language of thought", highlighting in particular the
ways in which such a language would not be like spoken language:

#+BEGIN_QUOTE
- Much mental information is represented in parallel and is processed in parallel.
- Reference to states of the senses and the body has to be done by something like pointers. Natural languages use descriptions, because one person can’t give another a pointer to his visual cortex. (A robot might tell another robot, “Look through my eyes, and you’ll see it.”)
- We don’t think in terms of long sentences.
- Much human thought is contiguous with the thought of the animals from which we evolved.
- For robots, logic is appropriate, but a robot internal language may also include pointers.
- A language of thought must operate on a shorter time scale than speech does. A batter needs to do at least some thinking about a pitched ball, and a fielder often needs to do quite a bit of thinking about where to throw the ball. Pointers to processes while they are operating may be important elements of its sentences.
#+END_QUOTE

While we won't directly accommodate all of these features, but we can
find languages that deal with several of them.

** <<2.1>> 2.1 Inference Anchoring Theory + Content (IATC)

Our modelling approach builds on /argumentation theory/; in particular
Inference Anchoring Theory (IAT), which was devised by Budzynska et al
\cite{budzynska2014model} to model the pro-and-contra logical
structure of dialogical arguments.  IAT has since been adapted to
model mathematical arguments \cite{gabi-iatc, corneli2017towards}.
The primary features of this adaptation are: (1) to introduce more
explicit relationships between pieces of mathematical content; and (2)
to describe a range of intermediate relations that model the way these
objects fit together in discourse.  These include inferential
structure, judgements of validity or usefulness, and reasoning
tactics.  Later in this article we will describe "IAT+Content" (IATC)
in more detail .

** <<2.2>> 2.2 Conceptual Dependence (CD)

Conceptual Dependence was initially introduced as a tool for
understanding natural language \cite{schank1972conceptual}.  However,
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.  Later, we will show that CD primitives are
analogous to IAT performatives, and what follows from this.

** <<2.3>> 2.3 Structured proofs

Although we are not focusing on formal proofs, at the level of
mathematical content we are talking about similar things: mathematical
objects and mathematical propositions.  Formal mathematics models the
same universe of discourse, but the discourse itself is not
necessarily formal.  Accordingly, we can derive a useful sanity check from
Lamport's notion of a ``structured proof'' \cite{lamport1995write}.
In essence, a structured proof combine a summary (or ``proof sketch'')
with a mode of writing out details so way that each step is made clear
and each assumption and assertion is a label.  We emphasize that
structured proofs are trees.  As first introduced, there were just a
few keywords: =assume=, =prove=, =let=, and =case=.  In a more recent
reassessment \cite{lamport2012write21st}, Lamport states "The way I
now write proofs has profited by my recent experience designing and
using a formal language for machine-checked proofs."  In line with
this, additional keywords =new=, =suffices=, and =pick= are imported
from his "Temporal Logic of Actions+" (TLA$^{+}$) language
\cite{lamport1999specifying}, along with a shorthand for equational
proofs.  More recently, a second version of this language,
TLA$^{+2}$, has been made available, with new keywords (and now with
lambda expressions) \cite{lamport2014tla2}.[fn:1] Lamport's structured
proof is an interesting example of a ``missing link'' between informal
and formal mathematics.  The TLA\(^+\) language seems in our opinion
to be reasonably well aligned with typical mathematical style.  The
history of its development helps show which features can be considered
most essential.  We note that in principle it should be possible to
coherently map to any formal mathematical language from our content
layer.

[fn:1] In full, TLA\(^{+2}\)'s keywords are: =action=, =assumption=, =axiom=, =by=, =corollary=, =def=, =define=, =defs=, =have=, =hide=, =lambda=, =lemma=, =new=, =obvious=, =omitted=, =only=, =pick=, =proof=, =proposition=, =prove=, =qed=, =recursive=, =state=, =suffices=, =take=, =temporal=, =use=, =witness=.

** <<2.4>> 2.4 The Lakatos Game (LG)

Lakatos \cite{lakatos1976proofs} developed an abstract, dialectical,
model of mathematical creativity which has recently been formalised as
a \emph{dialogue game} \cite{pease2017lakatos}.  In the "Lakatos
Game", assertions are made and then adjusted: for instance, a
statement may be sharpened so that it applies to a restricted class of
objects ("Strategic Withdrawal"), or a putative counterexample may be
shown not to be a counterexample at all ("Monster Barring"). Lakatos's
theory is limited, first, because it commits almost exclusively to
Hegelian dialectic.  Secondly, when we zoom in and look at concrete
details of mathematical objects, it should be no surprise that there
are a range of issues that an abstract model will not cover.  In
short, as a representation of reasoning the Lakatos Game is at least
somewhat descriptive, but not explicitly runnable.  We hope to
overcome these limitations.

* 3 IMPLEMENTATION ISSUES (REQUIREMENTS) :JOE:

An informal proof is in general not a tree, even if a structured proof
-- or the trace of the moves made in a dialogue game -- does rather
satisfactorily /describe/ the proof as a tree.  In the limit of full
formality, tree-shaped descriptions are machine checkable -- and by
the Curry-Howard correspondence, proofs-as-programs are even runnable.
However, by default these objects give very little information about
the proof's (or program's) genesis.  Indeed, as we shall see, we soon
run into problems even with a still-more-general network model.

** <<3.1>> 3.1 Look, it's a graph; no it's a hypergraph!

Figure [[fig:gcp-implements]] is an excerpt from a larger diagram[fn:2]
that analyses Gowers's walk-through of the solution to the problem
"What is the 500th digit of $(\sqrt{2}+\sqrt{3})^{2012}$?" Figure
[[fig:iatc-key]] provides a graphical key to the color-coding of IATC
operations.  We focus in on this step of the proof:
#+BEGIN_QUOTE
And $(\sqrt{3}-\sqrt{2})^{2012}$ is a very small number. Maybe the final answer is "9"?
#+END_QUOTE

#+CAPTION: GCP (detail)
#+NAME: fig:gcp-implements
[[./gowers-example-selection.png]]

#+CAPTION: IATC (key)
#+NAME: fig:iatc-key
[[./iatc-key.png]]

In IATC, utterances expand to performatives: here, in Figure
[[fig:gcp-implements]], simply a list of assertions (two of which are only
implied by the quoted utterance).  Performatives, in turn, expand to
nodes that convey inferential structure (in pink), reasoning tactics
(in blue), and judgements of validity or usefulness -- which often
take the form of heuristics (in green), as well as content-level
relations (colorless; as, for example, the relation "contains as
summand").  Intermediate nodes typically have targets in the content
layer.  For example, the assertion that
"\((\sqrt{3}-\sqrt{2})^{2012}\)" =has_property= "is small" is typical
in this regard.  However, the =implements= node poses some difficulty,
since its outbound arrow does not have another node as a target.  What
it means to say is that the subgraph implements a heuristic idea that
was proposed earlier: "The trick might be: it is close to something we
can compute."  Without the =implements= certificate, we would see a
proliferation of heuristic suggestions without any sense of which ones
are actually used.  And yet, it is clear that this is an assertion
about a subgraph, and not a specific piece of logic.  Recall
McCarthy's assertion about the language of thought: "Pointers to
processes while they are operating may be important elements of its
sentences."  Whereas a structured proof would presumably just give the
indicated subgraph a name and push it down the hierarchy into a lemma,
we can see from the diagram that such a representation strategy poses
problems with locality: /vide/ the inbound links to =sums= (from a
previous assertion) and to "some integer" (from a subsequent step in
the reasoning).  These reflections suggest the need for /hypergraphs/,
not just graphs.[fn:3] With a hypergraph, pointing to a subset of
nodes is straightforward.  Actually, we want one of the standard
generalizations of hypergraphs: the ability for an edge to point to another edge.
This way we can lasso the "lemma" as an object of interest, and point to
it, without the need to bracket it off from the rest of the proof.

[fn:2] http://metameso.org/ar/gowers-example.pdf.
[fn:3] Edges are first class objects and can be linked to; e.g., ``Mom resents the fact that John disapproves of Jane and Jim's marriage.'' Cf. https://www.slideshare.net/delaray/knowledge-extraction-presentation

** <<3.2>> 3.2 The search for the `quantum of progress'

There is a further issue here, which the =implements= certificate
hints at.  Just how does the person working through a proof attempt
decide which step to take next?  In another setting, Gowers provides
some very helpful guidance.

The Polymath project aimed to answer the question "is massively
collaborative mathematics possible?" This project was convened by
Gowers in 2009, and he developed 15 rules to address the "questions of procedure"
that he anticipated would arise in the project.[fn:: http://gowers.wordpress.com/questions-of-procedure/ ] The basic premise was that people would work together on a
shared blog to discuss a given mathematical problem in the open,
and jointly work out a solution.[fn:: Incidentally, the answer to the main motivating question was at least a tentative ``yes'' \cite{gowers2009massively}. New collaborative Polymath research projects continue to be run to the present day. Four Minipolymath projects (the third of which we refer to here as "MPM") have been convened in the same spirit, focusing on competition problems rather than research problems. However, these projects cannot be said to be "massive," if we use collaborations in other scientific disciplines as our standard.]

Gowers carefully explicated the imperative to share comments that are
"not fully thought out."[fn:UMEM] A good contribution to the project
would comprise what he called a "quantum of progress."  Continuing
with this metaphor, as the KRR strategy we are developing comes more
fully into focus, it should be clear that we need to better understand
the "fields" that generate these quanta!  That is, in order to build a
functional representation of mathematical reasoning, we need to model
both what's there at any given step, and also how it evolves -- noting
that such evolution is generally heuristic.

Here one can compare Gowers's work with Ganesalingam on a
``human-oriented theorem proving'' system \cite{Ganesalingam2016}.
First, we will comment that this work motivated the presentation of
GCP.  However, Ganesalingam and Gowers's system was only able to solve
more straightforward "textbook" problems, in which the next step is
always more or less "obvious".  Under the hood, there is a Logic of
Computable Functions (LCF) style inference system.  Because the system
generates proofs in natural language /and/ also makes its internal
processing explicit, it is quite straightforward to diagram its
operations in IATC (Figure [[fig:robotone-selection]]).[fn::
http://metameso.org/ar/robotone-example.pdf.]  In Figure
[[fig:robotone-selection]] the heuristics -- which in this case correspond
to pre-programmed LCF moves -- are disconnected from both the natural
language and content.  This could be rectified in a revision: the main
point being that a careful study of the relationship between the
underlying logic and the IATC representation would need to be
developed.  Clearly, this applies to more informal proof systems as
well. *Possibly comment here about how this variant is not "driven" by
the natural language, but the NL is sort of an epiphenomenon.*

#+CAPTION: ROBOTONE example (detail)
#+NAME: fig:robotone-selection
[[./robotone-example-selection.png]]


[fn:UMEM] Ursula Martin had commented ten years earlier, with regard
to the emerging field of "experimental mathematics," that the growth
of experimentation requires the "development of community standards as
to experimental methodology," emphasizing not only technical matters,
but also "the early sharing of insights" \cite{martin1999computers}.

* 4 APPLICATIONS Our latest efforts produce more detailed models of mathematical arguments. :JOE:

One example Sussman gives of modelling "`how to' as well as `what is'"
\cite{sussman2005programming} is a LISP program that he wrote with
Richard Stallman that can replicate the process of analyzing a circuit
\cite{sussman2011programming}.  The program explains /why/ it comes up
with the answers it does.  The "why question" is even more important
(and interesting) when nontrivial ``creativity'' is involved in the
reasoning process \cite{gucklesberger2017addressing}.  In the case of
Ganesalingam and Gowers's ROBOTONE, described above, the answer will
always be more or less the same: /because this is what LCF tells me to
do./ In other words, the program has little or nothing in the way of
context sensitivity.  This is, let's say, fine, given its limited
scope of application, but it would not work for a system that was
supposed to participate in mathematical dialogues, nor (presumably)
for a system that was exploring some entirely new area of mathematics
instead of "textbook" problems.  Here, we aim to describe a language
that can (in principle) reason equally well about both monological
"textbook" and dialogical Polymath-style discussions.

We are aided by the fact that CD has already been used to reason about
informally-constructed scenarios.  For instance given a description of
a restaurant in the form of a script, and a CD representation of a
story such as 
#+BEGIN_QUOTE
John went to a restaurant.  He sat down. He got mad. He left.
#+END_QUOTE
SAM can produce a paraphrase and make inferences such as concluding
that John was upset because the waiter did not come.
\cite{barr1981handbook}.  Furthermore, by augmenting the knowledge
base with goals and plans, it is possible to explain actions.  For
instance, given the narrative fragment 
#+BEGIN_QUOTE
Willa was hungry.  She picked up the Michelin guide.
#+END_QUOTE
one could explain why she picked up the guide as follows: The first
sentence suggests the goal of finding food, the resaurant script
describes a way of satisfying this goal but requires that one know the
location of a restaurant, hence the guide.

#+CAPTION: MPM example (detail)
#+NAME: fig:mpm-selection
[[./mpm-example-selection.png]]

Given the relation between goals, values, and performatives and the
way these are similar to what goes on in game playing and story
understanding systems, it should be possible to have the system look
at a transcribed dialogue from MPM, for instance (compare Figure
[[fig:mpm-selection]]),[fn::
http://metameso.org/ar/minipolymath-example.pdf.] and
answer questions like:

- "Why does Thomas agree with Anonymous?"
- "Why does Gal says the suggestion is beautiful?"
- "Why did Anonymous suggest `perhaps even the line does not matter'?"

The premise here is that the dynamics at work are based on
performatives being chosen based upon current valuations, goals, and
other contextual features.  We discuss both kinematics and dynamics
below.

** <<4.1>> 4.1 Kinematics (IATC+CD)

Lytinen \cite{lytinen1992conceptual} gives the following example which
schematizes the sentence "John gave Mary a book" as an s-expression,
rooted on the =ATRANS= primative:

#+BEGIN_SRC lisp
(ATRANS ACTOR  (PERSON NAME JOHN)
        OBJECT (PHYS-OBJ TYPE BOOK)
        RECIP  (PERSON NAME MARY))
#+END_SRC

We would like to do the same sort of thing here, using IATC
performatives as our primatives.  Like the standard CD primatives,
these performatives have slots, described as follows:[fn:: See \cite{gabi-iatc} for further details.]

- =Assert= (/s/ [, /a/ ]): Assert belief that statement /s/ is true, optionally because of /a/.
- =Agree= (/s/ [, /a/ ]): Agree with a previous assertion.
- =Challenge= (/s/ [, /a/ ]): Assert belief that statement /s/ is false, optionally because of /a/.
- =Retract= (/s/ [, /a/ ]): Retract a previous assertion /s/, optionally because of /a/.
- =Define= (/o/, /p/): Define (name) object /o/ by property /p/.
- =Judge= (/s/): Apply a heuristic value judgement /s/ to some statement.
- =Suggest= (/s/): Advance a tactical reasoning move, /s/.
- =Query= (/s/): Ask for the truth value of /s/.
- =QueryE= ({/pi/(/X/)} . /i/): Ask for the class of objects /X/ for which all of the properties /pi/ hold.

Similarly, the statements that are introduced via these performatives
also have slots, for example:

- =has_property= (/o/, /p/): Object /o/ has property /p/.
- =strategy= (/m/, /s/): Method /m/ may be used to prove statement /s/.
- =beautiful= (/s/): Statement /s/ is mathematically elegant.

As we've seen in our examples we may want to point to a subgraph
rather than a "statement", as with the =implements= relation in Figure
[[fig:gcp-implements]].  Assertions that are fully unfolded generally bottom
out in the content layer: assertions can be made directly about objects
and propositions, or relationships between , as in Figure
[[fig:gcp-implements]]'s =contains as summand= relation; content
they can be addressed through other intermediate assertions, such as
"\((\sqrt{3}-\sqrt{2})^{2012}\)" =has_property= "is small" in the same
figure.  In effect, s-expressions parse statements in natural language
and use the resulting structures to build graphs like the ones shown
in our figures.  The assertions from Figure [[fig:gcp-implements]]
(along with a few pieces of text that are off-screen in that image)
may be represented thusly:

#+BEGIN_SRC lisp
(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"))

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

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

We defer the somewhat technical matter of indexing a specific subgraph
to Section [[5.2]].

** <<4.2>> 4.2 Dynamics
# (Lytinen's stuff with goals and scripts)

Static graphical representations of mathematical reasoning do not by
themselves live up to promise of /functional/ models.  We need to be
able to reason about structure: answering "why" questions, as above,
or introducing new reasoned statements into a dialogue.  Here we are
inspired by Sowa and Majumdar's treatment of reasoning by analogy
\cite{sowa2003analogical}.  For example, early in GCP, Gowers asks:

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

One linguistically tricky issue here is the resolution of the anaphora
"this".  We can see that "this" refers to /computing the 500th digit
of X/.  The anaphoristic relation is grounded in several proposed
analogies:

#+BEGIN_SRC lisp
(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"))
#+END_SRC

We can see the analogies even more clearly when the content is
represented in graphical form, i.e., when the constituent objects and
functions have been fully expanded.  Figure [[fig:qa-fig]] shows an
example from \cite{corneli2017towards} that describes an analogy
between a known theorem for finite groups, and a structurally
related conjecture for infinite groups.

#+CAPTION: Q&A example (lightly adapted from \cite[Fig. 1]{corneli2017towards})
#+NAME: fig:qa-fig
[[./revised-qa-question.png]]

The analogy between the two clusters is clear: in one case $G$ is a
finite group, in the other $G$ is an infinite group.  Naturally, this
is not the same "\(G\)".  Using a typed formalism we could be more
specific about the difference between the two sides, while retaining a
structural similarity on the two sides of the analogy:[fn:: Something
along the lines of clojure.spec may be useful these purposes; it
provides a "standard, expressive, powerful and integrated system for
specification and testing"; see https://clojure.org/about/spec.]

#+BEGIN_SRC c
G: group           -> X: group
G has_card finite  -> X has_card infinite
#+END_SRC

In short, if we can expand the statements in sufficient detail, we can
start to see the specific analogies between them.  We can then form
hypotheses like "Anonymous suggests `perhaps even the line does not
matter' by strict analogy with Nemanja's immediately previous
assertion "we can start with any point and `just' need to choose a
second point through which we will draw a line."  Here, Nemanja has
described a specific simplification, and Anonymous wonder if things
can be simplified again.

Given sufficently detailed representations - sometimes requiring
background theories (like group theory in the Q&A example, or plane
geometry in MPM), we expect analogical reasoning to serve as the main
explanatory mechanism.  Sowa and Majumdar describe three ways of doing
analogical reasoning about conceptual graphs:

#+BEGIN_QUOTE
The first compares two nodes by what they contain in themselves
independent of any other nodes; the second compares nodes by their
relationships to other nodes; and the third compares the mediating
transformations that may be necessary to make the graphs comparable.
#+END_QUOTE

Pushing the reasoning problem "back" to the natural language
processing layer by suggesting that sufficiently rich representations
are the main thing we need to proceed with reasoning may seem like it
is dodging the issue.  However, there is in fact a (high-order)
analogy between what goes on in parsing and reasoning.  Lytinen
\cite{lytinen1992conceptual} summarises Schank and Birnbaum
\cite{schank-and-birnbaum} on semantic parsing, again, referring to
three aspects of the parser:

#+BEGIN_QUOTE
... its /control structure/, or the processes that occur during
parsing; its /representational structures/, or the representations
which it builds during the parsing process; and its /knowledge base/,
or the set of rules which the parser draws on and which drive the
parse of a text.
#+END_QUOTE

Functional reasoning moves also have a control structure,
representational structures, and a knowledge base, though they start
from pre-parsed content.  Sowa and Majumdar refer to a "graph
grammar"; this topic developed in more detail by Ehrig et al
\cite{ehrig1992introduction}.  We will show a example relevant to our
setting in the following section.

Having described some systems of knowledge representation and some of
the reasoning which can be done with these representations, we now
turn our attention to implemenation.  Originally, the various systems
were implemented in different sofwtware pakages such as SA, PAM, and
VAE.  Rather then adapt these packages and interface them, we will
take a different approach.  Since our systems are based upon
hypergraphs, we will start with a general framework for computing with
hypergraphs and implement our representations there.

* 5 MECHANICAL ENGINEERING DESIGNS A graphical formalism and a corresponding prototype implementation will be described. :RAY:

** <<5.1>> 5.1 Import and improve technical stuff on Arxana (cf. Nemas doc)
** <<5.2>> 5.2 Example

In order to store graphical representations of knowledge in memory and
query them, we will make use of a system called /Arxana/ which we have
been developing in LISP.  The basis of this system 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.  In addition, all
the links are bidirectional and no fundamental distinction is made
between links and nodes.

For convenience and flexibility, this package has been designed in a
modular and extensible fashion.  Basic functionality is provided by a
back-end which manages the data of the network.  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.

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

- Identifier
- Source
- Sink
- Content

The identifier comes in two forms, a unique numerical identifier which
the computer assigns to it when it is entered into the database and
human-readable aliases which may be assigned by the user.  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.

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.  Storing content is what
allows nemata 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, encode a representation of the
inference used in a link which asserts that some statement implies
another.

By choosing suitable conventions, one can build up more complex
functionalisty from the basic features. For instance, one can
introduce typing by designating a certian nema as the ``home nema''
for that type and interpreting a link whose source is the home nema
and whose sink is some other nema as stating that the sink nema is of
that type.  Likewise, one can encode subhypergraphs by designating a
nema as a representative the subhypergraph and specifying the
components of the hypergraph by links from that representative nema.
For instance, we could use this construction to make the *implements*
relation [???] point to a subgraph by pointing making the sink of the
implements arrow be a nema which represents the subgraph in question.

In order to make this respresentation actionable, we will use two main
facilities: hypergraph matching and hypergraphs as programs.

Given a hypergraph, we can query it for subhypergraphs which match
some suitable criterion.  A query consists of a hypergraph whose
articles contain predicates and a match consists of a mapping of
hypergraphs from the query onto a subhypergraph such that, for every
article in the query, the predicate it contains is true of the
contents of the corresponding database article.  Since the predicate
can be any lisp function, perhaps one which is nested and recursive,
this feature can be quite powerful.

By modelling various structures as hypergraphs, we can search for
instances of them.  For instance, if we implement subcollections by
using representative nemata as described above, we can use hypergraph
matching to restrict operations to subcollections.  Or, if we
represent logical inferences in terms of a hypergraph for the premise
and a hypergraph for the conclusion which share subgraphs, then we can
use hypergraph matching to find and verify reasoning.

Since the content of a node is a lisp object, it can potentially be a
piece of executable code.  To make the most of this possibility, we
have a utility which runs this code in a context which is determined
by links out of the node containing the code.

An important use of this facility 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.  For instance, if we wanted to represent
something like the left-hand side of an equation which is found in
some node then, rather than copying the left-hand side into another
node, we could point a link to the original node whose content is
code for extracting the left-hand side.

This is also a mechanism which allows us to operationalize our
graphical representations.  Given a node corresponding to a
performative of predicate, as content we can take a routine which
verifies that the predicate indeed holds of the content to which the
node points.  Then running that node would carry out the verification.

* 6 RELATED WORK (GAMES, POETRY): parallels between dialogues and discursive Q&A, traditional proofs. :JOE:

# No one would insist that a nonlinear film like /Amores Perros/ or
# /Pulp Fiction/ needs to be represented as a tree.  Propp-style
# theories of storytelling tell us how stories are "supposed" to be
# written, but in general these models don't stand up to scrutiny.  The
# title of Robbe-Grillet's short novel /Dans le labyrinthe/, in a way,
# says it all.

# ** <<6.1>> 6.1 prior art: board games, story stuff; table that compares between.
# ** <<6.2>> 6.2 Alexander: "a city is not a tree"; compare Lamport

# ** Text

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

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 (Table [[tab:comparison]]).

#+CAPTION: Comparison between computation in different domains
#+NAME: tab:comparison
| /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  | trivial           | multiple strategies   | ethical dilemmas      |

According to David Moshman \cite{moshman2004inference},
/inference/, /thinking/, and /reasoning/ are defined as follows:

#+BEGIN_QUOTE
- *Inference*---going beyond the data---is elementary and ubiquitous.
- *Thinking* is the deliberate application and coordination of one’s inferences to serve one’s purposes
- *Reasoning* is epistemically self-constrained thinking [...] with the intent of conforming to what they deem to be appropriate inferential norms.
#+END_QUOTE

Reasoning is particularly effective in social settings, according to
Sperber & Mercier \cite{mercier2017enigma}.  Even if we are not
interacting directly with others, "appropriate inferential norms" are
social constructions. Indeed, Minsky saw thought as inherently social.

Quite contrary to the sentiment conveyed by the
misattributed quote ``Mathematics is a game played according to
certain simple rules with meaningless marks on paper,'' David Hilbert,
an early and important proponent of mathematical formalism, emphasised
the role of intuition and experience, and discussed conjectural
thinking and the fallibility of mathematical reasoning
\cite{hilbert1992natur,corry1997origins}.[fn:thomae]

[fn:thomae] The actual source of the quote appears to be Carl Johannes
Thomae, /Elementare Theorie der analytische Functionen einer complexen
Veraenderlichen/ (1898), p. 3: ``For the formalist, arithmetic is a game
with signs, which are called empty. That means they have no other
content (in the calculating game) than they are assigned by their
behaviour with respect to certain rules of combination (rules of the
game).'' It is worth noting that Thomae nevertheless continues on to
remark on the difference between arithmetic and chess, insofar as
``numbers can be related to concrete manifolds by means of simple
axioms.''  Cf. this discussion in the ``Foundations of Mathematics''
mailing list:
https://www.cs.nyu.edu/pipermail/fom/2005-April/008889.html.

# * 7 PART TWO In our planned next steps we plan to bring in explicit type-theoretic representations of mathematical objects within a service-oriented architecture. :onhold:

# ** <<7.1>> 7.1 There is a degree of formality in the specifications, but also informality in the heuristics.

# * 8 MOB PROGRAMMING :onhold:

# ** <<8.1>>
# ** <<8.2>>

# * 9 RELATED WORK music from corneli, pease, stefanou survey ("Chapter 6"); NNexus project; Socratic :onhold:

# ** <<9.1>>
# ** <<9.2>>

# * 10 CONCLUSION :onhold:

# ** <<10.1>>
# ** <<10.2>>