X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=c0b48965fffb3bf3f2275c74f0cd6cd83e5d1726;hb=7e80b8d7a4b2c38729512dee28b3e0ecf9595c2a;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..c0b48965f 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]

@@ -73,9 +73,11 @@ version 2 - library + helena + + +
- (static LDDL directory) @@ -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 [spacer]
Here is a numerical account of the specification's contents and its timeline. @@ -144,29 +144,29 @@ sizes files - 83 + 138 characters - 55955 + 109280 nodes - 191279 + 546141 propositions theorems - 33 + 45 lemmas - 211 + 395 total - 244 + 440 concepts declared - 15 - defined 23 + defined + 32 total - 38 + 55 @@ -180,6 +180,20 @@
Stage "A2": "Extending the Applicability Condition"
+
    +
  • + 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 +335,7 @@ λδ version 2 is started.
-
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [spacer]
This table reports the specification's components and their planes.
@@ -343,70 +357,160 @@ - relocation - ranged equivalence for closures - freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) - freq_freq - + rt-transition + counted context-sensitive rt-transition + cpg ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr +
- +
- + static typing + parameters + sh + sd +
- context-sensitive free variables - frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) - frees_weight frees_lreq frees_frees - +
- + + + +
+ + restricted ref. for atomic arity assignment + lsuba ( ? ⊢ ? ⫃⁝ ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba + +
+ +
- +
- generic slicing for local environments - drops_vector ( ⬇*[?,?] ? ≡ ? ) - + atomic arity assignment + aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) + aaa_drops aaa_fqus aaa_lfeq aaa_aaa +
- +
- + + + +
+ + restricted ref. for local env. + lsubr ( ? ⫃ ? ) + lsubr_length lsubr_drops lsubr_lsubr + +
+ +
- +
- + equivalence for closures on referred entries + ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) + ffeq_freq +
- drops ( ⬇*[?,?] ? ≡ ? ) - drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops - +
- + + + +
+ + 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_fqup lfxs_lfxs + +
+ + +
+ + + + +
+ + context-sensitive free variables + frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) + frees_weight frees_lreq frees_frees + +
+ + +
+ + + + s-computation + iterated structural successor for closures + fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) + fqus_weight fqus_drops fqus_fqup fqus_fqus + +
+ +
- generic relocation for terms - lifts_vector ( ⬆*[?] ? ≡ ? ) - lifts_lift_vector + + + +
+ + +
+ + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) + fqup_weight fqup_drops fqup_fqup + +
+ + +
+ + + + s-transition + structural successor for closures + fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) + fquq_length fquq_weight
@@ -421,8 +525,8 @@
- lifts ( ⬆*[?] ? ≡ ? ) - lifts_simple lifts_weight lifts_lifts + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu_length fqu_weight
@@ -431,42 +535,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 +624,20 @@ grammar + append for local environments + append ( ? @@ ? ) + append_length + +
+ + +
+ + + + +
+ context-sensitive equivalences for terms ceq ceq_ceq @@ -540,7 +702,9 @@ lenv lenv_weight ( ♯{?} ) lenv_length ( |?| ) - lenv_append ( ? @@ ? ) + +
+ @@ -592,7 +756,7 @@
- [Spacer] + [Spacer]

@@ -617,6 +781,6 @@

-
Last update: Sun, 27 Mar 2016 18:42:29 +0200
+
Last update: Thu, 19 May 2016 12:17:40 +0200