X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fbasic_2.html;h=734f9a84db5d24daf86541728a4761cc3a2be3f0;hb=f8d439221f776979c62409c12ca223cfdf91c584;hp=2094c96026e325fafb7ef0cc59bad72cad8588f7;hpb=6f7c6b72cc2b8574333de5dee02ef60c2638abde;p=helm.git diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 2094c9602..734f9a84d 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -29,7 +29,7 @@
category | objects | |||||
sizes | files | 134 | bytes | 494214 | ||
propositions | theorems | 58 | lemmas | 531 | total | 589 |
concepts | declared | 34 | defined | 42 | total | 76 |
category | objects | |||||
sizes | files | 142 | bytes | 523918 | ||
propositions | theorems | 59 | lemmas | 572 | total | 631 |
concepts | declared | 35 | defined | 44 | total | 79 |
component | plane | files | |||||||
examples | |||||||||
dynamic typing | native type assignment | nta ( �,?⦠⢠? : ? ) | nta_lift | ||||||
equivalence | context-sensitive equivalence | lcpcs ( ? ⢠â¬* ? ) | lcpcs_aaa | lcpcs_lcprs | lcpcs_lcpcs | ||||
cpcs ( ? ⢠? â¬* ? ) | cpcs_cprs | cpcs_cpcs | |||||||
conversion | context-sensitive conversion | lcpc ( ? ⢠⬠? ) | lcpc_lcpc | ||||||
cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||||||
computation | weakly normalizing computation | cpe ( ? ⢠? ⢠â¡* ð[?] ) | cpe_cpe | ||||||
strongly normalizing computation | csn_vector ( â¬* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa | |||||
csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr | |||||
context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_aaa | lcprs_cprs | lcprs_lcprs | |||||
cprs (? ⢠? â¡* ?) | cprs_lift | cprs_ltpr | 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_aaa | lcpr_cpr | lcpr_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 | ltpr_ltpss | ltpr_aaa | ltpr_ltpr | |||
tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_tpr | ||||||
context-free reducible forms | trf ( ð[?] ) | tif ( ð[?] ) | |||||||
static typing | static type assignment | sta ( �,?⦠⢠? ⢠? ) | sta_lift | sta_sta | |||||
local env. ref. for atomic arity assignment | lsuba ( ? ։ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | |||||
atomic arity assignment | aaa ( ? ⢠? ÷ ? ) | aaa_lift | aaa_lifts | aaa_ltpss | aaa_aaa | ||||
parameters | sh | ||||||||
unfold | term inverse relocation | delift ( ? ⢠? [?,?] ⡠? ) | delift_lift | ||||||
partial unfold | ltpss ( ? [?,?] â¶* ? ) | ltpss_ldrop | ltpss_tps | ltpss_tpss | ltpss_ltpss | ||||
tpss ( ? ⢠? [?,?] â¶* ? ) | tpss_lift | tpss_tpss | tpss_alt ( ? ⢠? [?,?] â¶â¶* ? ) | ||||||
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 | 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 |
component | plane | files | |||||||
examples | |||||||||
dynamic typing | native type assignment | nta ( �,?⦠⢠? : ? ) | nta_lift | nta_sta | |||||
equivalence | context-sensitive equivalence | lcpcs ( ? ⢠â¬* ? ) | lcpcs_aaa | lcpcs_lcprs | lcpcs_lcpcs | ||||
cpcs ( ? ⢠? â¬* ? ) | cpcs_cprs | cpcs_cpcs | |||||||
conversion | context-sensitive conversion | lcpc ( ? ⢠⬠? ) | lcpc_lcpc | ||||||
cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||||||
computation | weakly normalizing computation | cpe ( ? ⢠? ⢠â¡* ð[?] ) | cpe_cpe | ||||||
strongly normalizing computation | csn_vector ( â¬* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa | |||||
csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr | |||||
context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_aaa | lcprs_cprs | lcprs_lcprs | |||||
cprs (? ⢠? â¡* ?) | cprs_lift | cprs_ltpr | 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_aaa | lcpr_cpr | lcpr_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 | ltpr_ltpss | ltpr_aaa | ltpr_ltpr | |||
tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_tpr | ||||||
context-free reducible forms | trf ( ð[?] ) | tif ( ð[?] ) | |||||||
static typing | static type assignment | sta ( �,?⦠⢠? ⢠? ) | sta_lift | sta_sta | |||||
local env. ref. for atomic arity assignment | lsuba ( ? ։ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | |||||
atomic arity assignment | aaa ( ? ⢠? ÷ ? ) | aaa_lift | aaa_lifts | aaa_ltpss | aaa_aaa | ||||
parameters | sh | ||||||||
unfold | basic local env. thinning | thin ( ? [?,?] â¡ ? ) | thin_ldrop | thin_delift | |||||
inverse basic term relocation | delift ( ? ⢠? [?,?] â¡ ? ) | delift_lift | delift_tpss | delift_ltpss | delift_delift | delift_alt ( ? ⢠? [?,?] â¡â¡ ? ) | |||
partial unfold | ltpss ( ? [?,?] â¶* ? ) | ltpss_ldrop | ltpss_tps | ltpss_tpss | ltpss_ltpss | ||||
tpss ( ? ⢠? [?,?] â¶* ? ) | tpss_lift | tpss_tpss | tpss_alt ( ? ⢠? [?,?] â¶â¶* ? ) | ||||||
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 | 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 |