X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=41d3bf7500a735ec39f90ab30264a18b697d4824;hb=aedbc9769bb8e65b2a99ef86c44b446b0f9a2dc7;hp=6c2afdca79833f36da0a81edefb0fb30661ca3e2;hpb=5b42070b6644e184a762ac3c4e4a0f3cf5532b8c;p=helm.git diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 6c2afdca7..41d3bf750 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


native typing
nty


conversioncontext-sensitivecpcs


computationstrongly normalizingcsn



context-sensitivecprs


reductioncontext-sensitivelcpr




cprcpr_liftcpr_ltprcpr_cpr

context-freeltprltpr_ldrop



tprtpr_lifttpr_tpsstpr_tpr
static typingatomic arity ass.aaaaaa_liftaaa_aaa

static type ass.stysty_liftsty_sty
unfoldpartialltpssltpss_ldropltpss_tpsltpss_ltpss


tpsstpss_lifttpss_tpsstpss_ltps
substitutionparallelltpsltps_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 computationlsubcs




csncsn_crcsn_aarity

context-sensitive computationcprs



support for abstract comptation propertieslsubc




acpacp_cr

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 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]