X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=5075e40e11bcc0bf86bc321623e146c661b17625;hb=3080bf8226d155d017c5ec5c4e852d952f5b878c;hp=d48c03de785f09136188205e128fd41bbb29e62f;hpb=6f1f9e20aa2775d41bba64289fc903e6612baaf3;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index d48c03de7..5075e40e1 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - \lambda\delta version 2 + + \lambda\delta home page @@ -19,19 +19,83 @@ [lambdadelta home] -
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
+
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
[Spacer]
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + documentation + + specification + +
+ 		+ implementation +
+ foreword + + milestones + + version 2 + + version 2 + (background - core - applications) + library +
+ citations + + visibility + + version 1 + + version 1 + +
+ 		+ helena +
+
-
Summary of the Specification
+
Summary of the Specification [spacer] +
Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].
@@ -58,20 +122,20 @@ - + - + - + - + - + - + @@ -86,48 +150,54 @@
sizes files361360 characters431938433402 nodes18611351874774
propositions theorems128130 lemmas12891286 total14171416
concepts
-
Stage "B"
+
Stage "B"
-
Stage "A": "Weakening the Applicability Condition"
+
Stage "A": "Extending the Applicability Condition"
+ -
Logical Structure of the Specification
-
The source files are grouped in planes and components - according to the following table. - Notation files covering the whole specification are provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). +
Logical Structure of the Specification [spacer] +
+
This table reports the specification's components and their planes.
@@ -246,7 +313,7 @@ - + @@ -307,7 +374,7 @@
- + @@ -317,7 +384,7 @@ - + - + - - + + - + - + @@ -483,7 +550,7 @@ - + - + - + @@ -582,27 +649,9 @@ - - - - - - - - - - - + + + @@ -614,8 +663,8 @@ - - + + @@ -627,7 +676,7 @@ - + - + - + @@ -671,7 +720,7 @@ - + - + - + @@ -911,7 +960,7 @@ - + @@ -939,7 +988,7 @@ - + @@ -951,7 +1000,7 @@ - + @@ -1091,7 +1140,7 @@ - + - + - + @@ -1176,8 +1225,8 @@ - - + + @@ -1291,10 +1340,6 @@
examples terms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_reflex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preservesnv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve
equivalencedecomposed extended equivalencedecomposed rt-equivalence scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) scpes_aaa scpes_cpcs scpes_scpes @@ -355,7 +422,7 @@
computationevaluation for context-sensitive extended reductionevaluation for context-sensitive rt-reduction cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
@@ -386,8 +453,8 @@
strongly normalizing qrst-computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb ( ⦥[?,?] ⦃?,?,?⦄ )fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ ) fsb_aaa fsb_csx
@@ -397,7 +464,7 @@
strongly normalizing extended computationstrongly normalizing rt-computation lcosx ( ? ⊢ ~⬊*[?,?,?] ? ) lcosx_cpx @@ -474,7 +541,7 @@ fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbu fpbs_fpbc fpbs_fpbsfpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs

decomposed extended computationdecomposed rt-computation scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) scpds_lift scpds_aaa scpds_scpds @@ -497,7 +564,7 @@
context-sensitive extended computationcontext-sensitive rt-computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs @@ -515,7 +582,7 @@
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxscpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
reduction parallel qrst-reductionfpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )fpbc_fleq -
- 		-
-
-
- 		-
- 		fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_lleq fpbu_fleq -
- 		fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )fpbq_lift fpbq_aaa

fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaafpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lift fpb_lleq fpb_fleq

normal forms for context-sensitive extended reductionnormal forms for context-sensitive rt-reduction cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) cnx_lift cnx_crx cnx_cix @@ -641,7 +690,7 @@
context-sensitive extended reductioncontext-sensitive rt-reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) lpx_drop lpx_frees lpx_lleq lpx_aaa @@ -659,7 +708,7 @@
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cixcpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix

irreducible forms for context-sensitive extended reductionirreducible forms for context-sensitive rt-reduction cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) cix_lift @@ -685,7 +734,7 @@
reducible forms for context-sensitive extended reductionreducible forms for context-sensitive rt-reduction crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) crx_lift @@ -897,7 +946,7 @@
lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleqlleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq
lazy pointwise extension of a relation llpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llorllpx_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
context-sensitive exclusion from free variables frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_liftfrees_append frees_lreq frees_lift

contxt-sensitive extended multiple substitutioncontxt-sensitive multiple rt-substitution cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) cpys_lift cpys_cpys
contxt-sensitive extended ordinary substitutioncontxt-sensitive ordinary rt-substitution cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_nlift cpy_cpy @@ -1105,7 +1154,7 @@
local env. ref. for extended substitutionlocal env. ref. for rt-substitution lsuby ( ? ⊆[?,?] ? ) lsuby_lsuby @@ -1135,7 +1184,7 @@ basic local env. slicing drop ( ⬇[?,?,?] ? ≡ ? )drop_append drop_leq drop_dropdrop_append drop_lreq drop_drop
grammar equivalence for local environmentsleq ( ? ⩬[?,?] ? )leq_leqlreq ( ? ⩬[?,?] ? )lreq_lreq
-
Physical Structure of the Specification
-
The source files are grouped in directories, - one for each component. -
[Spacer]
@@ -1321,6 +1366,6 @@

-
Last update: Thu, 02 Oct 2014 23:21:16 +0200
+
Last update: Tue, 04 Nov 2014 16:21:23 +0100