X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=5d9118e0d39c10cb6a2cf3ee1e5a39d00be7de8c;hb=ff11fcced84c3e18f0f73be101bc7b2086fc0a52;hp=58087e46d43676ec01d4581d3575a3d058393fa3;hpb=9b077c63115106e3b61a4f06f5c03f7a059e7f45;p=helm.git diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 58087e46d..5d9118e0d 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -14,11 +14,51 @@
[lambda_delta home]
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
[Spacer]
-
Logical structure of the contribution
-
The source files are grouped in planes and components according to the following table.
-
componentplanefiles


native typing
nty


conversioncontext-sensitivecpcs


computationstrongly normalizingcsn



context-sensitivecprs


reductioncontext-sensitivelcpr




cprcpr_liftcpr_tpsscpr_cpr

context-freeltprltpr_drop



tprtpr_lifttpr_tpsstpr_tpr
static typingatomic arity ass.aaaaaa_liftaaa_aaa

static type ass.stysty_liftsty_sty
unfoldpartialltpssltpss_dropltpss_tpsltpss_ltpss


tpsstpss_lifttpss_tpsstpss_ltps
substitutionparallelltpsltps_dropltps_tpsltps_ltps


tpstps_lifttps_tps

local env. droppingdropdrop_drop


term relocationliftlift_lift

grammarlocal env. ref. for substitutionlsubslsubs_lsubs


term hom.thomthom_thom


closurescl_shiftcl_weight


internal syntaxlenvlenv_weightlenv_length


termterm_weightterm_simple


item



external syntaxaarity



parameterssh


-
Physical structure of the contribution
-
The source files are grouped in directories, one for each component.
-
[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]
+
System's Syntax and Behavior
+
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. + **** Sort level k in terms only. +
+ +
Summary of the Specification
+
Here is a numerical acount of the specification's contents + and its timeline. +
+
categoryobjects




propositionstheorems43lemmas409total452
conceptsdeclared32defined35total67
+ + + + + + +
Logical Structure of the Specification
+
The source files are grouped in planes and components + according to the following table. + A notation file covering the whole specification is provided. + The notation for the relations or functions introduced in each file + is shown in parentheses. +
+
componentplanefiles



examples





native typing
nty



conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )



computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_lcpr_vectorcsn_aaa



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

context-sensitive computationcprs (? ⊢ ? ➡* ?)cprs_lcprcprs_cprscprs_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_tstc



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-02-24+01:00