X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=a7e304e3ca68b485d1a0ee190f11dd6c99baa58d;hb=f51ead46bde4e49bbaf4925dea9f9e9bfaecb255;hp=4003948a122714eaebe56cba462424f74d8ba675;hpb=560e9f41516968588e97bb6ff2049f85a425ac0a;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 4003948a1..a7e304e3c 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 - 83 + 221 characters - 55955 + 212835 nodes - 191279 + 1046738 propositions theorems - 33 + 49 lemmas - 211 + 693 total - 244 + 742 concepts declared - 15 + 29 defined - 23 + 62 total - 38 + 91 @@ -180,6 +180,38 @@
Stage "A2": "Extending the Applicability Condition"
+
    +
  • + 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. + Grammatical component reconstructed: + grammar, relocation, s_transition, s_computation, static + (anniversary milestone). +
    • +
+
    +
  • + 2016 March 25. + Relocation with reference transforming maps (rtmap). +
    • +
  • 2015 October 9. @@ -300,7 +332,7 @@
    • 2012 January 27. - Support for abstract candidates of reducibility. + Generic candidates of reducibility.
      @@ -321,7 +353,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,159 +364,285 @@ component plane files - +
    - + + + rt-computation + uncounted context-sensitive rt-transition + cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) +
    - + + + rt-transition + parallel qrst-rtransition + fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) +
    - relocation - ranged equivalence for closures - freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - freq_freq - +
    - + t-bound context-sensitive rt-transition + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr + + + +
    + +
    + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops - +
    - context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - +
    - + cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx + + +
    + uncounted context-sensitive rt-transition + cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) + cnx_simple cnx_drops - +
    - generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - +
    - + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa + + +
    - +
    + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfdeq - +
    - + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr + + + static typing + generic reducibility + lsubc ( ? ⊢ ? ⫃[?] ? ) + lsubc_drop lsubc_drops lsubc_lsubr lsubc_lsuba + + + +
    + +
    - drops ( ⬇*[?,?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops - + gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) + gcp_aaa + + + +
    + +
    - + gcp +
    - +
    - generic relocation for terms - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lift_vector - + atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + + +
    - +
    + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfdeq aaa_aaa - +
    - + degree-based equivalence on referred entries + ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) + ffdeq_fqup ffdeq_ffdeq + + +
    - lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts - +
    - + lfdeq ( ? ≡[?,?,?] ? ) + lfdeq_length lfdeq_fqup lfdeq_lfdeq + + +
    + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs - +
    - ranged equivalence for local environments - lreq ( ? ≡[?] ? ) - lreq_length lreq_lreq - + context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees + + +
    - +
    + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_weight frees_drops frees_fqup frees_frees + + + +
    + + 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
    - generic entrywise extension of context-sensitive relations for terma - lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs - +
    - + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight + + + relocation + generic slicing for local environments + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) +
    - - - +
    - +
    - + drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) + drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops + + +
    - + generic relocation for terms + lifts_vector ( ⬆*[?] ? ≡ ? ) + lifts_lifts_vector + + +
    + +
    + + lifts ( ⬆*[?] ? ≡ ? ) + lifts_simple lifts_weight lifts_tdeq lifts_lifts - grammar - context-sensitive equivalences for terms - ceq - ceq_ceq - +
    - + 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 + + +
    + degree-based equivalence for terms + deq ( ? ≡[?,?] ? ) + deq_deq @@ -492,10 +650,14 @@ same top term structure tsts ( ? ≂ ? ) - tsts_tsts tsts_vector - + tsts_tsts tsts_vector + + +
    + closures + cl_weight ( ♯{?,?,?} )
    @@ -504,12 +666,10 @@
    - closures - cl_weight ( ♯{?,?,?} ) - cl_restricted_weight ( ♯{?,?} ) - +
    + cl_restricted_weight ( ♯{?,?} )
    @@ -518,14 +678,30 @@
    - internal syntax + global environments genv - +
    - + + + +
    + + local environments + lenv_length ( |?| ) + +
    + + + + +
    + +
    + lenv_weight ( ♯{?} )
    @@ -538,9 +714,19 @@
    lenv - lenv_weight ( ♯{?} ) - lenv_length ( |?| ) - lenv_append ( ? @@ ? ) + +
    + + + + +
    + + terms + term_vector ( Ⓐ?.? ) + +
    + @@ -549,10 +735,10 @@
    - term - term_weight ( ♯{?} ) - term_simple ( 𝐒⦃?⦄ ) - term_vector ( Ⓐ?.? ) + term_simple ( 𝐒⦃?⦄ ) + +
    + @@ -561,29 +747,63 @@
    - item - + term_weight ( ♯{?} ) +
    - + + +
    + +
    + + term
    - +
    - external syntax - aarity - + items + item_sd +
    - + + +
    + +
    + + item_sh + +
    + + + + +
    + + +
    + + item + +
    + + + + +
    + + atomic arities + aarity
    @@ -592,7 +812,7 @@
    - [Spacer] + [Spacer]

    @@ -617,6 +837,6 @@

    -
    Last update: Sun, 27 Mar 2016 18:42:29 +0200
    +
    Last update: Sun, 19 Feb 2017 19:57:19 +0100