From 0cb16b42f119c1cb6135f237092892e2f82929ee Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 18 Jan 2015 16:51:36 +0000 Subject: [PATCH] - we add an informational page on \lambda\delta version 1 (core) - web site update --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 27 +- helm/www/lambdadelta/basic_1.html | 729 ++++++++++++++++++ helm/www/lambdadelta/basic_2.html | 19 +- helm/www/lambdadelta/documentation.html | 9 +- helm/www/lambdadelta/ground_2.html | 13 +- helm/www/lambdadelta/implementation.html | 9 +- helm/www/lambdadelta/index.html | 9 +- helm/www/lambdadelta/news.html | 9 +- helm/www/lambdadelta/specification.html | 46 +- helm/www/lambdadelta/web/home/sitemap.tbl | 1 + .../web/home/specification.ldw.xml | 37 +- .../lambdadelta/apps_2/web/apps_2.ldw.xml | 2 +- .../lambdadelta/apps_2/web/apps_2_src.tbl | 2 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../lambdadelta/ground_2/web/ground_2.ldw.xml | 2 +- 17 files changed, 866 insertions(+), 58 deletions(-) create mode 100644 helm/www/lambdadelta/basic_1.html diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index e33fe4a91..a436738f2 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Thu, 15 Jan 2015 16:54:45 +0100
+
Last update: Sun, 18 Jan 2015 17:28:58 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 379c28ce3..2e773d14b 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -45,6 +45,9 @@
+ +
+ implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
+ library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -117,7 +124,7 @@
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
@@ -145,29 +152,29 @@ sizes files - 4 + 14 characters - 68581 + 6787 nodes - 3637 + 10070 propositions theorems 2 lemmas - 1 + 4 total - 3 + 6 concepts declared - 3 + 6 defined - 9 + 11 total - 12 + 17 @@ -251,6 +258,6 @@

-
Last update: Thu, 15 Jan 2015 16:54:45 +0100
+
Last update: Sun, 18 Jan 2015 17:28:58 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html new file mode 100644 index 000000000..ffaf8b48b --- /dev/null +++ b/helm/www/lambdadelta/basic_1.html @@ -0,0 +1,729 @@ + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + documentation + + specification + +
+ 		+
+ 		+ implementation + +
+
+ foreword + + milestones + + version 2 + + version 2 + (background - core - applications) +
+ 		+ library + (static LDDL directory)
+ citations + + visibility + + version 1 + + version 1 + (core)(static HELM directory) + helena + +
+
+
+ +
Summary of the Specification [spacer] +
+
Here is a numerical account of the specification's contents + and its timeline. +
+ +
    +
  • + January 2015. + Update with with backports from the abandoned specification of λδ version 2. +
    • +
+
    +
  • + May 2008. + Specification is concluded. +
    • +
+
    +
  • + November 2006. + Decidability of native type assignment, λδ version 1 is released. +
    • +
+
    +
  • + December 2005. + Preservation of native type by reduction, λδ version 1 is announced. +
    • +
+
    +
  • + May 2004. + Specification starts. +
    • +
+
Logical Structure of the Specification [spacer] +
+
This table reports the specification's components and their planes. +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
examplesterms with special features + levels_ex0 + ty3_ex1 + nf2_ex2 + +
+
+ + + +
+
dynamic typingwell-formed contexts + wf3_defs + + wf3_props +
+
+ 		context ref. for native type assignment + csubt_defs + + csubt_props + csubt_arity_props +
+
+ 		native type assignment + ty3_defs + + ty3_props + ty3_gen + ty3_gen_context + ty3_gen_nf2 + ty3_lift + ty3_subst0 + ty3_arity_props + ty3_nf2_gen + ty3_sred + ty3_sred_props + ty3_dec +
equivalencecontext-sensitive equivalence + pc3_defs + + pc3_props + pc3_gen + pc3_gen_context + pc3_subst0 +
+
+ 		context-free equivalence + pc1_defs + + pc1_props +
+ + + +
+
computationcontext ref. for reducibility + csubc_defs + + csubc_props +
+
+ 		reducibility + sc3_defs + + sc3_props + sc3_arity +
+
+ 		strongly normalizing computation + sn3_defs + + sn3_gen + sn3_props +
+
+ 		context-sensitive computation + pr3_defs + + pr3_props + pr3_gen + pr3_gen_context + pr3_iso + pr3_subst1 + pr3_confluence +
+
+ 		context-free computation + pr1_defs + + pr1_props + pr1_confluence +
reductionnormal forms for context-sensitive reduction + nf2_defs + + nf2_props + nf2_gen + nf2_dec +
+
+ 		context-sensitive reduction + pr2_defs + + pr2_gen + pr2_gen_context + pr2_lift + pr2_subst1 + pr2_confluence +
+
+ 		normal forms for context-free reduction + + nf0_dec +
+
+ 		context-free reduction + wcpr0_defs + +
+
+
+ 		+
+ 		+ pr0_defs + + pr0_gen + pr0_lift + pr0_subst0 + pr0_subst1 + pr0_confluence +
unfolditerated static type assignment + sty1_defs + + sty1_props +
static typingstatic type assignment + sty0_defs + + sty0_props +
+
+ 		context ref. for binary arity assignment + csuba_defs + + csuba_props +
+
+ 		binary arity assignment + arity_defs + + arity_props + arity_gen + arity_subst0 + arity_sred +
+
+ 		binary arity + levels_defs + llt_defs + aprem_defs + +
+
+
+ 		parameters + parameter_defs + +
+
+
+ 		basic context ref. + csubv_defs + +
+
multiple substitutioniterated context slicing + drop1_defs + + drop1_props +
+
+ 		generic term relocation + lift1_defs + + lift1_props +
substitutionordinary substitution + subst_defs + + subst_props +
+
+ 		+
+ 		+ csubst1_defs + + csubst1_props +
+
+ 		+
+ 		+ subst1_defs + + subst1_gen + subst1_lift + subst1_subst1 + subst1_confluence +
+
+ 		normal forms for ordinary strict substitution + + dnf_dec +
+
+ 		ordinary strict substitution + fsubst0_defs + +
+
+
+ 		+
+ 		+ csubst0_defs + +
+
+
+ 		+
+ 		+ subst0_defs + + subst0_gen + subst0_tlt + subst0_lift + subst0_subst0 + subst0_confluence +
+
+ 		basic local env. slicing + getl_defs + + getl_props +
+
+ 		+
+ 		+ drop_defs + + drop_props +
+
+ 		basic term relocation + lift_defs + + lift_props + lift_gen + lift_tlt +
grammarclosures + flt_defs + +
+
+
+ 		contexts + contexts_defs + clt_defs + ctail_defs + app_defs + cnt_defs + +
+
+
+ 		terms + tlist_defs + +
+
+
+ 		+
+ 		+ terms_defs + tlt_defs + iso_defs + +
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 18 Jan 2015 17:28:58 +0100
+ + diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index d3ea2991a..16a6a66ce 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -45,6 +45,9 @@
+ +
+ implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
+ library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -109,7 +116,7 @@ -->
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
@@ -141,7 +148,7 @@ characters 433402 nodes - 1874774 + 1874778 propositions @@ -204,7 +211,7 @@
  • 2014 April 16. Lazy equivalence on local environments - addded as q-step to rst-computation on closures + added as q-step to rst-computation on closures (anniversary milestone).
    • @@ -1012,7 +1019,7 @@
    - contxt-sensitive multiple rt-substitution + context-sensitive multiple rt-substitution cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) cpys_lift cpys_cpys @@ -1152,7 +1159,7 @@
    - contxt-sensitive ordinary rt-substitution + context-sensitive ordinary rt-substitution cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_nlift cpy_cpy @@ -1377,6 +1384,6 @@

    -
    Last update: Thu, 15 Jan 2015 16:54:45 +0100
    +
    Last update: Sun, 18 Jan 2015 17:28:58 +0100
    diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 71b7318d6..1bc4c29ae 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -45,6 +45,9 @@
    + +
    + implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
    + library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -359,6 +366,6 @@

    -
    Last update: Thu, 15 Jan 2015 16:54:44 +0100
    +
    Last update: Sun, 18 Jan 2015 17:28:58 +0100
    diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 88f2bef4a..89716b516 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -45,6 +45,9 @@
    + +
    + implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
    + library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -97,7 +104,7 @@
    Summary of the Specification [spacer]
    -
    Here is a numerical acount of the specification's contents +
    Here is a numerical account of the specification's contents and its timeline.
    @@ -127,7 +134,7 @@ files 30 characters - 68581 + 46649 nodes 62380 @@ -290,6 +297,6 @@

    -
    Last update: Thu, 15 Jan 2015 16:54:45 +0100
    +
    Last update: Sun, 18 Jan 2015 17:28:58 +0100
    diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index b11b5b995..27a1d0f1b 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -45,6 +45,9 @@
    + +
    + implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
    + library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -248,6 +255,6 @@

    -
    Last update: Thu, 15 Jan 2015 16:54:44 +0100
    +
    Last update: Sun, 18 Jan 2015 17:28:58 +0100
    diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 34855b0ee..d96d0d541 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -45,6 +45,9 @@
    + +
    + implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
    + library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -195,6 +202,6 @@

    -
    Last update: Thu, 15 Jan 2015 16:54:44 +0100
    +
    Last update: Sun, 18 Jan 2015 17:28:58 +0100
    diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index ebd699892..ce97adae0 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -45,6 +45,9 @@
    + +
    + implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
    + library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -328,6 +335,6 @@

    -
    Last update: Fri, 16 Jan 2015 16:47:03 +0100
    +
    Last update: Sun, 18 Jan 2015 17:28:58 +0100
    diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 043b472e1..21336180b 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -45,6 +45,9 @@
    + +
    + implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
    + library @@ -84,6 +90,7 @@ version 1 + (core) (static HELM directory) helena @@ -171,6 +178,26 @@
    +
    + Informational pages on the specifications are provided. +
    +
      +
    • + Notice on displayed numerical acounts: + nodes are counted according to the "intrinsic complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. +
      • +
    +
      +
    • + Notice on displayed logical structures: + from the logical standpoint, the source scripts are grouped in "planes" + and these are grouped in "components"; + the notation for the relations or functions + introduced in each script, is shown in parentheses (? are placeholders). +
      • +
    [spacer] λδ version 2 (active)
    @@ -201,19 +228,6 @@ Background, Core, Applications. -
    -
    - Notice on numerical acounts: - nodes are counted according to the "intrinsic complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. -
    -
    - Notice on displayed logical structures: - from the logical standpoint, the source scripts are grouped in "planes" - and these are grouped in "components"; - the notation for the relations or functions - introduced in each script, is shown in parentheses (? are placeholders).
    @@ -283,6 +297,10 @@ Notice: the HELM rendering engine is offline. +
    + Informational pages on the parts of the specification: +Core. +
    [Spacer]
    @@ -309,6 +327,6 @@

    -
    Last update: Fri, 16 Jan 2015 16:47:03 +0100
    +
    Last update: Sun, 18 Jan 2015 17:41:31 +0100
    diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 091a90a73..8d6b24e85 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -24,6 +24,7 @@ table [ @@("apps_2" "applications") ^ ")" * ] [ @@("specification#v1" "version 1") + "(" ^ @@("basic_1" "core") ^ ")" "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")" * ] } diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 9712c9a83..5c7813d83 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -28,6 +28,23 @@ + + Informational pages on the specifications are provided. + + + + nodes are counted according to the "intrinsic complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. + + + + from the logical standpoint, the source scripts are grouped in "planes" + and these are grouped in "components"; + the notation for the relations or functions + introduced in each script, is shown in parentheses (? are placeholders). + + λδ version 2 (active) @@ -59,19 +76,6 @@ Core, Applications. - - - nodes are counted according to the "intrinsic complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. - - - - from the logical standpoint, the source scripts are grouped in "planes" - and these are grouped in "components"; - the notation for the relations or functions - introduced in each script, is shown in parentheses (? are placeholders). - @@ -130,5 +134,12 @@ + + Informational pages on the parts of the specification: + + Core. + + +
    diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index dada75abd..027c6b1d9 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -24,7 +24,7 @@ Summary of the Specification - Here is a numerical acount of the specification's contents + Here is a numerical account of the specification's contents and its timeline.
    diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 29d687e7f..9a19a7715 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -13,7 +13,7 @@ table { class "orange" [ { "MLTT1" * } { [ { "" * } { - [ "genv_primitive" "judgement" * ] + [ "genv_primitive" "judgment" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 6b5037b85..93b218306 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -20,7 +20,7 @@ --> Summary of the Specification - Here is a numerical acount of the specification's contents + Here is a numerical account of the specification's contents and its timeline.
    @@ -49,7 +49,7 @@ Lazy equivalence on local environments - addded as q-step to rst-computation on closures + added as q-step to rst-computation on closures (anniversary milestone). diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 0714b94ec..fe54a52fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -229,7 +229,7 @@ table { [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_lreq" + "frees_lift" * ] } ] - [ { "contxt-sensitive multiple rt-substitution" * } { + [ { "context-sensitive multiple rt-substitution" * } { [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } ] @@ -264,7 +264,7 @@ table { [ "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ] } ] - [ { "contxt-sensitive ordinary rt-substitution" * } { + [ { "context-sensitive ordinary rt-substitution" * } { [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml index 9c79f972c..af06ffa1d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml @@ -8,7 +8,7 @@ Summary of the Specification - Here is a numerical acount of the specification's contents + Here is a numerical account of the specification's contents and its timeline.
    -- 2.39.2