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