org/farm-2017.org

   1 #+TITLE:     Functional models of mathematical reasoning
   2 #+AUTHOR:    Joseph Corneli and Raymond Puzio
   3 #+EMAIL:     contact@planetmath.org
   4 #+DATE:      May 27, 2017 for Thursday 1 June, 2017 deadline
   5 #+DESCRIPTION: Outline and draft of 12 page paper on math text analysis for FARM workshop at ICFP 2017
   6 #+KEYWORDS: arxana, hypertext, inference anchoring theory
   7 #+LANGUAGE: en
   8 #+OPTIONS: H:3 num:nil toc:t \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
   9 #+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
  10 #+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
  11 #+EXPORT_SELECT_TAGS: export
  12 #+EXPORT_EXCLUDE_TAGS: noexport
  13 #+LINK_UP:
  14 #+LINK_HOME:
  15 #+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
  16 #+BIBLIOGRAPHY: farm-refs plain
  17 #+LATEX_HEADER: \usepackage[backend=bibtex,sorting=none]{biblatex}
  18 #+LATEX_HEADER: \addbibresource{farm-refs}
  19 #+STARTUP: showeverything
  20
  21
  22 #+BEGIN_QUOTE
  23 Functional Programming has emerged as a mainstream software
  24 development paradigm, and its artistic and creative use is booming. A
  25 growing number of software toolkits, frameworks and environments for
  26 art, music and design now employ functional programming languages and
  27 techniques. FARM is a forum for exploration and critical evaluation of
  28 these developments, for example to consider potential benefits of
  29 greater consistency, tersity, and closer mapping to a problem domain.
  30
  31 FARM encourages submissions from across art, craft and design,
  32 including textiles, visual art, *music*, 3D sculpture, animation, GUIs,
  33 video *games*, 3D printing and architectural models, choreography,
  34 *poetry*, and even VLSI layouts, GPU configurations, or
  35 *mechanical engineering designs*.  *Theoretical foundations*, *language design*,
  36 *implementation issues*, and *applications* in industry or the arts are
  37 all within the scope of the workshop.  The language used need not be
  38 purely functional (“mostly functional” is fine), and may be manifested
  39 as a domain specific language or tool.  Moreover, submissions focusing
  40 on questions or issues about the use of functional programming are
  41 within the scope.
  42 #+END_QUOTE
  43
  44 * 0 Introduction
  45
  46 ** 0.1 CONTEXT OF APPLICATION
  47 - modelling mathematical dialogues, people don't just write their things in metamath
  48 - people may make different expository choices
  49 - mathematical text contains argumentation an narrative in addition to logic and calculations ([[1.2][1.2]])
  50 ** 0.2 FORCES
  51 - push to make everything formal (QED, Tarski, LCF) [[1.1][1.1]]
  52 - push to make everything understandable (Alexander)
  53 ** 0.3 PROBLEM
  54 - each different user will have a different "way in", depending on their background knowledge ([[3.2][3.2]])
  55 - how to get behind the scenes to see why?
  56 - how to tailor a given formal content to a given reader?
  57 ** 0.4 SOLUTION (STRATEGY)
  58 - focus on expressivity
  59 - focus on representing process
  60 - formalization and efficiency are important, but will be left for later.
  61 ** 0.5 RATIONALE
  62 - objective: understand mathematics as people do it (literary criticism, rhetoric, argumentation)
  63 - objective: learn from these methods to build new mathematical texts
  64 - build on intuitive diagrams
  65 - build on the idea of parsing natural language (complementary to Mohan's work)
  66 ** 0.6 RESOLUTION of FORCES
  67 - outcome: sharing diagrams with people who can use them
  68 - potential: draw new diagrams
  69 - philosophical: bridging 'two cultures' (proof checkers and artists/designers/hackers)
  70
  71 * 1 THEORETICAL FOUNDATIONS Informal mathematical language is more general, and  the reasoning involved may be abductive, inductive, or heuristic. :RAY:
  72
  73 Even though a mathematical result and its proof involve strict logic,
  74 the process of formulating, motivating proving and explaining go
  75 beyond strict formality. (Pierce, Lautman)
  76
  77 ** <<1.1>> 1.1 Examples of actual texts (different registers)
  78
  79 *** TODO Pull up examples from real texts.
  80
  81 - E.g. Artin's Galois theory book
  82 - E.g. Gowers's "Eventually this is something a computer can solve"
  83
  84 ** <<1.2>> 1.2 A formal language doesn't do anything with this ("Proofs and Prologues")
  85
  86 - (Conclusion from inductive reasoning in 1.1.)
  87
  88 * 2 LANGUAGE DESIGN The presentation here will describe a strategy we have been developing for representing mathematical dialogues and other informal texts. :JOE:
  89
  90 Since we cannot simply build on formal theorem proving, we need to
  91 look further afield for prior work on which to build. (Bundy: choosing
  92 representation strategy that fits can make the problem easier to
  93 solve; Corneli: here we are looking for representations *of*
  94 reasoning, so this gives us a heuristic to guide our search.)
  95
  96 ** <<2.1>> 2.1 Gabi's work on IATC
  97 ** <<2.2>> 2.2 Lytinen CD
  98
  99 * 3 IMPLEMENTATION ISSUES (REQUIREMENTS) :JOE:
 100
 101 We've already seen an *abstract* model of social creativity in
 102 Lakatos, but when we try to zoom in and look at concrete details, we
 103 see further challenges. We know that a `city is not a tree', let's
 104 generalise and assert that a proof dialogue is not a tree.  This gives
 105 us a guiding principle.
 106
 107 ** <<3.1>> 3.1 Let's look at one of our illustrations: it's a graph, no it's a hypergraph!
 108
 109 ** <<3.2>> 3.2 Reason as a social thing (Minsky, Sperber & Mercier, Gowers 'quantum of progress' from Polymath)
 110
 111 ** <<3.3>> 3.3 Lakatos stuff: How is this different from what we're doing?
 112
 113 * 4 APPLICATIONS Our latest efforts produce more detailed models of mathematical arguments. :JOE:
 114
 115 We need to model what's there and how it evolves, noting that evolution is heuristic
 116
 117 ** <<4.1>> 4.1 Kinematics (IATC+CD)
 118 ** <<4.2>> 4.2 Dynamics (Lytinen's stuff with goals and scripts)
 119
 120 * 5 MECHANICAL ENGINEERING DESIGNS A graphical formalism and a corresponding prototype implementation will be described. :RAY:
 121
 122 ** <<5.1>> 5.1 Import and improve technical stuff on Arxana (cf. Nemas doc)
 123 ** <<5.2>> 5.2 Example
 124
 125 * 6 RELATED WORK (GAMES, POETRY): parallels between dialogues and discursive Q&A, traditional proofs. :JOE:
 126
 127 How does this look in a broader context?
 128
 129 ** <<6.1>> 6.1 prior art: board games, story stuff; table that compares between.
 130 ** <<6.2>> 6.2 Alexander: "a city is not a tree"; compare Lamport
 131
 132 -----
 133
 134 * 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:
 135
 136 ** <<7.1>> 7.1 There is a degree of formality in the specifications, but also informality in the heuristics.
 137
 138 * 8 MOB PROGRAMMING :onhold:
 139
 140 ** <<8.1>>
 141 ** <<8.2>>
 142
 143 * 9 RELATED WORK music from corneli, pease, stefanou survey ("Chapter 6"); NNexus project; Socratic :onhold:
 144
 145 ** <<9.1>>
 146 ** <<9.2>>
 147
 148 * 10 CONCLUSION :onhold:
 149
 150 ** <<10.1>>
 151 ** <<10.2>>