Section 1

[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

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

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

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 gudance 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 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 the city is not a tree, 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 derive 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:

Since we cannot simply build on formal theorem proving, we need to
look further afield for prior work on which to build. (Bundy: choosing
representation strategy that fits can make the problem easier to
solve; Corneli: here we are looking for representations *of*
reasoning, so this gives us a heuristic to guide our search.)

** <<2.1>> 2.1 Gabi's work on IATC
** <<2.2>> 2.2 Lytinen CD

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

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

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

-----

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