From 84d31c59b46b61089b0df11c58ccde5c30361588 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 21 Nov 2011 17:45:16 +0000 Subject: [PATCH] Basic_2 file names update --- helm/www/lambda_delta/ld_basic_2.html | 2 +- helm/www/lambda_delta/web/home/ld_basic_2.tbl | 124 +++++++++--------- 2 files changed, 65 insertions(+), 61 deletions(-) diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 142598d2c..5cac746f8 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -16,7 +16,7 @@
[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


examples




native typing
nty


conversioncontext-sensitive conversioncpcs


computationstrongly normalizing computationcsn



context-sensitive computationcprs


reducibilitycontext-sensitive reductionlcpr




cprcpr_liftcpr_ltprcpr_cpr

context-free normal formstnf



context-free reductionltprltpr_ldrop



tprtpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingatomic arity ass.aaaaaa_liftaaa_aaa

static type ass.stysty_liftsty_sty
unfoldtelescopic substitutiontsubst



partial unfoldltpssltpss_ldropltpss_tpsltpss_ltpss


tpsstpss_lifttpss_tpsstpss_ltps
substitutionparallel substitutionltpsltps_ldropltps_tpsltps_ltps


tpstps_lifttps_tps

local env. droppingldropldrop_ldrop


term relocationliftlift_lift

grammarlocal env. ref. for substitutionlsubslsubs_lsubs


term hom.thomthom_thom


closurescl_shiftcl_weight


internal syntaxlenvlenv_weightlenv_length


termterm_weightterm_simple


item



external syntaxaarity



parameterssh


+
componentplanefiles


examples




native typing
nty


conversioncontext-sensitive conversioncpcs


computationstrongly normalizing computationcsn



context-sensitive computationcprs


reducibilitycontext-sensitive reductionlcpr




cprcpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnftnf


context-free reductionltprltpr_ldrop



tprtpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf



support for abstract reductionaprapr_cr

static typingstatic type ass.stysty_liftsty_sty

atomic arity ass.aaaaaa_liftaaa_aaa

parameterssh


unfoldterm inverse relocationdelift



partial unfoldltpssltpss_ldropltpss_tpsltpss_ltpss


tpsstpss_lifttpss_tpsstpss_ltps
substitutionparallel substitutionltpsltps_ldropltps_tpsltps_ltps


tpstps_lifttps_tps

local env. droppingldropldrop_ldrop


term relocationliftlift_lift

grammarlocal env. ref. for substitutionlsubslsubs_lsubs


term hom.thomthom_thom


closurescl_shiftcl_weight


internal syntaxlenvlenv_weightlenv_length


termterm_weightterm_simple


item



external syntaxaarity


Physical structure of the contribution
The source files are grouped in directories, one for each component.
[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]
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 bcbb90b8b..78d7b8237 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -11,80 +11,88 @@ table { ] class "blue" [ { "examples" * } { - [ { "" * } { - [ "" * ] - } - ] - } + [ { "" * } { + [ "" * ] + } + ] + } ] class "sky" [ { "native typing" * } { - [ { "" * } { - [ "nty" * ] - } - ] - } + [ { "" * } { + [ "nty" * ] + } + ] + } ] class "cyan" [ { "conversion" * } { - [ { "context-sensitive conversion" * } { - [ "cpcs" * ] - } - ] - } + [ { "context-sensitive conversion" * } { + [ "cpcs" * ] + } + ] + } ] class "water" [ { "computation" * } { - [ { "strongly normalizing computation" * } { - [ "csn" * ] - } - ] - [ { "context-sensitive computation" * } { - [ "cprs" * ] - } - ] - } + [ { "strongly normalizing computation" * } { + [ "csn" * ] + } + ] + [ { "context-sensitive computation" * } { + [ "cprs" * ] + } + ] + } ] class "green" [ { "reducibility" * } { - [ { "context-sensitive reduction" * } { - [ "lcpr" * ] - [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ] - } - ] - [ { "context-free normal forms" * } { - [ "tnf" * ] - } - ] - [ { "context-free reduction" * } { - [ "ltpr" "ltpr_ldrop" * ] - [ "tpr" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] - } - ] - [ { "context-free reducible forms" * } { - [ "trf" * ] - } - ] - } + [ { "context-sensitive reduction" * } { + [ "lcpr" * ] + [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ] + } + ] + [ { "context-free normal forms" * } { + [ "twhnf" "tnf" * ] + } + ] + [ { "context-free reduction" * } { + [ "ltpr" "ltpr_ldrop" * ] + [ "tpr" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] + } + ] + [ { "context-free reducible forms" * } { + [ "trf" * ] + } + ] + [ { "support for abstract reduction" * } { + [ "apr" "apr_cr" * ] + } + ] + } ] class "grass" [ { "static typing" * } { - [ { "atomic arity ass." * } { - [ "aaa" "aaa_lift" "aaa_aaa" * ] - } - ] - [ { "static type ass." * } { - [ "sty" "sty_lift" "sty_sty" * ] - } - ] - } - ] + [ { "static type ass." * } { + [ "sty" "sty_lift" "sty_sty" * ] + } + ] + [ { "atomic arity ass." * } { + [ "aaa" "aaa_lift" "aaa_aaa" * ] + } + ] + [ { "parameters" * } { + [ "sh" * ] + } + ] + } + ] class "yellow" [ { "unfold" * } { - [ { "telescopic substitution" * } { - [ "tsubst" * ] + [ { "term inverse relocation" * } { + [ "delift" * ] } - ] + ] [ { "partial unfold" * } { [ "ltpss" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] @@ -133,10 +141,6 @@ table { [ "aarity" * ] } ] - [ { "parameters" * } { - [ "sh" * ] - } - ] } ] } -- 2.39.2