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