From: Ferruccio Guidi Date: Sat, 21 Jan 2012 21:28:26 +0000 (+0000) Subject: big fixin the structure of Basic_2 X-Git-Tag: make_still_working~1971 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ce12633d55b42c4a5b4e3e601563747b873cc47;p=helm.git big fixin the structure of Basic_2 --- diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index d444f6a82..d98184f55 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -20,7 +20,7 @@ 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 (? ⊢ ? ➡* ?)



support for abstract computation propertieslsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba


acpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnftnf


context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingstatic type ass.stysty_liftsty_sty

atomic arity ass.lsuba ( ? ÷⊑ ? )




aaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_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 relocationgr2gr2_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_simpleterm_vector


item



external syntaxaarity


+
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 formstwhnftnf


context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingstatic type assignmentstysty_liftsty_sty

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



atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_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 relocationgr2gr2_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_simpleterm_vector


item



external syntaxaarity


Physical structure of the contribution
The source files are grouped in directories, one for each component. diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.tbl b/helm/www/lambda_delta/web/home/ld_basic_2.tbl index 11c116161..56905eacb 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -55,8 +55,11 @@ table { [ "cprs (? ⊢ ? ➡* ?)" * ] } ] - [ { "support for abstract computation properties" * } { + [ { "local env. ref. for abstract candidates of reducibility" * } { [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ] + } + ] + [ { "support for abstract computation properties" * } { [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ] } ] @@ -86,12 +89,15 @@ table { ] class "grass" [ { "static typing" * } { - [ { "static type ass." * } { + [ { "static type assignment" * } { [ "sty" "sty_lift" "sty_sty" * ] } ] - [ { "atomic arity ass." * } { + [ { "local env. ref. for atomic arity assignment" * } { [ "lsuba ( ? ÷⊑ ? )" * ] + } + ] + [ { "atomic arity assignment" * } { [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_aaa" * ] } ]