matita/matita/contribs/lambdadelta/web/changes.tbl

   1 name "changes"
   2
   3 table {
   4   class "gray"
   5   [ "specification" [ "aspect" [ "" "" "changes" ]]
   6   ]
   7
   8   class "orange"
   9   [ { "λδ-2B" + "(November 2019)" * }
  10     {
  11      [ [{ "validity" * }]
  12        { "@" "" "@" }
  13        { "+" "-" "*" }
  14        { "type assignment (terms)"
  15          "stratified higher validity (terms) removed"
  16          "primitive validity (terms)"
  17        }
  18      ]
  19      [ [{ "equivalences" * }]
  20        { "" "" "" "" }
  21        { "+" "+" "+" "-" }
  22        { "equivalence for full rt-reduction (terms)"
  23          "equivalence for whd rt-reduction (terms)"
  24          "equivalence for full rt-reduction (terms, referred lenvs, closures)"
  25          "syntactic equivalence (closures) removed"
  26        }
  27      ]
  28      [ [{ "partial orders" * }]
  29        { "" }
  30        { "+" }
  31        { "switch in primitive order relations for closures to enable the exclusion binder"
  32        }
  33      ]
  34      [ [{ "normal form predicates" * }]
  35        { "" "" "" "" "" }
  36        { "-" "-" "-" "-" "-" }
  37        { "irreducible forms for full rt-reduction (terms) removed"
  38          "reducible forms for full rt-reduction (terms) removed"
  39          "irreducible forms for reduction (terms) removed"
  40          "reducible forms for reduction (terms) removed"
  41          "abstract reducibility properties (items) removed"
  42        }
  43      ]
  44      [ [{ "substitution" * }]
  45        { "" }
  46        { "-" }
  47        { "zero or more refs (terms) removed"
  48        }
  49      ]
  50      [ [{ "relocation" * }]
  51        { "" "" "" "" }
  52        { "-" "*" "-" "*" }
  53        { "basic slicing (lenvs) removed"
  54          "primitive finite slicing (lenvs)"
  55          "basic relocation (lists of terms) removed"
  56          "primitive finite relocation (terms, lists of terms)"
  57        }
  58      ]
  59      [ [{ "free varibles" * }]
  60        { "" }
  61        { "+" }
  62        { "union (referred lenvs) removed"
  63        }
  64      ]
  65      [ [{ "syntax" * }]
  66        { "@" }
  67        { "+" }
  68        { "exclusion binder for lenvs"
  69        }
  70      ]
  71      [ [{ "ground" * }]
  72        { "" "" "" "" }
  73        { "+" "*" "+" "-" }
  74        { "rt-transition counters"
  75          "generic reference transforming maps as streams of non-negative integers"
  76          "extensional equality, labelled transitive closures and streams"
  77          "non-negative integers with infinity removed"
  78        }
  79      ]
  80     }
  81   ]
  82
  83   class "orange"
  84   [ { "λδ-2A" + "(October 2014)" * }
  85     {
  86      [ [{ "validity" * }]
  87        { "" "" "@" "" "" "" "@" }
  88        { "-" "-" "-" "+" "+" "+" "+" }
  89        { "flat or invalid entry clear (lenvs) removed"
  90          "refinement for type assignment (lenvs) removed"
  91          "primitive type assignment (terms, specialized lists of terms) removed"
  92          "confluence and preservation properties"
  93          "higher validity (terms)"
  94          "refinement for validity (lenvs)"
  95          "primitive stratified validity (terms)"
  96        }
  97      ]
  98      [ [{ "equivalences" * }]
  99        { "@" "" "@" "" "" "" }
 100        { "+" "+" "-" "-" "-" "+" }
 101        { "primitive decomposed rt-equivalence (terms)"
 102          "single-step context-sensitive r-eqivalence (terms)"
 103          "primitive context-sensitive r-eqivalence (terms) removed"
 104          "context-free r-eqivalence (terms) removed"
 105          "level equivalence (binary arities) removed"
 106          "syntactic equivalence (selected lenvs, referred lenvs, selected closures)"
 107        }
 108      ]
 109      [ [{ "partial orders" * }]
 110        { "" "" "" "" "" "" "" }
 111        { "+" "*" "+" "-" "-" "-" "-" }
 112        { "big-tree order relations (closures)"
 113          "primitive order relations for closures"
 114          "simple weight (restricted closures)"
 115          "order relation (lists of terms) based on lengths removed"
 116          "order relations (binary arities) based on weights removed"
 117          "simple weights (binary arities) removed"
 118          "complex weight (terms) removed"
 119        }
 120      ]
 121      [ [{ "reducibility" * }]
 122        { "" "" "" "" "" "" "" "" }
 123        { "+" "+" "*" "+" "*" "+" "*" "-" }
 124        { "compatibility predicate for strong normalization (referred lenvs)"
 125          "strong normalization for bt-reduction (referred closures)"
 126          "strong normalization for full rt-reduction (terms, lists of terms, referred lenvs)"
 127          "arrow candidate, arity interpretation"
 128          "abatract Tait's candidates with 7 postulates"
 129          "abstract computation for reducibility with 4 postulates"
 130          "atomic arities with sort, implication"
 131          "succerssor, addition, look-up predicate (binary arities) removed"
 132        }
 133      ]
 134      [ [{ "normal form predicates" * }]
 135        { "" "" "" "" "" "" "" "" "" }
 136        { "+" "+" "+" "+" "+" "-" "+" "+" "+" }
 137        { "evaluation for full rt-reduction (terms)"
 138          "normal form for full rt-reduction (terms)"
 139          "irreducible forms for fulld rt-reduction (terms)"
 140          "reducible forms for full rt-reduction (terms)"
 141          "evaluation for reduction (terms)"
 142          "normal form for reduction (lists of terms) removed"
 143          "irreducible forms for reduction (terms)"
 144          "reducible forms for reduction (terms)"
 145          "abstract reducibility properties (items)"
 146        }
 147      ]
 148      [ [{ "reduction and type synthesis" * }]
 149        { "" "" "@" "@" "" "" "" "@" "@" }
 150        { "+" "+" "+" "*" "-" "+" "-" "*" "-" }
 151        { "stratified full rt-computation (terms, lenvs)"
 152          "stratified full rt-transition (terms, lenvs)"
 153          "decomposed rt-computation (terms)"
 154          "primitive counted iterated type synthesis with δ,s,l,e (terms)"
 155          "syntax-oriented type synthesis (terms) removed"
 156          "refinement for reduction (lenvs)"
 157          "context-free computation (terms) removed"
 158          "primitive context-sensitive transition with typed β, δ, (wrong) ζ, θ, ε (terms, lenvs)"
 159          "context-free transition (terms, lenvs) removed"
 160        }
 161      ]
 162      [ [{ "substitution" * }]
 163        { "" "" "" "@"}
 164        { "-" "-" "+" "-" }
 165        { "every ref (terms) removed"
 166          "zero or more refs (lenvs) removed"
 167          "(restricted) zero or more selected refs (terms)"
 168          "one or more refs (terms, lenvs, closures) removed"
 169        }
 170      ]
 171      [ [{ "degree" * }]
 172        { "@" "" "@" "" }
 173        { "+" "+" "+" "+" }
 174        { "refinement for degree (lenvs)"
 175          "degree assignment (terms)"
 176          "concrete systems of reference"
 177          "abstract system of reference with compatibility condition"
 178        }
 179      ]
 180      [ [{ "relocation and slicing" * }]
 181        { "" "" "" "" "" "" }
 182        { "+" "+" "+" "-" "-" "-" }
 183        { "look-up predicate (genvs)"
 184          "abstract properties for relations"
 185          "switch in basic and finite slicing (lenvs)"
 186          "look-up predicate (lenvs) removed"
 187          "parametric relocation (terms) removed"
 188          "level update functions removed"
 189        }
 190      ]
 191      [ [{ "free varibles" * }]
 192        { "" "" }
 193        { "+" "+" }
 194        { "union (referred lenvs)"
 195          "hereditarily free variable predicate"
 196        }
 197      ]
 198      [ [{ "helpers" * }]
 199        { "" "" "" "" "" "" "" "" "" "" "" "" }
 200        { "+" "-" "-" "+" "+" "-" "-" "-" "-" "+" "+" "-" }
 201        { "unfold (closures)"
 202          "append (closures) removed"
 203          "refinement (lenvs) removed"
 204          "refinement (selected lenvs)"
 205          "append (lenvs)"
 206          "left cons (lenvs) removed"
 207          "flat construction clear (lenvs) removed"
 208          "sort extraction (lenvs) removed"
 209          "context predicate (terms) removed"
 210          "neutral predicate (terms)"
 211          "multiple application (terms)"
 212          "multiple head construction (terms) removed"
 213        }
 214      ]
 215      [ [{ "extension" * }]
 216        { "" "" }
 217        { "+" "+" }
 218        { "abstract properties with extension (lenvs, referred lenvs)"
 219          "for 3-relations (lenvs, referred lenvs)"
 220        }
 221      ]
 222      [ [{ "syntax" * }]
 223        { "@" "@" "@" "@" "@" "" }
 224        { "+" "+" "+" "-" "-" "-" }
 225        { "polarized binders for terms"
 226          "non-negative integer global references for terms"
 227          "syntactic support for genvs with typed abstraction, abbreviation"
 228          "numbered sorts, application, type annotation removed from lenvs"
 229          "exclusion binder removed from terms and lenvs"
 230          "specialized lists of terms removed with length, right cons"
 231        }
 232      ]
 233      [ [{ "parameters" * }]
 234        { "" "" }
 235        { "+" "-"}
 236        { "concrete sort hierarchies"
 237          "iterated next function (sort hierarchy) removed"
 238        }
 239      ]
 240      [ [{ "ground" * }]
 241        { "" "" "" }
 242        { "+" "+" "+" }
 243        { "lists and non-negative integers with infinity"
 244          "support for iterated functions"
 245          "library extension for transitive closures and booleans"
 246        }
 247      ]
 248     }
 249   ]
 250
 251   class "red"
 252   [ { "λδ-1A" + "(November 2006)" * }
 253     {
 254      [ [{ "validity" * }]
 255        { "@" "" "" }
 256        { "+" "+" "+" }
 257        { "flat or invalid entry clear (lenvs)"
 258          "refinement for type assignment (lenvs)"
 259          "primitive type assignment (terms, specialized lists of terms)"
 260        }
 261      ]
 262      [ [{ "equivalences" * }]
 263        { "" "@" "" "" "" }
 264        { "+" "+" "+" "+" "+" }
 265        { "(transitive closure) context-sensitive r-eqivalence (terms)"
 266          "primitive context-sensitive r-eqivalence (terms)"
 267          "context-free r-eqivalence (terms)"
 268          "equivalence for outer reduction (terms)"
 269          "level equivalence (binary arities)"
 270        }
 271      ]
 272      [ [{ "partial orders" * }]
 273        { "" "" "" "" }
 274        { "+" "+" "+" "+" }
 275        { "order relation (specialized lists of terms) based on lengths"
 276          "order relations (terms, lenvs, closures, binary arities) based on weights"
 277          "simple weights (terms, lenvs, closures, binary arities)"
 278          "complex weight (terms)"
 279        }
 280      ]
 281      [ [{ "reducibility" * }]
 282        { "" "" "" "" "" "" "" }
 283        { "+" "+" "+" "+" "+" "+" "+" }
 284        { "refinement for reducibility (lenvs)"
 285          "Girards's candidates (closures)"
 286          "strong normalization for reduction (terms, specialized lists of terms)"
 287          "refinement for arity (lenvs)"
 288          "arity assignment (terms)"
 289          "succerssor, addition, look-up predicate (binary arities)"
 290          "binary arities with sort, implication"
 291        }
 292      ]
 293      [ [{ "normal form predicates" * }]
 294        { "" }
 295        { "+" }
 296        { "normal form for context-sensitive reduction (terms, specialized lists of terms)"
 297        }
 298      ]
 299      [ [{ "reduction and type synthesis" * }]
 300        { "" "@" "" "" "" "@" }
 301        { "+" "+" "+" "+" "+" "+" }
 302        { "countless iterated type synthesis (terms)"
 303          "syntax-oriented type synthesis with δ,s,l (terms)"
 304          "context-sensitive computation (terms)"
 305          "context-free computation (terms)"
 306          "(restricted) context-sensitive transition (terms)"
 307          "context-free transition with untyped β, δ, ζ, θ, ε (terms, lenvs)"
 308        }
 309      ]
 310      [ [{ "substitution" * }]
 311        { "" "" "@"}
 312        { "+" "+" "+" }
 313        { "every ref (terms)"
 314          "zero or more refs (terms, lenvs)"
 315          "one or more refs (terms, lenvs, closures)"
 316        }
 317      ]
 318      [ [{ "relocation and slicing" * }]
 319        { "" "" "" "" "" "" "" "" }
 320        { "+" "+" "+" "+" "+" "+" "+" "+" }
 321        { "order relation (lenvs) based on look-up"
 322          "look-up predicate (lenvs)"
 323          "finite slicing (lenvs)"
 324          "basic slicing (lenvs)"
 325          "finite relocation (terms, specialized lists of terms)"
 326          "basic relocation (terms, specialized lists of terms)"
 327          "parametric relocation (terms)"
 328          "level update functions"
 329        }
 330      ]
 331      [ [{ "helpers" * }]
 332        { "" "" "" "" "" "" "" "" }
 333        { "+" "+" "+" "+" "+" "+" "+" "+" }
 334        { "append (closures)"
 335          "refinement (lenvs)"
 336          "length (lenvs)"
 337          "left cons (lenvs)"
 338          "flat entry clear (lenvs)"
 339          "sort extraction (lenvs)"
 340          "context predicate (terms)"
 341          "multiple head construction (terms)"
 342        }
 343      ]
 344      [ [{ "syntax" * }]
 345        { "@" "" "@" }
 346        { "+" "+" "+" }
 347        { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation"
 348          "specialized lists of terms with length, right cons"
 349          "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation"
 350        }
 351      ]
 352      [ [{ "parameters" * }]
 353        { "" "@" }
 354        { "+" "+" }
 355        { "iterated next function (sort hierarchy)"
 356          "abstract sort hierarchy with strict monotonicity condition based on non-negative integers"
 357        }
 358      ]
 359      [ [{ "ground" * }]
 360        { "" "" }
 361        { "+" "+" }
 362        { "finite reference transforming maps as compositions of basic ones"
 363          "library extension for logic and non-negative integers"
 364        }
 365      ]
 366     }
 367   ]
 368
 369 }
 370
 371 class "capitalize" [ 0 ]
 372
 373 class "center" { 2 3 }