X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=da3068b9315087f86b6f1124f3df44e3d489513f;hb=427efd63045c98ec6381c0c044108ded870111fc;hp=8e4dca57510fcd73e16e93fd1465e1e8d8e330d1;hpb=30df7ebabc6eb145c28a9724c6e8ad9612c784b1;p=helm.git diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 8e4dca575..da3068b93 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -14,11 +14,34 @@
[lambda_delta home]
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
[Spacer]
+
Summary of the contribution
+
Here is a numerical acount of the contribution's contents + and its timeline. +
+
categoryobjects


propositionstheorems39lemmas333
conceptsdeclared33defined46
+ + Support for abstract candidates of reducibility closed. + + + Confluence of context-sensitive parallel reduction closed. + + + Confluence of context-free parallel reduction closed. + + + Specification started. +
Logical structure of the contribution
-
The source files are grouped in planes and components according to the following table.
-
componentplanefiles


functionalunfoldliftsubst

examples




native typing
nty


conversioncontext-sensitive conversioncpcs


computationstrongly normalizing computationcsncsn_crcsn_aaa

context-sensitive computationcprs



support for abstract computation propertieslsubc




acpacp_cracp_aaa
reducibilitycontext-sensitive reductionlcpr




cprcpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnftnf


context-free reductionltprltpr_ldrop



tprtpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingstatic type ass.stysty_liftsty_sty

atomic arity ass.aaaaaa_liftaaa_aaa

parameterssh


unfoldterm inverse relocationdeliftdelift_lift


partial unfoldltpssltpss_ldropltpss_tpsltpss_ltpss


tpsstpss_lifttpss_tpsstpss_ltps

generic local env. slicingliftsldrops

substitutionparallel substitutionltpsltps_ldropltps_tpsltps_ltps


tpstps_lifttps_tps

global env. slicinggdrop



local env. slicingldropldrop_ldrop


term relocationliftlift_liftlift_vector
grammarlocal env. ref. for substitutionlsubslsubs_lsubs


term hom.thomthom_thom


closurescl_shiftcl_weight


internal syntaxlenvlenv_weightlenv_length


termterm_weightterm_simpleterm_vector


item



external syntaxaarity


+
The source files are grouped in planes and components + according to the following table. + The notation for the relations or functions introduced in each file + is shown in parentheses. +
+
componentplanefiles


functionalreduction and type machinertmrtm_step ( ? ⇨ ? )


unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )

examples




native typing
nty


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


computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa

context-sensitive computationcprs (? ⊢ ? ➡* ?)



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

support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

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

context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



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


term hom.thomthom_thom


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


internal syntaxgenv




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


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


item



external syntaxaarity


Physical structure of the contribution
-
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: 2011-12-25+01:00
+
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-01+01:00