org/scheme-talk.org

   1
   2 #+TITLE:     Extending the LISP model: from cons cells to triples, from trees to hypergraphs
   3 #+AUTHOR:    Joseph Corneli and Raymond Puzio
   4 #+EMAIL:     contact@planetmath.org
   5 #+DATE:      \Lightning[fill=yellow] Saturday, 3 September, 2017 (Scheme@ICFP) \Lightning[fill=yellow]
   6 #+DESCRIPTION: Organizer for presentation on arxana and math text analysis at Oxford.
   7 #+KEYWORDS: arxana, hypertext, inference anchoring
   8 #+LANGUAGE: en
   9 #+OPTIONS: H:1 num:t toc:nil \n:nil @:t ::t |:t ^:nil -:t f:t *:t <:t
  10 #+OPTIONS: TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
  11 #+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
  12 #+EXPORT_SELECT_TAGS: export
  13 #+EXPORT_EXCLUDE_TAGS: noexport
  14 #+LATEX_CLASS: beamer
  15 #+LATEX_CLASS_OPTIONS: [presentation,serif]
  16 #+LATEX_HEADER: \usefonttheme{professionalfonts}
  17 #+LATEX_HEADER: \usepackage{fontspec}
  18 #+LATEX_HEADER: \setromanfont{TeX Gyre Pagella}
  19 #+LATEX_HEADER: \usepackage{mathtools}
  20 #+LATEX_HEADER: \usepackage{unicode-math}
  21 #+LATEX_HEADER: \setmathfont{TeX Gyre Pagella Math}
  22 #+LATEX_HEADER: \setmonofont[Color=blue]{TeX Gyre Adventor}
  23 #+LATEX_HEADER: \usepackage{listings}
  24 #+LATEX_HEADER: \usepackage{parskip}
  25 #+LATEX_HEADER: \newfontfamily{\lstsansserif}[Scale=.85]{TeX Gyre Adventor}
  26 #+LATEX_HEADER: \lstset{basicstyle=\lstsansserif\color{blue},keywordstyle=\lstsansserif\color{blue}}
  27 #+LATEX_HEADER: \definecolor{fondpaille}{cmyk}{0,0,0.1,0}
  28 #+LATEX_HEADER: \definecolor{sepia}{rgb}{0.44, 0.26, 0.08}
  29 #+LATEX_HEADER: \setbeamercolor{background canvas}{bg=fondpaille}
  30 #+LATEX_HEADER: \setbeamercolor{normal text}{fg=sepia}
  31 #+LATEX_HEADER: \beamertemplatenavigationsymbolsempty
  32 #+LATEX_HEADER: \usepackage{lightning}
  33 #+LINK_UP:
  34 #+LINK_HOME:
  35 #+HTML_HEAD: <link rel="stylesheet" type="text/css" href="http://metameso.org/~joe/solarized-css/build/solarized-light.css" />
  36 #+STARTUP: showeverything
  37
  38 # convert example-graph.png -fuzz 1% -fill 'rgb(255,255,230)' -opaque white fond-graph.png
  39
  40 # #+LATEX_HEADER: \setbeamertemplate{footline}[frame number]
  41
  42 # * Title slide
  43
  44 # Extending the LISP model:
  45 # from cons cells to triples, from trees to hypergraphs
  46
  47 # Joseph Corneli and Raymond Puzio
  48
  49 # Saturday, 3 September, 2017
  50 # Scheme@ICFP
  51 # Oxford, UK
  52 * From cons cells to triples
  53
  54 # make clear that doesn't (yet) have an eval.
  55 *Arxana* makes use of a higher-dimensional data type to represent
  56 nested semantic networks.
  57
  58 In contradistinction to the standard s-expressions used in LISP where
  59 the fundamental building block is a cell =(a . b)= which is built from
  60 a =car= and a =cdr=, Arxana's fundamental building block is a triple,
  61 =(a c b)=, built from a =src=, =txt=, and =snk=.
  62
  63 In LISP, we use functions like =setcar= and =setcdr= to manipulate
  64 structure; in Arxana, we have analogous things such as =update-src=
  65 and =update-snk=.
  66
  67 * From trees to hypergraphs
  68
  69 Furthermore, in the language of the Semantic Web, every triple is
  70 `reified'.  Links and their contents can be augmented with offset
  71 annotations, and can contain further structure.
  72
  73 Pierre De Lacaze shared an illustrative example of the kind of
  74 structure we're talking about, and why it is different from more
  75 elementary relations in a semantic network.
  76
  77 /Mom resents the fact that John disapproves of Jane and Jim's
  78 marriage./
  79
  80 #+ATTR_ORG: :width 400
  81 #+ATTR_LATEX: :width 5cm
  82     [[file:./fond-mom.png]]
  83
  84 * Illustration of basic mechanics
  85
  86 Both nodes and links are represented as triples, and we collectively
  87 call them /nemas/.  A repository of nemas is a /plexus/.
  88
  89 1. Each plexus has a distinguished element =0=, called *ground*.
  90
  91 2. If we set =α:=(A D E)=, then =(α C B)= is an assertion about the
  92    link =(A D E)=.
  93
  94 3. On the other hand, =((get-src α) D E)= is about the =src= of =α=,
  95    which happens to be =a= at present (but nemas are mutable).
  96
  97 4. If we wanted to make an assertion about =A= "itself", we can
  98    represent it as a nema with the special form =β:=(0 A
  99    0)=.  Subsequently, =(β C B)= is an assertion about =A=.
 100
 101 # [That said, =β= would still be mutable, is this a problem? -JC]
 102
 103 * What do we get?
 104
 105 These facilities allow us to build, reason about, query, and program
 106 with hypergraphs rather than trees or networks.
 107
 108 Unlike mainstream graph databases, code can be stored on links.  This
 109 representation strategy is useful for building runnable conceptual
 110 models of complex and recursive structures.
 111
 112 In particular, we have found this representation strategy well-suited
 113 to modelling the non-deductive style of informal mathematical
 114 dialogues and expositions.
 115
 116 * Related work
 117
 118 Historical programming languages which support a similar annotative
 119 style include Kurzweil el al's /Flare/ and Nelson's /ZigZag/.
 120
 121 A more recent endeavour is /AtomSpace/, which is a more mature piece
 122 of software than Arxana, e.g., it comes with both Scheme and Python
 123 bindings and a range of optimisations.
 124
 125 The simplicity of Arxana makes it useful for prototyping!
 126
 127 Also, it is implemented in Emacs Lisp, which we have found useful (in
 128 particular, stable) for our sub-part-time workflow.
 129
 130 * History of development and outreach
 131
 132 - Free Culture and the Digital Library Symposium, Atlanta, 2005
 133 - Experiments with a Common Lisp + cl-elephant backend, 2007
 134 - Rewrite with a Common Lisp + SQL backend, 2010
 135 - Rewrite with the storage model described here, 2013
 136 - Presentations at LispNYC, 2005 and 2013
 137 - Presentation at the Emacs Conference, London, 2013
 138 - Presentation at the monthly Emacs Meetup, NYC, 2017
 139 - Next Saturday: presentation at FARM 2017
 140
 141 * Other relevant work: Conceptual Dependence theory
 142
 143 # Footnotes
 144
 145 E.g., "John gave Mary a book."
 146 #+ATTR_ORG: :width 800
 147 #+ATTR_LATEX: :width 11cm
 148     [[file:./fond-john.png]]
 149 #+BEGIN_SRC lisp
 150 (atrans actor  (person name john)
 151         object (phys-obj type book)
 152         recip  (person name mary))
 153 #+END_SRC
 154
 155 \bigskip
 156
 157 *NB. We view Conceptual Dependence /primitives/ (like =atrans=) as
 158 analogous to /performatives/ (like =Assert=, =Challenge=, etc.).*
 159
 160 * Illustration: Application to mathematics
 161 ``I have seen this problem, that if $G$ is a finite group and $H$ is a
 162 proper subgroup of $G$ with finite index then $ G \neq
 163 \bigcup\limits_{g \in G} ghg^{-1}$. Does this remain true for the infinite case also.''
 164 #+ATTR_ORG: :width 800
 165 #+ATTR_LATEX: :width 10cm
 166     [[file:./fond-graph.png]]
 167 *``There's something I don't understand here: do you perhaps mean
 168 $gHg^{-1}$ instead of $ghg^{-1}$?''*
 169
 170 * Input:
 171 For example, if we take the correction on board, the first assertion
 172 above might be written like this:
 173 #+BEGIN_SRC lisp
 174 (read-tree  '(Assert
 175               (implies
 176                (conjunction (finite-group G)
 177                             (subgroup H G)
 178                             (has_property (index H G)
 179                                           finite))
 180                (not (equal G
 181                            (union (times g
 182                                          H
 183                                          (inverse g))
 184                                   :over g :in G))))))
 185 #+END_SRC
 186
 187 * Output:
 188
 189 Nodes are given unique (=gensym='ed) labels; nested code is not.
 190 #+BEGIN_SRC lisp
 191 (Assert123
 192    (implies124
 193      (conjunction125 (finite-group G)
 194                      (subgroup H G)
 195                      (has_property126 (index H G)
 196                                       finite))
 197      (not127 (equal G (union (times g
 198                                     H
 199                                     (inverse g))
 200                              :over g :in G)))))
 201 #+END_SRC
 202
 203 The labels can then be referred to in subsequent input, so that
 204 additional structure can be added relative to existing structure.
 205
 206 * Illustration: nested structure
 207
 208 #+ATTR_ORG: :width 800
 209 #+ATTR_LATEX: :width 10cm
 210     [[file:./fond-nested.png]]
 211
 212
 213 * Summary
 214
 215 - local storage of code and data (like in LISP)
 216 - some of this code can act on the structures (like in LISP)
 217 - nested code can be be used to create overlaid structures, e.g., "cones" (sort of like Emacs text properties)
 218
 219 * Future work
 220
 221 - formalise the spec SO THAT it's consistent
 222 - re-integrate cool features from 2005 and improve SO THAT we can conveniently browse and edit, e.g., TeX documents
 223 - improve (code) libraries for search, interaction with cones, versioning, typing SO THAT we can treat the content as a (digital) library with actionable features
 224 - integrate with external database(s) SO THAT we can interact with "big data"
 225 - integrate features from /The Reasoned Schemer/ SO THAT we can reason effectively about data represented in our new data type
 226
 227 * The end
 228
 229 That's all for now!
 230
 231 - =joseph.corneli@ed.ac.uk=
 232 - =rspuzio@planetmath.info=
 233
 234 PS. Maybe see you on our "mob" branch.
 235
 236 - http://repo.or.cz/w/arxana.git
 237
 238 * outtakes                                                         :noexport:
 239
 240 ** Other things we've worked on
 241
 242 - "nemas" document:  http://metameso.org/ar/metamathematics.pdf
 243 - Joe's thesis Appendix B: http://metameso.org/ar/thesis-appendix-b.pdf
 244 - Metamathematics preprint: http://metameso.org/ar/mathematical-semantics.pdf
 245 - hcode function spec: http://metameso.org/ar/hcode.pdf
 246 - Lakatos game spec: http://metameso.org/ar/lakatos-flowchart.pdf
 247 - [[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.
 248 - [[http://metameso.org/cgi-bin/current.pl/Two_years_later][Two years later]] collects many of the mathematical themes in
 249   overview
 250 - [[http://metameso.org/cgi-bin/current.pl/samples_of_formal_mathematical_writing][samples of formal mathematical writing]] is a small collection
 251   of statements in mathematical language (leaving out ``the part
 252   in between dollar signs'')
 253
 254 #+C Local Variables:
 255 #+C org-tree-slide-skip-outline-level: 3
 256 #+C mode-line-format: nil
 257 #+C org-latex-compiler: "xelatex"
 258 #+C eval: (org-display-inline-images t t)
 259 #+C eval: (setq org-tree-slide-header nil)
 260 #+C End:
 261
 262 * Frame with references :noexport:
 263   :PROPERTIES:
 264   :BEAMER_OPT: fragile,allowframebreaks,label=
 265   :END:
 266   \printbibliography