pres-esop15/01.xhtml

   1 <?xml version="1.0" encoding="utf-8" ?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
   3           "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"
   4 [
   5           <!ENTITY in  "<small style='font-size:small'>∈</small>">
   6           <!ENTITY notin  "<small style='font-size:small'>∉</small>">
   7           <!ENTITY emptyset  "⦰">
   8           <!ENTITY cup       "∪">
   9           <!ENTITY cap       "∩">
  10           <!ENTITY mapsto  "↦">
  11           <!ENTITY rarrow   "⟶">
  12           <!ENTITY rsarrow   "→">
  13           <!ENTITY cduce   "&#x2102;Duce">
  14           <!ENTITY land    "∧" >
  15           <!ENTITY lor      "∨" >
  16           <!ENTITY setminus "∖" >
  17           <!ENTITY bottom   "<tt>Empty</tt>" > <!-- 𝟘 -->
  18           <!ENTITY top      "<tt>Any</tt>" > <!-- 𝟙 -->
  19           <!ENTITY subseteq "⊆" >
  20           <!ENTITY leq      "≤" >
  21           <!ENTITY Lrarrow  "⟺">
  22           <!ENTITY lbag  "⟅">
  23           <!ENTITY rbag  "⟆">
  24           <!ENTITY lbrack "<span style='font-size:xx-large;'>⟦</span>" >
  25           <!ENTITY rbrack "<span style='font-size:xx-large;'>⟧</span>" >
  26           <!ENTITY bcirc  "⏺" >
  27           <!ENTITY left  "<tt style='color:#d33'>L</tt>" >
  28           <!ENTITY right  "<tt style='color:#33d'>R</tt>">
  29           <!ENTITY ztop      "⊤" >
  30           <!ENTITY rleadsto  "⟿"> <!-- -->
  31           <!ENTITY rwave   "↝">
  32           <!ENTITY mathV     "𝓥">
  33           <!ENTITY mathT     "𝓣">
  34           <!ENTITY vdash     "⊢">
  35 ]
  36           >
  37 <html xmlns="http://www.w3.org/1999/xhtml" >
  38   <head>
  39     <title>A Core Calculus for XQuery 3.0</title>
  40
  41     <meta http-equiv="Content-Type"
  42           content="text/html; charset=utf-8" />
  43     <meta name="copyright"
  44           content="Copyright &#169; 2013 Kim Nguyễn" />
  45
  46     <!-- Load jQuery -->
  47     <script src="../jquery-2.0.3.min.js" type="text/javascript" ></script>
  48     <script src="../libs/raphael-min.js" type="text/javascript" ></script>
  49     <!-- Load the library -->
  50     <script src="../simpleWebSlides.js" type="text/javascript" ></script>
  51
  52     <link rel="stylesheet" href="../simpleWebSlides.css" type="text/css"  media="all" />
  53     <!-- Load a custom Theme, the class-element marks this style-sheet
  54          a "theme" that can be swtiched dynamicaly -->
  55     <link class="sws-theme" rel="stylesheet"  title="U-Psud style"  href="../themes/uPsud.css" type="text/css" />
  56
  57     <!-- Customize some templates and initialize -->
  58
  59     <script type="text/javascript">
  60       SWS.Config['sws-slide-change'] = SWS.Effects.slideChangeFadeOutIn;
  61       SWS.Config['sws-object-deactivate'] =  SWS.Effects.objectDeactivateFadeOut;
  62       SWS.Config['sws-object-activate'] = SWS.Effects.objectActivateFadeIn;
  63
  64       //Ensures that we load SWS at the very end, after MathJax has
  65       //been initialized
  66
  67       $(window).load(SWS.Presentation.init);
  68
  69       var col_change = function (sel, col) {
  70       return function (canvas) {
  71         canvas.find(".xpath *").css("color","");
  72         var objs = canvas.find(sel);
  73         objs.css("color", col);
  74       };
  75       };
  76       var reg = SWS.Presentation.registerCallback;
  77     </script>
  78     <style>
  79       <![CDATA[
  80
  81        @font-face {
  82          src: url("OpenSans-Regular.ttf") format("truetype");
  83          font-family: "Open Sans";
  84          font-weight: normal;
  85        }
  86
  87       @font-face {
  88          src: url("OpenSans-Bold.ttf") format("truetype");
  89          font-family: "Open Sans";
  90          font-weight: bold;
  91        }
  92
  93       @font-face {
  94          src: url("OpenSans-Italic.ttf") format("truetype");
  95          font-family: "Open Sans";
  96          font-style: italic;
  97        }
  98
  99       @font-face {
 100          src: url("OpenSans-BoldItalic.ttf") format("truetype");
 101          font-family: "Open Sans";
 102          font-weight: bold;
 103          font-style: italic;
 104        }
 105
 106          ]]>
 107
 108       body {
 109       font-family: 'Open Sans',sans-serif;
 110       font-size: 3.75vh;
 111       background-color: white;
 112       color:  #393938;
 113       }
 114
 115       .sws-canvas {
 116             color: #393938;
 117       }
 118       code, tt {
 119                   color: #292928;
 120       }
 121       pre, dfn, .infer { font-family : serif;
 122       font-style:normal;
 123       color: #292928;
 124       }
 125
 126       .stack {
 127       text-align:center;
 128       vertical-align:text-bottom;
 129       display:inline-block;
 130       }
 131       .over {
 132       display:block;
 133       font-size:small;
 134       margin: 0pt;
 135       padding: 0pt;
 136       }
 137
 138       .infer {
 139       text-align:center;
 140       vertical-align:text-bottom;
 141       display:inline-block;
 142       margin-bottom:1em;
 143       margin-top:0em;
 144       }
 145       .infer > span {
 146                display:block;
 147                margin: 0pt 0pt 0pt 0pt;
 148                padding: 0pt 0pt 0pt 0pt;
 149                border-width: 0pt;
 150       }
 151       .infer > span:last-child {
 152                margin: 0pt 0pt 0pt 0pt;
 153                padding: 0pt 0pt 0pt 0pt;
 154                border-width: 1pt 0pt 0pt 0pt;
 155                border-style: solid;
 156                border-color:  #292928;
 157       }
 158       .infer + span {
 159                vertical-align:text-top;
 160                position:relative;
 161                top:-1.75em;
 162                display:inline;
 163                font-size:80%;
 164                color: #00486c;
 165                margin: 0pt 0pt 0pt 0pt;
 166                padding: 0pt 0pt 0pt 0pt;
 167       }
 168       span.fill { display:inline-block;
 169                   width:100%;
 170                   height: 0pt;
 171       }
 172
 173     </style>
 174   </head>
 175   <body>
 176     <div class="sws-slide sws-cover sws-option-nofooter">
 177       <h1 style="font-size:200%;position:relative;top:-1em;">A Core Calculus for XQuery 3.0</h1>
 178       <h3>Combining Navigational and Pattern-Matching Approaches</h3>
 179       <div style="text-align:center;">
 180         <table style="display:inline-block">
 181           <tr>
 182             <td>Giuseppe Castagna<sup>1</sup></td>
 183             <td>Hyeonseung Im<sup>2</sup></td>
 184           </tr>
 185           <tr>
 186             <td><u>Kim Nguyễn</u><sup>3</sup></td>
 187             <td>Véronique Benzaken<sup>3</sup></td>
 188           </tr>
 189         </table>
 190       </div>
 191       <p style="font-size:80%;position:absolute;bottom:2.5em;left:4em;">
 192         1 CNRS, PPS, Université Paris-Diderot, Paris, France <br/>
 193         2 Kangwon National University, Chuncheon, Rep. of Korea<br/>
 194         3 LRI, Université Paris-Sud, Orsay, France
 195       </p>
 196     </div>
 197     <div class="sws-slide">
 198       <h1>XQuery 3.0</h1>
 199 <p>W3C standard to query XML documents</p>
 200 <code style="background:white;font-size:90%;">
 201    declare function <u>get_links</u>(<u>$page</u>, <u>$print</u>) {
 202        <span class="for">for</span> <u>$i</u> <span class="for">in</span> <u>$page</u><span class="xpath">/descendant::a[not(ancestor::b)]</span>
 203        <span class="for">return</span> <u>$print</u>(<u>$i</u>)
 204    }
 205
 206    declare function <u>pretty</u>(<u>$link</u>) {
 207        <span class="ts">typeswitch</span>(<u>$link</u>)
 208        <span class="ts">case</span> <u>$l</u> <span class="ts">as element(a)</span>
 209             return <span class="sw">switch</span> (<u>$l</u><span class="xpath">/@class</span>)
 210                    <span class="sw">case</span> "style1"
 211                      return &lt;a href={<u>$l</u><span class="xpath">/@href</span>}&gt;&lt;b&gt;{<u>$l</u><span class="xpath">/text()</span>}&lt;/b&gt;&lt;/a&gt;
 212                    default return <u>$l</u>
 213
 214        <span class="ts">default return</span> <u>$link</u>
 215    }
 216
 217    let $bold_links := get_links(document("file.xhtml"), $pretty)
 218 </code>
 219     <script type="text/javascript">
 220       reg ("0", col_change(".xpath, .for, .ts, .sw",""));
 221       reg ("1", col_change(".xpath", "#f80"));
 222       reg ("2", col_change(".for",""));
 223       reg ("2", col_change(".for", "#290"));
 224       reg ("3", col_change(".ts", ""));
 225       reg ("3", col_change(".ts", "#80f"));
 226       reg ("4", col_change(".sw", ""));
 227       reg ("4", col_change(".sw", "#0f2"));
 228     </script>
 229     </div>
 230     <div class="sws-slide">
 231       <h1>XQuery 3.0</h1>
 232       <ul>
 233         <li>Pros<br/>
 234           + standardized <br/>
 235           + nice declarative syntax for paths
 236         </li>
 237         <li>Cons<br/>
 238           - sometime tedious to extract subtrees while preserving the structure<br/>
 239           - <s>no typechecking for functions (typechecking is optional in 3.0)</s>
 240         </li>
 241       </ul>
 242       <p>It's a pity since XML <em>documents</em> are very precisely
 243       typed (DTD, XMLSchemas)</p>
 244       <p>Document type information is validated at runtime rather than
 245       checked statically</p>
 246     </div>
 247     <div class="sws-slide">
 248       <h1>&cduce;</h1>
 249       <p>A polymorphic functional language equipped with
 250       semantic subtyping</p>
 251
 252 <code style="font-size:90%">
 253   let <u>pretty</u> ((&lt;a&gt;Any <span class="typ">&rarrow;</span> &lt;a&gt;Any)  <span class="typ">&amp;</span>  (Any<span class="typ">\</span>&lt;a&gt;Any <span class="typ">&rarrow;</span> Any<span class="typ">\</span>&lt;a>Any)) =
 254       function
 255     | <span class="pat">&lt;a class="style1" href=<u>h</u> ..&gt; <u>l</u></span> &rarrow; &lt;a href=<u>h</u>&gt;[ &lt;b&gt;<u>l</u> ]
 256     | <span class="pat">x</span> &rarrow; x
 257
 258
 259   let <u>get_links</u> (page: &lt;(Any)&gt;Any) (print: &lt;a&gt;Any <span class="typ">&rarrow;</span> &lt;a&gt;Any) : <span class="typ">[ &lt;a&gt;Any * ]</span> =
 260
 261       match page with
 262       <span class="pat">&lt;a&gt;_ &amp; x</span> &rarrow; [ (print x) ]
 263     | <span class="pat">&lt; (_\‘b) &gt; l</span> &rarrow;
 264                  (<span class="lc">transform l with</span> <span class="pat">(i &amp; &lt;_&gt;_)</span> &rarrow; get_links i print)
 265     | <span class="pat">_</span> &rarrow; [ ]
 266 </code>
 267         <script type="text/javascript">
 268           reg ("0", col_change(".pat,.typ,.lc",""));
 269           reg ("1", col_change(".pat", "#f80"));
 270           reg ("2", col_change(".typ", "#290"));
 271           reg ("3", col_change(".lc", "#80f"));
 272     </script>
 273
 274     </div>
 275     <div class="sws-slide">
 276       <h1>&cduce;</h1>
 277       <ul>
 278         <li>Pros<br/>
 279           + Statically typed <br/>
 280           + compact (and efficient) type and value pattern-matching
 281         </li>
 282         <li>Cons<br/>
 283           - <s>complex navigation encoded through explicit recursion</s><br/>
 284           - no type inference for functions
 285         </li>
 286       </ul>
 287       <p>Writing functions to traverse documents is painfull</p>
 288     </div>
 289     <div class="sws-slide">
 290       <h1>This work</h1>
 291       <ol style="margin-left:1em; margin-right:0.25em;list-style-position:inside;">
 292         <li id="tobox" style="padding:1em 0em 1em 0em;"><span class="lh">Add support for path navigation to
 293             &cduce;</span>
 294           <ul style="margin-top:2em;">
 295             <li>Enrich the type algebra with <em>zippers</em> (à la Huet)</li>
 296             <li>Extend pattern-matching construct to <em>zipped values  and types</em></li>
 297             <li>Encode path expressions as recursive patterns</li>
 298           </ul>
 299         </li>
 300         <li class="ll" style="padding:1em 0em 1em 0em;">Perform a type-directed translation from XQuery to
 301           &cduce;</li>
 302       </ol>
 303       <script type="text/javascript">
 304         reg (1, col_change(".lh", "#f83"));
 305         reg (1, col_change(".ll", "#bbb"));
 306       </script>
 307     </div>
 308     <div class="sws-slide">
 309       <h1>&cduce;'s type algebra</h1>
 310 <p>A set &mathT; of types</p>
 311 <pre style="text-align:center;">    t ::=  b  |  c  |  <u>t × t</u>  |  <u>t &rarrow; t</u>  |  <mark>t &lor; t</mark>  |  <mark>t  &land; t</mark>  |  <mark>t &setminus; t</mark>  |  <mark>&top;</mark>  |  <mark>&bottom;</mark>  |  &alpha;
 312 </pre>
 313 <p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
 314    <dfn>c</dfn> : ranges over singleton types
 315    (<tt>`A</tt>, <tt>42</tt>, …)<br/>
 316    <u>Type constructors</u> <br/>
 317    <mark>Boolean connectives</mark> <br/>
 318    <dfn>&alpha;</dfn> : type variables<br/>
 319    types are interpreted co-inductively: recursive types and regular
 320    expression types<br/>
 321 </p>
 322 <div style="vertical-align:top;">
 323 <pre style="width:50%;display:inline-block;">      t<sub>1</sub> ≡ (<tt>Int</tt> × t<sub>1</sub>)    &lor;    t<sub>2</sub>
 324       t<sub>2</sub> ≡ (<tt>Bool</tt> × t<sub>2</sub>)  &lor; (<tt>Bool</tt> × <tt>`nil</tt>)
 325 </pre>
 326 <pre style="width:30%;display:inline-block;"> <span class="sws-pause">t<sub>1</sub> ≡ <tt>[ Int* Bool+ ]</tt></span></pre>
 327 </div>
 328     </div>
 329     <div class="sws-slide">
 330       <h1>Semantic subtyping</h1>
 331 <pre style="text-align:center;">
 332 t &leq; s   &Lrarrow;   &lbrack;t&rbrack; &subseteq;  &lbrack;s&rbrack;
 333 </pre>
 334 <p><dfn>&lbrack; &rbrack;</dfn> interpretation of types as sets of
 335   values<br/>
 336   Allows to reason <i>modulo</i> semantic equivalence of type connectives :
 337 </p>
 338 <pre >
 339       <tt>[ Int* (Int | Bool*)? ]</tt> &land; <tt>[ Int+ (Bool+ | Int)* ]</tt> ≡ <tt>[Int+ Bool*]</tt>
 340 </pre>
 341 </div>
 342 <div class="sws-slide">
 343 <h1>&cduce; data-model</h1>
 344 <p>The usual sets &mathV; of values:</p>
 345 <pre style="text-align:center">       v ::= <tt>1</tt>  |  …  |  <tt>`Foo</tt>  |   (v, v)  |  &lambda;x.e
 346 </pre>
 347 <p>Sequences are nested pairs (<i>à la</i> Lisp):</p>
 348 <pre style="text-align:center;"><tt>[</tt> v<sub>1</sub>  … v<sub>n</sub> <tt>]</tt> ≡ (v<sub>1</sub>, (…, (v<sub>n</sub>, <tt>`nil</tt>)))
 349 </pre>
 350 <p>XML documents are tagged sequences: <pre style="text-align:center;"><tt>&lt;foo&gt;[</tt> v<sub>1</sub>  … v<sub>n</sub> <tt>]</tt> ≡ (<tt>`foo</tt>, <tt>[</tt> v<sub>1</sub>  … v<sub>n</sub> <tt>]</tt>)</pre>
 351 </p>
 352 <p>(Sometimes we write <tt>[ ]</tt> for the variant <tt>`nil</tt>)</p>
 353 <p>Everything is built on top of products and variants</p>
 354 </div>
 355 <div class="sws-slide">
 356       <h1>&cduce; patterns</h1>
 357 <p><i>(a.k.a. the left-hand side of an arrow in a match … with)</i></p>
 358 <pre style="text-align:center;">    p ::=  t  | x | <u>(p, p)</u> |  <mark>p | p</mark>  |  <mark>p &amp; p</mark>    </pre>
 359 <p><dfn>t</dfn> ranges over types<br/>
 360   <dfn>x</dfn> ranges over capture variables<br/>
 361   <u>Pair patterns</u><br/>
 362   <mark> Alternation |, Intersection &amp;</mark><br/>
 363   patterns are also co-inductively interpreted (recursive patterns)
 364 </p>
 365 <p><dfn><u>v / p</u></dfn> : matching a value against a pattern yields a
 366   substitution from variables to values<br/>
 367    <dfn><u>&lbag; p &rbag;</u></dfn> : the set of values accepted by a
 368    pattern is <u>a type</u><br/>
 369    <dfn><u> t / p</u></dfn> : matching a type against a pattern yields a
 370    substitution from variables to types<br/>
 371 </p>
 372 </div>
 373 <div class="sws-slide">
 374       <h1>&cduce; patterns (example)</h1>
 375 <p>Assume <tt><u>l</u></tt> has type <tt>[ Int+ Bool* ]</tt>,  consider:</p>
 376 <code>
 377        match <u>l</u> with
 378        [ _* (<u>x</u> &amp; Int) Bool* (<u>y</u> &amp; Bool) ] &rarrow;  (<u>x</u>, <u>y</u>)
 379     |  [ _* (<u>x</u> &amp; Int) ]                  &rarrow;  (<u>x</u>, `false)
 380     |  [ ]                               &rarrow;  (0, `false)
 381 </code>
 382 <ol style="list-style-position:inside;">
 383 <li class="sws-pause"><dfn>&lbag;<tt>[ _* (<u>x</u> &amp; Int) Bool* (<u>y</u> &amp; Bool) ]</tt>&rbag;    <span style="display:inline-block;width:5em;text-align:center"> ≡</span>     <tt>[ &top;* Int Bool+ ]</tt></dfn><br/>
 384  <span style="text-align:right;display:inline-block;width:94%;">{ x &mapsto; <tt>Int</tt>, y &mapsto; <tt>Bool</tt> }</span>
 385 </li>
 386 <li class="sws-pause"><dfn>&lbag;<tt>[ _* (<u>x</u> &amp; Int) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ &top;* Int ]</tt></dfn><br/>
 387   <span style="text-align:right;display:inline-block;width:58%;"> { x &mapsto; <tt>Int</tt> }</span>
 388 </li>
 389 <li class="sws-pause">Since <dfn><tt>[Int+ Bool* ]</tt> &setminus; ( <tt>[ &top;* Int Bool+ ]</tt> &lor;  <tt>[ &top;* Int]</tt>) ≡ <s>&bottom;</s>  </dfn><br/>
 390     the third case is unreachable.
 391 </li>
 392
 393
 394 </ol>
 395
 396 </div>
 397
 398 <div class="sws-slide">
 399 <h1>Zippers (1/2)</h1>
 400 <ul>
 401   <li>Introduced in 1997 by Gérard Huet</li>
 402   <li>Stack of visited nodes</li>
 403   <li>Push the current node on the stack when traversing a pair</li>
 404   <li>Take the top of the stack to go backward</li>
 405   <li>Tag the elements of the stack to remember which component of a
 406   pair we have visited</li>
 407 </ul>
 408 <pre style="text-align:center;"> v ::=  …  |  v<sub>&delta;</sub>
 409  &delta; ::=  &bcirc;  | &left;v · &delta; | &right;v · &delta;
 410 </pre>
 411
 412 </div>
 413 <div class="sws-slide">
 414 <h1>Zippers (2/2)</h1>
 415 <p><tt><u>fst</u></tt> (resp. <tt><u>snd</u></tt>) takes the first (resp. second)
 416   projection of a pair and update its zipper accordingly:</p>
 417 <pre>      v<sub>1</sub> ≡ (1, (2, (3, (4, `nil))))<sub>&bcirc;</sub>
 418       v<sub>11</sub> ≡ <tt>fst</tt> v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
 419       v<sub>2</sub> ≡ <tt>snd</tt> v<sub>1</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
 420       v<sub>3</sub> ≡ <tt>snd</tt> v<sub>2</sub> ≡ (3, (4, `nil))<sub>&right;v<sub>2</sub> · &right;v<sub>1</sub> · &bcirc; </sub>
 421 </pre>
 422 <p><tt><u>up</u></tt> returns the head of the zipper: </p>
 423 <pre>      <tt>up</tt> v<sub>3</sub> ≡ v<sub>2</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
 424 </pre>
 425 </div>
 426 <div class="sws-slide">
 427   <h1>Zipper types</h1>
 428 <p>We extend the type-algebra with zipper types:</p>
 429 <pre style="text-align:center;"> t ::=  …  |  t<sub>&tau;</sub>
 430  &tau; ::=  &bcirc;  |  &left;t · &tau;  | &right;t · &tau;  |  &tau; &lor; &tau;  |  &tau; &setminus; &tau;  |  &ztop;
 431 </pre>
 432 <p><dfn>&bcirc;</dfn>: singleton type denoting the empty zipper (root element)<br/>
 433    <dfn>&ztop;</dfn>: the top zipper type<br/>
 434    Zipper types are interpreted co-inductively<br/><br/>
 435    <dfn><tt>Int</tt><sub>(&left;&top;)* &bcirc;</sub></dfn> <span style="float:right;">type of
 436    integers that are the leftmost descendant of a tree</span><br/><br/>
 437    <dfn><tt><![CDATA[<html>[ <head>[…] <body>[…] ]]]></tt><sub>&bcirc;</sub></dfn> <span style="float:right;">type of
 438    HTML documents</span><br/><br/>
 439    <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub> &ztop;</sub></dfn> <span style="float:right;">types of links  nested in any context</span>
 440 </p>
 441 </div>
 442 <div class="sws-slide">
 443 <h1>Tree navigation</h1>
 444 <p>Since patterns contain types, we can check complex
 445   conditions:</p>
 446 <pre style="margin-left:1em;width:62%;display:inline-block;border-width:0pt 1pt 0pt
 447   0pt; border-style:dashed;border-color: black;vertical-align:middle">   <span style="font-family:'Open Sans';">Has a descendant <tt>&lt;a&gt;_</tt>:</span>
 448      p ≡ <tt id="test">&lt;a&gt;_</tt>   &lor;   <tt>&lt;_&gt;[ _* <dfn>p</dfn> _* ]</tt>
 449
 450   <span style="font-family:'Open Sans';">Deos not have an ancestor <tt>&lt;b&gt;_</tt>:</span>
 451     &tau; ≡ &bcirc;   &lor;   &right;(&top;&setminus; <tt>&lt;b&gt;_</tt>) · &tau;   &lor;   &left;(&top;&setminus; <tt>&lt;b&gt;_</tt>) · &tau; </pre>
 452 <code style="width:20%;display:inline-block;vertical-align:middle">
 453     match <u>v</u> with
 454        <dfn>p<sub>&tau;</sub></dfn> &amp; <u>x</u> &rarrow; …
 455    | _        &rarrow; …</code>
 456 <p style="background:white">We want more, namely return <i>all</i> descendants (ancestors,
 457   children,  siblings, …) of a node matching a particular condition
 458 <br/><br/>
 459 Remark: (recursive) patterns <u>already perform a recursive traversal
 460   of the value</u>
 461 <br/>
 462 <em>Idea</em>: Piggy back on the traversal and <em>accumulate</em>
 463 nodes in special variables
 464 </p>
 465 </div>
 466 <div class="sws-slide">
 467   <h1>Operators and Accumulators</h1>
 468 <p>An <u>operator</u> is a 4-tupple <dfn>(o, n<sub>o</sub>,
 469     &rleadsto;<sub>o</sub>, &rarrow;<sub>o</sub>)</dfn>, where:</p>
 470 <p><dfn><u>o</u></dfn>: is the accumulator name<br/>
 471 <dfn><u>n<sub>o</sub></u></dfn>: is the arity of <u>o</u><br/>
 472 <dfn><u>&rleadsto;<sub>o</sub></u></dfn>:
 473 &mathV;<sup>n<sub>o</sub></sup> &rsarrow; &mathV;, the reduction relation <br/>
 474 <dfn><u>&rarrow;<sub>o</sub></u></dfn>:
 475 &mathT;<sup>n<sub>o</sub></sup> &rsarrow; &mathT;, the typing relation <br/>
 476 </p>
 477 <p>An <u>accumulator</u> is a variable (ranged over
 478   by <u>ẋ</u>, <u>ẏ</u>, …) with:<br/><br/>
 479   <dfn><u>Op(ẋ)</u></dfn>: an operator<br/>
 480   <dfn><u>Init(ẋ)</u> &in; &mathV;</dfn> : an initial value<br/>
 481 </p>
 482 </div>
 483 <div class="sws-slide">
 484   <h1>Some operators</h1>
 485   <pre style="margin-left:1em;">
 486     v, v' &rleadsto;<sup>cons,</sup> (v, v') <br/>
 487     v, <tt>`nil</tt> &rleadsto;<sup>snoc</sup> (v, <tt>`nil</tt>)<br/>
 488     v, (v',v'') &rleadsto;<sup>snoc</sup> (v', snoc(v,v''))<br/>
 489   </pre>
 490 <p>Now we can use accumulators equipped with cons/snoc in
 491   patterns. Instead of matching a single node against a variable, it
 492   <u>accumulates</u> that node in sequence (in reverse or in-order).</p>
 493 </div>
 494 <div class="sws-slide">
 495 <h1>Pattern matching semantics (simplified)</h1>
 496 <pre style="text-align:center;">
 497   &sigma; &vdash; v / p &rleadsto; &gamma;, &sigma;'
 498 </pre>
 499 <p style="font-size:90%"><dfn><u>&sigma;</u>, <u>&sigma;'</u></dfn>: mapping from accumulators to
 500   values. &nbsp;  Initially: <dfn> &sigma; = { ẋ &mapsto; Init(ẋ) | ẋ &in; p }</dfn><br/>
 501   <dfn><u>v</u></dfn>: input value<br/>
 502   <dfn><u>p</u></dfn>: pattern<br/>
 503   <dfn><u>&gamma;</u></dfn>: mapping from capture variables to
 504   values<br/>
 505 </p>
 506 <div style="padding:0em 1em 0em; text-align:justify;background:white;">
 507   <div class="infer">
 508     <span> v &in; &lbrack; t &rbrack;</span>
 509     <span>&sigma;; &delta; &vdash; v / t &rleadsto; &emptyset;,
 510       &sigma;</span>
 511   </div><span>(type)</span>
 512
 513   <div class="infer">
 514     <span></span>
 515     <span>&sigma; &vdash; v / ẋ &rleadsto; &emptyset;,
 516       &sigma;[ ẋ := Op(ẋ) (v, &sigma;(ẋ)) ]</span>
 517   </div><span>(acc)</span>
 518
 519   <div class="infer">
 520     <span></span>
 521     <span>&sigma; &vdash; v / x &rleadsto; { x &mapsto; v },
 522       &sigma;</span>
 523   </div><span>(var)</span>
 524
 525   <div class="infer">
 526     <span>&sigma; &vdash; (fst v)/p<sub>1</sub>
 527     &rleadsto; &gamma;<sub>1</sub>, &sigma;' </span>
 528     <span>&sigma;' &vdash; (snd v)/p<sub>2</sub>
 529       &rleadsto; &gamma;<sub>2</sub>, &sigma;''
 530     </span>
 531     <span>&sigma; &vdash; v /
 532       (p<sub>1</sub>, p<sub>2</sub>)  &rleadsto;
 533       &gamma;<sub>1</sub>&cup; &gamma;<sub>2</sub>,
 534       &sigma;''</span>
 535   </div><span>(pair)</span>  <span class="fill"></span>
 536 <span style="position:relative;top:-1em;">Remember, if <dfn>v ≡ (v1,v2)<sub>&delta;</sub></dfn> then <dfn><tt>fst v</tt> ≡ v<sub>1 &left;v · &delta;</sub></dfn> and <dfn><tt>snd v</tt> ≡ v<sub>2 &right;v · &delta;</sub></dfn><br/>
 537 (some other rules for alternation, failure, recursion, <i>etc.</i>)</span>
 538 </div>
 539 </div>
 540 <div class="sws-slide">
 541   <h1>Typing of patterns (with accumulators) 1/2</h1>
 542   <p>Well known that typing path expressions escapes regular tree languages
 543     (i.e. &cduce;'s types). Consider:
 544   </p>
 545 <pre style="margin:-3em 0pt -1em;">
 546       t ≡ <tt>&lt;c&gt;[ <u>&lt;a&gt;[]</u> t <u>&lt;b&gt;[]</u> ] </tt>   &lor;   <tt>&lt;c&gt;[]</tt>   <img style="margin-left:3em;width:15%;vertical-align:middle;" src="anbn_tree.svg" alt="anbn"/>
 547 </pre>
 548 <p>The set of all <tt><u>a</u></tt> or <tt><u>b</u></tt> labeled
 549   descendants
 550   is <dfn>{ <tt>[<u>&lt;a&gt;[]</u></tt><sup>n</sup> <tt><u>&lt;b&gt;[]</u></tt><sup>n</sup> <tt>]</tt>  | n ≥ 0 }</dfn>
 551 which is not a type.</p>
 552 <p> Intuitively it means that when applying a
 553   recursive pattern against a recursive type, we may generate an
 554   <s>infinite number of distinct types</s> for an accumulator.
 555 </p>
 556 </div>
 557 <div class="sws-slide">
 558   <h1>Typing of patterns (with accumulators) 2/2</h1>
 559   <p>We use the typing relation of operators to introduce
 560   approximations:</p>
 561   <pre>
 562     <u>t<sub>0</sub></u>, <tt>[</tt> (t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt> &rarrow;<sup>cons</sup> <tt>[</tt> (<u>t<sub>0</sub></u> &lor; t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt> <br/>
 563     <u>t<sub>0</sub></u>, <tt>[</tt> (t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt> &rarrow;<sup>snoc</sup> <tt>[</tt> (<u>t<sub>0</sub></u> &lor; t<sub>1</sub> &lor; … &lor; t<sub>n</sub>)<tt>* ]</tt>
 564   </pre>
 565   <p>Ensures termination of typechecking of patterns.</p>
 566 </div>
 567 <div class="sws-slide">
 568   <h1>Results</h1>
 569 <p>Zippers (in values, types, patterns) are a conservative extension</p>
 570 <ul>
 571   <li><u>Subtyping and typechecking</u> are extended straightforwardly</li>
 572   <li>Typing of patterns introduces <u>sound approximations</u> only for accumulators</li>
 573   <li>Provided the operators are sound, the whole language remains <u>type-safe</u></li>
 574 </ul>
 575 </div>
 576 <div class="sws-slide">
 577 <h1>Downward XPath axes</h1>
 578 <pre style="background:white">     <tt>self ::</tt> t ≡    (ẋ <tt>&amp;</tt> t | _ )<sub>&ztop;</sub>                                (Init(ẋ) = [], Op(ẋ) = <tt>snoc</tt>)
 579
 580      <span class="sws-pause"><tt>child ::</tt> t ≡  <tt>&lt;_&gt;[</tt> (ẋ <tt>&amp;</tt> t | _ )<tt>* ]</tt><sub>&ztop;</sub></span>
 581 </pre>
 582 <p class="sws-pause">Example: applying <tt><u>child::&lt;b&gt;_</u></tt>   to the document</p>
 583 <code>      &lt;doc&gt;[ &lt;a&gt;[]    &lt;b&gt;[]    &lt;c&gt;[]    &lt;b&gt;[] ]<sub>&bcirc;</sub>
 584         <span class="sws-pause">&lt;_&gt;[  <span class="sws-pause"> _</span>    <mark class="sws-pause">(ẋ &amp; &lt;b&gt;_)</mark>   <span>_</span>     <mark>(ẋ &amp; &lt;b&gt;_)</mark>]<sub >&ztop;</sub></span>
 585
 586         <span class="sws-pause"> ẋ&mapsto; [ &lt;b&gt;[]<sub>&left;… &right;… &right;… &bcirc;</sub>    &lt;b&gt;[]<sub>&left;… &right;… &right;… &right;… &right;… &bcirc;</sub>   ] </span>
 587 </code>
 588
 589 <pre class="sws-pause">
 590      <tt>descendant-or-self::</tt> t ≡   X ≡ ((ẋ <tt>&amp;</tt> t | _ ) <tt> &amp; </tt> (<tt>&lt;_&gt;[</tt> X <tt>* ]</tt>)<sub>&ztop;</sub> | _ )
 591
 592      <tt>descendant</tt> :: t ≡ <tt>&lt;_&gt;[ (descendant-or-self::</tt>t<tt>)* ]</tt><sub>&ztop;</sub>
 593 </pre>
 594 <!--
 595 <script type="text/javascript">
 596 /* <![CDATA[ */
 597   var svgDoc = null;
 598
 599   function reset () {
 600         svgDoc = svgDoc || document.getElementById("svgRBTree").contentDocument;
 601         var f = svgDoc.getElementById("nodef");
 602         f.style['fillOpacity'] = "0";
 603         var elems = svgDoc.getElementsByClassName("parentf");
 604         for(var i = 0; i < elems.length; i++) {
 605             elems[i].style['strokeWidth'] = '2px';
 606        };
 607   };
 608
 609   reg (0, function (c) {
 610          console.log(0);
 611          reset();
 612   });
 613
 614   reg (1, function (c) {
 615          console.log(1);
 616          var f = svgDoc.getElementById("nodef");
 617          console.log(' Opacity ' + f.style['fillOpacity']);
 618          f.style['fillOpacity'] = "0.5";
 619          console.log(' Opacity ' + f.style['fillOpacity']);
 620      });
 621
 622   reg (2, function (c) {
 623          console.log(2);
 624         var elems = svgDoc.getElementsByClassName("parentf");
 625         for(i = 0; i < elems.length; i++) {
 626              elems[i].style['strokeWidth'] = '6px';
 627           }
 628      });
 629    reg (3, function (c) {          console.log(3); reset(); });
 630 /*]]>*/
 631 </script>
 632 -->
 633 </div>
 634 <div class="sws-slide">
 635   <h1>Binary-tree encoding</h1>
 636   <p>We use  <u>regular expressions</u> over basic &left;/&right; zippers to encode upward XPath</p>
 637 <code style="width:50%;float:left;">   <![CDATA[<a>[ <b>[
 638           <c>[]
 639           <d>[]
 640           <e>[ <f> [] ]
 641         ]
 642    ]]]>
 643 </code><img style="width:17.5%;" src="ex_ntree.svg" alt="ex_ntree" /><br/>
 644 <p class="sws-pause"><img style="margin-top:-1em;margin-left:5%;width:85%;" src="rb_tree.svg" alt="rb_tree"/></p>
 645 </div>
 646
 647 <div class="sws-slide">
 648 <h1>Upward XPath axes</h1>
 649 <div style="position:absolute; width:80%; left:10%;top:15%">
 650 <object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%"  />
 651 <object class="sws-onframe-1" id="svgRBTree1" data="rb_tree01.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
 652 <object class="sws-onframe-2" id="svgRBTree2" data="rb_tree02.svg" type="image/svg+xml" style="z-index:3;position:absolute;width:100%"  />
 653 <object class="sws-onframe-3" id="svgRBTree3" data="rb_tree03.svg" type="image/svg+xml" style="z-index:4;position:absolute;width:100%"  />
 654 <object class="sws-onframe-4" id="svgRBTree4" data="rb_tree04.svg" type="image/svg+xml" style="z-index:5;position:absolute;width:100%"  />
 655 </div>
 656 <pre style="position:absolute;bottom:5%;z-index:1;">     <tt>parent ::</tt> t ≡   &top;<sub> (&left;_) · (&right;_)* · (&right; ẋ &amp; t) · (( (&left; _) · &ztop;)  &lor;  &bcirc; )</sub>
 657
 658 <span class="sws-onframe-5">     <tt>ancestor ::</tt> t ≡   &top;<sub> ( (&left;_) · (&right;_)* · (&right; ẋ &amp; t) )* · &bcirc; </sub></span>
 659
 660
 661
 662
 663 </pre>
 664 <pre style="position:absolute;bottom:5%;z-index:2;">
 665
 666                                   <span class="sws-onframe-1" style="font-size:110%;color:#1fb01b;">⬆</span> <span class="sws-onframe-2" style="font-size:110%;color:#1fb01b;">⬆</span>     <span class="sws-onframe-3" style="font-size:110%;color:#1fb01b;">⬆</span>     <span class="sws-onframe-4" style="font-size:110%;color:#1fb01b;">⬆</span>
 667
 668                                            <span class="sws-onframe-5" style="color:#1fb01b;border-color:#1fb01b;border-top-style:dashed;border-top-width:3pt;position:relative;top:0.5em;">         parent         </span>
 669
 670
 671
 672 </pre>
 673 </div>
 674 <div class="sws-slide">
 675   <h1>Other results</h1>
 676 <ul>
 677   <li>Encoding of paths is compositional</li>
 678   <li>Once we have paths, translation from XQuery to &cduce; is straightforward</li>
 679   <li>We also give a direct typing algorithm for XQuery 3.0 rather than typing the translation to &cduce;</li>
 680   <li>Accumulators in patterns allow to encode other XPath constructs (<tt>count()</tt>, <tt>position()</tt>, …)</li>
 681 </ul>
 682 <p>Still some problems in the on-going implementation</p>
 683 <ul>
 684   <li>Nice syntax to expose paths + patterns to the programmer</li>
 685   <li>Pretty printing of error messages: décompilation of regular expressions</li>
 686 </ul>
 687 </div>
 688 <div class="sws-slide">
 689 <h1>Conclusion, thoughts and future work</h1>
 690 <ul>
 691   <li style="padding-top:0.5em;">Adding path expressions to a functional language such as &cduce; is possible </li>
 692   <li style="padding-top:0.5em;">Semantic subtyping and regular expression types play nicely with zippers</li>
 693   <li style="padding-top:0.5em;">In terms of language design, exposing directly zippers to the programmer (still need work at the syntax level)</li>
 694   <li style="padding-top:0.5em;">Implementation on-going (including a &cduce; to javascript backend)</li>
 695   <li style="padding-top:0.5em;">Extend the approach to Json (google ``path language for json´´), i.e. generalize from products to extensible records</li>
 696 </ul>
 697 <p class="sws-pause" style="text-align:center;"><b><u>Thank you!</u></b></p>
 698 </div>
 699
 700   </body>
 701 </html>