org/scheme-talk.org

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