documentation changes

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

#+TITLE:     Reasoning about mathematics with graphical programs
#+AUTHOR:    *Joe Corneli*\newline \footnotesize{with Raymond Puzio, Gabi Rino Nesin, Alison Pease, Dave Murray-Rust, and Ursula Martin}
#+EMAIL:     contact@planetmath.org
#+DATE:      Tuesday 23 May, 2017 (CIAO)
#+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
#+KEYWORDS: arxana, hypertext, inference anchoring
#+LANGUAGE: en
#+OPTIONS: H:2 num:t toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
#+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
#+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
#+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport
#+LINK_UP:
#+LINK_HOME:
#+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
#+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex}
#+LATEX_HEADER: \bibliography{arxana-redux-refs}
#+LATEX_HEADER: \beamertemplatenavigationsymbolsempty
#+STARTUP: showeverything

* Overview 

** 

``I have seen this problem, that if $G$ is a finite group and $H$ is a
proper subgroup of $G$ with finite index then $ G \neq
\bigcup\limits_{g \in G} ghg^{-1}$.

Does this remain true for the infinite case also.''

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 11cm 
    [[file:./example-graph.png]]


``There's something I don't understand here: do you perhaps mean $gHg^{-1}$ instead of $ghg^{-1}$?''


** What we are (and are not) doing

- *Unlike* a classical proof which consists of mathematical statements
  and deductions, informal mathematical language is more general, and
  the reasoning involved may be abductive, inductive, or heuristic.

- The presentation here will describe a strategy we have been
  developing for representing mathematical dialogues and other
  *informal* texts.

** The research trajectory

- A publication appearing in /Artificial Intelligence/ this
  month describes the *high-level* features of informal
  mathematics.[fn:1: \fullcite{PEASE2017}.]

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 11cm 
    [[file:./lakatos-example.png]]

- What I will talk about today is instead a graphical formalism and a
  corresponding prototype *implementation (-in-progress)* dealing with
  *lower-level* features of reasoning.


** The prospects

Applications include modelling *collaborative proof dialogues* and
discursive Q&A, as well as more traditional "textbook," "journal,"
"exam," and "contest" style proofs.

\medskip

/What is the 500th digit of $(\sqrt{2}+\sqrt{3})^{2012}$?/

#+BEGIN_SRC
perf[assert](meta[goal](
 compute 500th digit of (sqrt(2)+sqrt(3))^2012))
#+END_SRC

/(Even this, eventually, a computer will be able to solve.)/

#+BEGIN_SRC 
perf[assert](rel[exists](meta[strategy](strategy X)))
perf[assert](rel[has_property](strategy X,HAL)
#+END_SRC

\medskip

In our planned next steps (touched on briefly later) we will bring in
explicit type-theoretic representations of mathematical objects within
a service-oriented architecture, for purposes of *proof synthesis*.


* Summary of the research problem and our approach

** 

Mathematical reasoning is made explicit in /potted arguments/ (proofs)
and /dialogues/.  This is what we take as our primary data.

\medskip

Our aim is to computationally model (and `simulate') mathematical
creativity.

\medskip

Our current toolkit is described below.

** Inference Anchoring Theory

/Inference Anchoring Theory/ was devised to model the logical
structure of dialogical arguments.[fn:2: \fullcite{BUDZYNSKA2014}] It
has since been extended to model *mathematical arguments*.[fn:3: \fullcite{CORNELI2017}]

** A scholia based document model for commons-based peer production

- Corneli and Krowne proposed a *scholia-based document model* for *commons-based peer production* -- i.e., online text resources grow "by attaching."[fn:4: \fullcite{CORNELI2005}]

- As it turns out, to work with mathematics we are often better served by /hypergraphs/ than by standard graphs.

  - E.g., if we say "In September 1993, an error was found in Wiles's proposed proof of Fermat's Last Theorem" in the first instance we'd like to point to the entire proposed proof.

** Arxana: computable hypertext

/Arxana/ ([[http://arxana.net][arxana.net]]) is the name given to a series of prototype
implementations (by Corneli & Puzio) of the scholium based document
model with an Emacs front-end.  Arxana is inspired in part by Ted
Nelson's Xanadu™ project, which was the first effort to work with
``hypertext'' per se.[fn:5: \fullcite{NELSON1981}]

** Conceptual Dependence

Conceptual Dependence was introduced as a tool for understanding
natural language.[fn:6: \fullcite{SCHANK1972}] It is also used to
represent knowledge about actions.[fn:7: \fullcite{LYTINEN1992}][fn:8: \fullcite{SOWA2008}]

- /primitives/ :: describe basic types of actions such as
                  *"PTRANS — transfer of location"*

- /slots/ :: each primitive comes with a set of /slots/ which
             accept objects of certain types.

- combinations :: By combining basic graphs, one can build up
                  more complicated CD graphs which describe
                  actions in greater detail.

** E.g., "John gave Mary a book."

\vspace{-2cm}

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 11cm 
    [[file:./john-example.png]]

#+BEGIN_SRC lisp
(atrans actor  (person name john)
        object (phys-obj type book)
        recip  (person name mary))
#+END_SRC

\bigskip

*NB. We view CD /primitives/ as analogous to IAT /performatives/.*

* Registers of mathematical discourse

** 

The natural language which occurs in mathematical texts comes in
several different types.  These types differ in their vocabulary,
manner of reasoning, subject matter, and degree of literality so it
simplifies the study of the subject to distinguish these types and
examine them individually.

** The formal register

One type of mathematical language is what we may call the
/formal register/.  This is the type of language which is used
to state mathematical propositions.  For example, "Every
natural number can be expressed as the sum of four squares." or
"In every triangle, the sum of the angles equals two right
angles."  This register of discourse has been studied
extensively by de Bruijn, Ranta, Ganesalingam and others.

\bigskip

Here we allow ourselves to introduce (models of) formal restatements
of propositions without worrying about how the translation from
natural language is effected.

** The expository register

Another type of mathematical language is what we will call the
/expository register/.  This is the sublanguage which is used
to express how and why one is interested in a particular formal
statement and describe mathematical reasoning.  Examples:

+ It is easy to see that our theory is complete if we assume
  the descending chain condition.

+ A more elegant way of proving theorem 5 is by induction on
  the degree; however, we chose to present the current proof
  because it makes it clear that the result depends upon the
  factorizibility condition.

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

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

* Features of the expository register

** We focus (mostly) on the expository register within IATC

#+ATTR_ORG: :width 500
    [[file:./legend.png]]

** Mathematical content

Here we are concerned with mathematical objects and mathematical
propositions and relationships between them.  Formal mathematics
models the objects in this universe of discourse and their
relationships, but the discourse itself is not necessarily formal.

** Metamathematical reasoning

Everyday mathematical discussions deal, selectively, with strategies:
not with just objects and valid derivations.  For instance, the
example statement "*It is easy to see that our theory is complete if
we assume the descending chain condition*" says something about a
proof (or a family of proofs), but it is not a purely formal
statement.

** Heuristics and value judgements

Whereas the formal register only has deductive reasoning of the
strictest sort, in the expository register we also have
*inductive* and *abductive* reasoning as well as reasoning by
analogy, heuristics, and looser forms of approximate and
plausible reasoning.

\medskip

Concomittantly, judgements made go beyond the truth values of formal
logic to vague assertions such as:

- "this statement sounds likely to be false"
- "this proof is elegant"
- "I don't get it"

This is closer to what one has in non-mathetical discourse.
These sorts of assertions influence the choice of actions and
strategies.

** We can compare:


| *Block World*     | *Board Games*         | *Story Comprehension* |
|-------------------+-----------------------+-----------------------|
| blocks on a table | game pieces on board  | everyday life         |
| instructions      | rules & strategy      | analogy               |
| consistency       | prediction of winning | costs and benefits    |



* The core language (kinematics)

** 

We now provide an overview of kinds of nodes we see in IATC diagrams.
This is the "core language" of IATC.  What I'll talk about is ``version
0.2,'' where 0.1 was written by Gabi.

** Content (=structure=)                                               :GRAY:

*** object $O$ is *=used_in=* proposition $P$
*** proposition $Q$ is a *=sub_proposition=* of proposition $P$
*** proposition $R$ is a *=reformed=* version of proposition $P$
*** $O$ *=instantiates=* some class $C$
*** $s$ *=expands=* $y$, $s$ *=sums=* $y$, $s$ *=contains_as_summand=* $t$
*** $M$ *=generalises=* $m$

** Propositions vs Objects vs Binders vs Inference rules?
Note that there are different kinds of `content'.  If for example I
say `\(0<a<b<1 \Rightarrow a^N < b^N\)', then this is more than just a
proposition, but something that can be used as a ``binder''; i.e., if
I fill in specific (valid) values of $a$ and $b$ (and, optionally,
$N$) I know the consequent holds for them.  This sort of "binder" is
presumably also a *theorem* that has been proved.  This is,
additionally, similar to an *inference rule* since it allows us to
move from one statement to another, schematically.  This suggests
that we should be a bit careful about how we think about content.

** Inferential structure (=rel=)                                       :PINK:

*** *=stronger=* (s,t)
*** *=not=* (s)
*** *=conjunction=* (s,t)
*** *=has_property=* (o,p)
*** *=instance_of=* (o,m)
*** *=independent_of=* (o,d)
*** *=case_split=* (s, {si}.i)

** reasoning tactics; "meta"/guiding (=meta=)                          :BLUE:
*** *=goal=* (s)
*** *=strategy=* (m,s)
How to show that a suggestion `has been implemented'?
We might need some other form of `certificate' for that.
E.g., it would say =implements(BLOB OF CODE,strategyx)=.
*** *=auxiliary=* (s,a)
*** *=analogy=* (s,t)

** heuristics and value judgements (=value=)                          :GREEN:

*** *=easy=* (s,t)
*** *=plausible=* (s)
*** *=beautiful=* (s)
*** *=useful=* (s)
*** *=heuristic=* (x)
(It seems that we will have several layers of `guidance'.)

** Performatives (=perf=)                                            :YELLOW:

*** *=Assert=* (s [, a ]), *=Agree=* (s [, a ])
*** *=Challenge=* (s [, c ])
*** *=Define=* (o,p)
*** *=Judge=* (s), *=Query=* (s), *=Suggest=* (s)
*** *=QueryE=* ({pi(X)}.i)
*** *=Retract=* (s [, a ])


** "=Assert=" nested structure

Here is an example from early in the "Gowers example":

#+BEGIN_SRC 
perf[assert](rel[exists](meta[strategy](strategy X)))
perf[assert](rel[has_property](strategy X,HAL)
#+END_SRC

But if you look at the diagram it's more like:

#+BEGIN_SRC c
Assert(exists(strategy(PROBLEM, strategy X))
       AND has_property(strategy X,HAL))
#+END_SRC

#+ATTR_ORG: :width 800
#+ATTR_LATEX: :width 11cm 
    [[file:./gowers-hal.png]]

* Extensions to the core (dynamics)

** 

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 and answer questions like:

- "Why do you think Thomas agreed with Anonymous?"
- "Why do you think Nemanja considers the proposition useful?"

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

** Example 1

*ANONYMOUS*: /One can start with any point (since every point of S should be pivot infinitely often), the direction of line that one starts with however matters!/

#+BEGIN_SRC
LAK> P: Lemma(‘we can start with any point’ L 11.1 ).
#+END_SRC

#+BEGIN_SRC
IATC> perf[assert](rel[equivalent](problem,
          forall_exists_problem))
IATC> rel[structural](problem, forall_exists_problem)
IATC> perf[assert](rel[not](rel[equivalent](problem,
          forall_forall_problem)))
IATC> rel[structural](problem, forall_forall_problem)
#+END_SRC

*NEMANJA*: /In other words, we can start with any point and ‘just’ need to choose a second point through which will we draw a line./

#+BEGIN_SRC
LAK> [Repetition of previous move.]
#+END_SRC

#+BEGIN_SRC
IATC> perf[assert](forall_exists_problem_detail)
IATC> rel[structural](forall_exists_problem,
          forall_exists_problem_detail)
#+END_SRC

** Example 1 (continued)

*ANONYMOUS*: /Perhaps even the line does not matter! Is it possible to prove that any point and any line will do?/

#+BEGIN_SRC
LAK> P: Lemma(‘the line does not matter‘ L 11.2 ).
LAK> P: ProofDone.
#+END_SRC

#+BEGIN_SRC
IATC> perf[query](forall_forall_problem)
#+END_SRC

*Here it probably would not make sense for Anonymous to say "Perhaps even the convex hull does not matter!"*

** Example 2

If $A$ is an operator, then there exists a unique
operator $A^*$, called the adjoint of $A$, such that
$(Ax,y) = (x,A^*y)$ for all $x$ and $y$; $A^*$ is
such that $\lVert A^* \rVert=\lVert A \rVert$.

\medskip

Write $\phi(x,y)=(Ax,y)$ and $\psi(x,y)=\phi^*(y,x)$
for all $x$ and $y$. Since, by Theorem 1, $\phi$ is
a bounded bilinear functional, and since this implies
that $\psi$ is a bounded bilinear functional with
$\lVert \psi \rVert=\lVert \phi \rVert=\lVert A \rVert$,
it follows from the converse part of Theorem 1 that
there exists an operator $A^*$ such that
$\psi(x,y)=(A^*x,y)$ for all $x$ and $y$, and
that $A^*$ is such that $\lVert A^* \rVert=\lVert \psi \rVert =\lVert A \rVert$.
Since the uniqueness of $A^*$ is clear, the proof is completed
by the obvious computation: $(Ax,y)=\phi(x,y)=\psi^*(y,x)=(A^*y,x)^*=(x,A^*y)$.[fn:9: \fullcite{HALMOS1957}]

** Example 2 (continued, A)

From an earlier schematic treatment:

#+BEGIN_SRC lisp
(defn adjoint-of-bounded-linear-op-on-hilbert-space
  (X Y A Astar)
  (hilbert-space X)
  (hilbert-space Y)
  (bounded-linear-operator A X Y)
  (and (map Astar Y X)
       (forall x :in X :st
       (forall y :in Y :st
        (eq (inner-product :on Y :of (A x) y)
            (inner-product :on X :of x (Astar y)))))))
#+END_SRC

*Actually we would like to represent these things more formally as "data types". Clojure.spec may be useful for this.*

** Example 2 (continued, B)

Here is how the proof was represented in a sort of "proto" IATC.

#+BEGIN_SRC lisp
(defproof
  adjoint-of-bounded-linear-op-on-hilbert-space:fact:
  adjoints-exist-and-are-unique (A X Y)
  (hilbert-space X)
  (hilbert-space Y)
  (bounded-linear-operator A X Y)
  (bind phi (map phi X Y :takes x
                 :to (inner-product :on Y
                                    :of (A x) y)))
  ;; We need to show that phi is linear - ‘easy’
  (shows (linear phi)
         (linear A)
         (properties-of-inner-product))
#+END_SRC

** Example 2 (continued, C)

#+BEGIN_SRC lisp
  ;; a lemma allows us to spawn a reasonable target
  (obtain v :st
          (unique v :in X :st
                  (forall u :in X :st
                    (eq (varphi u)
                        (inner-product :on X
                                       :of u v))))
          (unique-rep-linear-functional-by-inner-product
           X phi))
  (bind Astar (map Astar Y X :takes w :to v))
  ;; assert that the Astar so constructed is the adjoint
  (assert (adjoint-of-bounded-linear-op-on-hilbert-space X Y
                                                  A Astar)))
#+END_SRC

*This should be rewritten in IATC(D)!*

* Related work

** 

We can point to various pieces of related work (but will be brief).

** Modelling mathematical language

In a Lakatos setting disagreement is the primary engine that drives
discovery.

Other more general works:

- [[http://www.emis.de/monographs/Trzeciak/biglist.html][Mathematical English Usage - a Dictionary]] (Jerzy Trzeciak)
- [[https://case.edu/artsci/math/wells/pub/html/abouthbk.html][The Handbook of Mathematical Discourse]] (Charles Wells)
- [[http://universaar.uni-saarland.de/monographien/volltexte/2015/111/pdf/wolska_mathematicalProofs_komplett_e.pdf][Students' language in computer-assisted tutoring of mathematical proofs]] (Magdalena A. Wolska)

** Does what we're doing relate in any way to other formal proof checkers?

- The default answer should be "no" because most (Mizar, Coq, metamath, etc.) don't make a serious effort to deal with mathematical text.

 - There's a recent paper by Cezary Kaliszyk et al. that is somehow the exception that proves the rule.[fn:10: \fullcite{kaliszyk2014developing}] 

- There's also a generative program by Ganesalingam and Gowers that meshes natural language and formal mathematical reasoning.

- There are also various efforts with "mathematical vernacular" and, e.g., a weak type theory approach from Kamareddine and Wells called MathLang

** KRR

With the foregoing examples in mind, we assert that what we are doing
can be combined with proof checkers synergistically.  For instance,
one could attach scholia to the statements in an IAT representation
which contain formalized representations of the content, and scholia
which indicate that certain statements have been proved.  Possibly
work like the formalisation of Bourbaki could be useful as part of a
sort of Rosetta stone.

** Programming

\medskip

It is not just incidental that our work is implemented in LISP.
Actually, the kind of hypergraph programs we use are a natural
extension of the basic LISP data model.  Infrastructure-wise, Emacs
(and Org mode) are suitable for interacting with other programming
languages and long-running processes, e.g., MAXIMA -- and other
programming languages, e.g., Clojure.  Arxana will (hopefully)
continue in this direction.

\medskip

Of interest:

- /Program synthesis: opportunities for the next decade/,

* The end 
** 
That's all for now!  Happy to correspond joseph.corneli@ed.ac.uk

* outtakes                                                         :noexport:

** Other things we've worked on

- "nemas" document:  http://metameso.org/ar/metamathematics.pdf
- Joe's thesis Appendix B: http://metameso.org/ar/thesis-appendix-b.pdf
- Metamathematics preprint: http://metameso.org/ar/mathematical-semantics.pdf
- hcode function spec: http://metameso.org/ar/hcode.pdf
- Lakatos game spec: http://metameso.org/ar/lakatos-flowchart.pdf
- [[http://metameso.org/cgi-bin/current.pl?action=browse;oldid=Arxana;id=A_scholium-based_document_model][A scholium-based document model]] is the wiki homepage for Arxana and has several relevant discussions.
- [[http://metameso.org/cgi-bin/current.pl/Two_years_later][Two years later]] collects many of the mathematical themes in
  overview
- [[http://metameso.org/cgi-bin/current.pl/samples_of_formal_mathematical_writing][samples of formal mathematical writing]] is a small collection
  of statements in mathematical language (leaving out ``the part
  in between dollar signs'')


** Infrastructure

This file is in versioned storage in the "mob" branch of our arxana
repo; instructions to access are here:
http://repo.or.cz/w/arxana.git/blob_plain/d187e244a8eb7d2208f1fe98db1ef895c6cd4a36:/README.mob

A working copy of this repository is checked out at
=/home/shared-folder/arxana-redux/arxana/= on the Linode.

And a "scratch" copy of the file has been copied to:
=/home/shared-folder/arxana-redux/arxana-redux.org=

This can be edited in live sessions using =togetherly.el=.

** Progress on paper

*** Corpus/Examples: Hand-drawn diagrams in IAT+C

/We are allowed to submit an appendix without a size limit, so if we don't have room for all of the diagrams in the paper, we could put them in the appendix./

- Minipolymath, treated by Gabi in the Transactions on Social Computing paper, pdf available from https://www.overleaf.com/read/jyhzpqsythzq
- Our randomly selected MathOverflow discussion (from Q&A article)
- Gowers 2012 trick problem, http://metameso.org/ar/gowers-example.pdf
- Also there's Schuam's Abstract Algebra exercise 337, a diagram is shown on arxana.net.
 - Redone using IATC: http://metameso.org/ar/schuams-example.pdf
- An example from the Ganesalingam and Gowers paper: http://metameso.org/ar/robotone-example.pdf
- Galois theory. Emil Artin's book.
- Euclid algorithm
- possibly an example from metamath or coq or whatever to show that we can model that stuff as discourse...
- ...

*** Other Background

**** Conference and workshop "due dilligence"

Previous publications in the ICFP series touch on themes below (i.e.,
 this a selection of papers from the proceedings over the last 10
 years that mention "mathematics" or something similar; hopefully at
 least a few of them are relevant).  We plan to submit to the
 associated [[http://www.schemeworkshop.org/][Scheme and Functional Programming]] workshop, though perhaps
 we might also want to have a look at the [[http://functional-art.org/2017/cfp.html][Functional Art, Music,
 Modelling and Design]] workshop in case it proves to be a better fit.

- /A functional programmer's guide to homotopy type theory/,
- /Program synthesis: opportunities for the next decade/,
- /Lem: reusable engineering of real-world semantics/ [Lem stands for "[[http://www.cl.cam.ac.uk/~pes20/lem/][Lightweight executable mathematics]]"],
- /Functional programming with structured graphs/,
- /Painless programming combining reduction and search: design principles for embedding decision procedures in high-level languages/,
- /Using camlp4 for presenting dynamic mathematics on the web: DynaMoW, an OCaml language extension for the run-time generation of mathematical contents and their presentation on the web/,
- /TeachScheme!: a checkpoint/,
- /A functional I/O system or, fun for freshman kids/ and
- /Commutative monads, diagrams and knots/

**** Items we've worked on before

- iatc :: The primary features of the adaptation of IAT to IATC
          are:

1. to introduce more explicit relationships between pieces of
mathematical content; and
2. to advance a range of ``predicates'' that relate mathematical
propositions.

These predicates describe inferential structure, judgements of
validity or usefulness, and reasoning tactics.

- scholia :: The kind of collaborative online
             knowledge-building that happens on sites like
             Wikipedia \cite{BENKLER2002} (or in other digital
             libraries broadly construed \cite{KROWNE2003}).
             One familiar class of examples is provided by
             revision control systems, e.g., Git, which builds
             a network history of changes to documents in a
             directed acyclic graph (DAG).

- arxana :: We have been specifically interested in
            applications within mathematics, which has given
            Arxana a unique flavour.  In particular, we propose
            to use a scholium model to model *the logic of
            proofs*, not just to represent mathematical texts
            for reading.  Over the years as we've worked on
            Arxana, we have generated all sorts of files.  Many
            of these are stored in
            =/home/shared-folder/public_html/=, and accessible
            on the web at [[http://metameso.org/ar/]].  Earlier
            prototypes are available via http://arxana.net.

***** Research notes

- "nemas" document:  http://metameso.org/ar/metamathematics.pdf
- Joe's thesis Appendix B: http://metameso.org/ar/thesis-appendix-b.pdf
- Metamathematics preprint: http://metameso.org/ar/mathematical-semantics.pdf
- hcode function spec: http://metameso.org/ar/hcode.pdf
- Lakatos game spec: http://metameso.org/ar/lakatos-flowchart.pdf

***** Wiki

- [[http://metameso.org/cgi-bin/current.pl?action=browse;oldid=Arxana;id=A_scholium-based_document_model][A scholium-based document model]] is the wiki homepage for Arxana and has several relevant discussions.
- [[http://metameso.org/cgi-bin/current.pl/Two_years_later][Two years later]] collects many of the mathematical themes in
  overview
- [[http://metameso.org/cgi-bin/current.pl/samples_of_formal_mathematical_writing][samples of formal mathematical writing]] is a small collection
  of statements in mathematical language (leaving out ``the part
  in between dollar signs''

***** Website

- [[http://arxana.net][arxana.net]] has links to source code from various prototypes
 - It also has a small gallery of hand-drawn diagrams

**** And other things elsewhere:

- /Conceptual dependency theory/ has been used for such purposes, e.g.,
in the context of machine understanding of stories \cite{LEON2011}.
- Zooming in and out to find the right level of detail is related to Faré's categorical theory of levels of a computer system [add citation].
- /Handbook of artificial intelligence/ by Barr and Feigenbaum describes *SAM* and *PAM*, the /Script Applier Mechanism/ and /Plan Applier Mechanism/ by Schank and Abelson et al., on page 306 et seq. \cite{barr1981handbook}
- Winograd, Natural language and stories --- MIT AI Technical Report 235, February 1971 with the title "Procedures as a Representation for Data in a Computer Program for Understanding Natural Language" ([[http://hci.stanford.edu/winograd/shrdlu/AITR-235.pdf][link]])
 - Could we reuse this stuff for the "narrative"
 - How do we know how to read the text and transform it into IATC?
 - An example is Gowers's "total stuckness": how do we turn that into code?
- Conceptual dependency representation - from "Deep Blue" website ([[https://deepblue.lib.umich.edu/bitstream/handle/2027.42/30278/0000679.pdf?sequence=1][link]]).
 - Schank's MARGIE system is described on page 300 /et seq./ of \cite{barr1981handbook}.
- AI textbook in wiki.


** Proofs and prologues

In several of our examples, such as the Gowers problem and Artin's
book, on sees a structure in which a proof or calculation is preceded
by a kind of prologue in which the author describes motivation and
strategy.  Unlike the proof proper which consists of mathematical
statements and deductions, the language here is more general and
the reasoning may be abductive, inductive, or heuristic.

We would like to have a representation for these sorts of prologues
and indicate how they connect with the proof which they introduce
as well as the rest of the text.  A challenge here is that the
texts in question can allude and refer to all sorts of referents
including themselves at a high level of abstraction and require
a certain amount of common sense to be understood.

Since the issues that arise here are similar to those which arise in
undestanding and representing natural language stories, we should be
able to adapt techniques such as conceptual dependency relation or
goals and themes to a mathematical context.


*** TODO We should figure out what the inferences between basic assertions (I/R, I/E, etc.) would look like here. (e.g. fig. 7 of Lytinen)

- links between basic CD's
 - e.g., joe communicated the IP address to ray, by talking, so that ray could get on the server

** Goals

In order to figure out why and how actions take place, CD theory
introduces procedural knowledge in the form of scripts, MOPs, TOPs,
goals, and plans.  For our purposes, goals and plans will be used.

This relates to the =meta= items of the spec.  Maybe we should
expand the =goal= item using some sort of ontology like that of
Schank and Ableson.

** Parsing

We saw earlier how Lytinen schematizes the sentence "John gave Mary a
book" as an s-expression.


*** TODO Initial non-working pseudocode prototype

Here it makes sense to at least try and transcribe the main examples
in some "pseudocode", inspired by IATC and hcode, which we can then
refine into a working version later.

Several examples have been transcribed:

- http://metameso.org/ar/mpm3.html
- http://metameso.org/ar/gowers2012.html
- http://metameso.org/ar/robotone-opensets.html

However, as per the headline, these don't currently *do* anything.

*** TODO Basic working version

*** TODO Can the system come up with answers to new, basic, questions?

- Inspired by Nuamah et al's geography examples
- Simple comparisons, like, how does this concept relate to that concept?  We informally talk about this as ``analogy'' between concepts.  But...

*** TODO Foldable views (like in Org mode) so that people can browse proofs

- This may come after the May submission
- Folding and unfolding the definitions of terms in something like an APM context is relevant example.  Just `unpacking' terms.


#+C Local Variables:                        
#+C org-tree-slide-skip-outline-level: 3
#+C mode-line-format: nil
#+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