X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fbasic_2.html;h=cea859d387ce11b0ed0f43be3d17601f11480b1c;hb=93784f891de6d7840646a963c964e8877b3b50b2;hp=758975ef4d7402064d80802f92217ea81db74b62;hpb=08db2212621969b85852de3bd0677149135df0fe;p=helm.git diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 758975ef4..cea859d38 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -18,7 +18,7 @@
This is a summary of the "block structure" of the System's syntactic items and reductions.
-
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
+
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i

local typed declaration **Γ ⊢ -λWⓐV→βno#i

global typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i

local definition **Γ ⊢ -δVnolocal →δno#i

global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
* In terms only. ** In terms and local environments only. *** In global environments only. @@ -29,14 +29,29 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles137bytes491033

propositionstheorems59lemmas556total615
conceptsdeclared32defined43total75
+
categoryobjects




sizesfiles204bytes742579

propositionstheorems74lemmas889total963
conceptsdeclared40defined73total113
+ + + +
-
componentplanefiles






examples








native typing
nty






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





cpcs ( ? ⊢ ? ⬌* ? )cpcs_cprscpcs_cpcs




conversioncontext-sensitive conversionlcpc ( ? ⊢ ⬌ ? )lcpc_lcpc







cpc ( ? ⊢ ? ⬌ ? )cpc_cpc





computationweakly normalizing computationcpe ( ? ⊢ ? ⊢ ➡* 𝐍[?] )cpe_cpe






strongly normalizing computationcsn_vector ( ⬇* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa





csn ( ⬇* ? )csn_liftcsn_cprcsn_cprs ( ⬇** ? )csn_lcpr



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





cprs (? ⊢ ? ➡* ?)cprs_liftcprs_ltprcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

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




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




reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift






context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_aaalcpr_cprlcpr_lcpr





cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltpssscpr_ltprcpr_cpr


context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif





context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpssltpr_ltpsssltpr_aaaltpr_ltpr


tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr




context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )





static typingstatic type assignmentstysty_liftsty_sty





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




atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_ltpssaaa_ltpsssaaa_aaa


parameterssh






unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift






partial unfoldltpsss ( ? [?,?] ▶** ? )ltpsss_ldropltpsss_tpsltpsss_tpssltpsss_ltpsss




ltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_tpssltpss_ltpss




tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_alt ( ? ⊢ ? [?,?] ▶▶* ? )




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_ldrop






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







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





grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs






same head term formtshf ( ? ≈ ? )tshf_tshf






same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector





closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )






internal syntaxgenv








lenvlenv_weight ( #[?] )lenv_length ( |?| )






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-04-16+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