X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=374c3a7db77cd311b68881174df388362bc7e6ad;hb=b7de6afb9d3260ffea86ddf824e497419e1b56fb;hp=5ae7da3063e1448a8bed8e391e332259463afc03;hpb=ecb63d645415784352a937f8320f84c23da327f7;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5ae7da306..374c3a7db 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 - 102 + 212 characters - 69295 + 213959 nodes - 245853 + 1057531 propositions theorems - 34 + 62 lemmas - 256 + 741 total - 290 + 803 concepts declared - 21 + 31 defined - 29 + 78 total - 50 + 109 @@ -180,6 +180,61 @@
Stage "A2": "Extending the Applicability Condition"
+
    +
  • + 2017 October 17. + Exclusion binder in local environments. + Syntactic component updated: + syntax, relocation, s_transition, s_computation, static, i_static. +
    • +
+
    +
  • + 2017 April 16. + Strong rt-normalization + for simply typed terms + (anniversary milestone). +
    • +
+
    +
  • + 2017 March 16. + First behavioral component reconstructed: + rt_transition. +
    • +
+
    +
  • + 2017 February 19. + Generic candidates of reducibility. +
    • +
+
    +
  • + 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. + Syntactic component reconstructed: + syntax, relocation, s_transition, s_computation, static + (anniversary milestone). +
    • +
+
    +
  • + 2016 March 25. + Relocation with reference transforming maps (rtmap). +
    • +
  • 2015 October 9. @@ -231,7 +286,7 @@
    • 2014 January 20. - Parametrized slicing of local environments + Parametrized slicing on local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now).
      • @@ -300,7 +355,7 @@
      • 2012 January 27. - Support for abstract candidates of reducibility. + Generic candidates of reducibility.
        @@ -321,7 +376,7 @@ λδ 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.
      @@ -332,38 +387,46 @@ component plane files - -
      - - -
      -
      + + rt-transition + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr + + + iterated static typing + iterated extension on referred entries + tc_lfxs ( ? ⦻**[?,?] ? ) + tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs + static typing - parameters - sh - sd - + generic reducibility + lsubc ( ? ⊢ ? ⫃[?] ? ) + lsubc_drops lsubc_lsubr lsubc_lsuba + + +
      - +
      + gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) + gcp_aaa
      - restricted ref. for local env. - lsubr ( ? ⫃ ? ) - lsubr_length lsubr_drops lsubr_lsubr - +
      + gcp
      @@ -372,57 +435,93 @@
      - ranged equivalence for closures - freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - freq_freq - + atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + + +
      - +
      + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
      - context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - + degree-based equivalence on referred entries + ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) + ffdeq_fqup ffdeq_ffdeq + + +
      - +
      + lfdeq ( ? ≡[?,?,?] ? ) + lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq - s-computation - - +
      - + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + + +
      - + context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_lsubr lsubf_frees lsubf_lsubf + + +
      - +
      + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_drops frees_fqup frees_frees - s-transition - structural successor for closures - fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) - fquq_length fquq_weight - +
      - + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr + + + s-computation + iterated structural successor for closures + fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) + fqus_weight fqus_drops fqus_fqup fqus_fqus + + + +
      + +
      + fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) + fqup_weight fqup_drops fqup_fqup + + + s-transition + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_length fquq_weight @@ -431,28 +530,44 @@
      - fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) - fqu_length fqu_weight - + fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight + + + relocation + generic slicing for local environments + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + +
      + + + +
      - +
      + drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops - relocation - generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - +
      - + generic relocation + lifts_bind ( ⬆*[?] ? ≡ ? ) + lifts_weight_bind lifts_lifts_bind + + +
      - +
      + lifts_vector ( ⬆*[?] ? ≡ ? ) + lifts_lifts_vector @@ -461,81 +576,109 @@
      - drops ( ⬇*[?,?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops - + lifts ( ⬆*[?] ? ≡ ? ) + lifts_simple lifts_weight lifts_tdeq lifts_lifts + + +
      - + ranged equivalence for local environments + lreq ( ? ≡[?] ? ) + lreq_length lreq_lreq + + +
      + generic entrywise extension + lexs ( ? ⦻*[?,?,?] ? ) + lexs_length lexs_lexs - + syntax + append for local environments + append ( ? @@ ? ) + append_length + + +
      - generic relocation for terms - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lifts_vector - + head equivalence for terms + theq ( ? ⩳[?,?] ? ) + theq_simple theq_tdeq theq_theq theq_simple_vector + + +
      - + degree-based equivalence + tdeq_ext ( ? ≡[?,?] ? ) +
      - +
      - +
      - lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts - + tdeq ( ? ≡[?,?] ? ) + tdeq_tdeq + + +
      - + closures + cl_weight ( ♯{?,?,?} ) +
      - +
      - ranged equivalence for local environments - lreq ( ? ≡[?] ? ) - lreq_length lreq_lreq - +
      - + cl_restricted_weight ( ♯{?,?} ) +
      - +
      - generic entrywise extension of context-sensitive relations for terma - lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs - + global environments + genv +
      - + + + +
      + + local environments + lenv_ext2 +
      - grammar - append for local environments - append ( ? @@ ? ) - append_length - +
      + +
      + + lenv_length ( |?| )
      @@ -544,12 +687,10 @@
      - context-sensitive equivalences for terms - ceq - ceq_ceq - +
      + lenv_weight ( ♯{?} )
      @@ -558,12 +699,10 @@
      - same top term structure - tsts ( ? ≂ ? ) - tsts_tsts tsts_vector - +
      + lenv
      @@ -572,28 +711,38 @@
      - closures - cl_weight ( ♯{?,?,?} ) - cl_restricted_weight ( ♯{?,?} ) - + binders for local environments + ext2 + ext2_ext2 + + +
      - +
      + bind + bind_weight
      - internal syntax - genv - + terms + term_vector ( Ⓐ?.? ) +
      - + + +
      + +
      + + term_simple ( 𝐒⦃?⦄ )
      @@ -605,9 +754,7 @@
      - lenv - lenv_weight ( ♯{?} ) - lenv_length ( |?| ) + term_weight ( ♯{?} )
      @@ -620,40 +767,50 @@
      term - term_weight ( ♯{?} ) - term_simple ( 𝐒⦃?⦄ ) - term_vector ( Ⓐ?.? ) + +
      +
      - + items + item_sd +
      - item - + + +
      - +
      + item_sh
      - +
      - external syntax - aarity - +
      - + item +
      + + + +
      + + atomic arities + aarity
      @@ -662,7 +819,7 @@
      - [Spacer] + [Spacer]

      @@ -687,6 +844,6 @@

      -
      Last update: Fri, 01 Apr 2016 23:30:53 +0200
      +
      Last update: Tue, 17 Oct 2017 20:34:24 +0200