From: Ferruccio Guidi Date: Sat, 7 Jan 2012 22:11:51 +0000 (+0000) Subject: Basic_2: - we addedsome files X-Git-Tag: make_still_working~1988 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de392360825733c1c865d748f7711f34bfc027f3;p=helm.git Basic_2: - we addedsome files - we added some notation - we updated the table style --- diff --git a/helm/www/lambda_delta/css/xhtbl.css b/helm/www/lambda_delta/css/xhtbl.css index 1517decbb..b4dfb4743 100644 --- a/helm/www/lambda_delta/css/xhtbl.css +++ b/helm/www/lambda_delta/css/xhtbl.css @@ -17,17 +17,20 @@ td { /* content types ************************************************************/ .component { + font-family: serif; font-style: normal; text-transform: capitalize; } .plane { + font-family: serif; font-style: normal; text-transform: lowercase; } .file { - font-style: italic; + font-family: sans-serif; + 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 8e4dca575..6736d2813 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -15,10 +15,16 @@
[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


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 used in the files for the relation or function + introduced in each plane 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


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-01-07+01:00
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml index 080d62ea1..d38e7d73e 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml +++ b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml @@ -6,9 +6,15 @@ head = "cic:/matita/lambda_delta/Basic_2/ (λδ version 2)" > Logical structure of the contribution - The source files are grouped in planes and components according to the following table. + The source files are grouped in planes and components + according to the following table. + The notation for the relation or function introduced in each file + is shown in parentheses. + Physical structure of the contribution - The source files are grouped in directories, one for each component. + 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 5ef4c8603..a72869568 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -11,8 +11,12 @@ table { ] class "prune" [ { "functional" * } { + [ { "reduction and type machine" * } { + [ "rtm" "rtm_step" * ] + } + ] [ { "unfold" * } { - [ "lift" "subst" * ] + [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] } ] } @@ -52,7 +56,7 @@ table { } ] [ { "support for abstract computation properties" * } { - [ "lsubc" * ] + [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" * ] [ "acp" "acp_cr" "acp_aaa" * ] } ] @@ -87,7 +91,7 @@ table { } ] [ { "atomic arity ass." * } { - [ "aaa" "aaa_lift" "aaa_aaa" * ] + [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_aaa" * ] } ] [ { "parameters" * } { @@ -99,16 +103,20 @@ table { class "yellow" [ { "unfold" * } { [ { "term inverse relocation" * } { - [ "delift" "delift_lift" * ] + [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ] } ] [ { "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" * } { - [ "lifts" "ldrops" * ] + [ "ldrops ( ⇓*[?] ? ≡ ? )" "ldrops_ldrops" * ] + } + ] + [ { "generic relocation" * } { + [ "lifts ( ⇑*[?] ? ≡ ? )" "lifts_lifts" "lifts_vector" * ] } ] } @@ -116,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" * ] } ] [ { "local env. slicing" * } { - [ "ldrop" "ldrop_ldrop" * ] + [ "ldrop ( ⇓[?,?] ? ≡ ? )" "ldrop_ldrop" * ] } ] [ { "term relocation" * } { - [ "lift" "lift_lift" "lift_vector" * ] + [ "lift ( ⇑[?,?] ? ≡ ? )" "lift_lift" "lift_vector" * ] } ] } @@ -137,7 +145,7 @@ table { class "red" [ { "grammar" * } { [ { "local env. ref. for substitution" * } { - [ "lsubs" "lsubs_lsubs" * ] + [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ] } ] [ { "term hom." * } { @@ -145,12 +153,13 @@ table { } ] [ { "closures" * } { - [ "cl_shift" "cl_weight" * ] + [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ] } ] [ { "internal syntax" * } { - [ "lenv" "lenv_weight" "lenv_length" * ] - [ "term" "term_weight" "term_simple" "term_vector" * ] + [ "genv" * ] + [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ] + [ "term" "term_weight ( #[?] )" "term_simple" "term_vector" * ] [ "item" * ] } ]