X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=2fa39845b66689d7259a7225e324650c6aadf7c3;hb=5cf322d1dd867701a2ef715f499f482f0b3d56aa;hp=0bd2b8a1e03b769b355f55478d394263972f88bd;hpb=baba23b670cb20eb478975fa9cb419c7ae58f7bc;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 0bd2b8a1e..2fa39845b 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -29,7 +29,7 @@
category | objects | |||||
sizes | files | 228 | characters | 430859 | nodes | 1197040 |
propositions | theorems | 82 | lemmas | 1004 | total | 1086 |
concepts | declared | 43 | defined | 76 | total | 119 |
category | objects | |||||
sizes | files | 232 | characters | 452299 | nodes | 1250421 |
propositions | theorems | 83 | lemmas | 1043 | total | 1126 |
concepts | declared | 43 | defined | 76 | total | 119 |
component | plane | files | ||||
dynamic typing | stratified native validity | snv ( �,?⦠⩠? :[?] ) | snv_lift snv_aaa snv_ssta snv_ltpr | |||
equivalence | focalized equivalence | lfpcs ( â¦?⦠â¬* â¦?⦠) | lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs | |||
fpcs ( â¦?,?⦠â¬* â¦?,?⦠) | fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs | |||||
local env. ref. for context-sensitive equivalence | lsubse ( ? â¢â¢â[?] ? ) | lsubse_ldrop lsubse_ssta lsubse_cpcs | ||||
context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) | cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs | ||||
conversion | focalized conversion | lfpc ( �⦠⬠�⦠) | lfpc_lfpc | |||
fpc ( �,?⦠⬠�,?⦠) | fpc_fpc | |||||
context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||
computation | extended computation | xprs ( â¦?,?⦠⢠? â¢â¡*[?] ? ) | xprs_lift xprs_aaa xpr_lsubss xprs_cprs xprs_xprs | |||
weakly normalizing computation | cpe ( ? ⢠â¡* ðâ¦?⦠) | cpe_cpe | ||||
strongly normalizing computation | csn_vector ( ? ⢠â¬* ? ) | csn_cpr_vector csn_tstc_vector csn_aaa | ||||
csn ( ? ⢠â¬* ? ) | csn_alt ( ? ⢠â¬â¬* ? ) | csn_lift csn_cpr csn_lfpr | ||||
focalized computation | lfprs ( â¦?⦠â¡* â¦?⦠) | lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs | ||||
fprs ( â¦?,?⦠â¡* â¦?,?⦠) | fprs_aaa fprs_fprs | |||||
context-sensitive computation | cprs (? ⢠? â¡* ?) | cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector | ||||
context-free computation | ltprs ( ? â¡* ? ) | ltprs_alt ( ? â¡â¡* ? ) | ltprs_ldrop ltprs_ltprs | |||
tprs ( ? â¡* ?) | tprs_lift tprs_tprs | |||||
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 | extended reduction | xpr ( â¦?,?⦠⢠? â¢â¡[?] ? ) | xpr_lift xpr_aaa xpr_lsubss | |||
context-sensitive focalized reduction | cfpr ( ? ⢠�,?⦠⡠�,?⦠) | cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr | ||||
context-free focalized reduction | lfpr ( â¦?⦠⡠â¦?⦠) | lfpr_alt ( â¦?⦠â¡â¡ â¦?⦠) | lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr | |||
fpr ( �,?⦠⡠�,?⦠) | fpr_cpr fpr_fpr | |||||
context-sensitive normal forms | cnf ( ? ⢠ðâ¦?⦠) | cnf_lift cnf_cif | ||||
context-sensitive reduction | cpr ( ? ⢠? ⡠? ) | cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr | ||||
context-sensitive reducible forms | crf ( ? ⢠ðâ¦?⦠) | crf_append | cif ( ? ⢠ðâ¦?⦠) | cif_append | ||
context-free normal forms | thnf ( ððâ¦?⦠) | |||||
context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr | ||||
tpr ( ? â¡ ? ) | tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr | |||||
unwind | ||||||
static typing | local env. ref. for stratified static type assignment | lsubss ( ? â¢â[?] ? ) | lsubss_ldrop lsubss_ssta lsubss_lsubss | |||
stratified static type assignment | ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) | ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta | ||||
local env. ref. for atomic arity assignment | lsuba ( ? ââ ? ) | lsuba_ldrop lsuba_aaa lsuba_lsuba | ||||
atomic arity assignment | aaa ( ? ⢠? â ? ) | aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa | ||||
parameters | sh | sd | ||||
unfold | basic local env. thinning | thin ( ? â¼*[?,?] â¡ ? ) | thin_ldrop thin_delift | |||
inverse basic term relocation | delift ( ? ⢠? â¼*[?,?] â¡ ? ) | delift_alt ( ? ⢠? â¼â¼*[?,?] â¡ ? ) | delift_lift delift_tpss delift_ltpss delift_delift | |||
partial unfold | ltpss_sn ( ? ⢠â¶*[?,?] ? ) | ltpss_sn_alt ( ? ⢠â¶â¶*[?,?] ? ) | ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn | |||
ltpss_dx ( ? â¶*[?,?] ? ) | ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx | |||||
tpss ( ? ⢠? â¶*[?,?] ? ) | tpss_alt ( ? ⢠? â¶â¶*[?,?] ? ) | tpss_lift | tpss_tpss | |||
generic local env. slicing | ldrops ( â©*[?] ? â¡ ? ) | ldrops_ldrop ldrops_ldrops | ||||
iterated restricted structural predecessor for closures | frsups ( â¦?,?⦠â§* â¦?,?⦠) | frsups_frsups | ||||
frsupp ( â¦?,?⦠â§+ â¦?,?⦠) | frsupp_frsupp | |||||
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_append ldrop_lpx ldrop_sfr ldrop_ldrop | ||||
local env. ref. for substitution | lsubs ( ? â¼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( â½[?,?] ? ) | |||
restricted structural predecessor for closures | frsup ( �,?⦠⧠�,?⦠) | |||||
basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | ||||
lift ( â§[?,?] ? â¡ ? ) | lift_lift | |||||
grammar | 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 ( |?| ) | lenv_append ( ? @@ ? ) | lenv_px lenv_px_bi | ||
term | term_weight ( â¯{?} ) | term_simple ( ðâ¦?⦠) | term_vector | |||
item | ||||||
external syntax | aarity |
component | plane | files | ||||
dynamic typing | stratified native validity | snv ( �,?⦠⩠? :[?] ) | snv_lift snv_aaa snv_ssta snv_ltpr | |||
equivalence | focalized equivalence | lfpcs ( â¦?⦠â¬* â¦?⦠) | lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs | |||
fpcs ( â¦?,?⦠â¬* â¦?,?⦠) | fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs | |||||
local env. ref. for context-sensitive equivalence | lsubse ( ? â¢â¢â[?] ? ) | lsubse_ldrop lsubse_ssta lsubse_cpcs | ||||
context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) | cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs | ||||
conversion | focalized conversion | lfpc ( �⦠⬠�⦠) | lfpc_lfpc | |||
fpc ( �,?⦠⬠�,?⦠) | fpc_fpc | |||||
context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||
computation | decomposed extended computation | dxprs ( â¦?,?⦠⢠? â¢*â¡*[?] ? ) | dxprs_lift dxprs_aaa dxpr_lsubss dxprs_dxprs | |||
weakly normalizing computation | cpe ( ? ⢠â¡* ðâ¦?⦠) | cpe_cpe | ||||
strongly normalizing computation | csn_vector ( ? ⢠â¬* ? ) | csn_cpr_vector csn_tstc_vector csn_aaa | ||||
csn ( ? ⢠â¬* ? ) | csn_alt ( ? ⢠â¬â¬* ? ) | csn_lift csn_cpr csn_lfpr | ||||
focalized computation | lfprs ( â¦?⦠â¡* â¦?⦠) | lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs | ||||
fprs ( â¦?,?⦠â¡* â¦?,?⦠) | fprs_aaa fprs_fprs | |||||
context-sensitive computation | cprs (? ⢠? â¡* ?) | cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector | ||||
context-free computation | ltprs ( ? â¡* ? ) | ltprs_alt ( ? â¡â¡* ? ) | ltprs_ldrop ltprs_ltprs | |||
tprs ( ? â¡* ?) | tprs_lift tprs_tprs | |||||
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 focalized reduction | cfpr ( ? ⢠�,?⦠⡠�,?⦠) | cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr | |||
context-free focalized reduction | lfpr ( â¦?⦠⡠â¦?⦠) | lfpr_alt ( â¦?⦠â¡â¡ â¦?⦠) | lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr | |||
fpr ( �,?⦠⡠�,?⦠) | fpr_cpr fpr_fpr | |||||
context-sensitive normal forms | cnf ( ? ⢠ðâ¦?⦠) | cnf_lift cnf_cif | ||||
context-sensitive reduction | cpr ( ? ⢠? ⡠? ) | cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr | ||||
context-sensitive reducible forms | crf ( ? ⢠ðâ¦?⦠) | crf_append | cif ( ? ⢠ðâ¦?⦠) | cif_append | ||
context-free normal forms | thnf ( ððâ¦?⦠) | |||||
context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr | ||||
tpr ( ? â¡ ? ) | tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr | |||||
unwind | iterated stratified static type assignment | sstas ( â¦?,?⦠⢠? â¢*[?] ? ) | sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas | |||
static typing | local env. ref. for stratified static type assignment | lsubss ( ? â¢â[?] ? ) | lsubss_ldrop lsubss_ssta lsubss_lsubss | |||
stratified static type assignment | ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) | ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta | ||||
local env. ref. for atomic arity assignment | lsuba ( ? ââ ? ) | lsuba_ldrop lsuba_aaa lsuba_lsuba | ||||
atomic arity assignment | aaa ( ? ⢠? â ? ) | aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa | ||||
parameters | sh | sd | ||||
unfold | basic local env. thinning | thin ( ? â¼*[?,?] â¡ ? ) | thin_ldrop thin_delift | |||
inverse basic term relocation | delift ( ? ⢠? â¼*[?,?] â¡ ? ) | delift_alt ( ? ⢠? â¼â¼*[?,?] â¡ ? ) | delift_lift delift_tpss delift_ltpss delift_delift | |||
partial unfold | ltpss_sn ( ? ⢠â¶*[?,?] ? ) | ltpss_sn_alt ( ? ⢠â¶â¶*[?,?] ? ) | ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn | |||
ltpss_dx ( ? â¶*[?,?] ? ) | ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx | |||||
tpss ( ? ⢠? â¶*[?,?] ? ) | tpss_alt ( ? ⢠? â¶â¶*[?,?] ? ) | tpss_lift | tpss_tpss | |||
generic local env. slicing | ldrops ( â©*[?] ? â¡ ? ) | ldrops_ldrop ldrops_ldrops | ||||
iterated restricted structural predecessor for closures | frsups ( â¦?,?⦠â§* â¦?,?⦠) | frsups_frsups | ||||
frsupp ( â¦?,?⦠â§+ â¦?,?⦠) | frsupp_frsupp | |||||
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_append ldrop_lpx ldrop_sfr ldrop_ldrop | ||||
local env. ref. for substitution | lsubs ( ? â¼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( â½[?,?] ? ) | |||
restricted structural predecessor for closures | frsup ( �,?⦠⧠�,?⦠) | |||||
basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | ||||
lift ( â§[?,?] ? â¡ ? ) | lift_lift | |||||
grammar | 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 ( |?| ) | lenv_append ( ? @@ ? ) | lenv_px lenv_px_bi | ||
term | term_weight ( â¯{?} ) | term_simple ( ðâ¦?⦠) | term_vector | |||
item | ||||||
external syntax | aarity |