X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=69093e53685835c023e634156fefa7743f388761;hb=73052ec76ff5492989f9cbae2ebe0b770fcb985f;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..69093e536 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 + 157 characters - 55955 + 138411 nodes - 191279 + 711276 propositions theorems - 33 + 45 lemmas - 211 + 506 total - 244 + 551 concepts declared - 15 - defined 23 + defined + 38 total - 38 + 61 @@ -180,6 +180,32 @@
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. @@ -321,7 +347,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.
@@ -343,70 +369,250 @@ - relocation - ranged equivalence for closures - freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - freq_freq - + rt-transition + t-bound context-sensitive rt-transition + lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) + lfpr_length lfpr_drops lfpr_fqup lfpr_lfpx lfpr_lfpr +
- +
- +
- context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - +
- + cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) + cpr_drops + +
+ +
- +
- generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - +
- + cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpm_simple cpm_drops cpm_lsubr cpm_cpx +
- +
- +
- + uncounted context-sensitive rt-transition + lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup lfpx_frees +
- drops ( ⬇*[?,?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops - +
- + + + +
+ + +
+ + cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) + cpx_simple cpx_drops cpx_lsubr + +
+ +
- + +
+ + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr + +
+ + +
+ + + + static typing + parameters + sh + sd + +
+ + +
+ + + + +
+ + restricted ref. for atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + +
+ + +
+ + + + +
+ + atomic arity assignment + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfeq aaa_aaa + +
+ + +
+ + + + +
+ + equivalence for closures on referred entries + ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + ffeq_freq + +
+ + +
+ + + + +
+ + equivalence for local environments on referred entries + lfeq ( ? ≡[?] ? ) + lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq + +
+ + +
+ + + + +
+ + generic extension on referred entries + lfxs ( ? ⦻*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs + +
+ + +
+ + + + +
+ + restricted ref. for context-sensitive free variables + lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) + lsubf_frees + +
+ + +
+ + + + +
+ + context-sensitive free variables + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_weight frees_lreq frees_drops frees_fqup frees_fqus frees_frees + +
+ + +
+ + + + +
+ + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr + +
+ +
- generic relocation for terms - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lift_vector + + + 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
@@ -421,8 +627,8 @@
- lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight
@@ -431,42 +637,86 @@ - + relocation + generic slicing for local environments + drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) +
- ranged equivalence for local environments - lreq ( ? ≡[?] ? ) - lreq_length lreq_lreq - +
- +
- +
- generic entrywise extension of context-sensitive relations for terma - lexs ( ? ⦻*[?,?,?] ? ) - lexs_length lexs_lexs - +
- + 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_lifts + +
+ + +
+ + + + +
+ + ranged equivalence for local environments + lreq ( ? ≡[?] ? ) + lreq_length lreq_lreq + +
+ + +
+ + + + +
+ + generic entrywise extension + lexs ( ? ⦻*[?,?,?] ? ) + lexs_length lexs_lexs
@@ -476,6 +726,20 @@ grammar + append for local environments + append ( ? @@ ? ) + append_length + +
+ + +
+ + + + +
+ context-sensitive equivalences for terms ceq ceq_ceq @@ -540,7 +804,9 @@ lenv lenv_weight ( ♯{?} ) lenv_length ( |?| ) - lenv_append ( ? @@ ? ) + +
+ @@ -592,7 +858,7 @@
- [Spacer] + [Spacer]

@@ -617,6 +883,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Tue, 17 Jan 2017 21:42:42 +0100