X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fbasic_2.html;h=cea859d387ce11b0ed0f43be3d17601f11480b1c;hb=9b925454b8e2fe77916f02f5b81641bdbf8344fc;hp=01f3ea9d6a0787390d31b0c59e607124acce669f;hpb=c66eccc53d2b3000a905f9172b66cf6f9e2131a6;p=helm.git diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 01f3ea9d6..cea859d38 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
+ @@ -58,10 +61,10 @@ Support for abstract candidates of reducibility.
-
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_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



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-29T19:32:27+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-18T16:59:43+02:00