X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=d894aef118022e999a9e4dc83f9471358a811d31;hb=011cf6478141e69822a5b40933f2444d0522532f;hp=95ea6d8e11ef30d1e8926ca86e3ee1dbf3faa179;hpb=ce747c4d4c3a087e1f59dca81b7b4962ffa8e02b;p=helm.git
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html
index 95ea6d8e1..d894aef11 100644
--- a/helm/www/lambda_delta/ld_basic_2.html
+++ b/helm/www/lambda_delta/ld_basic_2.html
@@ -16,45 +16,49 @@
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
System's Syntax and Behavior
This is a summary of the "block structure"
- of the System's syntactic items and reductions.
+ 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.
+ ** 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.
+ and its timeline.
- category | objects |
|
|
|
propositions | theorems | 41 | lemmas | 369 |
concepts | declared | 33 | defined | 50 |
+ category | objects |
|
|
|
|
|
volume | files | 112 |
|
|
|
|
propositions | theorems | 45 | lemmas | 437 | total | 482 |
concepts | declared | 32 | defined | 38 | total | 70 |
+ - In progress.
+ Context-sensitive strong normalization of simply typed terms.
+
- 2012 January 27.
- Support for abstract candidates of reducibility closed.
+ Support for abstract candidates of reducibility closed.
- 2011 September 21.
- Confluence of context-sensitive parallel reduction closed.
+ Confluence of context-sensitive parallel reduction closed.
- 2011 September 6.
- Confluence of context-free parallel reduction closed.
+ Confluence of context-free parallel reduction closed.
- 2011 April 17.
- Specification started.
+ 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.
+ 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.
- 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_lift | csn_cr | csn_aaa |
|
| 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 ( ? ⢠⡠? ) |
|
|
|
|
|
| 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 |
|
|
|
|
+ component | plane | files |
|
|
|
|
|
|
examples |
|
|
|
|
|
|
|
|
native typing |
| nty |
|
|
|
|
|
|
equivalence | context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) |
|
|
|
|
|
|
conversion | context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc |
|
|
|
|
|
computation | strongly normalizing computation | csn_vector ( â¬* ? ) | csn_lcpr_vector | csn_aaa |
|
|
|
|
|
| csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr |
|
|
| context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_cprs | lcprs_lcprs |
|
|
|
|
|
| cprs (? ⢠? â¡* ?) | cprs_lift | cprs_lcpr | cprs_cprs | cprs_lcprs | cprs_tstc | cprs_tstc_vector |
| 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 |
|
|
|
|
|
| same head term form | tshf ( ? â ? ) | tshf_tshf |
|
|
|
|
|
| same top term constructor | tstc ( ? â ? ) | tstc_tstc | tstc_vector |
|
|
|
|
| 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.
+
The source files are grouped in directories,
+ one for each component.
-
Last update: 2012-02-09+01:00
+
Last update: 2012-03-09+01:00