From: Ferruccio Guidi Date: Thu, 22 Nov 2012 15:08:05 +0000 (+0000) Subject: - additions in basic_2 X-Git-Tag: make_still_working~1451 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5b6caf1bdfc7a41aea3a1437ad666fd87654a899;p=helm.git - additions in basic_2 - bugfix in BTM.html --- diff --git a/helm/www/lambda_delta/BTM.html b/helm/www/lambda_delta/BTM.html index a0fba18ee..d41ec154b 100644 --- a/helm/www/lambda_delta/BTM.html +++ b/helm/www/lambda_delta/BTM.html @@ -18,8 +18,8 @@
This table shows how the first 45 positive integers are distributed in the four classes.
-
+
classcontents














p
147101316192225283134374043
q
5111517232933354145




s
268141820242632384244


t
39122127303639






-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-18T16:59:43+02:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-11-22T16:07:02+01:00
diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html index b02fa0daf..f77bae790 100644 --- a/helm/www/lambda_delta/apps_2.html +++ b/helm/www/lambda_delta/apps_2.html @@ -57,6 +57,6 @@
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-18T16:59:43+02:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-11-22T16:07:02+01:00
diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index cea859d38..c51e61ef2 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -29,7 +29,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles204bytes742579

propositionstheorems74lemmas889total963
conceptsdeclared40defined73total113
+
categoryobjects




sizesfiles226characters427252

propositionstheorems82lemmas981total1063
conceptsdeclared43defined76total119
-
componentplanefiles



dynamic typingstratified native validitysnv ( ⦃?,?⦄ ⊩ ? :[?] )snv_lift snv_aaa


equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs



context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs


conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc



context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc


computationextended computationxprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )xprs_lift xprs_aaa xprs_cprs



weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe



strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa




csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr


focalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_cprs lfprs_lfprs




fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs



context-sensitive computationcprs (? ⊢ ? ➡* ?)cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector



context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs



tprs ( ? ➡* ?)tprs_lift tprs_tprs



local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba



support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )acp_aaa

reducibilityextended reductionxpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )xpr_lift xpr_aaa



context-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr



context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr



fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr



context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif



context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr



context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append

context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )




context-free reductionltpr ( ? ➡ ? )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 typinglocal env. ref. for stratified static type assignmentlsubss ( ? ⁝⊑ ? )lsubss_ldrop lsubss_ssta lsubss_lsubss



stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta



local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa



parametersshsd


unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift



inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift


partial unfoldltpss_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_lifttpss_tpss

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrop ldrops_ldrops



generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector




lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts



support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps



global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop



basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop



local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )(lsubs_lsubs)lsubs_sfr ( ≽[?,?] ? )


basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector




lift ( ⇧[?,?] ? ≡ ? )lift_lift


grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf)



same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector



closurescl_shift ( ? @@ ? )cl_weight ( #{?,?} )



internal syntaxgenv





lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bi


termterm_weight ( #{?} )term_simple ( 𝐒⦃?⦄ )term_vector


item




external syntaxaarity



+
componentplanefiles



dynamic typingstratified native validitysnv ( ⦃?,?⦄ ⊩ ? :[?] )snv_lift snv_aaa snv_ssta


equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs




fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs



local env. ref. for context-sensitive equivalencelsubse ( ? ⊢•⊑[?] ? )lsubse_ldrop lsubse_ssta lsubse_cpcs



context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs


conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc




fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc



context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc


computationextended computationxprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )xprs_lift xprs_aaa xpr_lsubss xprs_cprs xprs_xprs



weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe



strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa




csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr


focalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_cprs lfprs_lfprs




fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs



context-sensitive computationcprs (? ⊢ ? ➡* ?)cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector



context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs



tprs ( ? ➡* ?)tprs_lift tprs_tprs



local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba



support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )acp_aaa

reducibilityextended reductionxpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )xpr_lift xpr_aaa xpr_lsubss



context-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr



context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr



fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr



context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif



context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr



context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append

context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )




context-free reductionltpr ( ? ➡ ? )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 typinglocal env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_lsubss



stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta



local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa



parametersshsd


unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift



inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift


partial unfoldltpss_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_lifttpss_tpss

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrop ldrops_ldrops



iterated restricted structural predecessor for closuresfrsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )frsups_frsups




frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )frsupp_frsupp



generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector




lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts



support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps



global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop



basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop



local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )(lsubs_lsubs)lsubs_sfr ( ≽[?,?] ? )


restricted structural predecessor for closuresfrsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )




basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector




lift ( ⇧[?,?] ? ≡ ? )lift_lift


grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf)



same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector



closurescl_shift ( ? @@ ? )cl_weight ( #{?,?} )



internal syntaxgenv





lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bi


termterm_weight ( #{?} )term_simple ( 𝐒⦃?⦄ )term_vector


item




external syntaxaarity



Physical Structure of the Specification
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-10-18T16:59:43+02:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-11-22T16:07:02+01:00
diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl index 776012207..28aacba87 100644 --- a/helm/www/lambda_delta/web/home/basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl @@ -40,7 +40,7 @@ table { ] *) [ { "stratified native validity" * } { - [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" * ] + [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" + "snv_ssta" * ] } ] } @@ -49,6 +49,11 @@ table { [ { "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" * } { @@ -60,7 +65,8 @@ table { class "sky" [ { "conversion" * } { [ { "focalized conversion" * } { - [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ] + [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ] + [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ] } ] [ { "context-sensitive conversion" * } { @@ -71,8 +77,15 @@ table { ] class "cyan" [ { "computation" * } { +(* + [ { "hyper computation" * } { + [ "ysteps ( ? ⊢ ⦃?,?⦄ •⭃*[g] ⦃?,?⦄ )" "ysteps_csups" * ] + [ "yprs ( ? ⊢ ⦃?,?⦄ •⥸*[g] ⦃?,?⦄ )" "yprs_csups" + "yprs_xprs" + "yprs_yprs" * ] + } + ] +*) [ { "extended computation" * } { - [ "xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )" "xprs_lift" + "xprs_aaa" + "xprs_cprs" * ] + [ "xprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )" "xprs_lift" + "xprs_aaa" + "xpr_lsubss" + "xprs_cprs" + "xprs_xprs" * ] } ] [ { "weakly normalizing computation" * } { @@ -86,7 +99,7 @@ table { ] [ { "focalized computation" * } { [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_cprs" + "lfprs_lfprs" * ] - [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] + [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] } ] [ { "context-sensitive computation" * } { @@ -110,8 +123,14 @@ table { ] class "water" [ { "reducibility" * } { +(* + [ { "hyper reduction" * } { + [ "ypr ( ? ⊢ ⦃?,?⦄ •⥸[g] ⦃?,?⦄ )" * ] + } + ] +*) [ { "extended reduction" * } { - [ "xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )" "xpr_lift" + "xpr_aaa" * ] + [ "xpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )" "xpr_lift" + "xpr_aaa" + "xpr_lsubss" * ] } ] [ { "context-sensitive focalized reduction" * } { @@ -163,7 +182,7 @@ table { class "grass" [ { "static typing" * } { [ { "local env. ref. for stratified static type assignment" * } { - [ "lsubss ( ? ⁝⊑ ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ] + [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ] } ] [ { "stratified static type assignment" * } { @@ -204,6 +223,11 @@ table { [ "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" * ] @@ -233,6 +257,10 @@ table { [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ] } ] + [ { "restricted structural predecessor for closures" * } { + [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ] + } + ] [ { "basic term relocation" * } { [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]