X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_1.html;h=d160de5dd84d9fe70a94cf6919c2e9c4b5847fda;hb=4e75ab41fb7a0a9a4f66cb777a791ce3950c57ce;hp=8560a6fcfd4477b536a098642759c09577b6ea8c;hpb=56dd0e9f60e0dabfb587b014755fd4dad27960bb;p=helm.git diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 8560a6fcf..d160de5dd 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -1,18 +1,828 @@ -\lambda\delta home page
[\lambda\delta home]
cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)
[Spacer]

homenewsspecification

documentationimplementation
forewordmilestonesversion 2(background - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Abstract Syntax and Behavior [butterfly]
This is a summary of available syntactic items and reductions (block structure). -
domainblockleader→ζ *annotator (with →ϵ *)applicator (with →θ *)reference *reduction
{X | Γ ⊢ ⊤}exclusionΓ ⊢ χyesnononono
{X | Γ ⊢ X : W}typed abstractionΓ ⊢ λWno<W>(V)#i→β *
{X | Γ ⊢ X = V}abbreviationΓ ⊢ δVyesnono#i→δ
nosortΓ ⊢ ⋆knonononono
* In terms only. -
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents + + + + + + + + \lambda\delta home page + + + + + + +
+ + [\lambda\delta home] + +
+
cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + helena + + Open Symbolic Notation (OSN) +
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + library + (static LDDL directory)
+
+
Abstract Syntax and Behavior [butterfly] +
+
This is a summary of available syntactic items and reductions (block structure). +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
domainblockleader→ζ *annotator (with →ϵ *)applicator (with →θ *)reference *reduction
{X | Γ ⊢ ⊤}exclusionΓ ⊢ χyesnononono
{X | Γ ⊢ X : W}typed abstractionΓ ⊢ λWno<W>(V)#i→β *
{X | Γ ⊢ X = V}abbreviationΓ ⊢ δVyesnono#i→δ
nosortΓ ⊢ ⋆knonononono
+
+
* In terms only. +
+
Summary of the Specification [butterfly] +
+
Here is a numerical account of the specification's contents and its timeline. -
categoryobjects




sizesfiles120characters198089nodes1449099
propositionstheorems81lemmas618total699
conceptsdeclared39defined47total86
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects +
+ 		+
+ 		+
+ 		+
+ 		+
+
sizesfiles120characters198089nodes1449099
propositionstheorems81lemmas618total699
conceptsdeclared39defined47total86
+
+ + + + +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes. -
componentplanefiles
examplesterms with special featureslevels_ex0ty3_ex1nf2_ex2

dynamic typingwell-formed contextswf3_defswf3_props

context ref. for native type assignmentcsubt_defscsubt_propscsubt_arity_props

native type assignmentty3_defsty3_propsty3_genty3_gen_contextty3_gen_nf2ty3_liftty3_subst0ty3_arity_propsty3_nf2_genty3_sredty3_sred_propsty3_dec
equivalencecontext-sensitive equivalencepc3_defspc3_propspc3_genpc3_gen_contextpc3_subst0

context-free equivalencepc1_defspc1_props

computationcontext ref. for reducibilitycsubc_defscsubc_props

reducibilitysc3_defssc3_propssc3_arity

strongly normalizing computationsn3_defssn3_gensn3_props

context-sensitive computationpr3_defspr3_propspr3_genpr3_gen_contextpr3_isopr3_subst1pr3_confluence

context-free computationpr1_defspr1_propspr1_confluence
reductionnormal forms for context-sensitive reductionnf2_defsnf2_propsnf2_gennf2_dec

context-sensitive reductionpr2_defspr2_genpr2_gen_contextpr2_liftpr2_subst1pr2_confluence

normal forms for context-free reductionnf0_dec

context-free reductionwcpr0_defs


pr0_defspr0_genpr0_liftpr0_subst0pr0_subst1pr0_confluence
unfolditerated static type assignmentsty1_defssty1_props
static typingstatic type assignmentsty0_defssty0_props

context ref. for binary arity assignmentcsuba_defscsuba_props

binary arity assignmentarity_defsarity_propsarity_genarity_subst0arity_sred

binary aritylevels_defsllt_defsaprem_defs

parametersparameter_defs

basic context ref.csubv_defs
multiple substitutioniterated context slicingdrop1_defsdrop1_props

generic term relocationlift1_defslift1_props
substitutionordinary substitutionsubst_defssubst_props


csubst1_defscsubst1_props


subst1_defssubst1_gensubst1_liftsubst1_subst1subst1_confluence

normal forms for ordinary strict substitutiondnf_dec

ordinary strict substitutionfsubst0_defs


csubst0_defs


subst0_defssubst0_gensubst0_tltsubst0_liftsubst0_subst0subst0_confluence

basic local env. slicinggetl_defsgetl_props


drop_defsdrop_props

basic term relocationlift_defslift_propslift_genlift_tlt
grammarclosuresflt_defs

contextscontexts_defsclt_defsctail_defsapp_defscnt_defs

termstlist_defs


terms_defstlt_defsiso_defs
[Spacer]

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

Last update: Thu, 09 Mar 2017 13:38:17 +0100
+ + +
Logical Structure of the Specification [butterfly] +
+
This table reports the specification's components and their planes. +
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
examplesterms with special features + levels_ex0 + ty3_ex1 + nf2_ex2 + +
+
+ + + +
+
dynamic typingwell-formed contexts + wf3_defs + + wf3_props +
+
+ 		context ref. for native type assignment + csubt_defs + + csubt_props + csubt_arity_props +
+
+ 		native type assignment + ty3_defs + + ty3_props + ty3_gen + ty3_gen_context + ty3_gen_nf2 + ty3_lift + ty3_subst0 + ty3_arity_props + ty3_nf2_gen + ty3_sred + ty3_sred_props + ty3_dec +
equivalencecontext-sensitive equivalence + pc3_defs + + pc3_props + pc3_gen + pc3_gen_context + pc3_subst0 +
+
+ 		context-free equivalence + pc1_defs + + pc1_props +
+ + + +
+
computationcontext ref. for reducibility + csubc_defs + + csubc_props +
+
+ 		reducibility + sc3_defs + + sc3_props + sc3_arity +
+
+ 		strongly normalizing computation + sn3_defs + + sn3_gen + sn3_props +
+
+ 		context-sensitive computation + pr3_defs + + pr3_props + pr3_gen + pr3_gen_context + pr3_iso + pr3_subst1 + pr3_confluence +
+
+ 		context-free computation + pr1_defs + + pr1_props + pr1_confluence +
reductionnormal forms for context-sensitive reduction + nf2_defs + + nf2_props + nf2_gen + nf2_dec +
+
+ 		context-sensitive reduction + pr2_defs + + pr2_gen + pr2_gen_context + pr2_lift + pr2_subst1 + pr2_confluence +
+
+ 		normal forms for context-free reduction + + nf0_dec +
+
+ 		context-free reduction + wcpr0_defs + +
+
+
+ 		+
+ 		+ pr0_defs + + pr0_gen + pr0_lift + pr0_subst0 + pr0_subst1 + pr0_confluence +
unfolditerated static type assignment + sty1_defs + + sty1_props +
static typingstatic type assignment + sty0_defs + + sty0_props +
+
+ 		context ref. for binary arity assignment + csuba_defs + + csuba_props +
+
+ 		binary arity assignment + arity_defs + + arity_props + arity_gen + arity_subst0 + arity_sred +
+
+ 		binary arity + levels_defs + llt_defs + aprem_defs + +
+
+
+ 		parameters + parameter_defs + +
+
+
+ 		basic context ref. + csubv_defs + +
+
multiple substitutioniterated context slicing + drop1_defs + + drop1_props +
+
+ 		generic term relocation + lift1_defs + + lift1_props +
substitutionordinary substitution + subst_defs + + subst_props +
+
+ 		+
+ 		+ csubst1_defs + + csubst1_props +
+
+ 		+
+ 		+ subst1_defs + + subst1_gen + subst1_lift + subst1_subst1 + subst1_confluence +
+
+ 		normal forms for ordinary strict substitution + + dnf_dec +
+
+ 		ordinary strict substitution + fsubst0_defs + +
+
+
+ 		+
+ 		+ csubst0_defs + +
+
+
+ 		+
+ 		+ subst0_defs + + subst0_gen + subst0_tlt + subst0_lift + subst0_subst0 + subst0_confluence +
+
+ 		basic local env. slicing + getl_defs + + getl_props +
+
+ 		+
+ 		+ drop_defs + + drop_props +
+
+ 		basic term relocation + lift_defs + + lift_props + lift_gen + lift_tlt +
grammarclosures + flt_defs + +
+
+
+ 		contexts + contexts_defs + clt_defs + ctail_defs + app_defs + cnt_defs + +
+
+
+ 		terms + tlist_defs + +
+
+
+ 		+
+ 		+ terms_defs + tlt_defs + iso_defs + +
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sat, 11 Mar 2017 19:30:41 +0100
+ +