helm/www/lambda_delta/ld_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" xmlns:ld="http://lambda_delta.info">
   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 version 2"/>
  10     <title>lambda_delta version 2</title>
  11     <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
  12     <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
  13     <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
  14     <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
  15   </head>
  16   <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/Basic_2/ (λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div>
  17    <div class="head2">Summary of the contribution</div>
  18    <div class="text">Here is a numerical acount of the contribution's contents
  19             and its timeline.
  20    </div>
  21    <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">39</td><td class="snns plane green">lemmas</td><td class="ssnn number green">333</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">33</td><td class="snss plane yellow">defined</td><td class="sssn number yellow">46</td></tr></tbody></table></div>
  22
  23             Support for abstract candidates of reducibility closed.
  24
  25
  26             Confluence of context-sensitive parallel reduction closed.
  27
  28
  29             Confluence of context-free parallel reduction closed.
  30
  31
  32             Specification started.
  33
  34    <div class="head2">Logical structure of the contribution</div>
  35    <div class="text">The source files are grouped in planes and components
  36             according to the following table.
  37             The notation for the relations or functions introduced in each file
  38             is shown in parentheses.
  39    </div>
  40    <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">functional</td><td class="snns plane prune">reduction and type machine</td><td class="snns file prune">rtm</td><td class="snnn file prune">rtm_step ( ? ⇨ ? )</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="nnns component prune"><br/></td><td class="snns plane prune">unfold</td><td class="snns file prune">lift ( ↑[?,?] ? )</td><td class="snnn file prune">subst ( [?←?] ? )</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">examples</td><td class="snns plane blue"><br/></td><td class="snns file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">native typing</td><td class="snns plane sky"><br/></td><td class="snns file sky">nty</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">conversion</td><td class="snns plane cyan">context-sensitive conversion</td><td class="snns file cyan">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">computation</td><td class="snns plane water">strongly normalizing computation</td><td class="snns file water">csn ( ⬇* ? )</td><td class="snnn file water">csn_cr</td><td class="snnn file water">csn_aaa</td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive computation</td><td class="snns file water">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">local env. ref. for abstract candidates of reducibility</td><td class="snns file water">lsubc ( ? [?] ⊑ ? )</td><td class="snnn file water">lsubc_ldrop</td><td class="snnn file water">lsubc_ldrops</td><td class="ssnn file water">lsubc_lsuba</td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">support for abstract computation properties</td><td class="snns file water">acp</td><td class="snnn file water">acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )</td><td class="snnn file water">acp_aaa</td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">reducibility</td><td class="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⊢ ➡ ? )</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file green">cpr_lift</td><td class="snnn file green">cpr_ltpr</td><td class="ssnn file green">cpr_cpr</td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free normal forms</td><td class="snns file green">twhnf ( 𝐖𝐇𝐍[?] )</td><td class="snnn file green">tnf ( 𝐍[?] )</td><td class="snnn file green">tnf_tif</td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reduction</td><td class="snns file green">ltpr ( ? ➡ ? )</td><td class="snnn file green">ltpr_ldrop</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">tpr ( ? ➡ ? )</td><td class="snnn file green">tpr_lift</td><td class="snnn file green">tpr_tpss</td><td class="ssnn file green">tpr_tpr</td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reducible forms</td><td class="snns file green">trf ( 𝐑[?] )</td><td class="snnn file green">tif ( 𝐈[?] )</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">static type assignment</td><td class="snns file grass">sty</td><td class="snnn file grass">sty_lift</td><td class="snnn file grass">sty_sty</td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ÷⊑ ? )</td><td class="snnn file grass">lsuba_ldrop</td><td class="snnn file grass">lsuba_aaa</td><td class="ssnn file grass">lsuba_lsuba</td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⊢ ? ÷ ? )</td><td class="snnn file grass">aaa_lift</td><td class="snnn file grass">aaa_lifts</td><td class="ssnn file grass">aaa_aaa</td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">term inverse relocation</td><td class="snns file yellow">delift ( ? ⊢ ? [?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss ( ? [?,?] ▶* ? )</td><td class="snnn file yellow">ltpss_ldrop</td><td class="snnn file yellow">ltpss_tps</td><td class="ssnn file yellow">ltpss_ltpss</td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⊢ ? [?,?] ▶* ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="ssnn file yellow">tpss_ltps</td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift</td><td class="snnn file yellow">lifts_lifts</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @ [ ? ] ? ≡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td><td class="ssnn file yellow">gr2_gr2</td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">ltps ( ? [?,?] ▶ ? )</td><td class="snnn file orange">ltps_ldrop</td><td class="snnn file orange">ltps_tps</td><td class="ssnn file orange">ltps_ltps</td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">tps ( ? ⊢ ? [?,?] ▶ ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">local env. ref. for substitution</td><td class="snns file red">lsubs ( ? [?,?] ≼ ? )</td><td class="snnn file red">lsubs_lsubs</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">term hom.</td><td class="snns file red">thom</td><td class="snnn file red">thom_thom</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @ ? )</td><td class="snnn file red">cl_weight ( #[?,?] )</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #[?] )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #[?] )</td><td class="snnn file red">term_simple ( 𝐒[?] )</td><td class="ssnn file red">term_vector</td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
  41    <div class="head2">Physical structure of the contribution</div>
  42    <div class="text">The source files are grouped in directories, one for each
  43             component.
  44    </div>
  45    <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-02-01+01:00</div>
  46 </body>
  47 </html>