X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambda_delta%2Fbasic_2.html;h=413f1c44bfe89bc4274d2912f6a8b60716841a41;hb=335ae5716c5abbdbaaa4f115c56f7fdcc91320a4;hp=c4501f60b52ece438469d1a5df7f6dd6f103a001;hpb=badd398f31309584efc39254e26b056683157a65;p=helm.git diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index c4501f60b..413f1c44b 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,7 +29,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles153bytes580977

propositionstheorems60lemmas669total729
conceptsdeclared37defined50total87
+
categoryobjects




sizesfiles169bytes630979

propositionstheorems60lemmas715total775
conceptsdeclared38defined54total92
+
-
componentplanefiles







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






cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_ltprcpcs_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_alt ( ? ⊢ ⬇⬇* ? )csn_liftcsn_cprcsn_lcpr




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






cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_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_deliftcpr_ltprcpr_cpr



context-free normal formstwhnf ( 𝐖𝐇𝐍⦃?⦄ )tnf ( 𝐍⦃?⦄ )tnf_tif






context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpssltpr_aaaltpr_ltpr




tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr




context-free reducible formstrf ( 𝐑⦃?⦄ )tif ( 𝐈⦃?⦄ )






unwindstratified unwindsstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )sstas_liftsstas_ltpsssstas_sstas




static typingstratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_liftssta_ltpssssta_ssta





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





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpssaaa_aaa




parametersshsd






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






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



partial unfoldltpss ( ? ▶*[?,?] ? )ltpss_ldropltpss_tpsltpss_tpssltpss_ltpss





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_ldropldrop_sfr






local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )lsubs_lsubslsubs_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 ( |?| )







termterm_weight ( #[?] )term_simple ( 𝐒⦃?⦄ )term_vector






item








external syntaxaarity







+
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

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





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








context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpssltpr_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_ltpssssta_aaassta_ssta




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





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpssaaa_aaa




parametersshsd






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






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



partial unfoldltpss ( ? ▶*[?,?] ? )ltpss_ldropltpss_tpsltpss_tpssltpss_ltpss





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_sfrldrop_ldrop





local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )lsubs_lsubslsubs_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 ( ? @@ ? )






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-07-13T18:55:07+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-07-26T16:59:06+02:00