X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=eaa539756361fd4ffbe76b12d40f63239b00c76a;hb=b8a14a6fab91a49325c4a9cea1ca1e6cd19c2d8f;hp=dab3a5e30354ecd047f63458d0a7774ea9fee20f;hpb=bca27d3594ce368ee5afb6bc6300a6254c4b45d9;p=helm.git
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html
index dab3a5e30..eaa539756 100644
--- a/helm/www/lambda_delta/ld_basic_2.html
+++ b/helm/www/lambda_delta/ld_basic_2.html
@@ -15,10 +15,16 @@
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
Logical structure of the contribution
- The source files are grouped in planes and components according to the following table.
- | component | plane | files |
|
|
|
| examples |
|
|
|
|
|
| native typing |
| nty |
|
|
|
| conversion | context-sensitive | cpcs |
|
|
|
| computation | strongly normalizing | csn |
|
|
|
| context-sensitive | cprs |
|
|
|
| reducibility | context-sensitive reduction | lcpr |
|
|
|
|
| cpr | cpr_lift | cpr_ltpr | cpr_cpr |
| context-free normal forms | tnf |
|
|
|
| context-free reduction | ltpr | ltpr_ldrop |
|
|
|
| tpr | tpr_lift | tpr_tpss | tpr_tpr |
| context-free reducible forms | trf |
|
|
|
| static typing | atomic arity ass. | aaa | aaa_lift | aaa_aaa |
|
| static type ass. | sty | sty_lift | sty_sty |
|
| unfold | partial | ltpss | ltpss_ldrop | ltpss_tps | ltpss_ltpss |
|
| tpss | tpss_lift | tpss_tpss | tpss_ltps |
| substitution | parallel | ltps | ltps_ldrop | ltps_tps | ltps_ltps |
|
| tps | tps_lift | tps_tps |
|
| local env. dropping | ldrop | ldrop_ldrop |
|
|
| term relocation | lift | lift_lift |
|
|
| grammar | local env. ref. for substitution | lsubs | lsubs_lsubs |
|
|
| term hom. | thom | thom_thom |
|
|
| closures | cl_shift | cl_weight |
|
|
| internal syntax | lenv | lenv_weight | lenv_length |
|
|
| term | term_weight | term_simple |
|
|
| item |
|
|
|
| external syntax | aarity |
|
|
|
| parameters | sh |
|
|
|
The source files are grouped in planes and components
+ according to the following table.
+ The notation for the relation or function 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_ldrops |
|
|
| generic relocation | lifts ( â§*[?] ? â¡ ? ) | lifts_lifts | lifts_vector |
|
| substitution | parallel substitution | ltps ( ? [?,?] ⶠ? ) | ltps_ldrop | ltps_tps | ltps_ltps |
|
| tps ( ? ⢠? [?,?] ⶠ? ) | tps_lift | tps_tps |
|
| global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop |
|
|
| local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_ldrop |
|
|
| term relocation | lift ( â§[?,?] ? â¡ ? ) | lift_lift | lift_vector |
|
| 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
- The source files are grouped in directories, one for each component.
-
+ The source files are grouped in directories, one for each
+ component.
+
+
Last update: 2012-01-08+01:00
![[lambda_delta home]](http://lambda-delta.info/images/crux_32.png "lambda_delta home")
![[Spacer]](http://lambda-delta.info/images/rainbow.png "lambda_delta rainbow rule")
![[Generated from XML via XSL]](http://lambda-delta.info/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://lambda-delta.info/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")