X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=80ad18b876caa18d6f9ee1485a3b793a6ef9d086;hb=6a4711dbb4bec52222e9d0586326ef03b9fbc81b;hp=1b36b571ecadb27ea144a55017df85d4ad269276;hpb=3bbf660fbb8eb231292a9a5d0befb676f4a376d4;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 1b36b571e..80ad18b87 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -16,12 +16,12 @@
- [lambdadelta home] + [\lambda\delta home]
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
- [Spacer] + [Spacer]

@@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -73,13 +73,15 @@ version 2 - library + helena + + + Open Symbolic Notation (OSN) - (static LDDL directory) - citations + citations visibility @@ -93,11 +95,9 @@ version 1 - helena - - -
+ library + (static LDDL directory) @@ -114,7 +114,7 @@ **** Sort level k in terms only. --> -
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -144,29 +144,29 @@ sizes files - 360 + 177 characters - 437272 + 179834 nodes - 1935835 + 938855 propositions theorems - 130 + 49 lemmas - 1303 + 618 total - 1433 + 667 concepts declared - 54 + 24 defined - 89 + 42 total - 143 + 66 @@ -179,11 +179,50 @@ for native type assignment. -
Stage "A": "Extending the Applicability Condition"
+
Stage "A2": "Extending the Applicability Condition"
+
    +
  • + 2017 January 17. + Confluence for parallel r-transition on referred entries of local environments. +
    • +
+
    +
  • + 2016 September 15. + Confluence for context-sensitive parallel r-transition on terms. +
    • +
+
    +
  • + 2016 April 16. + Grammatical component reconstructed: + grammar, relocation, s_transition, s_computation, static + (anniversary milestone). +
    • +
+
    +
  • + 2016 March 25. + Relocation with reference transforming maps (rtmap). +
    • +
+
    +
  • + 2015 October 9. + λδ version 2A2 is started. +
    • +
+
Stage "A1": "Extending the Applicability Condition"
+
    +
  • + 2015 August 27. + λδ version 2A1 appears too complex and is dismissed. +
    • +
  • 2014 October 28. - λδ version 2A is released. + λδ version 2A1 is released.
    @@ -305,10 +344,10 @@
    • 2011 April 17. - Specification starts. + λδ version 2 is started.
    -
    Logical Structure of the Specification [spacer] +
    Logical Structure of the Specification [butterfly]
    This table reports the specification's components and their planes.
    @@ -330,347 +369,13 @@ - examples - terms with special features - ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta - -
    - - -
    - - -
    - - - - - - - -
    - - -
    - - -
    - - - - dynamic typing - local env. ref. for stratified native validity - lsubsv ( ? ⊢ ? ⫃¡[?,?] ? ) - lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv - -
    - - -
    - - - - -
    - - stratified native validity - shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) - -
    - - -
    - - -
    - - - - -
    - - -
    - - snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) - snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve - -
    - - -
    - - - - equivalence - decomposed rt-equivalence - scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) - scpes_aaa scpes_cpcs scpes_scpes - -
    - - -
    - - - - -
    - - context-sensitive equivalence - cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? ) - cpcs_aaa cpcs_cprs cpcs_cpcs - -
    - - -
    - - - - conversion - context-sensitive conversion - cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? ) - cpc_cpc - -
    - - -
    - - - - computation - evaluation for context-sensitive rt-reduction - cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) - -
    - - -
    - - -
    - - - - -
    - - evaluation for context-sensitive reduction - cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) - cpre_cpre - -
    - - -
    - - - - -
    - - strongly normalizing qrst-computation - fsb ( ⦥[?,?] ⦃?,?,?⦄ ) - fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ ) - fsb_aaa fsb_csx - -
    - - - - -
    - - strongly normalizing rt-computation - lcosx ( ? ⊢ ~⬊*[?,?,?] ? ) - 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-computation - fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) - fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg - -
    - - -
    - - - - -
    - - -
    - - fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) - fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) - fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs - -
    - - - - -
    - - decomposed rt-computation - scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) - scpds_lift scpds_aaa scpds_scpds - -
    - - -
    - - - - -
    - - context-sensitive rt-computation - lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) - 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 computation - lprs ( ⦃?,?⦄ ⊢ ➡* ? ) - lprs_drop lprs_cprs lprs_lprs - -
    - - -
    - - - - -
    - - -
    - - cprs ( ⦃?,?⦄ ⊢ ? ➡* ?) - cprs_lift cprs_cprs - -
    - - -
    - - - - -
    - - local env. ref. for generic reducibility - lsubc ( ? ⊢ ? ⫃[?] ? ) - lsubc_drop lsubc_drops lsubc_lsuba - -
    - - -
    - - - - -
    - - support for generic computation properties - gcp - gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) - gcp_aaa - + rt-transition + t-bound context-sensitive rt-transition + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr +
    - - - reduction - parallel qrst-reduction - fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) - fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ ) - fpbq_lift fpbq_aaa
    @@ -682,8 +387,8 @@
    - fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) - fpb_lift fpb_lleq fpb_fleq + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops
    @@ -695,9 +400,11 @@
    - normal forms for context-sensitive rt-reduction - cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) - cnx_lift cnx_crx cnx_cix + +
    + + cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_cpx
    @@ -709,9 +416,9 @@
    - context-sensitive rt-reduction - lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) - lpx_drop lpx_frees lpx_lleq lpx_aaa + uncounted context-sensitive rt-transition + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa
    @@ -726,22 +433,8 @@
    - cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) - cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix - -
    - - -
    - - - - -
    - - irreducible forms for context-sensitive rt-reduction - cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) - cix_lift + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_lsubr
    @@ -753,9 +446,9 @@
    - reducible forms for context-sensitive rt-reduction - crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) - crx_lift + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr
    @@ -764,84 +457,80 @@ - -
    - - normal forms for context-sensitive reduction - cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ ) - cnr_lift cnr_crr cnr_cir - + static typing + parameters + sh + sd +
    - +
    - +
    - context-sensitive reduction - lpr ( ⦃?,?⦄ ⊢ ➡ ? ) - lpr_drop lpr_lpr - + restricted ref. for atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba +
    - +
    - -
    - - +
    - cpr ( ⦃?,?⦄ ⊢ ? ➡ ? ) - cpr_lift cpr_llpx_sn cpr_cir - + atomic arity assignment + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfeq aaa_aaa +
    - +
    - +
    - irreducible forms for context-sensitive reduction - cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ ) - cir_lift - + equivalence for closures on referred entries + ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + ffeq_freq +
    - +
    - +
    - reducible forms for context-sensitive reduction - crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ ) - crr_lift - + equivalence for local environments on referred entries + lfeq ( ? ≡[?] ? ) + lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq +
    - +
    - unfold - unfold - unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) - +
    + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
    @@ -853,9 +542,9 @@
    - iterated static type assignment - lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? ) - lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas + restricted ref. for context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees
    @@ -864,52 +553,38 @@ - static typing - local env. ref. for degree assignment - lsubd ( ? ⊢ ? ⫃▪[?,?] ? ) - lsubd_da lsubd_lsubd - -
    - - -
    - - - - +
    - degree assignment - da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) - da_lift da_aaa da_da - + context-sensitive free variables + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_weight frees_lreq frees_drops frees_fqup frees_fqus frees_frees +
    - +
    - +
    - parameters - sh - sd - + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr +
    - +
    - -
    - - local env. ref. for atomic arity assignment - lsuba ( ? ⊢ ? ⫃⁝ ? ) - lsuba_aaa lsuba_lsuba + s-computation + iterated structural successor for closures + fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) + fqus_weight fqus_drops fqus_fqup fqus_fqus
    @@ -921,23 +596,11 @@
    - atomic arity assignment - aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) - aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa - -
    - - -
    - - - - +
    - restricted local env. ref. - lsubr ( ? ⫃ ? ) - lsubr_lsubr + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) + fqup_weight fqup_drops fqup_fqup
    @@ -946,138 +609,10 @@ - multiple substitution - lazy equivalence - fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ ) - fleq_fleq - -
    - - -
    - - - - -
    - - -
    - - lleq ( ? ≡[?,?] ? ) - lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq - -
    - - -
    - - - - -
    - - lazy pointwise extension of a relation - llpx_sn - llpx_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 environments - llor ( ? ⋓[?,?] ? ≡ ? ) - llor_alt llor_drop - -
    - - -
    - - - - -
    - - context-sensitive exclusion from free variables - frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ ) - frees_append frees_lreq frees_lift - -
    - - -
    - - - - -
    - - context-sensitive multiple rt-substitution - cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) - cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) - cpys_lift cpys_cpys - -
    - - - - -
    - - iterated structural successor for closures - fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) - fqus_alt fqus_fqus - -
    - - -
    - - - - -
    - - -
    - - fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) - fqup_fqup - -
    - - -
    - - - - -
    - - iterated local env. slicing - drops ( ⬇*[?,?] ? ≡ ? ) - drops_drop drops_drops - -
    - - -
    - - - - -
    - - generic term relocation - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lift_vector + s-transition + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_length fquq_weight
    @@ -1092,8 +627,8 @@
    - lifts ( ⬆*[?] ? ≡ ? ) - lifts_lift lifts_lifts + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight
    @@ -1102,20 +637,12 @@ - + relocation + generic slicing for local environments + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) +
    - support for multiple relocation - mr2 ( @⦃?,?⦄ ≡ ? ) - mr2_plus ( ? + ? ) - mr2_minus ( ? ▭ ? ≡ ? ) - mr2_mr2 - - - substitution - structural successor for closures - fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) - fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
    @@ -1130,10 +657,8 @@
    - fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) - -
    - + drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
    @@ -1145,9 +670,9 @@
    - global env. slicing - gget ( ⬇[?] ? ≡ ? ) - gget_gget + generic relocation for terms + lifts_vector ( ⬆*[?] ? ≡ ? ) + lifts_lifts_vector
    @@ -1159,23 +684,11 @@
    - context-sensitive ordinary rt-substitution - cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) - cpy_lift cpy_nlift cpy_cpy - -
    - - -
    - - - - +
    - local env. ref. for rt-substitution - lsuby ( ? ⊆[?,?] ? ) - lsuby_lsuby + lifts ( ⬆*[?] ? ≡ ? ) + lifts_simple lifts_weight lifts_lifts
    @@ -1187,9 +700,9 @@
    - pointwise extension of a relation - lpx_sn - lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn + ranged equivalence for local environments + lreq ( ? ≡[?] ? ) + lreq_length lreq_lreq
    @@ -1201,9 +714,9 @@
    - basic local env. slicing - drop ( ⬇[?,?,?] ? ≡ ? ) - drop_append drop_lreq drop_drop + generic entrywise extension + lexs ( ? ⦻*[?,?,?] ? ) + lexs_length lexs_lexs
    @@ -1212,40 +725,24 @@ - -
    - - basic term relocation - lift_vector ( ⬆[?,?] ? ≡ ? ) - lift_lift_vector - + grammar + append for local environments + append ( ? @@ ? ) + append_length +
    - +
    - -
    - - -
    - - lift ( ⬆[?,?] ? ≡ ? ) - lift_neq lift_lift - -
    - - +
    - - - grammar - equivalence for local environments - lreq ( ? ⩬[?,?] ? ) - lreq_lreq + context-sensitive equivalences for terms + ceq + ceq_ceq
    @@ -1307,7 +804,9 @@ lenv lenv_weight ( ♯{?} ) lenv_length ( |?| ) - lenv_append ( ? @@ ? ) + +
    + @@ -1359,7 +858,7 @@
    - [Spacer] + [Spacer]

    @@ -1384,6 +883,6 @@

    -
    Last update: Sun, 06 Sep 2015 21:40:58 +0200
    +
    Last update: Thu, 19 Jan 2017 19:22:38 +0100