From 856e2bc4494e0aa16acda30e01cdbfa3a93538b9 Mon Sep 17 00:00:00 2001 From: Joe Corneli Date: Wed, 31 May 2017 19:06:31 +0100 Subject: [PATCH] some more --- org/farm-2017.org | 87 +++++++++++++++++++++++++++++++++++++++++++++---------- org/farm-refs.bib | 16 +++++++++- 2 files changed, 87 insertions(+), 16 deletions(-) diff --git a/org/farm-2017.org b/org/farm-2017.org index a852d52..1a32714 100644 --- a/org/farm-2017.org +++ b/org/farm-2017.org @@ -99,18 +99,20 @@ 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 3, thread 11 - part of a collaborative online - effort to a problem from the 2011 International Mathematics - Olympiad.[fn:: https://polymathprojects.org/2011/07/19/minipolymath3-project-2011-imo/] +- *MPM* :: Mini-polymath 3, threads 3, 11, and 14 - selected portions + of a collaborative online effort to solve a problem from + the 2011 International Mathematics Olympiad.[fn:: + https://polymathprojects.org/2011/07/19/minipolymath3-project-2011-imo/] -- *GCP* :: Timothy Gowers - What is the 500th digit of - $(\sqrt{2}+\sqrt{3})^{2012}$? +- *GCP* :: Timothy Gowers's - What is the 500th digit of + $(\sqrt{2}+\sqrt{3})^{2012}$? from his Maxwell Institute + Lecture "Modelling the mathematical discovery process" - *AGT* :: Section II.H, ``Normal Extensions'' of ``Galois Theory'' by - Emil Artin. + Emil Artin. -- *HHS* :: Section 22, ``Adjoints'' of ``Introduction to Hilbert Space'' - by P. R. Halmos. +- *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 @@ -340,8 +342,8 @@ 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, +\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 @@ -524,6 +526,7 @@ answer questions like: - "Why does Thomas agree with Anonymous?" - "Why does Gal says the suggestion is beautiful?" +- "Why did Anonymous suggest `perhaps even the line does not matter'?" The premise here is that the dynamics at work are based on performatives being chosen based upon current valuations, goals, and @@ -544,7 +547,7 @@ rooted on the =ATRANS= primative: We would like to do the same sort of thing here, using IATC performatives as our primatives. Like the standard CD primatives, -these performatives have slots \cite{gabi-iatc}, described as follows: +these performatives have slots, described as follows:[fn:: See \cite{gabi-iatc} for further details.] - =Assert= (/s/ [, /a/ ]): Assert belief that statement /s/ is true, optionally because of /a/. - =Agree= (/s/ [, /a/ ]): Agree with a previous assertion. @@ -554,7 +557,7 @@ these performatives have slots \cite{gabi-iatc}, described as follows: - =Judge= (/s/): Apply a heuristic value judgement /s/ to some statement. - =Suggest= (/s/): Advance a tactical reasoning move, /s/. - =Query= (/s/): Ask for the truth value of /s/. -- =QueryE= ({/pi(X)/}./i/): Ask for the class of objects /X/ for which all of the properties /pi/ hold. +- =QueryE= ({/pi/(/X/)} . /i/): Ask for the class of objects /X/ for which all of the properties /pi/ hold. Similarly, the statements that are introduced via these performatives also have slots, for example: @@ -644,11 +647,65 @@ example from \cite{corneli2017towards} that describes an analogy between a known theorem for finite groups, and a structurally related conjecture for infinite groups. -#+CAPTION: Q&A example (Fig. 1 from \cite{corneli2017towards}) +#+CAPTION: Q&A example (lightly adapted from \cite[Fig. 1]{corneli2017towards}) #+NAME: fig:qa-fig -[[./qa-fig-1.png]] +[[./revised-qa-question.png]] -- parsing and querying +The analogy between the two clusters is clear: in one case $G$ is a +finite group, in the other $G$ is an infinite group. Naturally, this +is not the same "\(G\)". Using a typed formalism we could be more +specific about the difference between the two sides, while retaining a +structural similarity on the two sides of the analogy:[fn:: Something along the lines of clojure.spec may be useful these purposes; it provides a "standard, expressive, powerful and integrated system for specification and testing"; see https://clojure.org/about/spec.] + +#+BEGIN_SRC +G: group -> X: group +G has_card finite -> X has_card infinite +#+END_SRC + +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 +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. + +Given sufficently detailed representations - sometimes requiring +background theories (like group theory in the Q&A example, or plane +geometry in MPM), we expect analogical reasoning to serve as the main +explanatory mechanism. Sowa and Majumdar describe three ways of doing +analogical reasoning about conceptual graphs: + +#+BEGIN_QUOTE +The first compares two nodes by what they contain in themselves +independent of any other nodes; the second compares nodes by their +relationships to other nodes; and the third compares the mediating +transformations that may be necessary to make the graphs comparable. +#+END_QUOTE + +Pushing the reasoning problem "back" to the natural language +processing layer by suggesting that sufficiently rich representations +are the main thing we need to proceed with reasoning may seem like it +is dodging the issue. However, there is in fact a (high-order) +analogy between what goes on in parsing and reasoning. Lytinen +\cite{lytinen1992conceptual} summarises Schank and Birnbaum +\cite{schank-and-birnbaum} on semantic parsing, again, referring to +three aspects of the parser: + +#+BEGIN_QUOTE +... its /control structure/, or the processes that occur during +parsing; its /representational structures/, or the representations +which it builds during the parsing process; and its /knowledge base/, +or the set of rules which the parser draws on and which drive the +parse of a text. +#+END_QUOTE + +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. * 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 cb4defc..9b7b101 100644 --- a/org/farm-refs.bib +++ b/org/farm-refs.bib @@ -407,4 +407,18 @@ url="http://dx.doi.org/10.1007/s10817-016-9377-1" pages={879--881}, year={2009}, publisher={Nature Publishing Group} -} \ No newline at end of file +} + +@misc{gowers-talk, + author={Gowers, W.T. and Ganesalingam, M.}, + title={Modelling the mathematical discovery process}, + note={Maxwell Institute Lecture, Fri, November 2, 4pm -- 5pm, James Clerk Maxwell Building, University of Edinburgh}, + year={2012}, +} + +@techreport{schank-and-birnbaum, + title={Memory, meaning, and syntax}, + author={Schank, R. and Birnbaum, L}, + institution={Department of Computer Science, Yale University}, + number={189}, + year={1980}} \ No newline at end of file -- 2.11.4.GIT