web site update

[helm.git] / matita / matita / contribs / lambdadelta / web / changes.tbl

diff --git a/matita/matita/contribs/lambdadelta/web/changes.tbl b/matita/matita/contribs/lambdadelta/web/changes.tbl
index bf985679d8c0459016396b8e3a34e02e00eaebd6..9ef76e8f408e1b07422d902293e6b9ee84ea6d9f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/web/changes.tbl
+++ b/matita/matita/contribs/lambdadelta/web/changes.tbl
@@ -9,63 +9,143 @@ table {
   [ { "λδ-2B" + "(November 2019)" * }
     {
      [ [{ "validity" * }]
   [ { "λδ-2B" + "(November 2019)" * }
     {
      [ [{ "validity" * }]

-       { "@" "" "@" }
-       { "+" "-" "*" }
-       { "type assignment (terms)"
-         "stratified higher validity (terms) removed"
+       { "" "@" "" "@" }
+       { "+" "+" "-" "*" }
+       { "iterated type assignment (terms)"
+         "type assignment (terms)"
+         "higher validity (terms) removed"

          "primitive validity (terms)"
        }
      ]
      [ [{ "equivalences" * }]
          "primitive validity (terms)"
        }
      ]
      [ [{ "equivalences" * }]

-       { "" "" "" "" }
-       { "+" "+" "+" "-" }
-       { "equivalence for full rt-reduction (terms)"
+       { "" "" "" "" "" "" "" }
+       { "+" "-" "+" "+" "+" "+" "-" }
+       { "derived rt-equivalence (terms)"
+         "primitive decomposed rt-equivalence (terms) removed"

          "equivalence for whd rt-reduction (terms)"
          "equivalence for whd rt-reduction (terms)"

-         "equivalence for full rt-reduction (terms, referred lenvs, closures)"
-         "syntactic equivalence (closures) removed"
+         "equivalence for full rt-reduction (terms, items, referred lenvs, referred closures)"
+         "equivalence up to exclusion binders (selected lenvs)"
+         "syntactic equivalence (items)"
+         "syntactic equivalence (selected closures) removed"

        }
      ]
      [ [{ "partial orders" * }]
        }
      ]
      [ [{ "partial orders" * }]

-       { "" }
-       { "+" }
-       { "switch in primitive order relations for closures to enable the exclusion binder"
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "properties with inclusion (hereditarily free variables)"
+         "inclusion (hereditarily free variables)"
+         "inclusion (applicability)"
+         "switch in primitive order relations (closures) to enable the exclusion binder"
+         "simple weight (items, genvs)"
+       }
+     ]
+     [ [{ "reducibility" * }]
+       { "" "" "" }
+       { "+" "-" "*" }
+       { "compatibility relation for strong normalization (referred lenvs)"
+         "compatibility predicate for strong normalization (referred lenvs) removed"
+         "abatract Tait's candidates with 6 postulates"

        }
      ]
      [ [{ "normal form predicates" * }]
        }
      ]
      [ [{ "normal form predicates" * }]

-       { "" "" "" "" "" }
-       { "-" "-" "-" "-" "-" }
-       { "irreducible forms for full rt-reduction (terms) removed"
+       { "" "" "" "" "" "" "" "" "" "" }
+       { "+" "-" "+" "*" "+" "-" "-" "-" "-" "-" }
+       { "properties with evaluation"
+         "evaluation for full rt-reduction (terms) removed"
+         "whd evaluation for mixed rt-reduction (terms)"
+         "evaluation for mixed rt-reduction (terms)"
+         "whd normal form for mixed rt-reduction (terms)"
+         "irreducible forms for full rt-reduction (terms) removed"

          "reducible forms for full rt-reduction (terms) removed"
          "irreducible forms for reduction (terms) removed"
          "reducible forms for reduction (terms) removed"
          "abstract reducibility properties (items) removed"
        }
      ]
          "reducible forms for full rt-reduction (terms) removed"
          "irreducible forms for reduction (terms) removed"
          "reducible forms for reduction (terms) removed"
          "abstract reducibility properties (items) removed"
        }
      ]

+     [ [{ "reduction and type synthesis" * }]
+       { "" "" "@" "" "" "@" "" "" "@" "@" }
+       { "*" "*" "-" "+" "*" "+" "*" "+" "*" "+" }
+       { "counted iterated type synthesis (terms)"
+         "full rt-computation (terms, items, lenvs)"
+         "decomposed rt-computation (terms) removed"
+         "r-computation (items)"
+         "mixerd rt-computation (terms)"
+         "counted type synthesis (terms) with δ,s,l,e"
+         "full rt-transition (terms, items, lenvs, referred lenvs)"
+         "r-transition (items)"
+         "mixed rt-transition (terms)"
+         "primitive generic rt transition (terms) with typed β, δ, (correct) ζ, θ, ε"
+       }
+     ]

      [ [{ "substitution" * }]
      [ [{ "substitution" * }]

-       { "" }
-       { "-" }
-       { "zero or more refs (terms) removed"
+       { "" "" }
+       { "-" "-" }
+       { "(restricted) zero or more selected refs (terms) removed"
+         "zero or more refs (terms) removed"

        }
      ]
        }
      ]

-     [ [{ "relocation" * }]
-       { "" "" "" "" }
-       { "-" "*" "-" "*" }
-       { "basic slicing (lenvs) removed"
+     [ [{ "degree" * }]
+       { "" "@" }
+       { "-" "-" }
+       { "refinement for degree (lenvs) removed"
+         "degree assignment (terms) removed"
+       }
+     ]
+     [ [{ "relocation and slicing" * }]
+       { "" "" "" "" "" "" "" }
+       { "-" "+" "-" "*" "-" "+" "*" }
+       { "look-up predicate (genvs) removed"
+         "properties with abstract relocation (terms/items)"
+         "basic slicing (lenvs) removed"

          "primitive finite slicing (lenvs)"
          "primitive finite slicing (lenvs)"

-         "basic relocation (lists of terms) removed"
+         "basic relocation (terms, lists of terms) removed"
+         "primitive finite relocation (items)" 

          "primitive finite relocation (terms, lists of terms)"
        }
      ]
      [ [{ "free varibles" * }]
          "primitive finite relocation (terms, lists of terms)"
        }
      ]
      [ [{ "free varibles" * }]

-       { "" }
-       { "+" }
-       { "union (referred lenvs) removed"
+       { "" "" }
+       { "+" "-" }
+       { "refinement for hereditarily free variables (lenvs)"
+         "union (referred lenvs) removed"
+       }
+     ]
+     [ [{ "helpers" * }]
+       { "" "" "" "" "" }
+       { "-" "+" "+" "-" "+" }
+       { "unfold (closures) removed"
+         "append (restricted closures) wrong on excluded entries"
+         "length (genvs)"
+         "refinement (selected lenvs) removed"
+         "abstract properties with append (lenvs)"
+       }
+     ]
+     [ [{ "extension" * }]
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "properties with iterated extension (referred lenvs)"
+         "iterated for 3-relations (referred lenvs)"
+         "abstract properties with extension (selected lenvs)"
+         "for 3-relations (selected lenvs)"
+         "for 2-relations and 3-relations (items)"

        }
      ]
      [ [{ "syntax" * }]
        }
      ]
      [ [{ "syntax" * }]

-       { "@" }
-       { "+" }
-       { "exclusion binder for lenvs"
+       { "@" "" }
+       { "+" "+" }
+       { "exclusion binder (lenvs)"
+         "bonding items (lenvs)"
+       }
+     ]
+     [ [{ "parameters" * }]
+       { "" "" "@" "" "" "@" }
+       { "+" "+" "+" "-" "+" "*" }
+       { "instances (applicability)"
+         "predicates (applicability)"
+         "abstract applicability condition"
+         "instances (sort hierarchy) removed"
+         "predicates (sort hierarchy) including strict monotonicity condition based on non-negative integers"
+         "abstract sort hierarchy without predicates"

        }
      ]
      [ [{ "ground" * }]
        }
      ]
      [ [{ "ground" * }]


@@ -81,7 +161,7 @@ table {
   ]
 
   class "orange"
   ]
 
   class "orange"

-  [ { "λδ-2A" + "(October 2014)" * }
+  [ { "λδ-2A" + "(August 2015)" * }

     {
      [ [{ "validity" * }]
        { "" "" "@" "" "" "" "@" }
     {
      [ [{ "validity" * }]
        { "" "" "@" "" "" "" "@" }


@@ -96,24 +176,26 @@ table {
        }
      ]
      [ [{ "equivalences" * }]
        }
      ]
      [ [{ "equivalences" * }]

-       { "@" "" "@" "" "" "" }
-       { "+" "+" "-" "-" "-" "+" }
+       { "@" "" "@" "" "" "" "" }
+       { "+" "+" "-" "-" "-" "+" "+" }

        { "primitive decomposed rt-equivalence (terms)"
          "single-step context-sensitive r-eqivalence (terms)"
          "primitive context-sensitive r-eqivalence (terms) removed"
          "context-free r-eqivalence (terms) removed"
          "level equivalence (binary arities) removed"
        { "primitive decomposed rt-equivalence (terms)"
          "single-step context-sensitive r-eqivalence (terms)"
          "primitive context-sensitive r-eqivalence (terms) removed"
          "context-free r-eqivalence (terms) removed"
          "level equivalence (binary arities) removed"

-         "syntactic equivalence (selected lenvs, referred lenvs, selected closures)"
+         "properties with syntactic equivalence (referred lenvs)"
+         "syntactic equivalence (selected lenvs, referred lenvs, referred closures)"

        }
      ]
      [ [{ "partial orders" * }]
        }
      ]
      [ [{ "partial orders" * }]

-       { "" "" "" "" "" "" "" }
-       { "+" "*" "+" "-" "-" "-" "-" }
+       { "" "" "" "" "" "" "" "" }
+       { "+" "*" "+" "-" "-" "-" "-" "-" }

        { "big-tree order relations (closures)"
        { "big-tree order relations (closures)"

-         "primitive order relations for closures"
+         "primitive order relations (closures)"

          "simple weight (restricted closures)"
          "simple weight (restricted closures)"

+         "order relation (lenvs) based on look-up removed"

          "order relation (lists of terms) based on lengths removed"
          "order relation (lists of terms) based on lengths removed"

-         "order relations (binary arities) based on weights removed"
+         "order relations (terms, lenvs, binary arities) based on weights removed"

          "simple weights (binary arities) removed"
          "complex weight (terms) removed"
        }
          "simple weights (binary arities) removed"
          "complex weight (terms) removed"
        }


@@ -132,11 +214,12 @@ table {
        }
      ]
      [ [{ "normal form predicates" * }]
        }
      ]
      [ [{ "normal form predicates" * }]

-       { "" "" "" "" "" "" "" "" "" }
-       { "+" "+" "+" "+" "+" "-" "+" "+" "+" }
+       { "" "" "" "" "" "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" "+" "-" "+" "+" "+" }

        { "evaluation for full rt-reduction (terms)"
        { "evaluation for full rt-reduction (terms)"

+         "evaluation for reduction (terms)"

          "normal form for full rt-reduction (terms)"
          "normal form for full rt-reduction (terms)"

-         "irreducible forms for fulld rt-reduction (terms)"
+         "irreducible forms for full rt-reduction (terms)"

          "reducible forms for full rt-reduction (terms)"
          "evaluation for reduction (terms)"
          "normal form for reduction (lists of terms) removed"
          "reducible forms for full rt-reduction (terms)"
          "evaluation for reduction (terms)"
          "normal form for reduction (lists of terms) removed"


@@ -146,14 +229,15 @@ table {
        }
      ]
      [ [{ "reduction and type synthesis" * }]
        }
      ]
      [ [{ "reduction and type synthesis" * }]

-       { "" "" "@" "@" "" "" "" "@" "@" }
-       { "+" "+" "+" "*" "-" "+" "-" "*" "-" }
+       { "" "" "@" "@" "" "" "" "" "@" "@" }
+       { "+" "+" "+" "*" "-" "+" "+" "-" "*" "-" }

        { "stratified full rt-computation (terms, lenvs)"
          "stratified full rt-transition (terms, lenvs)"
          "decomposed rt-computation (terms)"
          "primitive counted iterated type synthesis with δ,s,l,e (terms)"
          "syntax-oriented type synthesis (terms) removed"
          "refinement for reduction (lenvs)"
        { "stratified full rt-computation (terms, lenvs)"
          "stratified full rt-transition (terms, lenvs)"
          "decomposed rt-computation (terms)"
          "primitive counted iterated type synthesis with δ,s,l,e (terms)"
          "syntax-oriented type synthesis (terms) removed"
          "refinement for reduction (lenvs)"

+         "context-sensitive computation (lenvs)"

          "context-free computation (terms) removed"
          "primitive context-sensitive transition with typed β, δ, (wrong) ζ, θ, ε (terms, lenvs)"
          "context-free transition (terms, lenvs) removed"
          "context-free computation (terms) removed"
          "primitive context-sensitive transition with typed β, δ, (wrong) ζ, θ, ε (terms, lenvs)"
          "context-free transition (terms, lenvs) removed"


@@ -169,7 +253,7 @@ table {
        }
      ]
      [ [{ "degree" * }]
        }
      ]
      [ [{ "degree" * }]

-       { "@" "" "@" "" }
+       { "" "@" "" "@" }

        { "+" "+" "+" "+" }
        { "refinement for degree (lenvs)"
          "degree assignment (terms)"
        { "+" "+" "+" "+" }
        { "refinement for degree (lenvs)"
          "degree assignment (terms)"


@@ -204,7 +288,7 @@ table {
          "refinement (selected lenvs)"
          "append (lenvs)"
          "left cons (lenvs) removed"
          "refinement (selected lenvs)"
          "append (lenvs)"
          "left cons (lenvs) removed"

-         "flat construction clear (lenvs) removed"
+         "flat entry clear (lenvs) removed"

          "sort extraction (lenvs) removed"
          "context predicate (terms) removed"
          "neutral predicate (terms)"
          "sort extraction (lenvs) removed"
          "context predicate (terms) removed"
          "neutral predicate (terms)"


@@ -232,8 +316,8 @@ table {
      ]
      [ [{ "parameters" * }]
        { "" "" }
      ]
      [ [{ "parameters" * }]
        { "" "" }

-       { "+" "-"}
-       { "concrete sort hierarchies"
+       { "+" "-" }
+       { "instances (sort hierarchy)"

          "iterated next function (sort hierarchy) removed"
        }
      ]
          "iterated next function (sort hierarchy) removed"
        }
      ]


@@ -249,7 +333,7 @@ table {
   ]
 
   class "red"
   ]
 
   class "red"

-  [ { "λδ-1A" + "(November 2006)" * }
+  [ { "λδ-1A" + "(May 2008)" * }

     {
      [ [{ "validity" * }]
        { "@" "" "" }
     {
      [ [{ "validity" * }]
        { "@" "" "" }


@@ -270,9 +354,10 @@ table {
        }
      ]
      [ [{ "partial orders" * }]
        }
      ]
      [ [{ "partial orders" * }]

-       { "" "" "" "" }
-       { "+" "+" "+" "+" }
-       { "order relation (specialized lists of terms) based on lengths"
+       { "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" }
+       { "order relation (lenvs) based on look-up"
+         "order relation (specialized lists of terms) based on lengths"

          "order relations (terms, lenvs, closures, binary arities) based on weights"
          "simple weights (terms, lenvs, closures, binary arities)"
          "complex weight (terms)"
          "order relations (terms, lenvs, closures, binary arities) based on weights"
          "simple weights (terms, lenvs, closures, binary arities)"
          "complex weight (terms)"


@@ -293,7 +378,7 @@ table {
      [ [{ "normal form predicates" * }]
        { "" }
        { "+" }
      [ [{ "normal form predicates" * }]
        { "" }
        { "+" }

-       { "normal form for context-sensitive reduction (terms, specialized lists of terms)"
+       { "normal form for reduction (terms, specialized lists of terms)"

        }
      ]
      [ [{ "reduction and type synthesis" * }]
        }
      ]
      [ [{ "reduction and type synthesis" * }]


@@ -316,10 +401,9 @@ table {
        }
      ]
      [ [{ "relocation and slicing" * }]
        }
      ]
      [ [{ "relocation and slicing" * }]

-       { "" "" "" "" "" "" "" "" }
-       { "+" "+" "+" "+" "+" "+" "+" "+" }
-       { "order relation (lenvs) based on look-up"
-         "look-up predicate (lenvs)"
+       { "" "" "" "" "" "" "" }
+       { "+" "+" "+" "+" "+" "+" "+" }
+       { "look-up predicate (lenvs)"

          "finite slicing (lenvs)"
          "basic slicing (lenvs)"
          "finite relocation (terms, specialized lists of terms)"
          "finite slicing (lenvs)"
          "basic slicing (lenvs)"
          "finite relocation (terms, specialized lists of terms)"