clean up section 2, more references

[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
- people may make different expository choices
- mathematical text contains argumentation an narrative in addition to logic and calculations ([[1.2][1.2]])
** 0.2 FORCES
- push to make everything formal (QED, Tarski, LCF) [[1.1][1.1]]
- push to make everything understandable (Alexander)
** 0.3 PROBLEM
- each different user will have a different "way in", depending on their background knowledge ([[3.2][3.2]])
- how to get behind the scenes to see why?
- how to tailor a given formal content to a given reader?
** 0.4 SOLUTION (STRATEGY)
- focus on expressivity
- focus on representing process
- formalization and efficiency are important, but will be left for later.
** 0.5 RATIONALE
- objective: understand mathematics as people do it (literary criticism, rhetoric, argumentation)
- objective: learn from these methods to build new mathematical texts
- build on intuitive diagrams
- build on the idea of parsing natural language (complementary to Mohan's work)
** 0.6 RESOLUTION of FORCES
- outcome: sharing diagrams with people who can use them
- potential: draw new diagrams
- philosophical: bridging 'two cultures' (proof checkers and artists/designers/hackers)

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

- *GCP* :: Timothy Gowers - What is the 500th digit of
  $(\sqrt{2}+\sqrt{3})^{2012}$?

- *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 barraget 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 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" 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 how CD primitives can be seen to
be 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.  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}$' 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=.

* 3 IMPLEMENTATION ISSUES (REQUIREMENTS) :JOE:

We've already seen an *abstract* model of social creativity in
Lakatos, but when we try to zoom in and look at concrete details, we
see there are further challenges. We know that a `city is not a tree',
let's generalise and assert that a proof dialogue is not a tree.  This
gives us a guiding principle.

** <<3.1>> 3.1 Let's look at one of our illustrations: it's a graph, no it's a hypergraph!

** <<3.2>> 3.2 Reason as a social thing (Minsky, Sperber & Mercier, Gowers 'quantum of progress' from Polymath)

When we introduced argumentation theory we remarked that reasoning is
often particularly effective in social settings
\cite{mercier2017enigma}.  However, even when we are not engaging
directly with others, we reason in what are often socially-validated
ways.  According to David Moshman \cite{moshman2004inference},
/inference/, /thinking/, and /reasoning/ are defined like this:

#+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

** <<3.3>> 3.3 Lakatos stuff: How is this different from what we're doing?

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

We need to model what's there and how it evolves, noting that
evolution is heuristic.  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 perhaps even more important (and interesting) when
nontrivial ``creativity'' is involved in the reasoning process
\cite{gucklesberger2016addressing}.

#+BEGIN_COMMENT
The program could take the wiring diagram of the circuit, calculate
the current at some point, and recapitulate the assumptions and rules
that led the program to its answer.
#+END_COMMENT

** <<4.1>> 4.1 Kinematics (IATC+CD)
** <<4.2>> 4.2 Dynamics (Lytinen's stuff with goals and scripts)

* 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


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

How does this look in a broader context?

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

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  | none              | multiple strategies   | ethical dilemmas      |


-----

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