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