helm/www/lambdadelta/web/home/implementation.ldw.xml

   1 <?xml version="1.0" encoding="UTF-8"?>
   2
   3 <page xmlns="http://lambdadelta.info/"
   4       description = "\lambda\delta home page"
   5       title = "\lambda\delta home page"
   6       head = "The Formal Systems of the λδ (\lambda\delta) Family"
   7 >
   8    <sitemap name="sitemap"/>
   9
  10    <section5 name="tools">Tools</section5>
  11
  12    <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
  13    <body>
  14       The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
  15       and contains resources expressed in the systems of the λδ family.
  16    </body>
  17    <topitem name="contents">
  18       <notice class="alpha" notice="Contents:"/>
  19       Landau's "Grundlagen der Analysis"
  20       (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
  21    </topitem>
  22    <topitem name="access">
  23       <notice class="alpha" notice="Access:"/>
  24       <rlink to="static/lddl/">static pages</rlink> (updated <notice class="gamma" notice="2015-01"/>),
  25       <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="gamma" notice="2014-12"/>),
  26       <rlink to="xml/">HELM server URL</rlink> (updated <notice class="gamma" notice="2014-12"/>).
  27    </topitem>
  28    <topitem name="examples">
  29       <notice class="alpha" notice="Examples:"/>
  30       <rlink to="static/lddl/Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
  31          Grundlagen's definition "t234"</rlink>
  32       in λδ version 4.
  33    </topitem>
  34
  35    <subsection name="helena"><helena-icon/>Helena</subsection>
  36
  37    <body>
  38       Helena is a processor for the systems of the λδ family,
  39       implemented in <link to="http://caml.inria.fr/">Caml</link>
  40       as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
  41       meant for testing both their stable and unstable features.
  42    </body>
  43    <body>
  44       The processor source code is available in the directory
  45       <link to="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</link>
  46       of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
  47       The Svn revisions containing the stable versions of Helena are indicated next.
  48    </body>
  49
  50    <topitem name="v3">
  51       <notice class="gamma" notice="Version 0.8.3 (2015-12)."/>
  52       Supports exportation to λProlog
  53       (two formats for ELPI,
  54       and two formats for <link to="http://teyjus.cs.umn.edu/">Teyjus</link>).
  55       Employs optimized conditional compilation through
  56       <link to="http://camlp5.gforge.inria.fr/">camlp5</link> code preprocessor (pa_macro)
  57       to reduce a performance loss, which is expected to disappear
  58       by employing a different code preprocessor.
  59       Overall validation speed of the "Grundlagen der Analysis" with respect to version 0.8.2:
  60       +3% with optimized compilation, +5% without optimized compilation.
  61       [Svn revision: 13108] (<rlink to="download/helena_0.8.3.tar.gz">archived source code</rlink>).
  62       <list><item>
  63          <notice class="gamma" notice="2015-06."/>
  64          The corrected specification of Landau's "Grundlagen der Analysis"
  65          is successfully validated in a λProlog implementation of λδ version 3.
  66       </item></list>
  67    </topitem>
  68
  69    <topitem name="v2">
  70       <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
  71       Uses λδ version 3 with layer variables as core language.
  72       Supports exportation to Gallina
  73       (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
  74       and to Grafite
  75       (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
  76       The overall validation speed of the "Grundlagen der Analysis"
  77       increases of 34% with respect to version 0.8.1.
  78       <rlink to="documentation.html#ldJ3a">Documentation (J3a)</rlink>.
  79       [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
  80       <list><item>
  81          The specification of Landau's "Grundlagen der Analysis"
  82          for <link to="http://coq.inria.fr/">Coq 8</link>:
  83          <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
  84          (revised <notice class="gamma" notice="2015-02"/>).
  85       </item><item>
  86          The specification of Landau's "Grundlagen der Analysis"
  87          for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
  88          <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
  89          (revised <notice class="gamma" notice="2015-02"/>).
  90       </item><item>
  91          The corrected specification of Landau's "Grundlagen der Analysis":
  92          <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
  93          (revised <notice class="gamma" notice="2014-12"/>).
  94       </item><item>
  95          <notice class="gamma" notice="2015-02."/>
  96          The translated specification of Landau's "Grundlagen der Analysis"
  97          is successfully validated in CC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
  98       </item><item>
  99          <notice class="gamma" notice="2014-12."/>
 100          The corrected specification of Landau's "Grundlagen der Analysis"
 101          is successfully validated in λδ version 3.
 102       </item></list>
 103    </topitem>
 104
 105    <topitem name="v1">
 106       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
 107       Uses a subset of λδ version 4 as intermediate language.
 108       Features importation from ".hln" files containing λδ textual syntax.
 109       The overall validation speed of the "Grundlagen der Analysis"
 110       increases of 22% with respect to version 0.8.0.
 111       [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>).
 112       <list><item>
 113          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
 114          for editing ".hln" files (containing λδ textual syntax):
 115          <rlink to="download/helena.sl">helena.sl</rlink>
 116          (revised <notice class="alpha" notice="2010-11"/>).
 117       </item><item>
 118          <notice class="beta" notice="2009-12."/>
 119          Helena appears in F. Wiedijk's
 120          <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
 121             index of computer math systems</link>.
 122       </item></list>
 123    </topitem>
 124
 125    <topitem name="v0">
 126       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
 127       Supports λδ version 2 with naive implementation of impredicative sort inclusion.
 128       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
 129       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
 130       <rlink to="documentation.html#ldR2a">Documentation (R2a)</rlink>.
 131       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
 132       <list><item>
 133          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
 134          for editing ".aut" files
 135          (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
 136          <rlink to="download/automath.sl">automath.sl</rlink>
 137          (revised <notice class="gamma" notice="2008-07"/>).
 138       </item><item>
 139          <notice class="beta" notice="2009-09."/>
 140          Jutting's specification of Landau's "Grundlagen der Analysis"
 141          enters λδ Digital Library.
 142       </item><item>
 143          <notice class="beta" notice="2009-06."/>
 144          Jutting's specification of Landau's "Grundlagen der Analysis"
 145          is successfully processed, enabling sort inclusion.
 146       </item></list>
 147    </topitem>
 148
 149    <subsection name="osn"><osn-icon/>Open Symbolic Notation</subsection>
 150    <body>
 151       Open Symbolic Notation (OSN) is an easy data-interchange textual format
 152       based on <link to="https://en.wikipedia.org/wiki/S-expression">symbolic expressions</link>.
 153       OSN is completely language independent but uses widely accepted conventions.
 154       These features make OSN ideal for storing and exchanging tree-like data structures
 155       in a lightweight manner.
 156    </body>
 157    <body>
 158       An OSN text uses the <link to="http://www.utf-8.com/">UTF-8</link> character set
 159       and contains the next tokens:
 160    </body>
 161    <list><item>
 162       <ebnf>
 163          <prod of="symbol"/> <def/>
 164             <prod of="symbol_char"/> <prod of="symbol_char"/> <star/>
 165          <stop/> <newline/>
 166          <prod of="symbol_char"/> <def/>
 167             <chr of="+"/> <or/> <chr of="-"/> <or/> <chr of="."/> <or/>
 168             <chr of="0"/> <or/> <etc/> <or/> <chr of="9"/> <or/>
 169             <chr of="A"/> <or/> <etc/> <or/> <chr of="Z"/> <or/>
 170             <chr of="_"/> <or/> <chr of="a"/> <or/> <etc/> <or/> <chr of="z"/>
 171          <stop/>
 172       </ebnf> <newline/>
 173       this token can represent the identifiers and the numerical constants of most programming languages;
 174    </item><item>
 175       <ebnf>
 176          <prod of="string"/> <def/>
 177             <chr of="&quot;"/> <open/>
 178             <prod of="string_char"/> <or/>
 179             <chr of="\"/> <prod of="escape"/>
 180             <close/> <star/> <chr of="&quot;"/>
 181          <stop/>
 182       </ebnf> <newline/>
 183       every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ <newline/>
 184       the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ <newline/>
 185       morover, the escape sequences \x &lt;two hexadecimal digits&gt; and \u &lt;four hexadecimal digits&gt;
 186       allow to specify a character by its code point <newline/>
 187       finally the escape sequences \( for U+0002 and \) for U+0003 are available
 188    </item><item>
 189       <ebnf>
 190          <prod of="qualifier"/> <def/> <chr of=":"/> <stop/>
 191       </ebnf>
 192    </item><item>
 193       <ebnf>
 194          <prod of="left"/> <def/>
 195             <chr of="("/> <or/> <chr of="&lt;"/> <or/> <chr of="["/> <or/> <chr of="{"/>
 196          <stop/>
 197       </ebnf> <newline/>
 198       this token starts a compound symbolic expression;
 199    </item><item>
 200       <ebnf>
 201          <prod of="right"/> <def/>
 202             <chr of=")"/> <or/> <chr of="&gt;"/> <or/> <chr of="]"/> <or/> <chr of="}"/>
 203          <stop/>
 204       </ebnf> <newline/>
 205       this token ends a compound symbolic expression;
 206    </item><item>
 207       &lt;ignored&gt; each of the characters U+0009..U+000D U+0020 , ; = <newline/>
 208       these characters are ignored and separate the other tokens
 209    </item><item>
 210       &lt;reserved&gt; any character not starting any other token <newline/>
 211       these characters are not allowed,
 212       and those in the range U+0021..U+007E are
 213       ! # $ % &amp; ' * / ? @ \ ^ ` | ~
 214    </item></list>
 215
 216    <footer/>
 217 </page>