helm/www/lambdadelta/basic_2.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="lambdadelta version 2" />
  10     <title>lambdadelta version 2</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="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
  20       </a>
  21     </div>
  22     <div class="head1">cic:/matita/lambdadelta/basic_2/ (λδ version 2)</div>
  23     <div class="spacer">
  24       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
  25     </div>
  26    <div xmlns:ld="http://lambdadelta.info/" class="head2">System's Syntax and Behavior</div>
  27    <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of the "block structure"
  28          of the System's syntactic items and reductions.
  29    </div>
  30    <div xmlns:ld="http://lambdadelta.info/" class="text">
  31       <table cellpadding="4" cellspacing="0">
  32         <tbody>
  33           <tr>
  34             <td class="snns text grey">domain</td>
  35             <td class="snns plane grey">block</td>
  36             <td class="snns text grey">leader</td>
  37             <td class="snns text grey">applicator (with →θ)*</td>
  38             <td class="snns text grey">reduction</td>
  39             <td class="snns text grey">→ζ *</td>
  40             <td class="ssns text grey">reference *</td>
  41           </tr>
  42           <tr>
  43             <td class="snns text">{X | Γ ⊢ X : W}</td>
  44             <td class="snns plane wine">local typed abstraction *</td>
  45             <td class="snns text wine">Γ ⊢ +λW</td>
  46             <td class="snns text wine">ⓐV</td>
  47             <td class="snns text wine">→β</td>
  48             <td class="snns text wine">no</td>
  49             <td class="ssns text wine">#i</td>
  50           </tr>
  51           <tr>
  52             <td class="nnns text">
  53               <br />
  54             </td>
  55             <td class="snns plane magenta">local typed declaration **</td>
  56             <td class="snns text magenta">Γ ⊢ -λW</td>
  57             <td class="snns text magenta">ⓐV</td>
  58             <td class="snns text magenta">→β</td>
  59             <td class="snns text magenta">no</td>
  60             <td class="ssns text magenta">#i</td>
  61           </tr>
  62           <tr>
  63             <td class="nnns text">
  64               <br />
  65             </td>
  66             <td class="snns plane prune">global typed declaration ***</td>
  67             <td class="snns text prune">Γ ⊢ pλW</td>
  68             <td class="snns text prune">no</td>
  69             <td class="snns text prune">no</td>
  70             <td class="snns text prune">no</td>
  71             <td class="ssns text prune">$p</td>
  72           </tr>
  73           <tr>
  74             <td class="nnns text">
  75               <br />
  76             </td>
  77             <td class="snns plane blue">native type annotation *</td>
  78             <td class="snns text blue">Γ ⊢ ⓝW</td>
  79             <td class="snns text blue">no</td>
  80             <td class="snns text blue">no</td>
  81             <td class="snns text blue">yes</td>
  82             <td class="ssns text blue">no</td>
  83           </tr>
  84           <tr>
  85             <td class="snns text">{X | Γ ⊢ X = V}</td>
  86             <td class="snns plane sky">local abbreviation *</td>
  87             <td class="snns text sky">Γ ⊢ +δV</td>
  88             <td class="snns text sky">no</td>
  89             <td class="snns text sky">local →δ</td>
  90             <td class="snns text sky">yes</td>
  91             <td class="ssns text sky">#i</td>
  92           </tr>
  93           <tr>
  94             <td class="nnns text">
  95               <br />
  96             </td>
  97             <td class="snns plane cyan">local definition **</td>
  98             <td class="snns text cyan">Γ ⊢ -δV</td>
  99             <td class="snns text cyan">no</td>
 100             <td class="snns text cyan">local →δ</td>
 101             <td class="snns text cyan">no</td>
 102             <td class="ssns text cyan">#i</td>
 103           </tr>
 104           <tr>
 105             <td class="nnns text">
 106               <br />
 107             </td>
 108             <td class="snns plane water">global definition ***</td>
 109             <td class="snns text water">Γ ⊢ pδV</td>
 110             <td class="snns text water">no</td>
 111             <td class="snns text water">global →δ</td>
 112             <td class="snns text water">no</td>
 113             <td class="ssns text water">$p</td>
 114           </tr>
 115           <tr>
 116             <td class="snss text">no</td>
 117             <td class="snss plane green">sort ****</td>
 118             <td class="snss text green">Γ ⊢ ⋆k</td>
 119             <td class="snss text green">no</td>
 120             <td class="snss text green">no</td>
 121             <td class="snss text green">no</td>
 122             <td class="ssss text green">no</td>
 123           </tr>
 124         </tbody>
 125       </table>
 126     </div>
 127    <div xmlns:ld="http://lambdadelta.info/" class="text">* In terms only.
 128          ** In terms and local environments only.
 129          *** In global environments only.
 130          **** Sort level k in terms only.
 131    </div>
 132
 133    <div xmlns:ld="http://lambdadelta.info/" class="head2">Summary of the Specification</div>
 134    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
 135          and its timeline.
 136          Nodes are counted according to the "intrinsinc complexity measure"
 137          [F. Guidi: "Procedural Representation of CIC Proof Terms"
 138          Journal of Automated Reasoning 44(1-2), Springer (February 2010),
 139          pp. 53-78].
 140    </div>
 141    <div xmlns:ld="http://lambdadelta.info/" class="text">
 142       <table cellpadding="4" cellspacing="0">
 143         <tbody>
 144           <tr>
 145             <td class="snns component grey">category</td>
 146             <td class="snns plane grey">objects</td>
 147             <td class="snnn number grey">
 148               <br />
 149             </td>
 150             <td class="snnn plane grey">
 151               <br />
 152             </td>
 153             <td class="snnn number grey">
 154               <br />
 155             </td>
 156             <td class="snnn plane grey">
 157               <br />
 158             </td>
 159             <td class="ssnn number grey">
 160               <br />
 161             </td>
 162           </tr>
 163           <tr>
 164             <td class="snns component cyan">sizes</td>
 165             <td class="snns plane cyan">files</td>
 166             <td class="snnn number cyan">310  </td>
 167             <td class="snns plane cyan">characters</td>
 168             <td class="snnn number cyan">491788</td>
 169             <td class="snns plane cyan">nodes</td>
 170             <td class="ssnn number cyan">1422888</td>
 171           </tr>
 172           <tr>
 173             <td class="snns component green">propositions</td>
 174             <td class="snns plane green">theorems</td>
 175             <td class="snnn number green">90</td>
 176             <td class="snns plane green">lemmas</td>
 177             <td class="snnn number green">964</td>
 178             <td class="snns plane green">total</td>
 179             <td class="ssnn number green">1054</td>
 180           </tr>
 181           <tr>
 182             <td class="snss component yellow">concepts</td>
 183             <td class="snss plane yellow">declared</td>
 184             <td class="snsn number yellow">48</td>
 185             <td class="snss plane yellow">defined</td>
 186             <td class="snsn number yellow">75</td>
 187             <td class="snss plane yellow">total</td>
 188             <td class="sssn number yellow">123</td>
 189           </tr>
 190         </tbody>
 191       </table>
 192     </div>
 193    <ul xmlns:ld="http://lambdadelta.info/">
 194       <li>
 195         <span class="date">In progress.</span>
 196          Context-sensitive subject equivalence
 197          for native type assignment.
 198    </li>
 199     </ul>
 200    <ul xmlns:ld="http://lambdadelta.info/">
 201       <li>
 202         <span class="date">In progress.</span>
 203          Closure of context-sensitive extended computation
 204          for native validity.
 205    </li>
 206     </ul>
 207    <ul xmlns:ld="http://lambdadelta.info/">
 208       <li>
 209         <span class="date">2013 August 7.</span>
 210          Passive support for global environments.
 211    </li>
 212     </ul>
 213    <ul xmlns:ld="http://lambdadelta.info/">
 214       <li>
 215         <span class="date">2013 July 27.</span>
 216          Reaxiomatized β-reductum as in extended β-reduction
 217    </li>
 218     </ul>
 219    <ul xmlns:ld="http://lambdadelta.info/">
 220       <li>
 221         <span class="date">2013 July 20.</span>
 222          Context-sensitive extended strong normalization
 223          for simply typed terms.
 224    </li>
 225     </ul>
 226    <ul xmlns:ld="http://lambdadelta.info/">
 227       <li>
 228         <span class="date">2013 April 16.</span>
 229          Reaxiomatized substitution and reduction
 230          commute with respect to subclosure
 231          (anniversary milestone).
 232    </li>
 233     </ul>
 234    <ul xmlns:ld="http://lambdadelta.info/">
 235       <li>
 236         <span class="date">2013 March 16.</span>
 237          Mutual recursive preservation of stratified native validity
 238          for "big tree" computation on closures.
 239    </li>
 240     </ul>
 241    <ul xmlns:ld="http://lambdadelta.info/">
 242       <li>
 243         <span class="date">2012 October 16.</span>
 244          Confluence for context-free parallel reduction on closures.
 245    </li>
 246     </ul>
 247    <ul xmlns:ld="http://lambdadelta.info/">
 248       <li>
 249         <span class="date">2012 July 26.</span>
 250          Term binders polarized to control ζ-reduction.
 251    </li>
 252     </ul>
 253    <ul xmlns:ld="http://lambdadelta.info/">
 254       <li>
 255         <span class="date">2012 April 16.</span>
 256          Context-sensitive subject equivalence
 257          for atomic arity assignment
 258          (anniversary milestone).
 259    </li>
 260     </ul>
 261    <ul xmlns:ld="http://lambdadelta.info/">
 262       <li>
 263         <span class="date">2012 March 15.</span>
 264          Context-sensitive strong normalization
 265          for simply typed terms.
 266    </li>
 267     </ul>
 268    <ul xmlns:ld="http://lambdadelta.info/">
 269       <li>
 270         <span class="date">2012 January 27.</span>
 271          Support for abstract candidates of reducibility.
 272    </li>
 273     </ul>
 274    <ul xmlns:ld="http://lambdadelta.info/">
 275       <li>
 276         <span class="date">2011 September 21.</span>
 277          Confluence for context-sensitive parallel reduction on terms.
 278    </li>
 279     </ul>
 280    <ul xmlns:ld="http://lambdadelta.info/">
 281       <li>
 282         <span class="date">2011 September 6.</span>
 283          Confluence for context-free parallel reduction on terms.
 284    </li>
 285     </ul>
 286    <ul xmlns:ld="http://lambdadelta.info/">
 287       <li>
 288         <span class="date">2011 April 17.</span>
 289          Specification starts.
 290    </li>
 291     </ul>
 292
 293    <div xmlns:ld="http://lambdadelta.info/" class="head2">Logical Structure of the Specification</div>
 294    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
 295          according to the following table.
 296          Notation files covering the whole specification are provided.
 297          The notation for the relations or functions introduced in each file
 298          is shown in parentheses (? are placeholders).
 299    </div>
 300    <div xmlns:ld="http://lambdadelta.info/" class="text">
 301       <table cellpadding="4" cellspacing="0">
 302         <tbody>
 303           <tr>
 304             <td class="snns component grey">component</td>
 305             <td class="snns plane grey">plane</td>
 306             <td class="snns file grey">files</td>
 307             <td class="snnn file grey">
 308               <br />
 309             </td>
 310             <td class="snnn file grey">
 311               <br />
 312             </td>
 313             <td class="ssnn file grey">
 314               <br />
 315             </td>
 316           </tr>
 317           <tr>
 318             <td class="snns component prune">dynamic typing</td>
 319             <td class="snns plane prune">local env. ref. for stratified native validity</td>
 320             <td class="snns file prune">lsubsv ( ? ⊢ ? ¡⊑[?,?] ? )</td>
 321             <td class="snnn file prune">lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv</td>
 322             <td class="snnn file prune">
 323               <br />
 324             </td>
 325             <td class="ssnn file prune">
 326               <br />
 327             </td>
 328           </tr>
 329           <tr>
 330             <td class="nnns component prune">
 331               <br />
 332             </td>
 333             <td class="snns plane prune">stratified native validity</td>
 334             <td class="snns file prune">snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )</td>
 335             <td class="snnn file prune">snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs</td>
 336             <td class="snnn file prune">
 337               <br />
 338             </td>
 339             <td class="ssnn file prune">
 340               <br />
 341             </td>
 342           </tr>
 343           <tr>
 344             <td class="snns component blue">equivalence</td>
 345             <td class="snns plane blue">decomposed extended equivalence</td>
 346             <td class="snns file blue">cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )</td>
 347             <td class="snnn file blue">cpes_cpds</td>
 348             <td class="snnn file blue">
 349               <br />
 350             </td>
 351             <td class="ssnn file blue">
 352               <br />
 353             </td>
 354           </tr>
 355           <tr>
 356             <td class="nnns component blue">
 357               <br />
 358             </td>
 359             <td class="snns plane blue">context-sensitive equivalence</td>
 360             <td class="snns file blue">cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )</td>
 361             <td class="snnn file blue">cpcs_aaa cpcs_cprs cpcs_cpcs</td>
 362             <td class="snnn file blue">
 363               <br />
 364             </td>
 365             <td class="ssnn file blue">
 366               <br />
 367             </td>
 368           </tr>
 369           <tr>
 370             <td class="snns component sky">conversion</td>
 371             <td class="snns plane sky">context-sensitive conversion</td>
 372             <td class="snns file sky">cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )</td>
 373             <td class="snnn file sky">cpc_cpc</td>
 374             <td class="snnn file sky">
 375               <br />
 376             </td>
 377             <td class="ssnn file sky">
 378               <br />
 379             </td>
 380           </tr>
 381           <tr>
 382             <td class="snns component cyan">computation</td>
 383             <td class="snns plane cyan">context-sensitive extended evaluation</td>
 384             <td class="snns file cyan">cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )</td>
 385             <td class="snnn file cyan">
 386               <br />
 387             </td>
 388             <td class="snnn file cyan">
 389               <br />
 390             </td>
 391             <td class="ssnn file cyan">
 392               <br />
 393             </td>
 394           </tr>
 395           <tr>
 396             <td class="nnns component cyan">
 397               <br />
 398             </td>
 399             <td class="snns plane cyan">context-sensitive evaluation</td>
 400             <td class="snns file cyan">cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )</td>
 401             <td class="snnn file cyan">cpre_cpre</td>
 402             <td class="snnn file cyan">
 403               <br />
 404             </td>
 405             <td class="ssnn file cyan">
 406               <br />
 407             </td>
 408           </tr>
 409           <tr>
 410             <td class="nnns component cyan">
 411               <br />
 412             </td>
 413             <td class="snns plane cyan">strongly normalizing "big tree" computation</td>
 414             <td class="snns file cyan">fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )</td>
 415             <td class="snnn file cyan">fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )</td>
 416             <td class="snnn file cyan">fsb_aaa fsb_csx</td>
 417             <td class="ssnn file cyan">
 418               <br />
 419             </td>
 420           </tr>
 421           <tr>
 422             <td class="nnns component cyan">
 423               <br />
 424             </td>
 425             <td class="snns plane cyan">strongly normalizing extended computation</td>
 426             <td class="snns file cyan">lsx ( ? ⊢ ⬊*[?,?,?] ? )</td>
 427             <td class="snnn file cyan">lsx_cpxs lsx_csx</td>
 428             <td class="snnn file cyan">
 429               <br />
 430             </td>
 431             <td class="ssnn file cyan">
 432               <br />
 433             </td>
 434           </tr>
 435           <tr>
 436             <td class="nnns component cyan">
 437               <br />
 438             </td>
 439             <td class="nnns plane cyan">
 440               <br />
 441             </td>
 442             <td class="snns file cyan">csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
 443             <td class="snnn file cyan">csx_tstc_vector csx_aaa</td>
 444             <td class="snnn file cyan">
 445               <br />
 446             </td>
 447             <td class="ssnn file cyan">
 448               <br />
 449             </td>
 450           </tr>
 451           <tr>
 452             <td class="nnns component cyan">
 453               <br />
 454             </td>
 455             <td class="nnns plane cyan">
 456               <br />
 457             </td>
 458             <td class="snns file cyan">csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
 459             <td class="snnn file cyan">csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )</td>
 460             <td class="snnn file cyan">csx_lift csx_lpx csx_fpbs</td>
 461             <td class="ssnn file cyan">
 462               <br />
 463             </td>
 464           </tr>
 465           <tr>
 466             <td class="nnns component cyan">
 467               <br />
 468             </td>
 469             <td class="snns plane cyan">"big tree" parallel computation</td>
 470             <td class="snns file cyan">fpbg ( ⦃?,?,?⦄ &gt;⋕[?,?] ⦃?,?,?⦄ )</td>
 471             <td class="snnn file cyan">fpbg_lift fpbg_fpns fpbg_fpbg</td>
 472             <td class="snnn file cyan">
 473               <br />
 474             </td>
 475             <td class="ssnn file cyan">
 476               <br />
 477             </td>
 478           </tr>
 479           <tr>
 480             <td class="nnns component cyan">
 481               <br />
 482             </td>
 483             <td class="nnns plane cyan">
 484               <br />
 485             </td>
 486             <td class="snns file cyan">fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )</td>
 487             <td class="snnn file cyan">fpbc_fpns fpbc_fpbs</td>
 488             <td class="snnn file cyan">
 489               <br />
 490             </td>
 491             <td class="ssnn file cyan">
 492               <br />
 493             </td>
 494           </tr>
 495           <tr>
 496             <td class="nnns component cyan">
 497               <br />
 498             </td>
 499             <td class="nnns plane cyan">
 500               <br />
 501             </td>
 502             <td class="snns file cyan">fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )</td>
 503             <td class="snnn file cyan">fpbu_lift fpbu_fpns</td>
 504             <td class="snnn file cyan">
 505               <br />
 506             </td>
 507             <td class="ssnn file cyan">
 508               <br />
 509             </td>
 510           </tr>
 511           <tr>
 512             <td class="nnns component cyan">
 513               <br />
 514             </td>
 515             <td class="nnns plane cyan">
 516               <br />
 517             </td>
 518             <td class="snns file cyan">fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )</td>
 519             <td class="snnn file cyan">fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )</td>
 520             <td class="snnn file cyan">fpbs_lift fpbs_aaa fpbs_fpns fpbs_fpbs</td>
 521             <td class="ssnn file cyan">
 522               <br />
 523             </td>
 524           </tr>
 525           <tr>
 526             <td class="nnns component cyan">
 527               <br />
 528             </td>
 529             <td class="snns plane cyan">parallel computation for "big tree" normal forms</td>
 530             <td class="snns file cyan">fpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )</td>
 531             <td class="snnn file cyan">fpns_fpns</td>
 532             <td class="snnn file cyan">
 533               <br />
 534             </td>
 535             <td class="ssnn file cyan">
 536               <br />
 537             </td>
 538           </tr>
 539           <tr>
 540             <td class="nnns component cyan">
 541               <br />
 542             </td>
 543             <td class="snns plane cyan">decomposed extended computation</td>
 544             <td class="snns file cyan">cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )</td>
 545             <td class="snnn file cyan">cpds_lift cpds_aaa cpds_cpds</td>
 546             <td class="snnn file cyan">
 547               <br />
 548             </td>
 549             <td class="ssnn file cyan">
 550               <br />
 551             </td>
 552           </tr>
 553           <tr>
 554             <td class="nnns component cyan">
 555               <br />
 556             </td>
 557             <td class="snns plane cyan">context-sensitive extended computation</td>
 558             <td class="snns file cyan">lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )</td>
 559             <td class="snnn file cyan">lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )</td>
 560             <td class="snnn file cyan">lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs</td>
 561             <td class="ssnn file cyan">
 562               <br />
 563             </td>
 564           </tr>
 565           <tr>
 566             <td class="nnns component cyan">
 567               <br />
 568             </td>
 569             <td class="nnns plane cyan">
 570               <br />
 571             </td>
 572             <td class="snns file cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
 573             <td class="snnn file cyan">cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
 574             <td class="snnn file cyan">
 575               <br />
 576             </td>
 577             <td class="ssnn file cyan">
 578               <br />
 579             </td>
 580           </tr>
 581           <tr>
 582             <td class="nnns component cyan">
 583               <br />
 584             </td>
 585             <td class="snns plane cyan">context-sensitive computation</td>
 586             <td class="snns file cyan">lprs ( ⦃?,?⦄ ⊢ ➡* ? )</td>
 587             <td class="snnn file cyan">lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? )</td>
 588             <td class="snnn file cyan">lprs_ldrop lprs_cprs lprs_lprs</td>
 589             <td class="ssnn file cyan">
 590               <br />
 591             </td>
 592           </tr>
 593           <tr>
 594             <td class="nnns component cyan">
 595               <br />
 596             </td>
 597             <td class="nnns plane cyan">
 598               <br />
 599             </td>
 600             <td class="snns file cyan">cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)</td>
 601             <td class="snnn file cyan">cprs_lift cprs_cprs</td>
 602             <td class="snnn file cyan">
 603               <br />
 604             </td>
 605             <td class="ssnn file cyan">
 606               <br />
 607             </td>
 608           </tr>
 609           <tr>
 610             <td class="nnns component cyan">
 611               <br />
 612             </td>
 613             <td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td>
 614             <td class="snns file cyan">lsubc ( ? ⊢ ? ⊑[?] ? )</td>
 615             <td class="snnn file cyan">lsubc_ldrop lsubc_ldrops lsubc_lsuba</td>
 616             <td class="snnn file cyan">
 617               <br />
 618             </td>
 619             <td class="ssnn file cyan">
 620               <br />
 621             </td>
 622           </tr>
 623           <tr>
 624             <td class="nnns component cyan">
 625               <br />
 626             </td>
 627             <td class="snns plane cyan">support for abstract computation properties</td>
 628             <td class="snns file cyan">acp</td>
 629             <td class="snnn file cyan">acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
 630             <td class="snnn file cyan">acp_aaa</td>
 631             <td class="ssnn file cyan">
 632               <br />
 633             </td>
 634           </tr>
 635           <tr>
 636             <td class="snns component water">reduction</td>
 637             <td class="snns plane water">"big tree" parallel reduction</td>
 638             <td class="snns file water">fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )</td>
 639             <td class="snnn file water">fpb_lift fpb_aaa</td>
 640             <td class="snnn file water">
 641               <br />
 642             </td>
 643             <td class="ssnn file water">
 644               <br />
 645             </td>
 646           </tr>
 647           <tr>
 648             <td class="nnns component water">
 649               <br />
 650             </td>
 651             <td class="snns plane water">context-sensitive extended normal forms</td>
 652             <td class="snns file water">cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )</td>
 653             <td class="snnn file water">cnx_lift cnx_crx cnx_cix</td>
 654             <td class="snnn file water">
 655               <br />
 656             </td>
 657             <td class="ssnn file water">
 658               <br />
 659             </td>
 660           </tr>
 661           <tr>
 662             <td class="nnns component water">
 663               <br />
 664             </td>
 665             <td class="snns plane water">context-sensitive extended reduction</td>
 666             <td class="snns file water">lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )</td>
 667             <td class="snnn file water">lpx_leq lpx_ldrop lpx_lleq lpx_aaa</td>
 668             <td class="snnn file water">
 669               <br />
 670             </td>
 671             <td class="ssnn file water">
 672               <br />
 673             </td>
 674           </tr>
 675           <tr>
 676             <td class="nnns component water">
 677               <br />
 678             </td>
 679             <td class="nnns plane water">
 680               <br />
 681             </td>
 682             <td class="snns file water">cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )</td>
 683             <td class="snnn file water">cpx_leq cpx_lift cpx_cix</td>
 684             <td class="snnn file water">
 685               <br />
 686             </td>
 687             <td class="ssnn file water">
 688               <br />
 689             </td>
 690           </tr>
 691           <tr>
 692             <td class="nnns component water">
 693               <br />
 694             </td>
 695             <td class="snns plane water">context-sensitive extended irreducible forms</td>
 696             <td class="snns file water">cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ )</td>
 697             <td class="snnn file water">cix_append cix_lift</td>
 698             <td class="snnn file water">
 699               <br />
 700             </td>
 701             <td class="ssnn file water">
 702               <br />
 703             </td>
 704           </tr>
 705           <tr>
 706             <td class="nnns component water">
 707               <br />
 708             </td>
 709             <td class="snns plane water">context-sensitive extended reducible forms</td>
 710             <td class="snns file water">crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )</td>
 711             <td class="snnn file water">crx_append crx_lift</td>
 712             <td class="snnn file water">
 713               <br />
 714             </td>
 715             <td class="ssnn file water">
 716               <br />
 717             </td>
 718           </tr>
 719           <tr>
 720             <td class="nnns component water">
 721               <br />
 722             </td>
 723             <td class="snns plane water">context-sensitive normal forms</td>
 724             <td class="snns file water">cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )</td>
 725             <td class="snnn file water">cnr_lift cnr_crr cnr_cir</td>
 726             <td class="snnn file water">
 727               <br />
 728             </td>
 729             <td class="ssnn file water">
 730               <br />
 731             </td>
 732           </tr>
 733           <tr>
 734             <td class="nnns component water">
 735               <br />
 736             </td>
 737             <td class="snns plane water">context-sensitive reduction</td>
 738             <td class="snns file water">lpr ( ⦃?,?⦄ ⊢ ➡ ? )</td>
 739             <td class="snnn file water">lpr_ldrop lpr_lpr</td>
 740             <td class="snnn file water">
 741               <br />
 742             </td>
 743             <td class="ssnn file water">
 744               <br />
 745             </td>
 746           </tr>
 747           <tr>
 748             <td class="nnns component water">
 749               <br />
 750             </td>
 751             <td class="nnns plane water">
 752               <br />
 753             </td>
 754             <td class="snns file water">cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )</td>
 755             <td class="snnn file water">cpr_lift cpr_cir</td>
 756             <td class="snnn file water">
 757               <br />
 758             </td>
 759             <td class="ssnn file water">
 760               <br />
 761             </td>
 762           </tr>
 763           <tr>
 764             <td class="nnns component water">
 765               <br />
 766             </td>
 767             <td class="snns plane water">context-sensitive irreducible forms</td>
 768             <td class="snns file water">cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )</td>
 769             <td class="snnn file water">cir_append cir_lift</td>
 770             <td class="snnn file water">
 771               <br />
 772             </td>
 773             <td class="ssnn file water">
 774               <br />
 775             </td>
 776           </tr>
 777           <tr>
 778             <td class="nnns component water">
 779               <br />
 780             </td>
 781             <td class="snns plane water">context-sensitive reducible forms</td>
 782             <td class="snns file water">crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )</td>
 783             <td class="snnn file water">crr_append crr_lift</td>
 784             <td class="snnn file water">
 785               <br />
 786             </td>
 787             <td class="ssnn file water">
 788               <br />
 789             </td>
 790           </tr>
 791           <tr>
 792             <td class="snns component green">unfold</td>
 793             <td class="snns plane green">unfold</td>
 794             <td class="snns file green">unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )</td>
 795             <td class="snnn file green">
 796               <br />
 797             </td>
 798             <td class="snnn file green">
 799               <br />
 800             </td>
 801             <td class="ssnn file green">
 802               <br />
 803             </td>
 804           </tr>
 805           <tr>
 806             <td class="nnns component green">
 807               <br />
 808             </td>
 809             <td class="snns plane green">iterated static type assignment</td>
 810             <td class="snns file green">lsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )</td>
 811             <td class="snnn file green">lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )</td>
 812             <td class="snnn file green">lsstas_lift lsstas_aaa lsstas_lsstas</td>
 813             <td class="ssnn file green">
 814               <br />
 815             </td>
 816           </tr>
 817           <tr>
 818             <td class="snns component grass">static typing</td>
 819             <td class="snns plane grass">local env. ref. for atomic arity assignment</td>
 820             <td class="snns file grass">lsuba ( ? ⊢ ? ⁝⊑ ? )</td>
 821             <td class="snnn file grass">lsuba_ldrop lsuba_aaa lsuba_lsuba</td>
 822             <td class="snnn file grass">
 823               <br />
 824             </td>
 825             <td class="ssnn file grass">
 826               <br />
 827             </td>
 828           </tr>
 829           <tr>
 830             <td class="nnns component grass">
 831               <br />
 832             </td>
 833             <td class="snns plane grass">atomic arity assignment</td>
 834             <td class="snns file grass">aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )</td>
 835             <td class="snnn file grass">aaa_lift aaa_lifts aaa_fqus aaa_da aaa_ssta aaa_aaa</td>
 836             <td class="snnn file grass">
 837               <br />
 838             </td>
 839             <td class="ssnn file grass">
 840               <br />
 841             </td>
 842           </tr>
 843           <tr>
 844             <td class="nnns component grass">
 845               <br />
 846             </td>
 847             <td class="snns plane grass">stratified static type assignment</td>
 848             <td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td>
 849             <td class="snnn file grass">ssta_lift ssta_ssta</td>
 850             <td class="snnn file grass">
 851               <br />
 852             </td>
 853             <td class="ssnn file grass">
 854               <br />
 855             </td>
 856           </tr>
 857           <tr>
 858             <td class="nnns component grass">
 859               <br />
 860             </td>
 861             <td class="snns plane grass">local env. ref. for degree assignment</td>
 862             <td class="snns file grass">lsubd ( ? ⊢ ? ▪⊑ ? )</td>
 863             <td class="snnn file grass">lsubd_da lsubd_lsubd</td>
 864             <td class="snnn file grass">
 865               <br />
 866             </td>
 867             <td class="ssnn file grass">
 868               <br />
 869             </td>
 870           </tr>
 871           <tr>
 872             <td class="nnns component grass">
 873               <br />
 874             </td>
 875             <td class="snns plane grass">degree assignment</td>
 876             <td class="snns file grass">da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )</td>
 877             <td class="snnn file grass">da_lift da_da</td>
 878             <td class="snnn file grass">
 879               <br />
 880             </td>
 881             <td class="ssnn file grass">
 882               <br />
 883             </td>
 884           </tr>
 885           <tr>
 886             <td class="nnns component grass">
 887               <br />
 888             </td>
 889             <td class="snns plane grass">parameters</td>
 890             <td class="snns file grass">sh</td>
 891             <td class="snnn file grass">sd</td>
 892             <td class="snnn file grass">
 893               <br />
 894             </td>
 895             <td class="ssnn file grass">
 896               <br />
 897             </td>
 898           </tr>
 899           <tr>
 900             <td class="snns component yellow">substitution</td>
 901             <td class="snns plane yellow">restricted local env. ref.</td>
 902             <td class="snns file yellow">lsubr ( ? ⊑ ? )</td>
 903             <td class="snnn file yellow">lsubr_lsubr</td>
 904             <td class="snnn file yellow">
 905               <br />
 906             </td>
 907             <td class="ssnn file yellow">
 908               <br />
 909             </td>
 910           </tr>
 911           <tr>
 912             <td class="nnns component yellow">
 913               <br />
 914             </td>
 915             <td class="snns plane yellow">iterated structural successor for closures</td>
 916             <td class="snns file yellow">fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )</td>
 917             <td class="snnn file yellow">fqus_alt fqus_lleq fqus_fqus</td>
 918             <td class="snnn file yellow">
 919               <br />
 920             </td>
 921             <td class="ssnn file yellow">
 922               <br />
 923             </td>
 924           </tr>
 925           <tr>
 926             <td class="nnns component yellow">
 927               <br />
 928             </td>
 929             <td class="nnns plane yellow">
 930               <br />
 931             </td>
 932             <td class="snns file yellow">fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )</td>
 933             <td class="snnn file yellow">fqup_lleq fqup_fqup</td>
 934             <td class="snnn file yellow">
 935               <br />
 936             </td>
 937             <td class="ssnn file yellow">
 938               <br />
 939             </td>
 940           </tr>
 941           <tr>
 942             <td class="nnns component yellow">
 943               <br />
 944             </td>
 945             <td class="snns plane yellow">generic local env. slicing</td>
 946             <td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td>
 947             <td class="snnn file yellow">ldrops_ldrop ldrops_ldrops</td>
 948             <td class="snnn file yellow">
 949               <br />
 950             </td>
 951             <td class="ssnn file yellow">
 952               <br />
 953             </td>
 954           </tr>
 955           <tr>
 956             <td class="nnns component yellow">
 957               <br />
 958             </td>
 959             <td class="snns plane yellow">generic term relocation</td>
 960             <td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td>
 961             <td class="snnn file yellow">lifts_lift_vector</td>
 962             <td class="snnn file yellow">
 963               <br />
 964             </td>
 965             <td class="ssnn file yellow">
 966               <br />
 967             </td>
 968           </tr>
 969           <tr>
 970             <td class="nnns component yellow">
 971               <br />
 972             </td>
 973             <td class="nnns plane yellow">
 974               <br />
 975             </td>
 976             <td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td>
 977             <td class="snnn file yellow">lifts_lift lifts_lifts</td>
 978             <td class="snnn file yellow">
 979               <br />
 980             </td>
 981             <td class="ssnn file yellow">
 982               <br />
 983             </td>
 984           </tr>
 985           <tr>
 986             <td class="nnns component yellow">
 987               <br />
 988             </td>
 989             <td class="snns plane yellow">support for generic relocation</td>
 990             <td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td>
 991             <td class="snnn file yellow">gr2_plus ( ? + ? )</td>
 992             <td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td>
 993             <td class="ssnn file yellow">gr2_gr2</td>
 994           </tr>
 995           <tr>
 996             <td class="snns component orange">relocation</td>
 997             <td class="snns plane orange">structural successor for closures</td>
 998             <td class="snns file orange">fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )</td>
 999             <td class="snnn file orange">fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )</td>
1000             <td class="snnn file orange">fquq_lleq</td>
1001             <td class="ssnn file orange">
1002               <br />
1003             </td>
1004           </tr>
1005           <tr>
1006             <td class="nnns component orange">
1007               <br />
1008             </td>
1009             <td class="nnns plane orange">
1010               <br />
1011             </td>
1012             <td class="snns file orange">fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )</td>
1013             <td class="snnn file orange">fqu_lleq</td>
1014             <td class="snnn file orange">
1015               <br />
1016             </td>
1017             <td class="ssnn file orange">
1018               <br />
1019             </td>
1020           </tr>
1021           <tr>
1022             <td class="nnns component orange">
1023               <br />
1024             </td>
1025             <td class="snns plane orange">lazy equivalence for local environments</td>
1026             <td class="snns file orange">lleq ( ? ⋕[?,?] ? )</td>
1027             <td class="snnn file orange">lleq_lleq</td>
1028             <td class="snnn file orange">
1029               <br />
1030             </td>
1031             <td class="ssnn file orange">
1032               <br />
1033             </td>
1034           </tr>
1035           <tr>
1036             <td class="nnns component orange">
1037               <br />
1038             </td>
1039             <td class="snns plane orange">global env. slicing</td>
1040             <td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td>
1041             <td class="snnn file orange">gdrop_gdrop</td>
1042             <td class="snnn file orange">
1043               <br />
1044             </td>
1045             <td class="ssnn file orange">
1046               <br />
1047             </td>
1048           </tr>
1049           <tr>
1050             <td class="nnns component orange">
1051               <br />
1052             </td>
1053             <td class="snns plane orange">basic local env. slicing</td>
1054             <td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td>
1055             <td class="snnn file orange">ldrop_append ldrop_lpx_sn ldrop_leq ldrop_ldrop</td>
1056             <td class="snnn file orange">
1057               <br />
1058             </td>
1059             <td class="ssnn file orange">
1060               <br />
1061             </td>
1062           </tr>
1063           <tr>
1064             <td class="nnns component orange">
1065               <br />
1066             </td>
1067             <td class="snns plane orange">basic term relocation</td>
1068             <td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td>
1069             <td class="snnn file orange">lift_lift_vector</td>
1070             <td class="snnn file orange">
1071               <br />
1072             </td>
1073             <td class="ssnn file orange">
1074               <br />
1075             </td>
1076           </tr>
1077           <tr>
1078             <td class="nnns component orange">
1079               <br />
1080             </td>
1081             <td class="nnns plane orange">
1082               <br />
1083             </td>
1084             <td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td>
1085             <td class="snnn file orange">lift_lift</td>
1086             <td class="snnn file orange">
1087               <br />
1088             </td>
1089             <td class="ssnn file orange">
1090               <br />
1091             </td>
1092           </tr>
1093           <tr>
1094             <td class="snns component red">grammar</td>
1095             <td class="snns plane red">equivalence for local environments</td>
1096             <td class="snns file red">leq ( ? ≃[?,?] ? ) </td>
1097             <td class="snnn file red">
1098               <br />
1099             </td>
1100             <td class="snnn file red">
1101               <br />
1102             </td>
1103             <td class="ssnn file red">
1104               <br />
1105             </td>
1106           </tr>
1107           <tr>
1108             <td class="nnns component red">
1109               <br />
1110             </td>
1111             <td class="snns plane red">pointwise extension of a relation</td>
1112             <td class="snns file red">lpx_sn</td>
1113             <td class="snnn file red">lpx_sn_tc lpx_sn_lpx_sn</td>
1114             <td class="snnn file red">
1115               <br />
1116             </td>
1117             <td class="ssnn file red">
1118               <br />
1119             </td>
1120           </tr>
1121           <tr>
1122             <td class="nnns component red">
1123               <br />
1124             </td>
1125             <td class="snns plane red">same top term constructor</td>
1126             <td class="snns file red">tstc ( ? ≃ ? )</td>
1127             <td class="snnn file red">tstc_tstc tstc_vector</td>
1128             <td class="snnn file red">
1129               <br />
1130             </td>
1131             <td class="ssnn file red">
1132               <br />
1133             </td>
1134           </tr>
1135           <tr>
1136             <td class="nnns component red">
1137               <br />
1138             </td>
1139             <td class="snns plane red">closures</td>
1140             <td class="snns file red">cl_shift ( ? @@ ? )</td>
1141             <td class="snnn file red">cl_weight ( ♯{?,?,?} )</td>
1142             <td class="snnn file red">
1143               <br />
1144             </td>
1145             <td class="ssnn file red">
1146               <br />
1147             </td>
1148           </tr>
1149           <tr>
1150             <td class="nnns component red">
1151               <br />
1152             </td>
1153             <td class="snns plane red">internal syntax</td>
1154             <td class="snns file red">genv</td>
1155             <td class="snnn file red">
1156               <br />
1157             </td>
1158             <td class="snnn file red">
1159               <br />
1160             </td>
1161             <td class="ssnn file red">
1162               <br />
1163             </td>
1164           </tr>
1165           <tr>
1166             <td class="nnns component red">
1167               <br />
1168             </td>
1169             <td class="nnns plane red">
1170               <br />
1171             </td>
1172             <td class="snns file red">lenv</td>
1173             <td class="snnn file red">lenv_weight ( ♯{?} )</td>
1174             <td class="snnn file red">lenv_length ( |?| )</td>
1175             <td class="ssnn file red">lenv_append ( ? @@ ? )</td>
1176           </tr>
1177           <tr>
1178             <td class="nnns component red">
1179               <br />
1180             </td>
1181             <td class="nnns plane red">
1182               <br />
1183             </td>
1184             <td class="snns file red">term</td>
1185             <td class="snnn file red">term_weight ( ♯{?} )</td>
1186             <td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td>
1187             <td class="ssnn file red">term_vector</td>
1188           </tr>
1189           <tr>
1190             <td class="nnns component red">
1191               <br />
1192             </td>
1193             <td class="nnns plane red">
1194               <br />
1195             </td>
1196             <td class="snns file red">item</td>
1197             <td class="snnn file red">
1198               <br />
1199             </td>
1200             <td class="snnn file red">
1201               <br />
1202             </td>
1203             <td class="ssnn file red">
1204               <br />
1205             </td>
1206           </tr>
1207           <tr>
1208             <td class="nnss component red">
1209               <br />
1210             </td>
1211             <td class="snss plane red">external syntax</td>
1212             <td class="snss file red">aarity</td>
1213             <td class="snsn file red">
1214               <br />
1215             </td>
1216             <td class="snsn file red">
1217               <br />
1218             </td>
1219             <td class="sssn file red">
1220               <br />
1221             </td>
1222           </tr>
1223         </tbody>
1224       </table>
1225     </div>
1226
1227    <div xmlns:ld="http://lambdadelta.info/" class="head2">Physical Structure of the Specification</div>
1228    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
1229          one for each component.
1230    </div>
1231    <div class="spacer">
1232       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
1233     </div>
1234     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1235       <br />
1236     </div>
1237     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1238       <a href="http://validator.w3.org/check?uri=referer">
1239         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
1240       </a>
1241       <a href="http://jigsaw.w3.org/css-validator/check/referer">
1242         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
1243       </a>
1244       <a href="http://www.w3.org/XML/">
1245         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
1246       </a>
1247       <a href="http://www.w3.org/Graphics/PNG/">
1248         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
1249       </a>
1250       <a href="http://www.anybrowser.org/campaign/">
1251         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
1252       </a>
1253     </div>
1254     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1255       <br />
1256     </div>
1257     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 15 Dec 2013 16:51:14 +0100</div>
1258 </body>
1259 </html>