X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fbasic_2.html;h=9a1f793eee92e438562d0a8092841cff0896eef4;hb=2fd3cd6a9477c2244391c16a230f69b4a231e5ab;hp=65a801e7edd93253ac50fbc1800fc6d6d1484c05;hpb=ae7427e8d3c57ccc77931e27913d8605d385cbda;p=helm.git diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 65a801e7e..9a1f793ee 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
* 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




sizesfiles113bytes422759

propositionstheorems45lemmas450total495
conceptsdeclared31defined39total70
+
categoryobjects




sizesfiles116bytes428758

propositionstheorems46lemmas453total499
conceptsdeclared31defined40total71
-
+
componentplanefiles






examples








native typing
nty






equivalencecontext-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )






conversioncontext-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )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_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_cpr







cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr



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





context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps






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_aaa




parameterssh






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






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





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




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 substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps





tps ( ? ⊢ ? [?,?] ▶ ? )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






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-03-15+01: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-03-17+01:00