From: Ferruccio Guidi Date: Fri, 6 Dec 2019 21:10:54 +0000 (+0100) Subject: λδ web site update X-Git-Tag: make_still_working~214 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a82d87a4c2ff9f518385fba7357dafb632a22882 λδ web site update + changes of λδ-2A vs λδ-1A completed + log page linked to site --- diff --git a/helm/www/lambdadelta/web/home/changes.ldw.xml b/helm/www/lambdadelta/web/home/changes.ldw.xml deleted file mode 100644 index 4287ac584..000000000 --- a/helm/www/lambdadelta/web/home/changes.ldw.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - Changes - - - - -
- diff --git a/helm/www/lambdadelta/web/home/changes.tbl b/helm/www/lambdadelta/web/home/changes.tbl deleted file mode 100644 index d25be28c7..000000000 --- a/helm/www/lambdadelta/web/home/changes.tbl +++ /dev/null @@ -1,118 +0,0 @@ -name "changes" - -table { - class "gray" - [ "version" [ "aspect" [ "" "changes" ]] - ] - - class "orange" - [ { "λδ-2B" + "(unreleased)" * } - { - [ [{ "equivalences" * }] - { "+" "+" "+" "-" } - { "equivalence for full rt-reduction (terms)" - "equivalence for whd rt-reduction (terms)" - "equivalence for extended rt-reduction (terms, referred lenvs, closures)" - "syntactic equivalence (closures) removed" - } - ] - [ [{ "weights" * }] - { "+" } - { "switch in primitive order relations for closures to enable the exclusion binder" - } - ] - [ [{ "relocation" * }] - { "" } - { "" - } - ] - [ [{ "syntax" * }] - { "+" } - { "exclusion binder for lenvs" - } - ] - [ [{ "ground" * }] - { "+" "*" "+" "-" } - { "rt-transition counters" - "generic reference transforming maps as streams of non-negative integers" - "extensional equality, labelled transitive closures and streams" - "non-negative integers with infinity removed" - } - ] - } - ] - - class "orange" - [ { "λδ-2A" + "(October 2014)" * } - { - [ [{ "equivalences" * }] - { "+" } - { "syntactic equivalence (selected lenvs, referred lenvs, closures)" - } - ] - [ [{ "weights" * }] - { "*" "-" } - { "primitive order relations for closures" - "complex weight (terms) removed" - } - ] - [ [{ "relocation" * }] - { "-" } - { "level update functions removed" - } - ] - [ [{ "syntax" * }] - { "+" "+" "+" "-" "-" } - { "polarized binders for terms" - "non-negative integer global references for terms" - "syntactic support for genvs with typed abstraction, abbreviation" - "numbered sorts, application, type annotation removed from lenvs" - "exclusion binder removed from terms and lenvs" - } - ] - [ [{ "ground" * }] - { "+" "+" } - { "lists and non-negative integers with infinity" - "library extension for transitive closures and booleans" - } - ] - } - ] - - class "red" - [ { "λδ-1A" + "(November 2006)" * } - { - [ [{ "equivalences" * }] - { "" } - { "equivalence for outer reduction (terms)" - } - ] - [ [{ "weights" * }] - { "" "" "" } - { "order relations (terms, lenvs, closures) based on weights" - "simple weights (terms, lenvs, closures)" - "complex weight (terms)" - } - ] - [ [{ "relocation" * }] - { "" } - { "level update functions" - } - ] - [ [{ "syntax" * }] - { "" "" } - { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation" - "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation" } - ] - [ [{ "ground" * }] - { "" "" } - { "finite reference transforming maps as compositions of basic ones" - "library extension for logic and non-negative integers" - } - ] - } - ] - -} - -class "center" { 2 } diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml index 92cd421bd..5625cdb8c 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -22,7 +22,7 @@ as a set of machine-checked digital specifications. - Current version: + λδ-2B for for Matita 0.99.4 (released: ). Documentation (J2a). diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index e76cdd5f8..3f840b7a0 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -12,7 +12,9 @@ table [ [ @@("html/news#visibility" "visibility") * ] } class "white" { - [ @@("html/specification" "specification") * ] + [ @@("html/specification" "specification") + @@("html/changes" "specification log") + * ] [ @@("html/specification#v2" "version 2") "(" ^ @@("html/ground_2" "background") + "-" + @@("html/static_2" "syntax") + "-" + diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 0dfec650c..721939a44 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -28,6 +28,12 @@
+ + + System and Specification + (updated ). + + Informational pages on the specifications are provided. diff --git a/matita/matita/contribs/lambdadelta/web/changes.ldw.xml b/matita/matita/contribs/lambdadelta/web/changes.ldw.xml new file mode 100644 index 000000000..2765bf488 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/web/changes.ldw.xml @@ -0,0 +1,24 @@ + + + + + + System and Specification Log + + The next table logs the system features and the specification features + changed in each version with respect to the previous one. + + + Marks: + "@" system feature, + "+" added feature, "*" replaced feature, "-" removed feature + +
+ +
+ diff --git a/matita/matita/contribs/lambdadelta/web/changes.tbl b/matita/matita/contribs/lambdadelta/web/changes.tbl new file mode 100644 index 000000000..bf985679d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/web/changes.tbl @@ -0,0 +1,373 @@ +name "changes" + +table { + class "gray" + [ "specification" [ "aspect" [ "" "" "changes" ]] + ] + + class "orange" + [ { "λδ-2B" + "(November 2019)" * } + { + [ [{ "validity" * }] + { "@" "" "@" } + { "+" "-" "*" } + { "type assignment (terms)" + "stratified higher validity (terms) removed" + "primitive validity (terms)" + } + ] + [ [{ "equivalences" * }] + { "" "" "" "" } + { "+" "+" "+" "-" } + { "equivalence for full rt-reduction (terms)" + "equivalence for whd rt-reduction (terms)" + "equivalence for full rt-reduction (terms, referred lenvs, closures)" + "syntactic equivalence (closures) removed" + } + ] + [ [{ "partial orders" * }] + { "" } + { "+" } + { "switch in primitive order relations for closures to enable the exclusion binder" + } + ] + [ [{ "normal form predicates" * }] + { "" "" "" "" "" } + { "-" "-" "-" "-" "-" } + { "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" + } + ] + [ [{ "substitution" * }] + { "" } + { "-" } + { "zero or more refs (terms) removed" + } + ] + [ [{ "relocation" * }] + { "" "" "" "" } + { "-" "*" "-" "*" } + { "basic slicing (lenvs) removed" + "primitive finite slicing (lenvs)" + "basic relocation (lists of terms) removed" + "primitive finite relocation (terms, lists of terms)" + } + ] + [ [{ "free varibles" * }] + { "" } + { "+" } + { "union (referred lenvs) removed" + } + ] + [ [{ "syntax" * }] + { "@" } + { "+" } + { "exclusion binder for lenvs" + } + ] + [ [{ "ground" * }] + { "" "" "" "" } + { "+" "*" "+" "-" } + { "rt-transition counters" + "generic reference transforming maps as streams of non-negative integers" + "extensional equality, labelled transitive closures and streams" + "non-negative integers with infinity removed" + } + ] + } + ] + + class "orange" + [ { "λδ-2A" + "(October 2014)" * } + { + [ [{ "validity" * }] + { "" "" "@" "" "" "" "@" } + { "-" "-" "-" "+" "+" "+" "+" } + { "flat or invalid entry clear (lenvs) removed" + "refinement for type assignment (lenvs) removed" + "primitive type assignment (terms, specialized lists of terms) removed" + "confluence and preservation properties" + "higher validity (terms)" + "refinement for validity (lenvs)" + "primitive stratified validity (terms)" + } + ] + [ [{ "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" + "syntactic equivalence (selected lenvs, referred lenvs, selected closures)" + } + ] + [ [{ "partial orders" * }] + { "" "" "" "" "" "" "" } + { "+" "*" "+" "-" "-" "-" "-" } + { "big-tree order relations (closures)" + "primitive order relations for closures" + "simple weight (restricted closures)" + "order relation (lists of terms) based on lengths removed" + "order relations (binary arities) based on weights removed" + "simple weights (binary arities) removed" + "complex weight (terms) removed" + } + ] + [ [{ "reducibility" * }] + { "" "" "" "" "" "" "" "" } + { "+" "+" "*" "+" "*" "+" "*" "-" } + { "compatibility predicate for strong normalization (referred lenvs)" + "strong normalization for bt-reduction (referred closures)" + "strong normalization for full rt-reduction (terms, lists of terms, referred lenvs)" + "arrow candidate, arity interpretation" + "abatract Tait's candidates with 7 postulates" + "abstract computation for reducibility with 4 postulates" + "atomic arities with sort, implication" + "succerssor, addition, look-up predicate (binary arities) removed" + } + ] + [ [{ "normal form predicates" * }] + { "" "" "" "" "" "" "" "" "" } + { "+" "+" "+" "+" "+" "-" "+" "+" "+" } + { "evaluation for full rt-reduction (terms)" + "normal form for full rt-reduction (terms)" + "irreducible forms for fulld rt-reduction (terms)" + "reducible forms for full rt-reduction (terms)" + "evaluation for reduction (terms)" + "normal form for reduction (lists of terms) removed" + "irreducible forms for reduction (terms)" + "reducible forms for reduction (terms)" + "abstract reducibility properties (items)" + } + ] + [ [{ "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)" + "context-free computation (terms) removed" + "primitive context-sensitive transition with typed β, δ, (wrong) ζ, θ, ε (terms, lenvs)" + "context-free transition (terms, lenvs) removed" + } + ] + [ [{ "substitution" * }] + { "" "" "" "@"} + { "-" "-" "+" "-" } + { "every ref (terms) removed" + "zero or more refs (lenvs) removed" + "(restricted) zero or more selected refs (terms)" + "one or more refs (terms, lenvs, closures) removed" + } + ] + [ [{ "degree" * }] + { "@" "" "@" "" } + { "+" "+" "+" "+" } + { "refinement for degree (lenvs)" + "degree assignment (terms)" + "concrete systems of reference" + "abstract system of reference with compatibility condition" + } + ] + [ [{ "relocation and slicing" * }] + { "" "" "" "" "" "" } + { "+" "+" "+" "-" "-" "-" } + { "look-up predicate (genvs)" + "abstract properties for relations" + "switch in basic and finite slicing (lenvs)" + "look-up predicate (lenvs) removed" + "parametric relocation (terms) removed" + "level update functions removed" + } + ] + [ [{ "free varibles" * }] + { "" "" } + { "+" "+" } + { "union (referred lenvs)" + "hereditarily free variable predicate" + } + ] + [ [{ "helpers" * }] + { "" "" "" "" "" "" "" "" "" "" "" "" } + { "+" "-" "-" "+" "+" "-" "-" "-" "-" "+" "+" "-" } + { "unfold (closures)" + "append (closures) removed" + "refinement (lenvs) removed" + "refinement (selected lenvs)" + "append (lenvs)" + "left cons (lenvs) removed" + "flat construction clear (lenvs) removed" + "sort extraction (lenvs) removed" + "context predicate (terms) removed" + "neutral predicate (terms)" + "multiple application (terms)" + "multiple head construction (terms) removed" + } + ] + [ [{ "extension" * }] + { "" "" } + { "+" "+" } + { "abstract properties with extension (lenvs, referred lenvs)" + "for 3-relations (lenvs, referred lenvs)" + } + ] + [ [{ "syntax" * }] + { "@" "@" "@" "@" "@" "" } + { "+" "+" "+" "-" "-" "-" } + { "polarized binders for terms" + "non-negative integer global references for terms" + "syntactic support for genvs with typed abstraction, abbreviation" + "numbered sorts, application, type annotation removed from lenvs" + "exclusion binder removed from terms and lenvs" + "specialized lists of terms removed with length, right cons" + } + ] + [ [{ "parameters" * }] + { "" "" } + { "+" "-"} + { "concrete sort hierarchies" + "iterated next function (sort hierarchy) removed" + } + ] + [ [{ "ground" * }] + { "" "" "" } + { "+" "+" "+" } + { "lists and non-negative integers with infinity" + "support for iterated functions" + "library extension for transitive closures and booleans" + } + ] + } + ] + + class "red" + [ { "λδ-1A" + "(November 2006)" * } + { + [ [{ "validity" * }] + { "@" "" "" } + { "+" "+" "+" } + { "flat or invalid entry clear (lenvs)" + "refinement for type assignment (lenvs)" + "primitive type assignment (terms, specialized lists of terms)" + } + ] + [ [{ "equivalences" * }] + { "" "@" "" "" "" } + { "+" "+" "+" "+" "+" } + { "(transitive closure) context-sensitive r-eqivalence (terms)" + "primitive context-sensitive r-eqivalence (terms)" + "context-free r-eqivalence (terms)" + "equivalence for outer reduction (terms)" + "level equivalence (binary arities)" + } + ] + [ [{ "partial orders" * }] + { "" "" "" "" } + { "+" "+" "+" "+" } + { "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)" + } + ] + [ [{ "reducibility" * }] + { "" "" "" "" "" "" "" } + { "+" "+" "+" "+" "+" "+" "+" } + { "refinement for reducibility (lenvs)" + "Girards's candidates (closures)" + "strong normalization for reduction (terms, specialized lists of terms)" + "refinement for arity (lenvs)" + "arity assignment (terms)" + "succerssor, addition, look-up predicate (binary arities)" + "binary arities with sort, implication" + } + ] + [ [{ "normal form predicates" * }] + { "" } + { "+" } + { "normal form for context-sensitive reduction (terms, specialized lists of terms)" + } + ] + [ [{ "reduction and type synthesis" * }] + { "" "@" "" "" "" "@" } + { "+" "+" "+" "+" "+" "+" } + { "countless iterated type synthesis (terms)" + "syntax-oriented type synthesis with δ,s,l (terms)" + "context-sensitive computation (terms)" + "context-free computation (terms)" + "(restricted) context-sensitive transition (terms)" + "context-free transition with untyped β, δ, ζ, θ, ε (terms, lenvs)" + } + ] + [ [{ "substitution" * }] + { "" "" "@"} + { "+" "+" "+" } + { "every ref (terms)" + "zero or more refs (terms, lenvs)" + "one or more refs (terms, lenvs, closures)" + } + ] + [ [{ "relocation and slicing" * }] + { "" "" "" "" "" "" "" "" } + { "+" "+" "+" "+" "+" "+" "+" "+" } + { "order relation (lenvs) based on look-up" + "look-up predicate (lenvs)" + "finite slicing (lenvs)" + "basic slicing (lenvs)" + "finite relocation (terms, specialized lists of terms)" + "basic relocation (terms, specialized lists of terms)" + "parametric relocation (terms)" + "level update functions" + } + ] + [ [{ "helpers" * }] + { "" "" "" "" "" "" "" "" } + { "+" "+" "+" "+" "+" "+" "+" "+" } + { "append (closures)" + "refinement (lenvs)" + "length (lenvs)" + "left cons (lenvs)" + "flat entry clear (lenvs)" + "sort extraction (lenvs)" + "context predicate (terms)" + "multiple head construction (terms)" + } + ] + [ [{ "syntax" * }] + { "@" "" "@" } + { "+" "+" "+" } + { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation" + "specialized lists of terms with length, right cons" + "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation" + } + ] + [ [{ "parameters" * }] + { "" "@" } + { "+" "+" } + { "iterated next function (sort hierarchy)" + "abstract sort hierarchy with strict monotonicity condition based on non-negative integers" + } + ] + [ [{ "ground" * }] + { "" "" } + { "+" "+" } + { "finite reference transforming maps as compositions of basic ones" + "library extension for logic and non-negative integers" + } + ] + } + ] + +} + +class "capitalize" [ 0 ] + +class "center" { 2 3 }