<!ENTITY land "∧" >
<!ENTITY lor "∨" >
<!ENTITY setminus "∖" >
- <!ENTITY bottom "𝟘" >
- <!ENTITY top "𝟙" >
+ <!ENTITY bottom "<tt>Empty</tt>" > <!-- 𝟘 -->
+ <!ENTITY top "<tt>Any</tt>" > <!-- 𝟙 -->
<!ENTITY subseteq "⊆" >
<!ENTITY leq "≤" >
<!ENTITY Lrarrow "⟺">
</table>
</div>
<p style="font-size:80%;position:absolute;bottom:2.5em;left:4em;">
- CNRS, PPS, Université Paris-Diderot, Paris, France <br/>
- Kangwon National University, Chuncheon, Rep. of Korea<br/>
- LRI, Université Paris-Sud, Orsay, France
+ 1 CNRS, PPS, Université Paris-Diderot, Paris, France <br/>
+ 2 Kangwon National University, Chuncheon, Rep. of Korea<br/>
+ 3 LRI, Université Paris-Sud, Orsay, France
</p>
</div>
<div class="sws-slide">
- <h1>XQuery 3.0</h1>
- <p>W3C standard language for querying XML
- databases/documents</p>
-<code style="background:white">
- declare function <u>get_links</u>(<u>$page</u>, <u>$print</u>) {
+ <h1>The XQuery 3.0 W3C Standard</h1>
+<code style="background:white;font-size:90%;">
+ declare function <u>get_links</u>(<u>$page</u>, <u>$print</u>) {
<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>
<span class="for">return</span> <u>print</u>(<u>$i</u>)
}
<span class="ts">default return</span> <u>$link</u>
}
+
+ let $bold_links := get_links(document("file.html"), $pretty)
</code>
<script type="text/javascript">
reg ("0", col_change(".xpath, .for, .ts, .sw",""));
</div>
<div class="sws-slide">
<h1>&cduce;</h1>
- <p>A polymorphic functional language (ML-style) equipped with
+ <p>A polymorphic functional language equipped with
semantic subtyping</p>
-<code>
- let <u>pretty</u> (<a>_ -> <a>_ & Any\<a>_ &rarrow; Any\<a>_)
-
- | <a class="style1" href=<u>h</u> ..> <u>l</u> &rarrow; <a href=<u>h</u>>[ <b><u>l</u> ]
- | x &rarrow; x
+<code style="font-size:90%"> <i>(* Here _ is an alias for the top type Any *)</i>
+ let <u>pretty</u> (<a>Any <span class="typ">&rarrow;</span> <a>Any <span class="typ">&</span> Any<span class="typ">\</span><a>Any <span class="typ">&rarrow;</span> Any<span class="typ">\</span><a>Any)
- let <u>get_links</u> (page: <_>_) (print: <a>_ -> <a>_) : [ <a>_ * ] =
-
- match page with
- <a>_ & x &rarrow; [ (print x) ]
- | < (_\‘b) > l &rarrow;
- (transform l with (i & <_>_) &rarrow; get_links i print)
- | _ -> [ ]
-
+ | <span class="pat"><a class="style1" href=<u>h</u> ..> <u>l</u></span> &rarrow; <a href=<u>h</u>>[ <b><u>l</u> ]
+ | <span class="pat">x</span> &rarrow; x
+ let <u>get_links</u> (page: <(Any)>Any) (print: <a>Any <span class="typ">&rarrow;</span> <a>Any) : <span class="typ">[ <a>Any * ]</span> =
+ match page with
+ <span class="pat"><a>_ & x</span> &rarrow; [ (print x) ]
+ | <span class="pat">< (_\‘b) > l</span> &rarrow;
+ (<span class="lc">transform l with</span> <span class="pat">(i & <_>_)</span> &rarrow; get_links i print)
+ | <span class="pat">_</span> &rarrow; [ ]
</code>
-
+ <script type="text/javascript">
+ reg ("0", col_change(".pat,.typ,.lc",""));
+ reg ("1", col_change(".pat", "#f80"));
+ reg ("2", col_change(".typ", "#290"));
+ reg ("3", col_change(".lc", "#80f"));
+ </script>
</div>
<div class="sws-slide">
+ compact (and efficient) type and value pattern-matching
</li>
<li>Cons<br/>
- - <s>complex navigation encoded through recursion</s>
+ - <s>complex navigation encoded through recursion</s><br/>
- no type inference for functions
</li>
</ul>
<ol style="margin-left:1em; margin-right:0.25em;list-style-position:inside;">
<li id="tobox" style="padding:1em 0em 1em 0em;"><span class="lh">Add support for path navigation to
&cduce;</span>
- <ul id="toshow" style="margin-top:2em;display:none;">
+ <ul style="margin-top:2em;">
<li>Enrich the type algebra with <em>zippers</em> (à la Huet)</li>
<li>Extend pattern-matching construct to <em>zipped values and types</em></li>
<li>Encode path expressions as recursive patterns</li>
</ul>
</li>
- <li style="padding:1em 0em 1em 0em;">Perform a type-directed translation from XQuery to
+ <li class="ll" style="padding:1em 0em 1em 0em;">Perform a type-directed translation from XQuery to
&cduce;</li>
-
</ol>
<script type="text/javascript">
- reg ("0", col_change(".lh",""));
- reg ("1", col_change(".lh", "#f80"));
-
- reg ("2", function (canvas) { $("#toshow").show(); });
- reg ("3", function (c) { $("#tobox").css (
- { 'background' : '#dfd', 'border-radius': '1em' });});
+ reg (1, col_change(".lh", "#f83"));
+ reg (1, col_change(".ll", "#bbb"));
</script>
</div>
<div class="sws-slide">
<h1>&cduce;'s type algebra</h1>
-<pre>
- t ::= b | c | t × t | t &rarrow; t | t &lor; t | t &land; t | t ∖ t | ⊤ | ⊥ | α
+<p>A set &mathT; of types</p>
+<pre style="text-align:center;"> t ::= b | c | <u>t × t</u> | <u>t &rarrow; t</u> | <a>t &lor; t</a> | <mark>t &land; t</mark> | <mark>t ∖ t</mark> | <mark>⊤</mark> | <mark>⊥</mark> | α
</pre>
<p><dfn>b</dfn> : ranges over basic types (<tt>Int</tt>, <tt>String</tt>, …)<br/>
<dfn>c</dfn> : ranges over singleton types
(<tt>`A</tt>, <tt>42</tt>, …)<br/>
+ <u>Type constructors</u> <br/>
+ <mark>Boolean connectives</mark> <br/>
<dfn>α</dfn> : type variables<br/>
- types are interpreted co-inductively (recursive types) and regular
+ types are interpreted co-inductively: recursive types and regular
expression types<br/>
</p>
-<pre>
- t<sub>1</sub> ≡ (<tt>Int</tt> × t<sub>1</sub>) &lor; t<sub>2</sub>
- t<sub>2</sub> ≡ (<tt>Bool</tt> × t<sub>2</sub>) &lor; (<tt>Bool</tt> × <tt>`nil</tt>)
-
- <span class="sws-pause">t<sub>1</sub> ≡ <tt>[ Int* Bool+ ]</tt></span>
-
+<div style="vertical-align:top;">
+<pre style="width:50%;display:inline-block;"> t<sub>1</sub> ≡ (<tt>Int</tt> × t<sub>1</sub>) &lor; t<sub>2</sub>
+ t<sub>2</sub> ≡ (<tt>Bool</tt> × t<sub>2</sub>) &lor; (<tt>Bool</tt> × <tt>`nil</tt>)
</pre>
+<pre style="width:30%;display:inline-block;"> <span class="sws-pause">t<sub>1</sub> ≡ <tt>[ Int* Bool+ ]</tt></span></pre>
+</div>
</div>
<div class="sws-slide">
<h1>Semantic subtyping</h1>
<tt>[ Int* (Int | Bool*)? ]</tt> &land; <tt>[ Int+ (Bool+ | Int)* ]</tt> ≡ <tt>[Int+ Bool*]</tt>
</pre>
</div>
+<div class="sws-slide">
+<h1>&cduce; data-model</h1>
+<p>The usual sets &mathV; of values:</p>
+<pre style="text-align:center"> v ::= <tt>1</tt> | … | <tt>`Foo</tt> | (v, v) | λx.e
+</pre>
+<p>Sequences are nested pairs (<i>à la</i> Lisp):</p>
+<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>)))
+</pre>
+<p>XML documents are tagged sequences: <pre style="text-align:center;"><tt><foo>[</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>
+</p>
+<p>(Sometimes we write <tt>[ ]</tt> for the variant <tt>`nil</tt>)</p>
+<p>Everything is built on top of products and variants</p>
+</div>
<div class="sws-slide">
<h1>&cduce; patterns</h1>
-<pre style="text-align:center;"> p ::= t | p | p | p & p | (p, p) | x </pre>
+<p><i>(a.k.a. the left-hand side of an arrow in a match … with)</i></p>
+<pre style="text-align:center;"> p ::= t | x | <u>(p, p)</u> | <mark>p | p</mark> | <mark>p & p</mark> </pre>
<p><dfn>t</dfn> ranges over types<br/>
<dfn>x</dfn> ranges over capture variables<br/>
+ <u>Pair patterns</u><br/>
+ <mark> Alternation |, Intersection &</mark><br/>
patterns are also co-inductively interpreted (recursive patterns)
</p>
<p><dfn><u>v / p</u></dfn> : matching a value against a pattern yields a
| [ ] &rarrow; (0, `false)
</code>
<ol>
-<li><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) Bool* (<u>y</u> & Bool) ]</tt>&rbag; ≡ <tt>[ ⊤* Int Bool+ ]</tt></dfn><br/>
- yield : { x ↦ <tt>Int</tt>, y ↦ <tt>Bool</tt> }
+<li><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) Bool* (<u>y</u> & Bool) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ ⊤* Int Bool+ ]</tt></dfn><br/>
+ <span style="text-align:right;display:inline-block;width:94%;">{ x ↦ <tt>Int</tt>, y ↦ <tt>Bool</tt> }</span>
</li>
-<li><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) ]</tt>&rbag; ≡ <tt>[ ⊤* Int ]</tt></dfn><br/>
- yield : { x ↦ <tt>Int</tt> }
+<li><dfn>&lbag;<tt>[ _* (<u>x</u> & Int) ]</tt>&rbag; <span style="display:inline-block;width:5em;text-align:center"> ≡</span> <tt>[ ⊤* Int ]</tt></dfn><br/>
+ <span style="text-align:right;display:inline-block;width:58%;"> { x ↦ <tt>Int</tt> }</span>
</li>
-<li>Since <dfn><tt>[Int+ Bool* ]</tt> ∖ ( <tt>[ ⊤* Int Bool+ ]</tt> &lor; <tt>[ ⊤* Int]</tt>) ≡ ⊥ </dfn>
+<li>Since <dfn><tt>[Int+ Bool* ]</tt> ∖ ( <tt>[ ⊤* Int Bool+ ]</tt> &lor; <tt>[ ⊤* Int]</tt>) ≡ ⊥ </dfn><br/>
the third case is unreachable.
</li>
</ol>
</div>
-<div class="sws-slide">
-<h1>&cduce; data-model</h1>
-<p>Sequences are nested pairs: <dfn><tt>[</tt> v<sub>1</sub> … v<sub>n</sub> <tt>]</tt> ≡ (v<sub>1</sub>, (…, (v<sub>n</sub>, <tt>`nil</tt>)))
-</dfn></p>
-<p>XML documents are tagged sequences: <pre style="text-align:center;"><tt><foo>[</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>
-</p>
-<p>Ususal lisp-like encoding of trees, how to perform navigation
- (including upward ?)</p>
-</div>
+
<div class="sws-slide">
<h1>Zippers (1/2)</h1>
<ul>
<li>Introduced in 1997 by Gérard Huet</li>
- <li>Stack of visited</li>
- <li>Push the current node on the stack when descending</li>
- <li>Put the top of the stack and pop it to go backward</li>
- <li>Tag the elements of the stack to remember which of a node we
- have visited</li>
+ <li>Stack of visited nodes</li>
+ <li>Push the current node on the stack when traversing a pair</li>
+ <li>Take the top of the stack to go backward</li>
+ <li>Tag the elements of the stack to remember which component of a
+ pair we have visited</li>
</ul>
<pre style="text-align:center;"> v ::= … | v<sub>δ</sub>
δ ::= &bcirc; | &left;v · δ | &right;v · δ
<p><tt><u>fst</u></tt> (resp. <tt><u>snd</u></tt>) takes the first (resp. second)
projection of a pair and update its zipper accordingly:</p>
<pre> v<sub>1</sub> ≡ (1, (2, (3, (4, `nil))))<sub>&bcirc;</sub>
- v<sub>11</sub> ≡ fst v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
- v<sub>2</sub> ≡ snd v<sub>1</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
- v<sub>3</sub> ≡ snd v<sub>2</sub> ≡ (3, (4, `nil))<sub>&right;v<sub>2</sub> · &right;v<sub>1</sub> · &bcirc; </sub>
+ v<sub>11</sub> ≡ <tt>fst</tt> v<sub>1</sub> ≡ 1<sub>&left;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
+ 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>
+ 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>
</pre>
-<p><tt><u>up</u></tt> pops returns the head of the zipper: </p>
-<pre> up v<sub>3</sub> ≡ v<sub>2</sub> ≡ (2, (3, (4, `nil)))<sub>&right;(1, (2, (3, (4, `nil))))<sub>&bcirc;</sub> · &bcirc; </sub>
+<p><tt><u>up</u></tt> returns the head of the zipper: </p>
+<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>
</pre>
</div>
<div class="sws-slide">
<pre style="text-align:center;"> t ::= … | t<sub>τ</sub>
τ ::= &bcirc; | &left;t · τ | &right;t · τ | τ &lor; τ | τ ∖ τ | &ztop;
</pre>
-<p><dfn>&bcirc;</dfn>: singleton type denoting the empty zipper<br/>
- <dfn>&ztop;</dfn>: the top zipper types<br/>
- Zipper types are interpreted co-inductively (regular expressions on
- zippers)<br/><br/>
- <dfn><tt>Int</tt><sub>(&left;⊤)* &bcirc;</sub></dfn>: type of
- integers that are the leftmost descendant of a tree.<br/>
- <dfn><tt><![CDATA[<html>[ <head>[…] <body>[…] ]]]></tt><sub>&bcirc;</sub></dfn>: type of
- HTML documents<br/>
- <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub>&ztop;</sub></dfn>: types of links in any context
-
+<p><dfn>&bcirc;</dfn>: singleton type denoting the empty zipper (root element)<br/>
+ <dfn>&ztop;</dfn>: the top zipper type<br/>
+ Zipper types are interpreted co-inductively<br/><br/>
+ <dfn><tt>Int</tt><sub>(&left;⊤)* &bcirc;</sub></dfn> <span style="float:right;">type of
+ integers that are the leftmost descendant of a tree</span><br/><br/>
+ <dfn><tt><![CDATA[<html>[ <head>[…] <body>[…] ]]]></tt><sub>&bcirc;</sub></dfn> <span style="float:right;">type of
+ HTML documents</span><br/><br/>
+ <dfn><tt><![CDATA[<a href=String>[ … ]]]></tt><sub> &ztop;</sub></dfn> <span style="float:right;">types of links nested in any context</span>
</p>
</div>
<div class="sws-slide">
<h1>Tree navigation</h1>
<p>Since patterns contain types, we can check complex
conditions:</p>
-<pre style="width:60%;display:inline-block;border-width:0pt 1pt 0pt 0pt; border-style:dashed;border-color: black;vertical-align:middle">
- p ≡ <tt id="test"><a>_</tt> &lor; <tt><_>[ _* p _* ]</tt>
+<pre style="width:62%;display:inline-block;border-width:0pt 1pt 0pt
+ 0pt; border-style:dashed;border-color: black;vertical-align:middle"> <span style="font-family:'Open Sans';">Has a descendant <tt><a>_</tt>:</span>
+ p ≡ <tt id="test"><a>_</tt> &lor; <tt><_>[ _* <dfn>p</dfn> _* ]</tt>
- τ ≡ &bcirc; &lor; &right;⊤ · τ &lor; &left;(⊤∖ <tt><b>_</tt>) · τ
-
-</pre>
+ <span style="font-family:'Open Sans';">Deos not have an ancestor <tt><b>_</tt>:</span>
+ τ ≡ &bcirc; &lor; &right;(⊤∖ <tt><b>_</tt>) · τ &lor; &left;(⊤∖ <tt><b>_</tt>) · τ </pre>
<code style="width:20%;display:inline-block;vertical-align:middle">
match <u>v</u> with
<dfn>p<sub>τ</sub></dfn> & <u>x</u> &rarrow; …
- | _ &rarrow; …
-</code>
-<p style="background:white">
-We want more, namely return <i>all</i> descendants (ancestor,
+ | _ &rarrow; …</code>
+<p style="background:white">We want more, namely return <i>all</i> descendants (ancestors,
children, siblings, …) of a node matching a particular condition
<br/><br/>
Remark: (recursive) patterns <u>already perform a recursive traversal
of the value</u>
-<br/><br/>
+<br/>
<em>Idea</em>: Piggy back on the traversal and <em>accumulate</em>
nodes in special variables
</p>
-<script type="text/javascript">
- reg (0, col_change ("#test", ""));
- reg (1, col_change ("#test", "orange"));
-</script>
</div>
<div class="sws-slide">
<h1>Operators and Accumulators</h1>
<u>accumulates</u> that node in sequence (in reverse or in-order).</p>
</div>
<div class="sws-slide">
-<h1>Pattern matching semantics (v/p)</h1>
+<h1>Pattern matching semantics (simplified)</h1>
<pre style="text-align:center;">
- σ; δ ⊢ v / p &rleadsto; γ, σ'
+ σ ⊢ v / p &rleadsto; γ, σ'
</pre>
<p style="font-size:90%"><dfn><u>σ</u>, <u>σ'</u></dfn>: mapping from accumulators to
values<br/>
<dfn><u>p</u></dfn>: pattern<br/>
<dfn><u>γ</u></dfn>: mapping from capture variables to
values<br/>
- <dfn><u>δ</u></dfn>: current context
</p>
-<div style="padding:0em 1em 0em; text-align:justify;font-size:85%;background:white;">
+<div style="padding:0em 1em 0em; text-align:justify;background:white;">
<div class="infer">
<span> v ∈ [ t ]</span>
<span>σ; δ ⊢ v / t &rleadsto; ∅,
<div class="infer">
<span></span>
- <span>σ; δ ⊢ v / ẋ &rleadsto; ∅,
- σ[ ẋ := Op(ẋ) (v<sub>δ</sub>, σ(ẋ)) ]</span>
+ <span>σ ⊢ v / ẋ &rleadsto; ∅,
+ σ[ ẋ := Op(ẋ) (v, σ(ẋ)) ]</span>
</div><span>(acc)</span>
<div class="infer">
<span></span>
- <span>σ; δ ⊢ v / x &rleadsto; { x ↦ v },
+ <span>σ ⊢ v / x &rleadsto; { x ↦ v },
σ</span>
</div><span>(var)</span>
<div class="infer">
- <span>σ; &left;v · δ ⊢ (fst v)/p<sub>1</sub>
+ <span>σ ⊢ (fst v)/p<sub>1</sub>
&rleadsto; γ<sub>1</sub>, σ' </span>
- <span>σ'; &right;v · δ ⊢ (snd v)/p<sub>2</sub>
+ <span>σ' ⊢ (snd v)/p<sub>2</sub>
&rleadsto; γ<sub>2</sub>, σ''
</span>
- <span>σ; δ ⊢ v /
+ <span>σ ⊢ v /
(p<sub>1</sub>, p<sub>2</sub>) &rleadsto;
γ<sub>1</sub>∪ γ<sub>2</sub>,
σ''</span>
</div><span>(pair)</span> <span class="fill"></span>
-<span>… and some other rules for alternation, failure, recursion, <i>etc.</i></span>
+<span style="position:relative;top:-1em;">Remember, if <dfn>v ≡ (v1,v2)<sub>δ</sub></dfn> then <dfn><tt>fst v</tt> ≡ v<sub>1 &left;v · δ</sub></dfn> and <dfn><tt>snd v</tt> ≡ v<sub>2 &right;v · δ</sub></dfn><br/>
+(some other rules for alternation, failure, recursion, <i>etc.</i>)</span>
</div>
</div>
<div class="sws-slide">
</div>
<div class="sws-slide">
<h1>Results</h1>
-<p>Zippers (in values, types, patterns) are orthogonal to the rest of the language</p>
+<p>Zippers (in values, types, patterns) are a conservative extension</p>
<ul>
<li><u>Subtyping and typechecking</u> are extended straightforwardly</li>
<li>Typing of patterns introduces <u>sound approximations</u> only for accumulators</li>
</ul>
</div>
<div class="sws-slide">
- <h1>From zippers to XPath</h1>
- <p>We use <u>regular expressions</u> over basic &left;/&right; zippers to encode XPath</p>
-<code style="width:50%;float:left;"> <![CDATA[<a>[ <b>[
- <c>[]
- <d>[]
- <e>[ <f> [] ]
- ]
- ]]]>
-</code><img style="width:17.5%;" src="ex_ntree.svg" alt="ex_ntree" /><br/>
-<p class="sws-pause"><img style="margin-top:-1em;margin-left:5%;width:85%;" src="rb_tree.svg" alt="rb_tree"/></p>
-</div>
-<div class="sws-slide">
-<h1>Downward axes</h1>
-<tt> <![CDATA[<a>[ <b>[ <c>[] <d>[] <e>[ <f> [] ] ] ]]]><sub>&bcirc;</sub></tt>
-<object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="margin-left:7.5%;width:85%" />
-<pre>
- <tt>self ::</tt> t ≡ (ẋ <tt>&</tt> t | _ )<sub>&ztop;</sub>
- <tt>child ::</tt> t ≡ <tt><_>[</tt> (ẋ <tt>&</tt> t | _ )<tt>* ]</tt><sub>&ztop;</sub>
- <tt>descendant-or-self::</tt> t ≡ X ≡ ((ẋ <tt>&</tt> t | _ ) <tt> & <_>[</tt> X <tt>* ]</tt>)<sub>&ztop;</sub>
+<h1>Downward XPath axes</h1>
+<pre style="background:white"> <tt>self ::</tt> t ≡ (ẋ <tt>&</tt> t | _ )<sub>&ztop;</sub> (Init(ẋ) = [], Op(ẋ) = <tt>snoc</tt>)
+
+ <span class="sws-pause"><tt>child ::</tt> t ≡ <tt><_>[</tt> (ẋ <tt>&</tt> t | _ )<tt>* ]</tt><sub>&ztop;</sub></span>
+</pre>
+<p class="sws-pause">Example: applying <tt><u>child::<b>_</u></tt> to the document</p>
+<code> <doc>[ <a>[] <b>[] <c>[] <b>[] ]<sub>&bcirc;</sub>
+ <span class="sws-pause"><_>[ <span class="sws-pause"> _</span> <mark class="sws-pause">(ẋ & <b>_)</mark> <span>_</span> <mark>(ẋ & <b>_)</mark>]<sub >&ztop;</sub></span>
+
+ <span class="sws-pause"> ẋ↦ [ <b>[]<sub>&left;… &right;… &right;… &bcirc;</sub> <b>[]<sub>&left;… &right;… &right;… &right;… &right;… &bcirc;</sub> ] </span>
+</code>
+
+<pre class="sws-pause">
+ <tt>descendant-or-self::</tt> t ≡ X ≡ ((ẋ <tt>&</tt> t | _ ) <tt> & </tt> (<tt><_>[</tt> X <tt>* ]</tt>)<sub>&ztop;</sub> | _ )
+
<tt>descendant</tt> :: t ≡ <tt><_>[ (descendant-or-self::</tt>t<tt>)* ]</tt><sub>&ztop;</sub>
</pre>
<!--
-->
</div>
<div class="sws-slide">
-<h1>Upward axes</h1>
-<tt> <![CDATA[<a>[ <b>[ <c>[] <d>[] <e>[ <f> [] ] ] ]]]><sub>&bcirc;</sub></tt>
-<object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="margin-left:7.5%;width:85%" />
-<pre>
- <tt>parent ::</tt> t ≡ ⊤<sub> (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;) &lor; &bcirc; )</sub>
- <tt>ancestor ::</tt> t ≡ ⊤<sub> ((&left;_) · (&right;_)* · (&right; ẋ & t))* · &bcirc; </sub>
+ <h1>Binary-tree encoding</h1>
+ <p>We use <u>regular expressions</u> over basic &left;/&right; zippers to encode upward XPath</p>
+<code style="width:50%;float:left;"> <![CDATA[<a>[ <b>[
+ <c>[]
+ <d>[]
+ <e>[ <f> [] ]
+ ]
+ ]]]>
+</code><img style="width:17.5%;" src="ex_ntree.svg" alt="ex_ntree" /><br/>
+<p class="sws-pause"><img style="margin-top:-1em;margin-left:5%;width:85%;" src="rb_tree.svg" alt="rb_tree"/></p>
+</div>
+
+<div class="sws-slide">
+<h1>Upward XPath axes</h1>
+<div style="position:absolute; width:80%; left:10%;top:15%">
+<object id="svgRBTree" data="rb_tree.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
+<object class="sws-onframe-1" id="svgRBTree1" data="rb_tree01.svg" type="image/svg+xml" style="z-index:1;position:absolute;width:100%" />
+<object class="sws-onframe-2" id="svgRBTree2" data="rb_tree02.svg" type="image/svg+xml" style="z-index:3;position:absolute;width:100%" />
+<object class="sws-onframe-3" id="svgRBTree3" data="rb_tree03.svg" type="image/svg+xml" style="z-index:4;position:absolute;width:100%" />
+<object class="sws-onframe-4" id="svgRBTree4" data="rb_tree04.svg" type="image/svg+xml" style="z-index:5;position:absolute;width:100%" />
+</div>
+<pre style="position:absolute;bottom:5%;z-index:1;"> <tt>parent ::</tt> t ≡ ⊤<sub> (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;) &lor; &bcirc; )</sub>
+
+<span class="sws-onframe-5"> <tt>ancestor ::</tt> t ≡ ⊤<sub> ( (&left;_) · (&right;_)* · (&right; ẋ & t) )* · &bcirc; </sub></span>
+
+
+
+
+</pre>
+<pre style="position:absolute;bottom:5%;z-index:2;">
+
+ <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>
+
+ <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>
+
+
+
</pre>
</div>
<div class="sws-slide">
<h1>Other results</h1>
<ul>
<li>Encoding of paths is compositional</li>
- <li>Once we have path, translation from XQuery to &cduce; is straightforward</li>
+ <li>Once we have paths, translation from XQuery to &cduce; is straightforward</li>
<li>We also give a direct typing algorithm for XQuery 3.0 rather than typing the translation to &cduce;</li>
</ul>
</div>
<ul>
<li>Adding path expressions to a functional language such as &cduce; is possible </li>
<li>Semantic subtyping and regular expression types play nicely with zippers</li>
- <li>In terms of language design, exposing directly zippers patterns to the programmer is a big no-no</li>
- <li>Can also be applied to XSLT</li>
+ <li>In terms of language design, exposing directly zippers to the programmer (still need work at the syntax level)</li>
<li>Implementation on-going (including a &cduce; to javascript backend)</li>
- <li>Extend the approach to Json (google ``path language for json''), i.e. generalise from products to extensible records</li>
+ <li>Extend the approach to Json (google ``path language for json´´), i.e. generalise from products to extensible records</li>
</ul>
-
+<p class="sws-pause" style="text-align:center;"><b><u>Thank you!</u></b></p>
</div>
</body>
projects / hacks / simpleWebSlides.git / blobdiff