helm/www/lambdadelta/basic_1.html

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
   3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
   4   <head>
   5     <meta http-equiv="Content-Language" content="en-us" />
   6     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
   7     <meta http-equiv="Content-Style-Type" content="text/css" />
   8     <meta name="author" content="Ferruccio Guidi" />
   9     <meta name="description" content="\lambda\delta home page" />
  10     <title>\lambda\delta home page</title>
  11     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
  12     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
  13     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
  14     <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
  15   </head>
  16   <body lang="en-US">
  17     <div class="spacer">
  18       <a href="http://lambdadelta.info/">
  19         <img class="icon32" alt="[\lambda\delta home]" title="\lambda\delta home" src="http://lambdadelta.info/images/crux_32.png" />
  20       </a>
  21     </div>
  22     <div class="head1">cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)</div>
  23     <div class="spacer">
  24       <img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
  25     </div>
  26     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
  27       <br />
  28     </div>
  29     <div xmlns:ld="http://lambdadelta.info/" class="text">
  30       <table cellpadding="4" cellspacing="0">
  31         <tbody>
  32           <tr>
  33             <td class="snns capitalize italic sky">
  34               <a href="http://lambdadelta.info/home.html">home</a>
  35             </td>
  36             <td class="snns capitalize italic magenta">
  37               <a href="http://lambdadelta.info/news.html">news</a>
  38             </td>
  39             <td class="snns capitalize italic white">
  40               <a href="http://lambdadelta.info/specification.html">specification</a>
  41             </td>
  42             <td class="snnn capitalize italic white">
  43               <br />
  44             </td>
  45             <td class="snnn capitalize italic white">
  46               <br />
  47             </td>
  48             <td class="snns capitalize italic orange">
  49               <a href="http://lambdadelta.info/documentation.html">documentation</a>
  50             </td>
  51             <td class="snns capitalize italic green">
  52               <a href="http://lambdadelta.info/implementation.html">implementation</a>
  53             </td>
  54             <td class="ssnn capitalize italic green">
  55               <br />
  56             </td>
  57           </tr>
  58           <tr>
  59             <td class="snns capitalize sky">
  60               <a href="http://lambdadelta.info/home.html#foreword">foreword</a>
  61             </td>
  62             <td class="snns capitalize magenta">
  63               <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
  64             </td>
  65             <td class="snns capitalize white">
  66               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
  67             </td>
  68             <td class="snnn capitalize white">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
  69             <td class="snnn capitalize white">
  70               <br />
  71             </td>
  72             <td class="snns capitalize orange">
  73               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
  74             </td>
  75             <td class="snns capitalize green">
  76               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
  77             </td>
  78             <td class="ssnn capitalize green">
  79               <a href="http://lambdadelta.info/osn/">Open Symbolic Notation (OSN)</a>
  80             </td>
  81           </tr>
  82           <tr>
  83             <td class="snss capitalize sky">
  84               <a href="http://lambdadelta.info/home.html#citations">citations</a>
  85             </td>
  86             <td class="snss capitalize magenta">
  87               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
  88             </td>
  89             <td class="snss capitalize white">
  90               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
  91             </td>
  92             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
  93             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
  94             <td class="snss capitalize orange">
  95               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
  96             </td>
  97             <td class="snss capitalize green">
  98               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
  99             </td>
 100             <td class="sssn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
 101           </tr>
 102         </tbody>
 103       </table>
 104     </div>
 105     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="blocks">Abstract Syntax and Behavior <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b6.png" />
 106     </div>
 107     <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of available syntactic items and reductions (block structure).
 108    </div>
 109     <div xmlns:ld="http://lambdadelta.info/" class="text">
 110       <table cellpadding="4" cellspacing="0">
 111         <tbody>
 112           <tr>
 113             <td class="snns top gray">domain</td>
 114             <td class="snns top italic gray">block</td>
 115             <td class="snns top gray">leader</td>
 116             <td class="snns top gray">→ζ *</td>
 117             <td class="snns top gray">annotator (with →ϵ *)</td>
 118             <td class="snns top gray">applicator (with →θ *)</td>
 119             <td class="snns top gray">reference *</td>
 120             <td class="ssns top gray">reduction</td>
 121           </tr>
 122           <tr>
 123             <td class="snns top">{X | Γ ⊢ ⊤}</td>
 124             <td class="snns top italic wine">exclusion</td>
 125             <td class="snns top wine">Γ ⊢ χ</td>
 126             <td class="snns top wine">yes</td>
 127             <td class="snns top wine">no</td>
 128             <td class="snns top wine">no</td>
 129             <td class="snns top wine">no</td>
 130             <td class="ssns top wine">no</td>
 131           </tr>
 132           <tr>
 133             <td class="snns top">{X | Γ ⊢ X : W}</td>
 134             <td class="snns top italic magenta">typed abstraction</td>
 135             <td class="snns top magenta">Γ ⊢ λW</td>
 136             <td class="snns top magenta">no</td>
 137             <td class="snns top magenta">&lt;W&gt;</td>
 138             <td class="snns top magenta">(V)</td>
 139             <td class="snns top magenta">#i</td>
 140             <td class="ssns top magenta">→β *</td>
 141           </tr>
 142           <tr>
 143             <td class="snns top">{X | Γ ⊢ X = V}</td>
 144             <td class="snns top italic prune">abbreviation</td>
 145             <td class="snns top prune">Γ ⊢ δV</td>
 146             <td class="snns top prune">yes</td>
 147             <td class="snns top prune">no</td>
 148             <td class="snns top prune">no</td>
 149             <td class="snns top prune">#i</td>
 150             <td class="ssns top prune">→δ</td>
 151           </tr>
 152           <tr>
 153             <td class="snss top">no</td>
 154             <td class="snss top italic blue">sort</td>
 155             <td class="snss top blue">Γ ⊢ ⋆k</td>
 156             <td class="snss top blue">no</td>
 157             <td class="snss top blue">no</td>
 158             <td class="snss top blue">no</td>
 159             <td class="snss top blue">no</td>
 160             <td class="ssss top blue">no</td>
 161           </tr>
 162         </tbody>
 163       </table>
 164     </div>
 165     <div xmlns:ld="http://lambdadelta.info/" class="text">* In terms only.
 166    </div>
 167     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b6.png" />
 168     </div>
 169     <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
 170          and its timeline.
 171    </div>
 172     <div xmlns:ld="http://lambdadelta.info/" class="text">
 173       <table cellpadding="4" cellspacing="0">
 174         <tbody>
 175           <tr>
 176             <td class="snns capitalize italic gray">category</td>
 177             <td class="snns italic gray">objects</td>
 178             <td class="snnn right italic gray">
 179               <br />
 180             </td>
 181             <td class="snnn italic gray">
 182               <br />
 183             </td>
 184             <td class="snnn right italic gray">
 185               <br />
 186             </td>
 187             <td class="snnn italic gray">
 188               <br />
 189             </td>
 190             <td class="ssnn right italic gray">
 191               <br />
 192             </td>
 193           </tr>
 194           <tr>
 195             <td class="snns capitalize italic water">sizes</td>
 196             <td class="snns italic water">files</td>
 197             <td class="snnn right italic water">120</td>
 198             <td class="snns italic water">characters</td>
 199             <td class="snnn right italic water">198089</td>
 200             <td class="snns italic water">nodes</td>
 201             <td class="ssnn right italic water">1449099</td>
 202           </tr>
 203           <tr>
 204             <td class="snns capitalize italic green">propositions</td>
 205             <td class="snns italic green">theorems</td>
 206             <td class="snnn right italic green">81</td>
 207             <td class="snns italic green">lemmas</td>
 208             <td class="snnn right italic green">618</td>
 209             <td class="snns italic green">total</td>
 210             <td class="ssnn right italic green">699</td>
 211           </tr>
 212           <tr>
 213             <td class="snss capitalize italic grass">concepts</td>
 214             <td class="snss italic grass">declared</td>
 215             <td class="snsn right italic grass">39</td>
 216             <td class="snss italic grass">defined</td>
 217             <td class="snsn right italic grass">47</td>
 218             <td class="snss italic grass">total</td>
 219             <td class="sssn right italic grass">86</td>
 220           </tr>
 221         </tbody>
 222       </table>
 223     </div>
 224     <ul xmlns:ld="http://lambdadelta.info/">
 225       <li>
 226         <span class="emph delta">January 2015.</span>
 227       Update with backports from the abandoned specification of λδ version 2.
 228    </li>
 229     </ul>
 230     <ul xmlns:ld="http://lambdadelta.info/">
 231       <li>
 232         <span class="emph delta">May 2008.</span>
 233       Specification is concluded.
 234    </li>
 235     </ul>
 236     <ul xmlns:ld="http://lambdadelta.info/">
 237       <li>
 238         <span class="emph gamma">November 2006.</span>
 239       Decidability of native type assignment, λδ version 1 is released.
 240    </li>
 241     </ul>
 242     <ul xmlns:ld="http://lambdadelta.info/">
 243       <li>
 244         <span class="emph beta">December 2005.</span>
 245       Preservation of native type by reduction, λδ version 1 is announced.
 246    </li>
 247     </ul>
 248     <ul xmlns:ld="http://lambdadelta.info/">
 249       <li>
 250         <span class="emph alpha">May 2004.</span>
 251       Specification starts.
 252    </li>
 253     </ul>
 254     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b6.png" />
 255     </div>
 256     <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
 257    </div>
 258     <div xmlns:ld="http://lambdadelta.info/" class="text">
 259       <table cellpadding="4" cellspacing="0">
 260         <tbody>
 261           <tr>
 262             <td class="snns top capitalize italic gray">component</td>
 263             <td class="snns top italic gray">plane</td>
 264             <td class="snns top gray">files</td>
 265             <td class="ssnn top gray">
 266               <br />
 267             </td>
 268           </tr>
 269           <tr>
 270             <td class="snns top capitalize italic wine">examples</td>
 271             <td class="snns top italic wine">terms with special features</td>
 272             <td class="snns top wine">
 273               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_ex0.txt">levels_ex0</a>
 274               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_ex1.txt">ty3_ex1</a>
 275               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_ex2.txt">nf2_ex2</a>
 276             </td>
 277             <td class="ssnn top wine">
 278               <br />
 279             </td>
 280           </tr>
 281           <tr>
 282             <td class="snns top capitalize italic magenta" />
 283             <td class="snns top italic magenta" />
 284             <td class="snns top magenta" />
 285             <td class="ssnn top magenta">
 286               <br />
 287             </td>
 288           </tr>
 289           <tr>
 290             <td class="snns top capitalize italic prune">dynamic typing</td>
 291             <td class="snns top italic prune">well-formed contexts</td>
 292             <td class="snns top prune">
 293               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_defs.txt">wf3_defs</a>
 294             </td>
 295             <td class="ssnn top prune">
 296               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wf3_props.txt">wf3_props</a>
 297             </td>
 298           </tr>
 299           <tr>
 300             <td class="nnns top capitalize italic prune">
 301               <br />
 302             </td>
 303             <td class="snns top italic prune">context ref. for native type assignment</td>
 304             <td class="snns top prune">
 305               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_defs.txt">csubt_defs</a>
 306             </td>
 307             <td class="ssnn top prune">
 308               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_props.txt">csubt_props</a>
 309               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubt_arity_props.txt">csubt_arity_props</a>
 310             </td>
 311           </tr>
 312           <tr>
 313             <td class="nnns top capitalize italic prune">
 314               <br />
 315             </td>
 316             <td class="snns top italic prune">native type assignment</td>
 317             <td class="snns top prune">
 318               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_defs.txt">ty3_defs</a>
 319             </td>
 320             <td class="ssnn top prune">
 321               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_props.txt">ty3_props</a>
 322               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen.txt">ty3_gen</a>
 323               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_context.txt">ty3_gen_context</a>
 324               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_gen_nf2.txt">ty3_gen_nf2</a>
 325               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_lift.txt">ty3_lift</a>
 326               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_subst0.txt">ty3_subst0</a>
 327               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_arity_props.txt">ty3_arity_props</a>
 328               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_nf2_gen.txt">ty3_nf2_gen</a>
 329               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred.txt">ty3_sred</a>
 330               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_sred_props.txt">ty3_sred_props</a>
 331               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ty3_dec.txt">ty3_dec</a>
 332             </td>
 333           </tr>
 334           <tr>
 335             <td class="snns top capitalize italic blue">equivalence</td>
 336             <td class="snns top italic blue">context-sensitive equivalence</td>
 337             <td class="snns top blue">
 338               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_defs.txt">pc3_defs</a>
 339             </td>
 340             <td class="ssnn top blue">
 341               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_props.txt">pc3_props</a>
 342               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen.txt">pc3_gen</a>
 343               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_gen_context.txt">pc3_gen_context</a>
 344               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc3_subst0.txt">pc3_subst0</a>
 345             </td>
 346           </tr>
 347           <tr>
 348             <td class="nnns top capitalize italic blue">
 349               <br />
 350             </td>
 351             <td class="snns top italic blue">context-free equivalence</td>
 352             <td class="snns top blue">
 353               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_defs.txt">pc1_defs</a>
 354             </td>
 355             <td class="ssnn top blue">
 356               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pc1_props.txt">pc1_props</a>
 357             </td>
 358           </tr>
 359           <tr>
 360             <td class="snns top capitalize italic sky" />
 361             <td class="snns top italic sky" />
 362             <td class="snns top sky" />
 363             <td class="ssnn top sky">
 364               <br />
 365             </td>
 366           </tr>
 367           <tr>
 368             <td class="snns top capitalize italic cyan">computation</td>
 369             <td class="snns top italic cyan">context ref. for reducibility</td>
 370             <td class="snns top cyan">
 371               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_defs.txt">csubc_defs</a>
 372             </td>
 373             <td class="ssnn top cyan">
 374               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubc_props.txt">csubc_props</a>
 375             </td>
 376           </tr>
 377           <tr>
 378             <td class="nnns top capitalize italic cyan">
 379               <br />
 380             </td>
 381             <td class="snns top italic cyan">reducibility</td>
 382             <td class="snns top cyan">
 383               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_defs.txt">sc3_defs</a>
 384             </td>
 385             <td class="ssnn top cyan">
 386               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_props.txt">sc3_props</a>
 387               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sc3_arity.txt">sc3_arity</a>
 388             </td>
 389           </tr>
 390           <tr>
 391             <td class="nnns top capitalize italic cyan">
 392               <br />
 393             </td>
 394             <td class="snns top italic cyan">strongly normalizing computation</td>
 395             <td class="snns top cyan">
 396               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_defs.txt">sn3_defs</a>
 397             </td>
 398             <td class="ssnn top cyan">
 399               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_gen.txt">sn3_gen</a>
 400               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sn3_props.txt">sn3_props</a>
 401             </td>
 402           </tr>
 403           <tr>
 404             <td class="nnns top capitalize italic cyan">
 405               <br />
 406             </td>
 407             <td class="snns top italic cyan">context-sensitive computation</td>
 408             <td class="snns top cyan">
 409               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_defs.txt">pr3_defs</a>
 410             </td>
 411             <td class="ssnn top cyan">
 412               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_props.txt">pr3_props</a>
 413               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen.txt">pr3_gen</a>
 414               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_gen_context.txt">pr3_gen_context</a>
 415               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_iso.txt">pr3_iso</a>
 416               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_subst1.txt">pr3_subst1</a>
 417               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr3_confluence.txt">pr3_confluence</a>
 418             </td>
 419           </tr>
 420           <tr>
 421             <td class="nnns top capitalize italic cyan">
 422               <br />
 423             </td>
 424             <td class="snns top italic cyan">context-free computation</td>
 425             <td class="snns top cyan">
 426               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_defs.txt">pr1_defs</a>
 427             </td>
 428             <td class="ssnn top cyan">
 429               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_props.txt">pr1_props</a>
 430               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr1_confluence.txt">pr1_confluence</a>
 431             </td>
 432           </tr>
 433           <tr>
 434             <td class="snns top capitalize italic water">reduction</td>
 435             <td class="snns top italic water">normal forms for context-sensitive reduction</td>
 436             <td class="snns top water">
 437               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_defs.txt">nf2_defs</a>
 438             </td>
 439             <td class="ssnn top water">
 440               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_props.txt">nf2_props</a>
 441               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_gen.txt">nf2_gen</a>
 442               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf2_dec.txt">nf2_dec</a>
 443             </td>
 444           </tr>
 445           <tr>
 446             <td class="nnns top capitalize italic water">
 447               <br />
 448             </td>
 449             <td class="snns top italic water">context-sensitive reduction</td>
 450             <td class="snns top water">
 451               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_defs.txt">pr2_defs</a>
 452             </td>
 453             <td class="ssnn top water">
 454               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen.txt">pr2_gen</a>
 455               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_gen_context.txt">pr2_gen_context</a>
 456               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_lift.txt">pr2_lift</a>
 457               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_subst1.txt">pr2_subst1</a>
 458               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr2_confluence.txt">pr2_confluence</a>
 459             </td>
 460           </tr>
 461           <tr>
 462             <td class="nnns top capitalize italic water">
 463               <br />
 464             </td>
 465             <td class="snns top italic water">normal forms for context-free reduction</td>
 466             <td class="snns top water" />
 467             <td class="ssnn top water">
 468               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/nf0_dec.txt">nf0_dec</a>
 469             </td>
 470           </tr>
 471           <tr>
 472             <td class="nnns top capitalize italic water">
 473               <br />
 474             </td>
 475             <td class="snns top italic water">context-free reduction</td>
 476             <td class="snns top water">
 477               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/wcpr0_defs.txt">wcpr0_defs</a>
 478             </td>
 479             <td class="ssnn top water">
 480               <br />
 481             </td>
 482           </tr>
 483           <tr>
 484             <td class="nnns top capitalize italic water">
 485               <br />
 486             </td>
 487             <td class="nnns top italic water">
 488               <br />
 489             </td>
 490             <td class="snns top water">
 491               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_defs.txt">pr0_defs</a>
 492             </td>
 493             <td class="ssnn top water">
 494               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_gen.txt">pr0_gen</a>
 495               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_lift.txt">pr0_lift</a>
 496               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst0.txt">pr0_subst0</a>
 497               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_subst1.txt">pr0_subst1</a>
 498               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/pr0_confluence.txt">pr0_confluence</a>
 499             </td>
 500           </tr>
 501           <tr>
 502             <td class="snns top capitalize italic green">unfold</td>
 503             <td class="snns top italic green">iterated static type assignment</td>
 504             <td class="snns top green">
 505               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_defs.txt">sty1_defs</a>
 506             </td>
 507             <td class="ssnn top green">
 508               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty1_props.txt">sty1_props</a>
 509             </td>
 510           </tr>
 511           <tr>
 512             <td class="snns top capitalize italic grass">static typing</td>
 513             <td class="snns top italic grass">static type assignment</td>
 514             <td class="snns top grass">
 515               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_defs.txt">sty0_defs</a>
 516             </td>
 517             <td class="ssnn top grass">
 518               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/sty0_props.txt">sty0_props</a>
 519             </td>
 520           </tr>
 521           <tr>
 522             <td class="nnns top capitalize italic grass">
 523               <br />
 524             </td>
 525             <td class="snns top italic grass">context ref. for binary arity assignment</td>
 526             <td class="snns top grass">
 527               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_defs.txt">csuba_defs</a>
 528             </td>
 529             <td class="ssnn top grass">
 530               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csuba_props.txt">csuba_props</a>
 531             </td>
 532           </tr>
 533           <tr>
 534             <td class="nnns top capitalize italic grass">
 535               <br />
 536             </td>
 537             <td class="snns top italic grass">binary arity assignment</td>
 538             <td class="snns top grass">
 539               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_defs.txt">arity_defs</a>
 540             </td>
 541             <td class="ssnn top grass">
 542               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_props.txt">arity_props</a>
 543               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_gen.txt">arity_gen</a>
 544               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_subst0.txt">arity_subst0</a>
 545               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/arity_sred.txt">arity_sred</a>
 546             </td>
 547           </tr>
 548           <tr>
 549             <td class="nnns top capitalize italic grass">
 550               <br />
 551             </td>
 552             <td class="snns top italic grass">binary arity</td>
 553             <td class="snns top grass">
 554               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/levels_defs.txt">levels_defs</a>
 555               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/llt_defs.txt">llt_defs</a>
 556               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/aprem_defs.txt">aprem_defs</a>
 557             </td>
 558             <td class="ssnn top grass">
 559               <br />
 560             </td>
 561           </tr>
 562           <tr>
 563             <td class="nnns top capitalize italic grass">
 564               <br />
 565             </td>
 566             <td class="snns top italic grass">parameters</td>
 567             <td class="snns top grass">
 568               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/parameter_defs.txt">parameter_defs</a>
 569             </td>
 570             <td class="ssnn top grass">
 571               <br />
 572             </td>
 573           </tr>
 574           <tr>
 575             <td class="nnns top capitalize italic grass">
 576               <br />
 577             </td>
 578             <td class="snns top italic grass">basic context ref.</td>
 579             <td class="snns top grass">
 580               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubv_defs.txt">csubv_defs</a>
 581             </td>
 582             <td class="ssnn top grass">
 583               <br />
 584             </td>
 585           </tr>
 586           <tr>
 587             <td class="snns top capitalize italic yellow">multiple substitution</td>
 588             <td class="snns top italic yellow">iterated context slicing</td>
 589             <td class="snns top yellow">
 590               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_defs.txt">drop1_defs</a>
 591             </td>
 592             <td class="ssnn top yellow">
 593               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop1_props.txt">drop1_props</a>
 594             </td>
 595           </tr>
 596           <tr>
 597             <td class="nnns top capitalize italic yellow">
 598               <br />
 599             </td>
 600             <td class="snns top italic yellow">generic term relocation</td>
 601             <td class="snns top yellow">
 602               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_defs.txt">lift1_defs</a>
 603             </td>
 604             <td class="ssnn top yellow">
 605               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift1_props.txt">lift1_props</a>
 606             </td>
 607           </tr>
 608           <tr>
 609             <td class="snns top capitalize italic orange">substitution</td>
 610             <td class="snns top italic orange">ordinary substitution</td>
 611             <td class="snns top orange">
 612               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_defs.txt">subst_defs</a>
 613             </td>
 614             <td class="ssnn top orange">
 615               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst_props.txt">subst_props</a>
 616             </td>
 617           </tr>
 618           <tr>
 619             <td class="nnns top capitalize italic orange">
 620               <br />
 621             </td>
 622             <td class="nnns top italic orange">
 623               <br />
 624             </td>
 625             <td class="snns top orange">
 626               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_defs.txt">csubst1_defs</a>
 627             </td>
 628             <td class="ssnn top orange">
 629               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst1_props.txt">csubst1_props</a>
 630             </td>
 631           </tr>
 632           <tr>
 633             <td class="nnns top capitalize italic orange">
 634               <br />
 635             </td>
 636             <td class="nnns top italic orange">
 637               <br />
 638             </td>
 639             <td class="snns top orange">
 640               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_defs.txt">subst1_defs</a>
 641             </td>
 642             <td class="ssnn top orange">
 643               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_gen.txt">subst1_gen</a>
 644               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_lift.txt">subst1_lift</a>
 645               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_subst1.txt">subst1_subst1</a>
 646               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst1_confluence.txt">subst1_confluence</a>
 647             </td>
 648           </tr>
 649           <tr>
 650             <td class="nnns top capitalize italic orange">
 651               <br />
 652             </td>
 653             <td class="snns top italic orange">normal forms for ordinary strict substitution</td>
 654             <td class="snns top orange" />
 655             <td class="ssnn top orange">
 656               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/dnf_dec.txt">dnf_dec</a>
 657             </td>
 658           </tr>
 659           <tr>
 660             <td class="nnns top capitalize italic orange">
 661               <br />
 662             </td>
 663             <td class="snns top italic orange">ordinary strict substitution</td>
 664             <td class="snns top orange">
 665               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/fsubst0_defs.txt">fsubst0_defs</a>
 666             </td>
 667             <td class="ssnn top orange">
 668               <br />
 669             </td>
 670           </tr>
 671           <tr>
 672             <td class="nnns top capitalize italic orange">
 673               <br />
 674             </td>
 675             <td class="nnns top italic orange">
 676               <br />
 677             </td>
 678             <td class="snns top orange">
 679               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/csubst0_defs.txt">csubst0_defs</a>
 680             </td>
 681             <td class="ssnn top orange">
 682               <br />
 683             </td>
 684           </tr>
 685           <tr>
 686             <td class="nnns top capitalize italic orange">
 687               <br />
 688             </td>
 689             <td class="nnns top italic orange">
 690               <br />
 691             </td>
 692             <td class="snns top orange">
 693               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_defs.txt">subst0_defs</a>
 694             </td>
 695             <td class="ssnn top orange">
 696               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_gen.txt">subst0_gen</a>
 697               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_tlt.txt">subst0_tlt</a>
 698               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_lift.txt">subst0_lift</a>
 699               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_subst0.txt">subst0_subst0</a>
 700               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/subst0_confluence.txt">subst0_confluence</a>
 701             </td>
 702           </tr>
 703           <tr>
 704             <td class="nnns top capitalize italic orange">
 705               <br />
 706             </td>
 707             <td class="snns top italic orange">basic local env. slicing</td>
 708             <td class="snns top orange">
 709               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_defs.txt">getl_defs</a>
 710             </td>
 711             <td class="ssnn top orange">
 712               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/getl_props.txt">getl_props</a>
 713             </td>
 714           </tr>
 715           <tr>
 716             <td class="nnns top capitalize italic orange">
 717               <br />
 718             </td>
 719             <td class="nnns top italic orange">
 720               <br />
 721             </td>
 722             <td class="snns top orange">
 723               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_defs.txt">drop_defs</a>
 724             </td>
 725             <td class="ssnn top orange">
 726               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/drop_props.txt">drop_props</a>
 727             </td>
 728           </tr>
 729           <tr>
 730             <td class="nnns top capitalize italic orange">
 731               <br />
 732             </td>
 733             <td class="snns top italic orange">basic term relocation</td>
 734             <td class="snns top orange">
 735               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_defs.txt">lift_defs</a>
 736             </td>
 737             <td class="ssnn top orange">
 738               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_props.txt">lift_props</a>
 739               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_gen.txt">lift_gen</a>
 740               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/lift_tlt.txt">lift_tlt</a>
 741             </td>
 742           </tr>
 743           <tr>
 744             <td class="snns top capitalize italic red">grammar</td>
 745             <td class="snns top italic red">closures</td>
 746             <td class="snns top red">
 747               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/flt_defs.txt">flt_defs</a>
 748             </td>
 749             <td class="ssnn top red">
 750               <br />
 751             </td>
 752           </tr>
 753           <tr>
 754             <td class="nnns top capitalize italic red">
 755               <br />
 756             </td>
 757             <td class="snns top italic red">contexts</td>
 758             <td class="snns top red">
 759               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/contexts_defs.txt">contexts_defs</a>
 760               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/clt_defs.txt">clt_defs</a>
 761               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/ctail_defs.txt">ctail_defs</a>
 762               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/app_defs.txt">app_defs</a>
 763               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/cnt_defs.txt">cnt_defs</a>
 764             </td>
 765             <td class="ssnn top red">
 766               <br />
 767             </td>
 768           </tr>
 769           <tr>
 770             <td class="nnns top capitalize italic red">
 771               <br />
 772             </td>
 773             <td class="snns top italic red">terms</td>
 774             <td class="snns top red">
 775               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlist_defs.txt">tlist_defs</a>
 776             </td>
 777             <td class="ssnn top red">
 778               <br />
 779             </td>
 780           </tr>
 781           <tr>
 782             <td class="nnss top capitalize italic red">
 783               <br />
 784             </td>
 785             <td class="nnss top italic red">
 786               <br />
 787             </td>
 788             <td class="snss top red">
 789               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/terms_defs.txt">terms_defs</a>
 790               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/tlt_defs.txt">tlt_defs</a>
 791               <a href="http://lambdadelta.info/static/coq/lambdadelta/basic_1/iso_defs.txt">iso_defs</a>
 792             </td>
 793             <td class="sssn top red">
 794               <br />
 795             </td>
 796           </tr>
 797         </tbody>
 798       </table>
 799     </div>
 800     <div class="spacer">
 801       <img class="rule" alt="[Spacer]" title="\lambda\delta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
 802     </div>
 803     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 804       <br />
 805     </div>
 806     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 807       <a href="http://validator.w3.org/check?uri=referer">
 808         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
 809       </a>
 810       <a href="http://jigsaw.w3.org/css-validator/check/referer">
 811         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
 812       </a>
 813       <a href="http://www.w3.org/XML/">
 814         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
 815       </a>
 816       <a href="http://www.w3.org/Graphics/PNG/">
 817         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
 818       </a>
 819       <a href="http://www.anybrowser.org/campaign/">
 820         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
 821       </a>
 822     </div>
 823     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
 824       <br />
 825     </div>
 826     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 24 Nov 2017 21:00:01 +0100</div>
 827   </body>
 828 </html>