From: Ferruccio Guidi Date: Sun, 8 Jan 2012 15:50:57 +0000 (+0000) Subject: Basic_2: restyling and more notation X-Git-Tag: make_still_working~1986 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8a14a6fab91a49325c4a9cea1ca1e6cd19c2d8f;p=helm.git Basic_2: restyling and more notation --- diff --git a/helm/www/lambda_delta/css/xhtbl.css b/helm/www/lambda_delta/css/xhtbl.css index b4dfb4743..7c90c511d 100644 --- a/helm/www/lambda_delta/css/xhtbl.css +++ b/helm/www/lambda_delta/css/xhtbl.css @@ -17,19 +17,16 @@ td { /* content types ************************************************************/ .component { - font-family: serif; - font-style: normal; + font-style: italic; text-transform: capitalize; } -.plane { - font-family: serif; - font-style: normal; +.plane { + font-style: italic; text-transform: lowercase; } -.file { - font-family: sans-serif; +.file { font-style: normal; text-transform: lowercase; } diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 6736d2813..eaa539756 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -17,14 +17,14 @@
Logical structure of the contribution
The source files are grouped in planes and components according to the following table. - The notation used in the files for the relation or function - introduced in each plane is shown in parentheses. + The notation for the relation or function 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 computationcsncsn_crcsn_aaa

context-sensitive computationcprs



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


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.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_ldrops


generic relocationlifts ( ⇑*[?] ? ≡ ? )lifts_liftslifts_vector
substitutionparallel substitutionltps ( ? [?,?] ≫ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ≫ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇓[?] ? ≡ ? )gdrop_gdrop


local env. slicingldrop ( ⇓[?,?] ? ≡ ? )ldrop_ldrop


term relocationlift ( ⇑[?,?] ? ≡ ? )lift_liftlift_vector
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 (? ⊢ ? ➡* ?)



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


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.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_ldrops


generic relocationlifts ( ⇧*[?] ? ≡ ? )lifts_liftslifts_vector
substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop


local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop


term relocationlift ( ⇧[?,?] ? ≡ ? )lift_liftlift_vector
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.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-01-07+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-01-08+01:00
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 a72869568..f40b1010c 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -12,7 +12,7 @@ table { class "prune" [ { "functional" * } { [ { "reduction and type machine" * } { - [ "rtm" "rtm_step" * ] + [ "rtm" "rtm_step ( ? ⇨ ? )" * ] } ] [ { "unfold" * } { @@ -40,7 +40,7 @@ table { class "cyan" [ { "conversion" * } { [ { "context-sensitive conversion" * } { - [ "cpcs" * ] + [ "cpcs ( ? ⊢ ? ⬌* ? )" * ] } ] } @@ -48,16 +48,16 @@ table { class "water" [ { "computation" * } { [ { "strongly normalizing computation" * } { - [ "csn" "csn_cr" "csn_aaa" * ] + [ "csn ( ⬇* ? )" "csn_cr" "csn_aaa" * ] } ] [ { "context-sensitive computation" * } { - [ "cprs" * ] + [ "cprs (? ⊢ ? ➡* ?)" * ] } ] [ { "support for abstract computation properties" * } { [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" * ] - [ "acp" "acp_cr" "acp_aaa" * ] + [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ] } ] } @@ -65,8 +65,8 @@ table { class "green" [ { "reducibility" * } { [ { "context-sensitive reduction" * } { - [ "lcpr" * ] - [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ] + [ "lcpr ( ? ⊢ ➡ ? )" * ] + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ] } ] [ { "context-free normal forms" * } { @@ -74,8 +74,8 @@ table { } ] [ { "context-free reduction" * } { - [ "ltpr" "ltpr_ldrop" * ] - [ "tpr" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" * ] + [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] } ] [ { "context-free reducible forms" * } { @@ -107,16 +107,16 @@ table { } ] [ { "partial unfold" * } { - [ "ltpss ( ? [?,?] ≫* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] - [ "tpss ( ? ⊢ ? [?,?] ≫* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] + [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] + [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] } ] [ { "generic local env. slicing" * } { - [ "ldrops ( ⇓*[?] ? ≡ ? )" "ldrops_ldrops" * ] + [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrops" * ] } ] [ { "generic relocation" * } { - [ "lifts ( ⇑*[?] ? ≡ ? )" "lifts_lifts" "lifts_vector" * ] + [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lifts" "lifts_vector" * ] } ] } @@ -124,20 +124,20 @@ table { class "orange" [ { "substitution" * } { [ { "parallel substitution" * } { - [ "ltps ( ? [?,?] ≫ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ] - [ "tps ( ? ⊢ ? [?,?] ≫ ? )" "tps_lift" "tps_tps" * ] + [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ] + [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ] } ] [ { "global env. slicing" * } { - [ "gdrop ( ⇓[?] ? ≡ ? )" "gdrop_gdrop" * ] + [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } ] [ { "local env. slicing" * } { - [ "ldrop ( ⇓[?,?] ? ≡ ? )" "ldrop_ldrop" * ] + [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ] } ] [ { "term relocation" * } { - [ "lift ( ⇑[?,?] ? ≡ ? )" "lift_lift" "lift_vector" * ] + [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" "lift_vector" * ] } ] }