X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=1b36b571ecadb27ea144a55017df85d4ad269276;hb=bc389dd4724959688aafc1ede450794f47b8d0b5;hp=b7988087c9fdae28483cef4ebc5d83dd925850bf;hpb=a255d83ebcb9b700a6f30cbcd109d223fc0d98cb;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index b7988087c..1b36b571e 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,1389 @@ - + - - - - - - lambdadelta version 2 - - - - + + + + + + \lambda\delta home page + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" + +
+ + [lambdadelta home] + +
+
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + library + (static LDDL directory)
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + helena + +
+
+
+ +
Summary of the Specification [spacer] +
+
Here is a numerical account of the specification's contents and its timeline.
-
categoryobjects




sizesfiles226characters427252

propositionstheorems82lemmas981total1063
conceptsdeclared43defined76total119
- +
Logical Structure of the Specification [spacer] +
+
This table reports the specification's components and their planes.
-
[Spacer]

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

Last update: 2012-12-02T17:25:27+01:00
- +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+ 		+
+ 		+
+
examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta +
+ 		+
+ 		+
+
+ + + +
+ 		+
+ 		+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv +
+ 		+
+
+
+ 		stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) +
+ 		+
+ 		+
+
+
+ 		+
+ 		snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve +
+ 		+
+
equivalencedecomposed rt-equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes +
+ 		+
+
+
+ 		context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs +
+ 		+
+
conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc +
+ 		+
+
computationevaluation for context-sensitive rt-reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) +
+ 		+
+ 		+
+
+
+ 		evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre +
+ 		+
+
+
+ 		strongly normalizing qrst-computationfsb ( ⦥[?,?] ⦃?,?,?⦄ )fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )fsb_aaa fsb_csx +
+
+
+ 		strongly normalizing rt-computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx +
+ 		+
+
+
+ 		+
+ 		lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx +
+
+
+ 		+
+ 		csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tsts_vector csx_aaa +
+ 		+
+
+
+ 		+
+ 		csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs +
+
+
+ 		parallel qrst-computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg +
+ 		+
+
+
+ 		+
+ 		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs +
+
+
+ 		decomposed rt-computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds +
+ 		+
+
+
+ 		context-sensitive rt-computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs +
+ 		+
+
+
+ 		+
+ 		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs +
+ 		+
+
+
+ 		context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs +
+ 		+
+
+
+ 		+
+ 		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs +
+ 		+
+
+
+ 		local env. ref. for generic reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba +
+ 		+
+
+
+ 		support for generic computation propertiesgcpgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa +
+
reductionparallel qrst-reductionfpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )fpbq_lift fpbq_aaa +
+
+
+ 		+
+ 		fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lift fpb_lleq fpb_fleq +
+ 		+
+
+
+ 		normal forms for context-sensitive rt-reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix +
+ 		+
+
+
+ 		context-sensitive rt-reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa +
+ 		+
+
+
+ 		+
+ 		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix +
+ 		+
+
+
+ 		irreducible forms for context-sensitive rt-reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift +
+ 		+
+
+
+ 		reducible forms for context-sensitive rt-reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift +
+ 		+
+
+
+ 		normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir +
+ 		+
+
+
+ 		context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr +
+ 		+
+
+
+ 		+
+ 		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir +
+ 		+
+
+
+ 		irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift +
+ 		+
+
+
+ 		reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift +
+ 		+
+
unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) +
+ 		+
+ 		+
+
+
+ 		iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas +
+ 		+
+
static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd +
+ 		+
+
+
+ 		degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_da +
+ 		+
+
+
+ 		parametersshsd +
+ 		+
+
+
+ 		local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba +
+ 		+
+
+
+ 		atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa +
+ 		+
+
+
+ 		restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr +
+ 		+
+
multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq +
+ 		+
+
+
+ 		+
+ 		lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq +
+ 		+
+
+
+ 		lazy pointwise extension of a relationllpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor +
+ 		+
+
+
+ 		pointwise union for local environmentsllor ( ? ⋓[?,?] ? ≡ ? )llor_alt llor_drop +
+ 		+
+
+
+ 		context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_lreq frees_lift +
+ 		+
+
+
+ 		context-sensitive multiple rt-substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys +
+
+
+ 		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus +
+ 		+
+
+
+ 		+
+ 		fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup +
+ 		+
+
+
+ 		iterated local env. slicingdrops ( ⬇*[?,?] ? ≡ ? )drops_drop drops_drops +
+ 		+
+
+
+ 		generic term relocationlifts_vector ( ⬆*[?] ? ≡ ? )lifts_lift_vector +
+ 		+
+
+
+ 		+
+ 		lifts ( ⬆*[?] ? ≡ ? )lifts_lift lifts_lifts +
+ 		+
+
+
+ 		support for multiple relocationmr2 ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )mr2_mr2
substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) +
+ 		+
+
+
+ 		+
+ 		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) +
+ 		+
+ 		+
+
+
+ 		global env. slicinggget ( ⬇[?] ? ≡ ? )gget_gget +
+ 		+
+
+
+ 		context-sensitive ordinary rt-substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy +
+ 		+
+
+
+ 		local env. ref. for rt-substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby +
+ 		+
+
+
+ 		pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn +
+ 		+
+
+
+ 		basic local env. slicingdrop ( ⬇[?,?,?] ? ≡ ? )drop_append drop_lreq drop_drop +
+ 		+
+
+
+ 		basic term relocationlift_vector ( ⬆[?,?] ? ≡ ? )lift_lift_vector +
+ 		+
+
+
+ 		+
+ 		lift ( ⬆[?,?] ? ≡ ? )lift_neq lift_lift +
+ 		+
+
grammarequivalence for local environmentslreq ( ? ⩬[?,?] ? )lreq_lreq +
+ 		+
+
+
+ 		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector +
+ 		+
+
+
+ 		closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) +
+ 		+
+
+
+ 		internal syntaxgenv +
+ 		+
+ 		+
+
+
+ 		+
+ 		lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+
+ 		+
+ 		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
+
+ 		+
+ 		item +
+ 		+
+ 		+
+
+
+ 		external syntaxaarity +
+ 		+
+ 		+
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 06 Sep 2015 21:40:58 +0200
+