From: Ferruccio Guidi Date: Mon, 20 Feb 2012 19:11:10 +0000 (+0000) Subject: additions to Basic_2 ... X-Git-Tag: make_still_working~1947 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=75e8188b0ce9aa9bd54ef004e2709f29078820f3;p=helm.git additions to Basic_2 ... --- diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 024c7740f..030109a2f 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -29,7 +29,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects


propositionstheorems43lemmas387
conceptsdeclared33defined49
+
categoryobjects


propositionstheorems46lemmas405
conceptsdeclared35defined49
@@ -52,12 +52,12 @@ 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_crcsn_aaa




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

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


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



term hom.thom ( ? ≈ ? )thom_thom



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



internal syntaxgenv





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



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


item




external syntaxaarity



+
componentplanefiles



functionalreduction and type machinertmrtm_step ( ? ⇨ ? )



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


examples





native typing
nty



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



computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_crcsn_aaa



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

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

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



term hom.thom ( ? ≈ ? )thom_thom



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-14+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-02-20+01:00
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl index 6918cceda..65e26acff 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl @@ -48,12 +48,12 @@ table { class "water" [ { "computation" * } { [ { "strongly normalizing computation" * } { - [ "csn_cr" "csn_aaa" * ] + [ "csn_vector ( ⬇* ? )" "csn_cr" "csn_aaa" * ] [ "csn ( ⬇* ? )" "csn_lift" "csn_cpr" "csn_cprs ( ⬇** ? )" "csn_lcpr" * ] } ] [ { "context-sensitive computation" * } { - [ "cprs (? ⊢ ? ➡* ?)" "cprs_lcpr" "cprs_cprs" * ] + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lcpr" "cprs_cprs" "cprs_tstc" * ] } ] [ { "local env. ref. for abstract candidates of reducibility" * } { @@ -170,6 +170,10 @@ table { [ "thom ( ? ≈ ? )" "thom_thom" * ] } ] + [ { "same top term constructor" * } { + [ "tstc ( ? ≃ ? )" "tstc_tstc" * ] + } + ] [ { "closures" * } { [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ] } diff --git a/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl b/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl index 7477a67ba..24badffe3 100644 --- a/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl +++ b/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl @@ -27,7 +27,7 @@ concepts declared - 21 + 22 defined 8