]> matita.cs.unibo.it Git - helm.git/commitdiff
- we added a web page (Apps_2) for the checked applications of Basic_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 24 Feb 2012 16:27:56 +0000 (16:27 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 24 Feb 2012 16:27:56 +0000 (16:27 +0000)
- we added some files to Basic_2
- we improved the Makefiles

helm/www/lambda_delta/bin/xhtbl/Makefile
helm/www/lambda_delta/ld_apps_2.html [new file with mode: 0644]
helm/www/lambda_delta/ld_basic_2.html
helm/www/lambda_delta/news.html
helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml [new file with mode: 0644]
helm/www/lambda_delta/web/home/ld_apps_2_src.tbl [new file with mode: 0644]
helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
helm/www/lambda_delta/web/home/ld_basic_2_src.tbl
helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl
helm/www/lambda_delta/xslt/ld_web_root.xsl

index 79a056af563afe3f57986c7919b6ddf439fbbe47..df0833cca2a3f780eb9d7c4c9d71b51eac88b68f 100644 (file)
@@ -17,18 +17,20 @@ LDSRCDIR  = ../../etc/lambda_delta/
 HOMEDIR   = ../../
 TBLDIRS   = $(SRCDIR) $(LDSRCDIR)
 
+LDWS  = $(shell find $(SRCDIR) -name "*.ldw.xml")
 TBLS  = $(shell find $(TBLDIRS) -name "*.tbl")
 XSLS  = xhtbl.xsl $(patsubst %.tbl, %.xsl, $(notdir $(TBLS)))
+HTMLS = $(patsubst %.ldw.xml, $(HOMEDIR)%.html, $(notdir $(LDWS)))
 LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl
 
-%.html: BASEURL = --stringparam baseurl $(LDURL)
+$(HOMEDIR)%.html: BASEURL = --stringparam baseurl $(LDURL)
 
-www: $(HOMEDIR)ld_basic_2.html
+www: $(HTMLS)
 
 $(XSLS:%=$(XSLDIR)%): $(TBLS) $(XHTBL)
        @echo "  XHTBL *.tbl"
        $(H)$(XHTBL) -O $(XSLDIR) $(TBLS)
 
-$(HOMEDIR)ld_basic_2.html: $(SRCDIR)ld_basic_2.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%)
+$(HOMEDIR)%.html: $(SRCDIR)%.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%)
        @echo "  XSLT $(notdir $<)"
        $(H)$(XSLT) -o $@ $(BASEURL) $(XSLDIR)ld_web.xsl $<
diff --git a/helm/www/lambda_delta/ld_apps_2.html b/helm/www/lambda_delta/ld_apps_2.html
new file mode 100644 (file)
index 0000000..8558d58
--- /dev/null
@@ -0,0 +1,62 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambda_delta.info">
+  <head>
+    <meta http-equiv="Content-Language" content="en-us"/>
+    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+    <meta http-equiv="Content-Style-Type" content="text/css"/>
+    <meta name="author" content="Ferruccio Guidi"/>
+    <meta name="description" content="applications of lambda_delta version 2"/>
+    <title>applications of lambda_delta version 2</title>
+    <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
+    <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
+    <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
+    <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
+  </head>
+  <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/Apps_2/ (applications of λδ 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>
+   <div class="head2">Contents of the Specification</div>
+   <div class="text">This specification comprises a collection of checked
+         applications of λδ version 2.
+        In particular it contains the components below.
+   </div>
+   <ul><li><span class="date">MLTT1.</span>
+         Martin-Löf's Type Theory with one universe
+        using λδ as the theory of expressions.
+   </li></ul>
+   <ul><li><span class="date">Functional.</span>
+         The validation algorithm for λδ as implemented in
+        <a href="http://lambda-delta.info/implementation.html#helena">Helena 0.8</a>.
+   </li></ul>
+   
+   <div class="head2">Summary of the Specification</div>
+   <div class="text">Here is a numerical acount of the specification's contents
+         and its timeline.
+   </div>
+   <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="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">4</td><td class="snns plane green">lemmas</td><td class="snnn number green">1</td><td class="snns plane green">total</td><td class="ssnn number green">5</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">3</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">10</td><td class="snss plane yellow">total</td><td class="sssn number yellow">13</td></tr></tbody></table></div>
+   <ul><li><span class="date">2012 February 24.</span>
+         The Applications directory is started.
+   </li></ul>
+   <ul><li><span class="date">2011 December 20.</span>
+         The Functional component is started
+        inside the specification of λδ version 2.
+   </li></ul>
+   <ul><li><span class="date">2011 December 12.</span>
+         The MLTT1 component is started.
+   </li></ul>
+
+   <div class="head2">Logical Structure of the Specification</div>
+   <div class="text">The source files are grouped in planes and components
+         according to the following table.
+         Each component contains its own notation file.
+        The notation for the relations or functions introduced in each file
+        is shown in parentheses.
+   </div>
+   <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="ssnn file grey"><br/></td></tr><tr><td class="snns component orange">MLTT1</td><td class="snns plane orange"><br/></td><td class="snns file orange">genv_primitive</td><td class="ssnn file orange">judgement</td></tr><tr><td class="snns component red">functional</td><td class="snns plane red">reduction and type machine</td><td class="snns file red">rtm</td><td class="ssnn file red">rtm_step ( ? ⇨ ? )</td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">unfold</td><td class="snss file red">lift ( ↑[?,?] ? )</td><td class="sssn file red">subst ( [?←?] ? )</td></tr></tbody></table></div>
+
+   <div class="head2">Physical Structure of the Specification</div>
+   <div class="text">The source files are grouped in directories,
+         one for each component.
+   </div>
+   <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-24+01:00</div>
+</body>
+</html>
index 030109a2fa050d8fa854ef8b6b5c8971672fad5d..5d9118e0d39c10cb6a2cf3ee1e5a39d00be7de8c 100644 (file)
   <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>
    <div class="head2">System's Syntax and Behavior</div>
    <div class="text">This is a summary of the "block structure"
-            of the System's syntactic items and reductions.
+         of the System's syntactic items and reductions.
    </div>
    <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns text grey">domain</td><td class="snns plane grey">block</td><td class="snns text grey">leader</td><td class="snns text grey">applicator (with →θ)*</td><td class="snns text grey">reduction</td><td class="snns text grey">→ζ *</td><td class="ssns text grey">reference *</td></tr><tr><td class="snns text">{X | Γ ⊢ X : W}</td><td class="snns plane wine">typed abstraction **</td><td class="snns text wine">Γ ⊢ λW</td><td class="snns text wine">ⓐV</td><td class="snns text wine">→β</td><td class="snns text wine">no</td><td class="ssns text wine">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane magenta">typed declaration ***</td><td class="snns text magenta">Γ ⊢ pλW</td><td class="snns text magenta">no</td><td class="snns text magenta">no</td><td class="snns text magenta">no</td><td class="ssns text magenta">$p</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane prune">native type annotation *</td><td class="snns text prune">Γ ⊢ ⓣW</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="snns text prune">yes</td><td class="ssns text prune">no</td></tr><tr><td class="snns text">{X | Γ ⊢ X = V}</td><td class="snns plane blue">local abbreviation **</td><td class="snns text blue">Γ ⊢ δV</td><td class="snns text blue">no</td><td class="snns text blue">local →δ</td><td class="snns text blue">yes</td><td class="ssns text blue">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane sky">global abbreviation ***</td><td class="snns text sky">Γ ⊢ pδV</td><td class="snns text sky">no</td><td class="snns text sky">global →δ</td><td class="snns text sky">no</td><td class="ssns text sky">$p</td></tr><tr><td class="snss text">no</td><td class="snss plane cyan">sort ****</td><td class="snss text cyan">Γ ⊢ ⋆k</td><td class="snss text cyan">no</td><td class="snss text cyan">no</td><td class="snss text cyan">no</td><td class="ssss text cyan">no</td></tr></tbody></table></div>
    <div class="text">* In terms only.
-           ** In terms and local environments only.
-            *** In global environments only.
-            **** Sort level k in terms only. 
+        ** In terms and local environments only.
+         *** In global environments only.
+         **** Sort level k in terms only. 
    </div>
    
    <div class="head2">Summary of the Specification</div>
    <div class="text">Here is a numerical acount of the specification's contents
-            and its timeline.
+         and its timeline.
    </div>
-   <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">46</td><td class="snns plane green">lemmas</td><td class="ssnn number green">405</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">35</td><td class="snss plane yellow">defined</td><td class="sssn number yellow">49</td></tr></tbody></table></div>
+   <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="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">43</td><td class="snns plane green">lemmas</td><td class="snnn number green">409</td><td class="snns plane green">total</td><td class="ssnn number green">452</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">32</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">35</td><td class="snss plane yellow">total</td><td class="sssn number yellow">67</td></tr></tbody></table></div>
    <ul><li><span class="date">In progress.</span>
-            Context-sensitive strong normalization of simply typed terms.
+         Context-sensitive strong normalization of simply typed terms.
    </li></ul>
    <ul><li><span class="date">2012 January 27.</span>
-            Support for abstract candidates of reducibility closed.
+         Support for abstract candidates of reducibility closed.
    </li></ul>
    <ul><li><span class="date">2011 September 21.</span>
-            Confluence of context-sensitive parallel reduction closed.
+         Confluence of context-sensitive parallel reduction closed.
    </li></ul>
    <ul><li><span class="date">2011 September 6.</span>
-            Confluence of context-free parallel reduction closed.
+         Confluence of context-free parallel reduction closed.
    </li></ul>
    <ul><li><span class="date">2011 April 17.</span>
-            Specification started.
+         Specification started.
    </li></ul>
 
    <div class="head2">Logical Structure of the Specification</div>
    <div class="text">The source files are grouped in planes and components
-            according to the following table.
-            The notation for the relations or functions introduced in each file
-           is shown in parentheses.
+         according to the following table.
+         A notation file covering the whole specification is provided.
+        The notation for the relations or functions introduced in each file
+        is shown in parentheses.
    </div>
-   <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="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="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="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="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="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="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_vector ( ⬇* ? )</td><td class="snnn file water">csn_cr</td><td class="snnn file water">csn_aaa</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="nnns plane water"><br/></td><td class="snns file water">csn ( ⬇* ? )</td><td class="snnn file water">csn_lift</td><td class="snnn file water">csn_cpr</td><td class="snnn file water">csn_cprs ( ⬇** ? )</td><td class="ssnn file water">csn_lcpr</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">cprs_lcpr</td><td class="snnn file water">cprs_cprs</td><td class="snnn file water">cprs_tstc</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="snnn file water">lsubc_lsuba</td><td class="ssnn file water"><br/></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="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">reducibility</td><td class="snns plane green">context-sensitive normal forms</td><td class="snns file green">cnf ( ? ⊢ 𝐍[?] )</td><td class="snnn file green">cnf_lift</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="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⊢ ➡ ? )</td><td class="snnn file green">lcpr_cpr</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_ltpss</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="snnn file green"><br/></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">ltpr_tps</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="snnn file green">tpr_tpr</td><td class="ssnn file green"><br/></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="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="snnn file grass"><br/></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="snnn file grass">lsuba_lsuba</td><td class="ssnn file grass"><br/></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="snnn file grass">aaa_aaa</td><td class="ssnn file grass"><br/></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="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="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="snnn file yellow">ltpss_ltpss</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">tpss ( ? ⊢ ? [?,?] ▶* ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="snnn file yellow">tpss_ltps</td><td class="ssnn file yellow"><br/></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="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">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="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="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">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="snnn file yellow">gr2_gr2</td><td class="ssnn file yellow"><br/></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="snnn file orange">ltps_ltps</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">tps ( ? ⊢ ? [?,?] ▶ ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</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">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="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="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="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="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="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="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">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc</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="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="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="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="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">term</td><td class="snnn file red">term_weight ( #[?] )</td><td class="snnn file red">term_simple ( 𝐒[?] )</td><td class="snnn file red">term_vector</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">item</td><td class="snnn file red"><br/></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="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
+   <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="snnn file grey"><br/></td><td class="ssnn file grey"><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="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="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="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_vector ( ⬇* ? )</td><td class="snnn file water">csn_lcpr_vector</td><td class="snnn file water">csn_aaa</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="nnns plane water"><br/></td><td class="snns file water">csn ( ⬇* ? )</td><td class="snnn file water">csn_lift</td><td class="snnn file water">csn_cpr</td><td class="snnn file water">csn_cprs ( ⬇** ? )</td><td class="ssnn file water">csn_lcpr</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">cprs_lcpr</td><td class="snnn file water">cprs_cprs</td><td class="snnn file water">cprs_tstc</td><td class="ssnn file water">cprs_tstc_vector</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="snnn file water">lsubc_lsuba</td><td class="ssnn file water"><br/></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="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">reducibility</td><td class="snns plane green">context-sensitive normal forms</td><td class="snns file green">cnf ( ? ⊢ 𝐍[?] )</td><td class="snnn file green">cnf_lift</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="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⊢ ➡ ? )</td><td class="snnn file green">lcpr_cpr</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_ltpss</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="snnn file green"><br/></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">ltpr_tps</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="snnn file green">tpr_tpr</td><td class="ssnn file green"><br/></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="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="snnn file grass"><br/></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="snnn file grass">lsuba_lsuba</td><td class="ssnn file grass"><br/></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="snnn file grass">aaa_aaa</td><td class="ssnn file grass"><br/></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="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="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="snnn file yellow">ltpss_ltpss</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">tpss ( ? ⊢ ? [?,?] ▶* ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="snnn file yellow">tpss_ltps</td><td class="ssnn file yellow"><br/></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="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">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="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="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">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="snnn file yellow">gr2_gr2</td><td class="ssnn file yellow"><br/></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="snnn file orange">ltps_ltps</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">tps ( ? ⊢ ? [?,?] ▶ ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</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">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="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="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="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="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="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">same head term form</td><td class="snns file red">tshf ( ? ≈ ? )</td><td class="snnn file red">tshf_tshf</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="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc</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="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="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="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="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">term</td><td class="snnn file red">term_weight ( #[?] )</td><td class="snnn file red">term_simple ( 𝐒[?] )</td><td class="snnn file red">term_vector</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">item</td><td class="snnn file red"><br/></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="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
 
    <div class="head2">Physical Structure of the Specification</div>
-   <div class="text">The source files are grouped in directories, one for each
-            component.
+   <div class="text">The source files are grouped in directories,
+         one for each component.
    </div>
-   <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-20+01:00</div>
+   <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-24+01:00</div>
 </body>
 </html>
index a1c4024ecb5698c4e481ce466fb8d49f2ce81fc7..aecc87973c8731d88b5328daef3c6e4faa0e8582 100644 (file)
@@ -61,11 +61,14 @@ December 2012.<br>
       </ul>
       <ul>
         <li><span style="font-weight: bold;">April 2011.</span> The
-specification of λδ version 2 is restarted in <a
+specification of λδ version 2 and related topics is restarted in <a
  href="http://matita.cs.unibo.it/">Matita 0.5</a>.</li>
         <ul>
           <li><a href="ld_basic_2.html">Here</a> is a page about the
-specification.<br>
+specification (Core).<br>
+          </li>
+          <li><a href="ld_apps_2.html">Here</a> is a page about the
+topics related to the specification (Applications).<br>
           </li>
         </ul>
       </ul>
@@ -90,10 +93,7 @@ started.<br>
       <ul>
         <li><span style="font-weight: bold;">June 2009.</span> <span
  style="font-style: italic;">Helena</span>, a <a
- href="implementation.html#helena">validator for </a><a
- href="implementation.html#helena">λ</a><a
- href="implementation.html#helena">δ version 2</a><span
- style="font-style: italic;"></span>, <span style="font-style: italic;"></span>is
+ href="implementation.html#helena">validator for λδ version 2</a>, is
 available
 as
 a
@@ -253,7 +253,7 @@ gives this site as the first result.</li>
  style="width: 88px; height: 31px;" alt="[PNG Used Here]"
  title="PNG Used Here" src="download/PNGnow2.png"><br>
 <br>
-Last update 2012-02-21 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+Last update 2012-02-24 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 Guidi</a><br>
 </div>
 </body>
diff --git a/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml
new file mode 100644 (file)
index 0000000..4254219
--- /dev/null
@@ -0,0 +1,52 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambda_delta.info"
+      description = "applications of lambda_delta version 2"
+      title = "applications of lambda_delta version 2"
+      head = "cic:/matita/lambda_delta/Apps_2/ (applications of λδ version 2)"
+>
+   <section>Contents of the Specification</section>
+   <body>This specification comprises a collection of checked
+         applications of λδ version 2.
+        In particular it contains the components below.
+   </body>
+   <news date="MLTT1.">
+         Martin-Löf's Type Theory with one universe
+        using λδ as the theory of expressions.
+   </news>
+   <news date="Functional.">
+         The validation algorithm for λδ as implemented in
+        <rlink to="implementation.html#helena">Helena 0.8</rlink>.
+   </news>
+   
+   <section>Summary of the Specification</section>
+   <body>Here is a numerical acount of the specification's contents
+         and its timeline.
+   </body>
+   <table name="ld_Apps_2_sum"/>
+   <news date="2012 February 24.">
+         The Applications directory is started.
+   </news>
+   <news date="2011 December 20.">
+         The Functional component is started
+        inside the specification of λδ version 2.
+   </news>
+   <news date="2011 December 12.">
+         The MLTT1 component is started.
+   </news>
+
+   <section>Logical Structure of the Specification</section>
+   <body>The source files are grouped in planes and components
+         according to the following table.
+         Each component contains its own notation file.
+        The notation for the relations or functions introduced in each file
+        is shown in parentheses.
+   </body>
+   <table name="ld_apps_2_src"/>
+
+   <section>Physical Structure of the Specification</section>
+   <body>The source files are grouped in directories,
+         one for each component.
+   </body>
+   <footer/>
+</page>
diff --git a/helm/www/lambda_delta/web/home/ld_apps_2_src.tbl b/helm/www/lambda_delta/web/home/ld_apps_2_src.tbl
new file mode 100644 (file)
index 0000000..df8a560
--- /dev/null
@@ -0,0 +1,38 @@
+name "ld_apps_2_src"
+
+table {
+   class "grey"
+   [ { "component" * } {
+        [ { "plane" * } { 
+             [ "files" * ]
+         }
+        ]
+     }
+   ]
+   class "orange"
+   [ { "MLTT1" * } {
+        [ { "" * } { 
+             [ "genv_primitive" "judgement" * ]
+         }
+        ]
+     }
+   ]
+   class "red"
+   [ { "functional" * } {
+        [ { "reduction and type machine" * } { 
+             [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+         }
+        ]
+        [ { "unfold" * } { 
+             [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
+         }
+        ]
+     }
+   ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
index 36cce9d1ab191be8167584c1182e5f4d7b72a7a5..7a1eef5f79965ae128ce8765702614aa0a2c4821 100644 (file)
@@ -1,53 +1,54 @@
 <?xml version="1.0" encoding="UTF-8"?>
 
-<ld:page xmlns:ld="http://lambda_delta.info"
+<page xmlns="http://lambda_delta.info"
       description = "lambda_delta version 2"
       title = "lambda_delta version 2"
       head = "cic:/matita/lambda_delta/Basic_2/ (λδ version 2)"
 >
-   <ld:section>System's Syntax and Behavior</ld:section>
-   <ld:body>This is a summary of the "block structure"
-            of the System's syntactic items and reductions.
-   </ld:body>
-   <ld:table name="ld_basic_2_blk"/>
-   <ld:body>* In terms only.
-           ** In terms and local environments only.
-            *** In global environments only.
-            **** Sort level k in terms only. 
-   </ld:body>
+   <section>System's Syntax and Behavior</section>
+   <body>This is a summary of the "block structure"
+         of the System's syntactic items and reductions.
+   </body>
+   <table name="ld_basic_2_blk"/>
+   <body>* In terms only.
+        ** In terms and local environments only.
+         *** In global environments only.
+         **** Sort level k in terms only. 
+   </body>
    
-   <ld:section>Summary of the Specification</ld:section>
-   <ld:body>Here is a numerical acount of the specification's contents
-            and its timeline.
-   </ld:body>
-   <ld:table name="ld_Basic_2_sum"/>
-   <ld:news date="In progress.">
-            Context-sensitive strong normalization of simply typed terms.
-   </ld:news>
-   <ld:news date="2012 January 27.">
-            Support for abstract candidates of reducibility closed.
-   </ld:news>
-   <ld:news date="2011 September 21.">
-            Confluence of context-sensitive parallel reduction closed.
-   </ld:news>
-   <ld:news date="2011 September 6.">
-            Confluence of context-free parallel reduction closed.
-   </ld:news>
-   <ld:news date="2011 April 17.">
-            Specification started.
-   </ld:news>
+   <section>Summary of the Specification</section>
+   <body>Here is a numerical acount of the specification's contents
+         and its timeline.
+   </body>
+   <table name="ld_Basic_2_sum"/>
+   <news date="In progress.">
+         Context-sensitive strong normalization of simply typed terms.
+   </news>
+   <news date="2012 January 27.">
+         Support for abstract candidates of reducibility closed.
+   </news>
+   <news date="2011 September 21.">
+         Confluence of context-sensitive parallel reduction closed.
+   </news>
+   <news date="2011 September 6.">
+         Confluence of context-free parallel reduction closed.
+   </news>
+   <news date="2011 April 17.">
+         Specification started.
+   </news>
 
-   <ld:section>Logical Structure of the Specification</ld:section>
-   <ld:body>The source files are grouped in planes and components
-            according to the following table.
-            The notation for the relations or functions introduced in each file
-           is shown in parentheses.
-   </ld:body>
-   <ld:table name="ld_basic_2_src"/>
+   <section>Logical Structure of the Specification</section>
+   <body>The source files are grouped in planes and components
+         according to the following table.
+         A notation file covering the whole specification is provided.
+        The notation for the relations or functions introduced in each file
+        is shown in parentheses.
+   </body>
+   <table name="ld_basic_2_src"/>
 
-   <ld:section>Physical Structure of the Specification</ld:section>
-   <ld:body>The source files are grouped in directories, one for each
-            component.
-   </ld:body>
-   <ld:footer/>
-</ld:page>
+   <section>Physical Structure of the Specification</section>
+   <body>The source files are grouped in directories,
+         one for each component.
+   </body>
+   <footer/>
+</page>
index 65e26acff7d2f1714932d9edcf6c38ef93a7fcb7..b5905e5cfabc8a7b4a62a2a561c6d90aabc50084 100644 (file)
@@ -9,18 +9,6 @@ table {
         ]
      }
    ]
-   class "prune"
-   [ { "functional" * } {
-        [ { "reduction and type machine" * } { 
-             [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
-         }
-        ]
-        [ { "unfold" * } { 
-             [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
-         }
-        ]
-     }
-   ]
    class "blue"
    [ { "examples" * } {
         [ { "" * } {
@@ -48,12 +36,12 @@ table {
    class "water"
    [ { "computation" * } {
         [ { "strongly normalizing computation" * } {
-            [ "csn_vector ( ⬇* ? )" "csn_cr" "csn_aaa" * ]
+            [ "csn_vector ( ⬇* ? )" "csn_lcpr_vector" "csn_aaa" * ]
             [ "csn ( ⬇* ? )" "csn_lift" "csn_cpr" "csn_cprs ( ⬇** ? )" "csn_lcpr" * ]
          }
         ]
         [ { "context-sensitive computation" * } {
-            [ "cprs (? ⊢ ? ➡* ?)" "cprs_lcpr" "cprs_cprs" "cprs_tstc" * ]
+            [ "cprs (? ⊢ ? ➡* ?)" "cprs_lcpr" "cprs_cprs" "cprs_tstc" "cprs_tstc_vector" * ]
          }
         ]
         [ { "local env. ref. for abstract candidates of reducibility" * } {
@@ -166,8 +154,8 @@ table {
              [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
           }
        ]
-       [ { "term hom." * } {
-             [ "thom ( ? ≈ ? )" "thom_thom" * ]
+       [ { "same head term form" * } {
+             [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
           }
        ]
        [ { "same top term constructor" * } {
index 24badffe370ab2cb3bd2140d0376d3749984898e..db1af39542a8bba9e0d3938b914e0826ff729d03 100644 (file)
@@ -15,6 +15,8 @@
         <td class="snns plane grey">objects</td>
         <td class="snnn number grey"><br/></td>
         <td class="snnn plane grey"><br/></td>
+        <td class="snnn number grey"><br/></td>
+        <td class="snnn plane grey"><br/></td>
         <td class="ssnn number grey"><br/></td>
       </tr>
       <tr>
@@ -22,6 +24,8 @@
         <td class="snns plane green">theorems</td>
         <td class="snnn number green">0</td>
         <td class="snns plane green">lemmas</td>
+        <td class="snnn number green">23</td>
+        <td class="snns plane green">total</td>
         <td class="ssnn number green">23</td>
       </tr>
       <tr>
@@ -29,7 +33,9 @@
         <td class="snss plane yellow">declared</td>
         <td class="snsn number yellow">22</td>
         <td class="snss plane yellow">defined</td>
-        <td class="sssn number yellow">8</td>
+        <td class="snsn number yellow">8</td>
+        <td class="snss plane yellow">total</td>
+        <td class="sssn number yellow">30</td>
       </tr>
     </tbody>
   </table>
index 1375316f8f29e9cd05c8880d1d1aa572ef7efd2a..2920bc6575635a7e91eb4e2b770bfb04699365e7 100644 (file)
    </div>
 </xsl:template>
 
+<xsl:template match="ld:rlink">
+   <a href="{$baseurl}{@to}">
+      <xsl:apply-templates/>
+   </a>
+</xsl:template>
+
 <xsl:template match="ld:news">
    <ul><li>
       <span class="date"><xsl:value-of select="@date"/></span>