move contents

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

#+TITLE:     \large{Modelling the Way Mathematics Is Actually Done}
#+AUTHOR:    Joseph Corneli, Ursula Martin, Dave Murray-Rust,\newline Alison Pease, Raymond Puzio, Gabriela Rino Nesin
#+EMAIL:     contact@planetmath.org
#+DATE:      9 September, 2017
#+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
#+KEYWORDS: arxana, hypertext, inference anchoring
#+LANGUAGE: en
#+OPTIONS: H:1 num:t toc:nil \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
#+LATEX_CLASS: beamer
#+LATEX_CLASS_OPTIONS: [presentation,serif]
#+LATEX_HEADER: \usepackage{beamerhacks}
#+LINK_UP:
#+LINK_HOME:
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
#+STARTUP: showeverything

# To change background
# convert example-graph.png -fuzz 1% -fill 'rgb(255,255,230)' -opaque white fond-graph.png

# To convert pdf to jpg
# convert -density 300 -trim test.pdf -quality 100 test.jpg

# To break an image into several images
# convert -crop 100%x25% +repage fond-bw.png fond-bw_%d.png


* "From cons cells to triples, from trees to hypergraphs"

/cons cell/ =(a . b)=, =car=, =cdr= \SoThat /nema/ =(a c b)=, =src=, =txt=, and =snk=.\newline
A repository of nemas is a /plexus/.  =(0 a 0)= is used to represent =a=.

/Mom resents the fact that John disapproves of Jane and Jim's
marriage./

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 8cm
    [[file:./fond-mom.png]]

\textbf{History}: *Arxana*: "A Scholia-based Document Model for Commons-based Peer Production", 2005;  various backends since then. *Inference Anchoring Theory + Content*, 2016-2017

* The problem:
 - Whereas formal mathematical theories are well studied, computers cannot yet adequately represent and reason about mathematical dialogues and other informal texts.
- Machine learning is likely to be useful for building mathematical AI.
- But for that we need representations of mathematics in which meaningful patterns can be found.
* Background
\textbf{Formal register}:
\begin{eqnarray*}
&& \hspace{-1cm}\text{\emph{``Every integer equals the sum of four squares.''}}\\
&\equiv& (\forall n \in \mathbb{N}) (\exists m_1,m_2,m_3,m_4 \in \mathbb{N}) \, n = \sum_{i=1}^{4} m_i^2
\end{eqnarray*}
- Nothing essential is lost in translating between the verbal and symbolic statements ("no reference is made ... to meaning").
- /Trees/ provide the look and feel of the formal register.

\textbf{Expository register}:
\begin{quote}
"Next, we will prove the four-square theorem using an algebraic identity similar to the one we just used to prove the two squares theorem."
\end{quote}

* Cities are not trees

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 10cm
    [[file:./fond-city-vs-tree2.png]]

*** \phantom{y}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.6
    :BEAMER_ENV: block
    :END:
*** \phantom{x}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.4
    :BEAMER_ENV: block
    :END:
-- Christopher Alexander

* Cities can be /imagined/ without overlapping systems...

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 10cm
    [[file:./abercrombie-plan-communities-map-1942.jpg]]

* Framing the Current Effort

The blocks world, board games, and story comprehension require increasingly sophisticated patterns of \emph{inference}, \emph{thinking}, and \emph{reasoning}.

\medskip

\begingroup\scriptsize
\begin{myenv}[1\textwidth]{3em}
\begin{tabular}{llll}
\emph{Level} & \textbf{Blocks World} & \textbf{Board Games} & \textbf{Story Comprehension}\\
\hline
elements & blocks on a table & game pieces on board & episodes from everyday life\\
inference & follow instructions & rules \& strategy & analogy\\
thinking & consistency & prediction of winning & costs and benefits\\
reasoning & (trivial) & multiple strategies & ethical dilemmas\\
\end{tabular}
\end{myenv}
\endgroup

\hspace{2.78in} \textcolor{brightpink}{$\uparrow$}

Understood as a computational challenge, mainstream mathematics lies
somewhere in between board games and story comprehension.

* Survey of Related Work

\textbf{Annotative programming}: \emph{Flare}, \emph{ZigZag}, \emph{AtomSpace}

\bigskip

\textbf{Models of Mathematical Reasoning}:

# http://www.fileformat.info/info/unicode/font/dejavu_sans_oblique/blockview.htm?block=emoticons
1. Inference Anchoring Theory + Content \deja{☺}
1. Conceptual Dependence \deja{☺}
1. Structured Proofs \deja{😐}
1. Lakatos Games \deja{😼}

* Inference Anchoring Theory + Content

This is what we use to model *what* people say when they talk about
mathematics.

\vspace{-.5cm}

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 11cm
    [[file:./fond-analogies.png]]

* Inference Anchoring Theory + Content (ctd.)

\textbf{Performatives}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{Assert} (\emph{s} [, \emph{a} ]) & Assert belief that statement \emph{s} is true, optionally because of \emph{a}.\\
\texttt{Agree} (\emph{s} [, \emph{a} ]) & Agree with a previous statement \emph{s}, optionally because of \emph{a}.\\
\texttt{Challenge} (\emph{s} [, \emph{a} ]) & Assert belief that statement \emph{s} is false, optionally because of \emph{a}.\\
\texttt{Retract} (\emph{s} [, \emph{a} ]) & Retract a previous statement \emph{s}, optionally because of \emph{a}.\\
\texttt{Define} (\emph{o}, \emph{p}) & Define object \emph{o} via property \emph{p}.\\
\texttt{Suggest} (\emph{s}) & Suggest a strategy \emph{s}.\\
\texttt{Judge} (\emph{s}) & Apply a heuristic value judgement \emph{s} to some statement.\\
\texttt{Query} (\emph{s}) & Ask for the truth value of statement \emph{s}.\\
\texttt{QueryE} (\{$p_i$($X$)\} . \emph{i}) & Ask for the class of objects \emph{X} for which all of the properties $p_i$ hold.
\end{tabular}
\endgroup

* Inference Anchoring Theory + Content (ctd.)

\textbf{Inferential Structure}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
% Gabi's notes used ``stronger'' but ``implies'' is more intuitive
\texttt{implies} (\emph{s}, \emph{t}) & Statement \emph{s} implies statement \emph{t}.\\
\texttt{not} (\emph{s}) & Negation of \emph{s}.\\
\texttt{conjunction} (\emph{s}, \emph{t}, \ldots) & Conjunction of statements \emph{s}, \emph{t}, \ldots \\
\texttt{has\_property} (\emph{o}, \emph{p}) & Object \emph{o} has property \emph{p}.\\
\texttt{instance\_of} (\emph{o}, \emph{m}) & Object \emph{o} is an instance of the broader class \emph{m}.\\
\texttt{indep\_of} (\emph{o}, \emph{d}) & Object \emph{o} does not depend on the choice of object \emph{d}.\\
\texttt{case\_split} (\emph{s}, \{$s_i$\} . \emph{i}) & Statement \emph{s} is equivalent to the conjunction of the $s_i$'s.\\
\texttt{wlog} (\emph{s}, \emph{t}) & Statement \emph{t} is equivalent to statement \emph{s} but easier to prove.\\
\end{tabular}
\endgroup

\textbf{Reasoning tactics}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{goal} (\emph{s}) & Used with \texttt{Suggest} to guide other agents to work on \emph{s}.\\
\texttt{strategy} (\emph{m}, \emph{s}) & Method \emph{m} may be used to prove \emph{s}.\\
\texttt{auxiliary} (\emph{s}, \emph{a}) & Statement \emph{s} requires an auxiliary lemma \emph{a}.\\
\texttt{analogy} (\emph{s}, \emph{t}) & Statement \emph{s} and statement \emph{t} should be seen as analogous in some way.\\
\texttt{implements} (\emph{s}, \emph{m}) & Statement \emph{s} implements the method \emph{m} from a previousl suggested strategy.\\
\texttt{generalises} (\emph{m}, \emph{n}) & Method \emph{m} generalises method \emph{n}.  \\
\end{tabular}
\endgroup

* Inference Anchoring Theory + Content (ctd.)

\textbf{Heuristics and Value Judgements}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{easy} (\emph{s} [, \emph{t}]) & Statement \emph{s} is easy to prove; opt., easier than statement \emph{t}.\\
\texttt{plausible} (\emph{s}) & Statement \emph{s} is plausible.\\
\texttt{beautiful} (\emph{s}) & Statement \emph{s} is beautiful (or mathematically elegant).\\
\texttt{useful} (\emph{s}) & Statement \emph{s} can be used in an eventual proof.\\
\texttt{heuristic} (\emph{x}) & Statement \emph{x} describes an heuristic (with less rigour than a strategy).\\
\end{tabular}
\endgroup

\textbf{Content-Focused Structural Relations}

\begingroup\scriptsize
\begin{tabular}{p{.3\columnwidth}@{\hspace{-.25ex}}p{.7\columnwidth}}
\texttt{used\_in} (\emph{o}, \emph{s}) & Object \emph{o} is used in statement \emph{s}.\\
\texttt{sub\_prop} (\emph{s}, \emph{t}) & Statement \emph{s} contains proposition \emph{t}.\\
\texttt{reform} (\emph{s}, \emph{t}) & Statement \emph{s} can be reformed into statement \emph{t}.\\
\texttt{extensional\_set} (\emph{p}) & The set of objects with property \emph{p}.\\
\texttt{instantiates} (\emph{s}, \emph{t}) & Statement \emph{s} schematically instantiates statement \emph{t}. \\
\texttt{expands} (\emph{x}, \emph{y}) & Expression \emph{x} expands to expression \emph{y}.\\
\texttt{sums} (\emph{x}, \emph{y}) & Expression \emph{x} sums to expression \emph{y}. \\
\texttt{cont\_summand} (\emph{x}, \emph{y}) & Expression \emph{x} contains \emph{y} as a summand. \\
\end{tabular}
\endgroup

* Conceptual Dependence

CD was used by Schank, Lytinen, and others to represent knowledge
about actions, and to \emph{reason about stories}.

*"Willa was hungry.  She picked up the Michelin guide." (Why?)*

CD data structures are generalised in Arxana.

\vspace{-.5cm}
#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 11cm
    [[file:./fond-cd-example.png]]

Using something like CD, a system might reason about *why* people say
what they do when they talk about mathematics.

* Structured Proofs

This semi-formal style of writing down proofs, due to Lamport, is not
all that well suited to describing \emph{informal} reasoning.

\vspace{-.5cm}

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 11cm
    [[file:./fond-structured.png]]

...

* Lakatos Games

This is a \emph{formalised} description of informal reasoning, with a
constrained structure.  It's plausible -- but not sufficient.

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 8cm
    [[file:./fond-lg.png]]

* The Search for the `Quantum of Progress'

Ganesalingam and Gowers's ROBOTONE:

\begin{quote}
can ... be regarded as repeatedly applying a single tactic, which is itself constructed by
taking a list of subsidiary tactics and applying the first
that can be applied.\footnote{M. Ganesalingam and W. T. Gowers. A Fully Automatic Theorem Prover with
Human-Style Output. \emph{Journal of Automated Reasoning}, pages 1–39, 2016.}
\end{quote}

Contrast this with HACKER.[fn:: Gerald J. Sussman. A Computational
Model of Skill Acquisition, PhD thesis, MIT, 1973.]

\begin{quote}
In fact, Hacker is not as good at solving blocks world problems as
would be a much simpler program that just goes about it directly
with some good heuristics and a minimum of exploration.
Hacker's justification is as an epistemological model, not
as a real problem solver.\footnote{M. Levin. On Bateson's Logical Levels of Learning Theory. Tech. Rep. TM-57, MIT/LCS, 1975.}
\end{quote}

* IATC Example

We saw part of this before.

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 10cm
    [[file:./fond-bw_0.png]]

* IATC Example

NB. Pointing to edges

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 10cm
    [[file:./fond-bw_1.png]]

* IATC Example

NB. Pointing to a subgraph

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 10cm
    [[file:./fond-bw_2.png]]

* IATC Example

NB. At least one relevant edge is not drawn.

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 10cm
    [[file:./fond-bw_3.png]]

# * IATC Example

# \begin{tikzpicture}[overlay,remember picture]
# \node[anchor=center]
# at (current page.center) {
# {\colorbox{fondpaille}{\includegraphics[trim=10cm 0cm 10cm 0,clip=true,width=\textwidth,page=1]{bw-split}}}
# };
# \end{tikzpicture}

# * IATC Example (ctd.)

# This is not deductive reasoning

# \begin{tikzpicture}[overlay,remember picture]
# \node[anchor=center,yshift=-5pt]
# at (current page.center) {
# {\colorbox{white}{\includegraphics[trim=10cm 0cm 10cm 0,clip=true,width=\textwidth,page=2]{bw-split}}}
# };
# \end{tikzpicture}

# * IATC Example (ctd.)

# NB. Pointing to edges

# \begin{tikzpicture}[overlay,remember picture]
# \node[anchor=center,yshift=-5pt]
# at (current page.center) {
# {\colorbox{white}{\includegraphics[trim=10cm 0cm 10cm 0,clip=true,width=\textwidth,page=3]{bw-split}}}
# };
# \end{tikzpicture}

# * IATC Example (ctd.)

# NB. Pointing to a subgraph

# \begin{tikzpicture}[overlay,remember picture]
# \node[anchor=center,yshift=-5pt]
# at (current page.center) {
# {\colorbox{white}{\includegraphics[trim=10cm 0cm 10cm 0,clip=true,width=\textwidth,page=4]{bw-split}}}
# };
# \end{tikzpicture}

# * IATC Example (ctd.)

# (At least one relevant edge is not drawn.)

# \begin{tikzpicture}[overlay,remember picture]
# \node[anchor=center,yshift=-5pt]
# at (current page.center) {
# {\colorbox{white}{\includegraphics[trim=10cm 0cm 10cm 0,clip=true,width=\textwidth,page=5]{bw-split}}}
# };
# \end{tikzpicture}

* Towards Functional Models of Math. Reasoning

\vspace{-.5cm}
*** \phantom{x}                           :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.5
    :BEAMER_ENV: block
    :END:
#+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"))
(Assert (implements #SUBGRAPH
"the trick might be: it
is close to something
we can compute"))
(Suggest (strategy
"numbers that are very close
to integers have \"9\"
in many places of their
decimal expansion"))
#+END_SRC

*** \phantom{x}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.5
    :BEAMER_ENV: block
    :END:

S-expressions like those at left can be fed to Arxana,
building up a graph representation.

\bigskip

But what about the reasoning that takes us from step to step?

\bigskip

Cf. Oxford Calculators, 14th C., *kinematics* vs *dynamics*

#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 4cm
    [[file:./quadrivial.jpg]]

* 

*** \phantom{y}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.5
    :BEAMER_ENV: block
    :END:
\vspace{-1cm}
#+ATTR_ORG: :width 400
#+ATTR_LATEX: :width 6cm
    [[file:./arxanap1.png]]

*** \phantom{x}                                               :B_block:BMCOL:
    :PROPERTIES:
    :BEAMER_COL: 0.4
    :BEAMER_ENV: block
    :END:
\vspace{-1cm}
#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 3cm
  [[file:./fond-conefig.png]]

Arxana's model of nemas and plexuses is similar to other graph
databases, some of which allow "reified triples."  *However, Arxana
also allows nested code*.

* Application to Mathematical Reasoning

In the paper, we describe one reasoning step in detail: the validation
of a certain =implements= link with a local proof certificate.
Arxana's nested code allows us to fold some details out of the way.
Notice the multiply-nested components in "B".

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 10cm
    [[file:./fond-nested.png]]

* Application to Mathematical Reasoning (ctd.)

Along with the knowledge expressed in the proof itself, we assume that
a suitable knowledge base is available to the system.[fn::Ask me later about the /Hyperreal Dictionary of Mathematics/ project.]

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 10cm
    [[file:./fond-hdmkb.png]]

* Application to Mathematical Reasoning (ctd.)

One of the more exciting features of reasoning with Arxana is that we
can encode inference rules in a /graph grammar/.

Here are the inference rules used to obtain the certificate:

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 10cm
    [[file:./fond-rules.png]]

* Application to Mathematical Reasoning (ctd.)

Lastly, here is the certificate itself as a tree, i.e., a lambda
expression, sitting inside of the =implements= node.

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 10cm
    [[file:./fond-certificate.png]]

Notice that this derivation was constructed by hand -- the higher
order reasoning required to select the premises, knowledge base
elements, inference rules, and to hook them all together in the
correct way is not yet programmed!

* Conclusions and Future Work

We have focused on a computational theory of the expository register.

We draw upon both classic and recent AI research which has
considered situations with which everyday mathematics shares common
features.

Future work may integrate themes from formal proof, embodiment and
cognitive science, linguistics and NLP, as well as machine learning.
Extensions to the system itself are planned to facilitate stepping
through the challenge described earlier.

\begin{quote}
It seems probable that once the machine thinking method had started, it would not take long to outstrip our feeble powers. There would be no question of the machines dying, and they would be able to converse with each other to sharpen their wits. -- Alan Turing
\end{quote}

\begin{quote}
We can only see a short distance ahead, but we can see plenty there that needs to be done. -- Alan Turing
\end{quote}

* outtakes                                                         :noexport:
** Other things we've worked on

#+C Local Variables:
#+C org-tree-slide-skip-outline-level: 3
#+C mode-line-format: nil
#+C org-latex-compiler: "xelatex"
#+C eval: (org-display-inline-images t t)
#+C eval: (setq org-tree-slide-header nil)
#+C End:

* Frame with references                                            :noexport:
  :PROPERTIES:
  :BEAMER_OPT: fragile,allowframebreaks,label=
  :END:
  \printbibliography