From 66786f6b57aef9d15062a97b62096c2374e52489 Mon Sep 17 00:00:00 2001 From: Joe Corneli Date: Wed, 31 May 2017 20:32:07 +0100 Subject: [PATCH] notes from our conversation --- org/farm-2017.org | 36 +++++++++++++++++++----------------- org/farm-refs.bib | 13 ++++++++++++- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/org/farm-2017.org b/org/farm-2017.org index 1a32714..582797c 100644 --- a/org/farm-2017.org +++ b/org/farm-2017.org @@ -48,29 +48,30 @@ within the scope. #+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 +- 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) +- 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 -- 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? +- 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. +- 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 +- 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) +- 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 -- philosophical: bridging 'two cultures' (proof checkers and artists/designers/hackers) +- potential: draw new diagrams? * 1 THEORETICAL FOUNDATIONS Informal mathematical language is more general, and the reasoning involved may be abductive, inductive, or heuristic. :RAY: @@ -436,7 +437,7 @@ 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] From Wikipedia: Formally, a hypergraph $H$ is a pair $H = (X,E)$ where $X$ is a set of elements called ``nodes'' or ``vertices'', and $E$ is a set of non-empty subsets of $X$ called ``hyperedges'' or ``edges''. (https://en.wikipedia.org/wiki/Hypergraph) +[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' @@ -510,7 +511,7 @@ 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 example, given a description of -a restaurant...* +a restaurant...* \cite{barr1981handbook}. #+CAPTION: MPM example (detail) #+NAME: fig:mpm-selection @@ -666,7 +667,7 @@ 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 +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. @@ -704,8 +705,9 @@ parse of a text. 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". We will show a example relevant to our setting in the -following section. +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. * 5 MECHANICAL ENGINEERING DESIGNS A graphical formalism and a corresponding prototype implementation will be described. :RAY: diff --git a/org/farm-refs.bib b/org/farm-refs.bib index 9b7b101..db17c05 100644 --- a/org/farm-refs.bib +++ b/org/farm-refs.bib @@ -421,4 +421,15 @@ url="http://dx.doi.org/10.1007/s10817-016-9377-1" author={Schank, R. and Birnbaum, L}, institution={Department of Computer Science, Yale University}, number={189}, - year={1980}} \ No newline at end of file + year={1980}} + +@article{ehrig1992introduction, + title={Introduction to graph grammars with applications to semantic networks}, + author={Ehrig, Hartmut and Habel, Annegret and Kreowski, Hans-J{\"o}rg}, + journal={Computers \& Mathematics with Applications}, + volume={23}, + number={6-9}, + pages={557--572}, + year={1992}, + publisher={Elsevier} +} -- 2.11.4.GIT