From: Ferruccio Guidi Date: Sat, 13 Oct 2012 21:37:29 +0000 (+0000) Subject: updates in basic_2 ... X-Git-Tag: make_still_working~1495 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=43d727778aacdda8feb1228cf37860e7713930f2;p=helm.git updates in basic_2 ... --- diff --git a/helm/www/lambda_delta/BTM.html b/helm/www/lambda_delta/BTM.html index 41c28a032..f7ad18288 100644 --- a/helm/www/lambda_delta/BTM.html +++ b/helm/www/lambda_delta/BTM.html @@ -20,6 +20,6 @@
-
[Spacer]

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

Last update: 2012-09-29T23:49:46+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-10-13T23:29:26+02:00
diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html index e51042f00..3000958e8 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-09-29T23:49:46+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-10-13T23:29:26+02:00
diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 9bb35569b..108da399f 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




sizesfiles190bytes718106

propositionstheorems68lemmas859total927
conceptsdeclared40defined71total111
+
categoryobjects




sizesfiles199bytes739801

propositionstheorems70lemmas880total950
conceptsdeclared40defined72total112
-
componentplanefiles







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





equivalencecontext-sensitive equivalencelcpcs ( ? ⊢ ⬌* ? )lcpcs_aaalcpcs_lcprslcpcs_lcpcs






cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_ltprcpcs_cprscpcs_cpcs


conversioncontext-sensitive conversionlcpc ( ? ⊢ ⬌ ? )lcpc_lcpc








cpc ( ? ⊢ ? ⬌ ? )cpc_cpc






computationextended computationxprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )xprs_liftxprs_aaaxprs_cprs





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







strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa






csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_liftcsn_cprcsn_lcpr




context-sensitive computationlcprs ( ? ⊢ ➡* ? )lcprs_aaalcprs_cprslcprs_lcprs






cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_ltprcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldropltprs_ltprs






tprs ( ? ➡* ?)tprs_lifttprs_tprs






local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldroplsubc_ldropslsubc_lsuba





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





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






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


cnf_cif



context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_aaalcpr_cprlcpr_lcpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_deliftcpr_ltprcpr_cpr



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





focalized reductionlfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )









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








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








context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpss_dxltpr_ltpss_snltpr_aaaltpr_ltpr



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr



unwind









static typinglocal env. ref. for stratified static type assignmentlsubss ( ? ⁝⊑ ? )lsubss_ldroplsubss_sstalsubss_lsubss





stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_liftssta_ltpss_dxssta_ltpss_snssta_aaassta_ssta



local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpss_dxaaa_ltpss_snaaa_aaa



parametersshsd






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






inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_liftdelift_tpssdelift_ltpssdelift_delift



partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_ldropltpss_sn_tpsltpss_sn_tpssltpss_sn_ltpss_snltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )




ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldropltpss_dx_tpsltpss_dx_tpssltpss_dx_ltpss_dx





tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss





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






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








lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts






support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2




substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lifttps_tps






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







basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_appendldrop_lpxldrop_sfrldrop_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_tstctstc_vector






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







internal syntaxgenv









lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_pxlenv_px_bi




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






item








external syntaxaarity







+
componentplanefiles








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






equivalencecontext-sensitive equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaalfpcs_lfprslfpcs_lfpcs







cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_aaacpcs_ltprcpcs_cprscpcs_cpcs


conversioncontext-sensitive conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc









cpc ( ? ⊢ ? ⬌ ? )cpc_cpc







computationextended computationxprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )xprs_liftxprs_aaaxprs_cprs






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








strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa







csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_liftcsn_cprcsn_lfpr





context-sensitive computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaalfprs_cprslfprs_lfprs







cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_aaacprs_ltprcprs_lfprcprs_cprscprs_lfprscprs_tstccprs_tstc_vector

context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldropltprs_ltprs







tprs ( ? ➡* ?)tprs_lifttprs_tprs







local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldroplsubc_ldropslsubc_lsuba






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






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







context-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpsscfpr_aaacfpr_cpr






context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_aaalfpr_cprlfpr_fprlfpr_lfprlfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )





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








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







context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_tpsscpr_ltpsscpr_deliftcpr_aaacpr_ltprcpr_cpr


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






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









context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpss_dxltpr_ltpss_snltpr_aaaltpr_ltpr




tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr




unwind










static typinglocal env. ref. for stratified static type assignmentlsubss ( ? ⁝⊑ ? )lsubss_ldroplsubss_sstalsubss_lsubss






stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_liftssta_ltpss_dxssta_ltpss_snssta_aaassta_ssta




local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba






atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpss_dxaaa_ltpss_snaaa_aaa




parametersshsd







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







inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_liftdelift_tpssdelift_ltpssdelift_delift




partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_ldropltpss_sn_tpsltpss_sn_tpssltpss_sn_ltpss_snltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )





ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldropltpss_dx_tpsltpss_dx_tpssltpss_dx_ltpss_dx






tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss






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







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









lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts







support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2





substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lifttps_tps







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








basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_appendldrop_lpxldrop_sfrldrop_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_tstctstc_vector







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








internal syntaxgenv










lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_pxlenv_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-09-29T23:49:46+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-10-13T23:29:26+02: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 30591ab89..40c29fa13 100644 --- a/helm/www/lambda_delta/web/home/basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl @@ -48,8 +48,8 @@ table { class "blue" [ { "equivalence" * } { [ { "context-sensitive equivalence" * } { - [ "lcpcs ( ? ⊢ ⬌* ? )" "lcpcs_aaa" "lcpcs_lcprs" "lcpcs_lcpcs" * ] - [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss" "cpcs_delift" "cpcs_ltpr" "cpcs_cprs" "cpcs_cpcs" * ] + [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" "lfpcs_lfprs" "lfpcs_lfpcs" * ] + [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss" "cpcs_delift" "cpcs_aaa" "cpcs_ltpr" "cpcs_cprs" "cpcs_cpcs" * ] } ] } @@ -57,7 +57,7 @@ table { class "sky" [ { "conversion" * } { [ { "context-sensitive conversion" * } { - [ "lcpc ( ? ⊢ ⬌ ? )" "lcpc_lcpc" * ] + [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ] [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] } ] @@ -75,12 +75,12 @@ table { ] [ { "strongly normalizing computation" * } { [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ] - [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" "csn_cpr" "csn_lcpr" * ] + [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" "csn_cpr" "csn_lfpr" * ] } ] [ { "context-sensitive computation" * } { - [ "lcprs ( ? ⊢ ➡* ? )" "lcprs_aaa" "lcprs_cprs" "lcprs_lcprs" * ] - [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_delift" "cprs_ltpr" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ] + [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" "lfprs_cprs" "lfprs_lfprs" * ] + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_delift" "cprs_aaa" "cprs_ltpr" "cprs_lfpr" "cprs_cprs" "cprs_lfprs" "cprs_tstc" "cprs_tstc_vector" * ] } ] [ { "context-free computation" * } { @@ -104,26 +104,29 @@ table { [ "xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )" "xpr_lift" "xpr_aaa" * ] } ] + [ { "context-sensitive focalized reduction" * } { + [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" "cfpr_aaa" "cfpr_cpr" * ] + } + ] + [ { "context-free focalized reduction" * } { + [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_aaa" "lfpr_cpr" "lfpr_fpr" "lfpr_lfpr" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" * ] + [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" * ] + } + ] [ { "context-sensitive normal forms" * } { - [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" *"cnf_cif" * ] + [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" "cnf_cif" * ] } ] [ { "context-sensitive reduction" * } { - [ "lcpr ( ? ⊢ ➡ ? )" "lcpr_aaa" "lcpr_cpr" "lcpr_lcpr" * ] - [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_delift" "cpr_ltpr" "cpr_cpr" * ] + [ "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" * ] } ] - [ { "focalized reduction" * } { - [ "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" * ] - [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" * ] - } - ] [ { "context-free normal forms" * } { - [ "thnf ( 𝐇𝐍⦃?⦄ )" * ] + [ "thnf ( 𝐇𝐍⦃?⦄ )" * ] } ] [ { "context-free reduction" * } {