From ae7427e8d3c57ccc77931e27913d8605d385cbda Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 15 Mar 2012 18:57:05 +0000 Subject: [PATCH] some renaming (ld_ prefix removed from file names) --- .../{ld_apps_2.html => apps_2.html} | 2 +- helm/www/lambda_delta/basic_2.html | 73 +++++++++++++++++ helm/www/lambda_delta/ld_basic_2.html | 73 ----------------- helm/www/lambda_delta/news.html | 6 +- .../{ld_apps_2.ldw.xml => apps_2.ldw.xml} | 4 +- .../{ld_apps_2_src.tbl => apps_2_src.tbl} | 0 .../{ld_basic_2.ldw.xml => basic_2.ldw.xml} | 6 +- .../{ld_basic_2_blk.tbl => basic_2_blk.tbl} | 0 .../{ld_basic_2_src.tbl => basic_2_src.tbl} | 0 helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl | 80 ------------------- 10 files changed, 82 insertions(+), 162 deletions(-) rename helm/www/lambda_delta/{ld_apps_2.html => apps_2.html} (86%) create mode 100644 helm/www/lambda_delta/basic_2.html delete mode 100644 helm/www/lambda_delta/ld_basic_2.html rename helm/www/lambda_delta/web/home/{ld_apps_2.ldw.xml => apps_2.ldw.xml} (96%) rename helm/www/lambda_delta/web/home/{ld_apps_2_src.tbl => apps_2_src.tbl} (100%) rename helm/www/lambda_delta/web/home/{ld_basic_2.ldw.xml => basic_2.ldw.xml} (95%) rename helm/www/lambda_delta/web/home/{ld_basic_2_blk.tbl => basic_2_blk.tbl} (100%) rename helm/www/lambda_delta/web/home/{ld_basic_2_src.tbl => basic_2_src.tbl} (100%) delete mode 100644 helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl diff --git a/helm/www/lambda_delta/ld_apps_2.html b/helm/www/lambda_delta/apps_2.html similarity index 86% rename from helm/www/lambda_delta/ld_apps_2.html rename to helm/www/lambda_delta/apps_2.html index e6634f9aa..0344bee55 100644 --- a/helm/www/lambda_delta/ld_apps_2.html +++ b/helm/www/lambda_delta/apps_2.html @@ -51,7 +51,7 @@ The notation for the relations or functions introduced in each file is shown in parentheses. -
componentplanefiles
MLTT1
genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
+
Physical Structure of the Specification
The source files are grouped in directories, diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html new file mode 100644 index 000000000..65a801e7e --- /dev/null +++ b/helm/www/lambda_delta/basic_2.html @@ -0,0 +1,73 @@ + + + + + + + + + + lambda_delta version 2 + + + + + +
[lambda_delta home]
cic:/matita/lambda_delta/basic_2/ (λδ version 2)
[Spacer]
+
System's Syntax and Behavior
+
This is a summary of the "block structure" + of the System's syntactic items and reductions. +
+
+
* In terms only. + ** In terms and local environments only. + *** In global environments only. + **** Sort level k in terms only. +
+ +
Summary of the Specification
+
Here is a numerical acount of the specification's contents + and its timeline. +
+
categoryobjects




sizesfiles113bytes422759

propositionstheorems45lemmas450total495
conceptsdeclared31defined39total70
+
  • In progress. + Context-sensitive subject equivalence + for native type assignment. +
+
  • In progress. + Context-sensitive subject equivalence + for atomic arity assignment. +
+
  • 2012 March 15. + Context-sensitive strong normalization + for simply typed terms. +
+
  • 2012 January 27. + Support for abstract candidates of reducibility. +
+
  • 2011 September 21. + Confluence for context-sensitive parallel reduction. +
+
  • 2011 September 6. + Confluence for context-free parallel reduction. +
+
  • 2011 April 17. + Specification starts. +
+ +
Logical Structure of the Specification
+
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. +
+
+ +
Physical Structure of the Specification
+
The source files are grouped in directories, + one for each component. +
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-03-15+01:00
+ + diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html deleted file mode 100644 index 8d1fc3ea5..000000000 --- a/helm/www/lambda_delta/ld_basic_2.html +++ /dev/null @@ -1,73 +0,0 @@ - - - - - - - - - - lambda_delta version 2 - - - - - -
[lambda_delta home]
cic:/matita/lambda_delta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" - of the System's syntactic items and reductions. -
-
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
- -
Summary of the Specification
-
Here is a numerical acount of the specification's contents - and its timeline. -
-
categoryobjects




sizesfiles113bytes422759

propositionstheorems45lemmas450total495
conceptsdeclared31defined39total70
-
  • In progress. - Context-sensitive subject equivalence - for native type assignment. -
-
  • In progress. - Context-sensitive subject equivalence - for atomic arity assignment. -
-
  • 2012 March 15. - Context-sensitive strong normalization - for simply typed terms. -
-
  • 2012 January 27. - Support for abstract candidates of reducibility. -
-
  • 2011 September 21. - Confluence for context-sensitive parallel reduction. -
-
  • 2011 September 6. - Confluence for context-free parallel reduction. -
-
  • 2011 April 17. - Specification starts. -
- -
Logical Structure of the Specification
-
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. -
-
componentplanefiles





examples







native typing
nty





equivalencecontext-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )





conversioncontext-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc




computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa




csn ( ⬇* ? )csn_liftcsn_cprcsn_cprs ( ⬇** ? )csn_lcpr


context-sensitive computationlcprs ( ? ⊢ ➡* ? )lcprs_cprslcprs_lcprs





cprs (? ⊢ ? ➡* ?)cprs_liftcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba



support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa



reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift





context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_cpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr


context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif




context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps





tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr



context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )




static typingstatic type assignmentstysty_liftsty_sty




local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_aaa



parameterssh





unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift





partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss




tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps



generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops




generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector






lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts




support for generic relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2


substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps




tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps




global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop





basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop





basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector






lift ( ⇧[?,?] ? ≡ ? )lift_lift




grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs





same head term formtshf ( ? ≈ ? )tshf_tshf





same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector




closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )





internal syntaxgenv







lenvlenv_weight ( #[?] )lenv_length ( |?| )





termterm_weight ( #[?] )term_simple ( 𝐒[?] )term_vector




item






external syntaxaarity





- -
Physical Structure of the Specification
-
The source files are grouped in directories, - one for each component. -
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-03-15+01:00
- - diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html index 388833406..987949365 100644 --- a/helm/www/lambda_delta/news.html +++ b/helm/www/lambda_delta/news.html @@ -71,10 +71,10 @@ restarted in Matita 0.5.
    -
  • Here is a page about +
  • Here is a page about the topics related to the specification (Applications).
    • -
  • Here is a page about +
  • Here is a page about the specification (Core).
    • @@ -279,7 +279,7 @@ relocation functions: s,

    - Last update 2012-02-24 by Ferruccio Guidi
diff --git a/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml b/helm/www/lambda_delta/web/home/apps_2.ldw.xml similarity index 96% rename from helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml rename to helm/www/lambda_delta/web/home/apps_2.ldw.xml index 5c6e7859e..253fbdc87 100644 --- a/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml +++ b/helm/www/lambda_delta/web/home/apps_2.ldw.xml @@ -23,7 +23,7 @@ Here is a numerical acount of the specification's contents and its timeline. - +
The Applications directory is started. @@ -42,7 +42,7 @@ The notation for the relations or functions introduced in each file is shown in parentheses. -
+
Physical Structure of the Specification
The source files are grouped in directories, diff --git a/helm/www/lambda_delta/web/home/ld_apps_2_src.tbl b/helm/www/lambda_delta/web/home/apps_2_src.tbl similarity index 100% rename from helm/www/lambda_delta/web/home/ld_apps_2_src.tbl rename to helm/www/lambda_delta/web/home/apps_2_src.tbl diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/basic_2.ldw.xml similarity index 95% rename from helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml rename to helm/www/lambda_delta/web/home/basic_2.ldw.xml index a542cc19a..6a1f30239 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml +++ b/helm/www/lambda_delta/web/home/basic_2.ldw.xml @@ -9,7 +9,7 @@ This is a summary of the "block structure" of the System's syntactic items and reductions. -
+
* In terms only. ** In terms and local environments only. *** In global environments only. @@ -20,7 +20,7 @@ Here is a numerical acount of the specification's contents and its timeline. -
+
Context-sensitive subject equivalence for native type assignment. @@ -53,7 +53,7 @@ The notation for the relations or functions introduced in each file is shown in parentheses. -
+
Physical Structure of the Specification
The source files are grouped in directories, diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl similarity index 100% rename from helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl rename to helm/www/lambda_delta/web/home/basic_2_blk.tbl diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl similarity index 100% rename from helm/www/lambda_delta/web/home/ld_basic_2_src.tbl rename to helm/www/lambda_delta/web/home/basic_2_src.tbl diff --git a/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl b/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl deleted file mode 100644 index c6ba91d7c..000000000 --- a/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl +++ /dev/null @@ -1,80 +0,0 @@ - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
- - - -- 2.39.2