X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=024c7740fda40d2d96c40eb32820118c5232aab5;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=e11f31a628937f2763baee755cc17a3f34401fd7;hpb=c7e7b6d0e8a6d8c148832dad8122c68c969f1c7c;p=helm.git
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html
index e11f31a62..024c7740f 100644
--- a/helm/www/lambda_delta/ld_basic_2.html
+++ b/helm/www/lambda_delta/ld_basic_2.html
@@ -14,17 +14,50 @@
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
- Logical structure of the contribution
+ System's Syntax and Behavior
+ This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+
+ domain block leader applicator (with âθ)* reduction âζ * reference * {X | Π⢠X : W} typed abstraction ** Π⢠λW âV âβ no #i typed declaration *** Π⢠pλW no no no $p native type annotation * Π⢠â£W no no yes no {X | Π⢠X = V} local abbreviation ** Π⢠δV no local âδ yes #i global abbreviation *** Π⢠pδV no global âδ no $p no sort **** Π⢠âk no no no no
+ * 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.
+
+ category objects propositions theorems 43 lemmas 387 concepts declared 33 defined 49
+ In progress.
+ Context-sensitive strong normalization of simply typed terms.
+
+ 2012 January 27.
+ Support for abstract candidates of reducibility closed.
+
+ 2011 September 21.
+ Confluence of context-sensitive parallel reduction closed.
+
+ 2011 September 6.
+ Confluence of context-free parallel reduction closed.
+
+ 2011 April 17.
+ Specification started.
+
+
+ Logical Structure of the Specification
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.
- component plane files functional reduction and type machine rtm rtm_step ( ? ⨠? ) unfold lift ( â[?,?] ? ) subst ( [?â?] ? ) examples native typing nty conversion context-sensitive conversion cpcs ( ? ⢠? â¬* ? ) computation strongly normalizing computation csn ( â¬* ? ) csn_cr csn_aaa context-sensitive computation cprs (? ⢠? â¡* ?) support for abstract computation properties lsubc ( ? [?] â ? ) lsubc_ldrop lsubc_ldrops acp acp_cr ( â¦?,?⦠ϵ ã?ã ) acp_aaa reducibility context-sensitive reduction lcpr ( ? ⢠⡠? ) cpr ( ? ⢠? â¡ ? ) cpr_lift cpr_ltpr cpr_cpr context-free normal forms twhnf tnf context-free reduction ltpr ( ? â¡ ? ) ltpr_ldrop tpr ( ? â¡ ? ) tpr_lift tpr_tpss tpr_tpr context-free reducible forms trf static typing static type ass. sty sty_lift sty_sty atomic arity ass. aaa ( ? ⢠? ÷ ? ) aaa_lift aaa_aaa parameters sh unfold term inverse relocation delift ( ? ⢠? [?,?] â¡ ? ) delift_lift partial unfold ltpss ( ? [?,?] â¶* ? ) ltpss_ldrop ltpss_tps ltpss_ltpss tpss ( ? ⢠? [?,?] â¶* ? ) tpss_lift tpss_tpss tpss_ltps generic local env. slicing ldrops ( â©*[?] ? â¡ ? ) ldrops_ldrop ldrops_ldrops generic term relocation lifts_vector ( â§*[?] ? â¡ ? ) lifts_lift_vector lifts ( â§*[?] ? â¡ ? ) lifts_lift lifts_lifts support for generic relocation gr2 gr2_gr2 substitution parallel substitution ltps ( ? [?,?] ⶠ? ) ltps_ldrop ltps_tps ltps_ltps tps ( ? ⢠? [?,?] ⶠ? ) tps_lift tps_tps global env. slicing gdrop ( â©[?] ? â¡ ? ) gdrop_gdrop basic local env. slicing ldrop ( â©[?,?] ? â¡ ? ) ldrop_ldrop basic term relocation lift_vector ( â§[?,?] ? â¡ ? ) lift_lift_vector lift ( â§[?,?] ? â¡ ? ) lift_lift grammar local env. ref. for substitution lsubs ( ? [?,?] â¼ ? ) lsubs_lsubs term hom. thom thom_thom closures cl_shift ( ? @ ? ) cl_weight ( #[?,?] ) internal syntax genv lenv lenv_weight ( #[?] ) lenv_length ( |?| ) term term_weight ( #[?] ) term_simple term_vector item external syntax aarity
- Physical structure of the contribution
+ component plane files functional reduction and type machine rtm rtm_step ( ? ⨠? ) unfold lift ( â[?,?] ? ) subst ( [?â?] ? ) examples native typing nty conversion context-sensitive conversion cpcs ( ? ⢠? â¬* ? ) computation strongly normalizing computation csn_cr csn_aaa csn ( â¬* ? ) csn_lift csn_cpr csn_cprs ( â¬** ? ) csn_lcpr context-sensitive computation cprs (? ⢠? â¡* ?) cprs_lcpr cprs_cprs local env. ref. for abstract candidates of reducibility lsubc ( ? [?] â ? ) lsubc_ldrop lsubc_ldrops lsubc_lsuba support for abstract computation properties acp acp_cr ( â¦?,?⦠ϵ ã?ã ) acp_aaa reducibility context-sensitive normal forms cnf ( ? ⢠ð[?] ) cnf_lift context-sensitive reduction lcpr ( ? ⢠⡠? ) lcpr_cpr cpr ( ? ⢠? â¡ ? ) cpr_lift cpr_ltpss cpr_ltpr cpr_cpr context-free normal forms twhnf ( ððð[?] ) tnf ( ð[?] ) tnf_tif context-free reduction ltpr ( ? â¡ ? ) ltpr_ldrop ltpr_tps tpr ( ? â¡ ? ) tpr_lift tpr_tpss tpr_tpr context-free reducible forms trf ( ð[?] ) tif ( ð[?] ) static typing static type assignment sty sty_lift sty_sty local env. ref. for atomic arity assignment lsuba ( ? ÷â ? ) lsuba_ldrop lsuba_aaa lsuba_lsuba atomic arity assignment aaa ( ? ⢠? ÷ ? ) aaa_lift aaa_lifts aaa_aaa parameters sh unfold term inverse relocation delift ( ? ⢠? [?,?] â¡ ? ) delift_lift partial unfold ltpss ( ? [?,?] â¶* ? ) ltpss_ldrop ltpss_tps ltpss_ltpss tpss ( ? ⢠? [?,?] â¶* ? ) tpss_lift tpss_tpss tpss_ltps generic local env. slicing ldrops ( â©*[?] ? â¡ ? ) ldrops_ldrop ldrops_ldrops generic term relocation lifts_vector ( â§*[?] ? â¡ ? ) lifts_lift_vector lifts ( â§*[?] ? â¡ ? ) lifts_lift lifts_lifts support for generic relocation gr2 ( @ [ ? ] ? â¡ ? ) gr2_plus ( ? + ? ) gr2_minus ( ? â ? â¡ ? ) gr2_gr2 substitution parallel substitution ltps ( ? [?,?] ⶠ? ) ltps_ldrop ltps_tps ltps_ltps tps ( ? ⢠? [?,?] ⶠ? ) tps_lift tps_tps global env. slicing gdrop ( â©[?] ? â¡ ? ) gdrop_gdrop basic local env. slicing ldrop ( â©[?,?] ? â¡ ? ) ldrop_ldrop basic term relocation lift_vector ( â§[?,?] ? â¡ ? ) lift_lift_vector lift ( â§[?,?] ? â¡ ? ) lift_lift grammar local env. ref. for substitution lsubs ( ? [?,?] â¼ ? ) lsubs_lsubs term hom. thom ( ? â ? ) thom_thom closures cl_shift ( ? @ ? ) cl_weight ( #[?,?] ) internal syntax genv lenv lenv_weight ( #[?] ) lenv_length ( |?| ) term term_weight ( #[?] ) term_simple ( ð[?] ) term_vector item external syntax aarity
+
+ Physical Structure of the Specification
The source files are grouped in directories, one for each
component.
-
Last update: 2012-01-16+01:00
+
Last update: 2012-02-14+01:00