From: Ferruccio Guidi Date: Wed, 1 Jun 2016 14:33:30 +0000 (+0000) Subject: - source web pages for lambdadelta_1 X-Git-Tag: make_still_working~570 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b4b18a8f2c3f33fe49edef3bc8068332edf299e2 - source web pages for lambdadelta_1 - minor bugs fixed in the web site --- diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml b/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml new file mode 100644 index 000000000..421276cf2 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml @@ -0,0 +1,46 @@ + + + + + + Abstract Syntax and Behavior + This is a summary of available syntactic items and reductions (block structure). + + + * In terms only. + + + Summary of the Specification + Here is a numerical account of the specification's contents + and its timeline. + +
+ + + Update with backports from the abandoned specification of λδ version 2. + + + Specification is concluded. + + + Decidability of native type assignment, λδ version 1 is released. + + + Preservation of native type by reduction, λδ version 1 is announced. + + + Specification starts. + + + Logical Structure of the Specification + This table reports the specification's components and their planes. + +
+ +
+ diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl new file mode 100644 index 000000000..996e35b50 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl @@ -0,0 +1,39 @@ +name "basic_1_blk" + +table { + class "gray" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "→ζ *" ] [ "annotator (with →ϵ *)" ] + [ "applicator (with →θ *)" ] [ "reference *" ] [ "reduction" ] + ] + } ] + [ { "{X | Γ ⊢ ⊤}" * } { + class "wine" [ + [ "exclusion" ] [ "Γ ⊢ χ" ] + [ "yes" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "magenta" [ + [ "typed abstraction" ] [ "Γ ⊢ λW" ] + [ "no" ] [ "<W>" ] [ "(V)" ] [ "#i" ] [ "→β *" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "prune" [ + [ "abbreviation" ] [ "Γ ⊢ δV" ] + [ "yes" ] [ "no" ] [ "no" ] [ "#i" ] [ "→δ" ] + ] + } ] + [ { "no" * } { + class "blue" [ + [ "sort" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "top" { * } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl new file mode 100644 index 000000000..6afa13d55 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl @@ -0,0 +1,218 @@ +name "basic_1_src" + +table uri "static/coq/lambdadelta/basic_1/" ext ".txt" { + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "wine" + [ { "examples" * } { + [ { "terms with special features" * } { + [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ] + } + ] + } + ] + class "magenta" + [ { "" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] +(* + [ { "higher order dynamic typing" * } { + [ { "higher order native type assignment" * } { + [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + } + ] + } + ] +*) + class "prune" + [ { "dynamic typing" * } { + [ { "well-formed contexts" * } { + [ @@"wf3_defs" @@"wf3_props" * ] + } + ] + [ { "context ref. for native type assignment" * } { + [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ] + } + ] + [ { "native type assignment" * } { + [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ] + } + ] + } + ] + class "blue" + [ { "equivalence" * } { + [ { "context-sensitive equivalence" * } { + [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ] + } + ] + [ { "context-free equivalence" * } { + [ @@"pc1_defs" @@"pc1_props" * ] + } + ] + } + ] + class "sky" + [ { "" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] + class "cyan" + [ { "computation" * } { + [ { "context ref. for reducibility" * } { + [ @@"csubc_defs" @@"csubc_props" * ] + } + ] + [ { "reducibility" * } { + [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ] + } + ] + [ { "strongly normalizing computation" * } { + [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ] + } + ] + [ { "context-sensitive computation" * } { + [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ] + } + ] + [ { "context-free computation" * } { + [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ] + } + ] + } + ] + class "water" + [ { "reduction" * } { + [ { "normal forms for context-sensitive reduction" * } { + [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ] + } + ] + [ { "context-sensitive reduction" * } { + [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ] + } + ] + [ { "normal forms for context-free reduction" * } { + [ "" @@"nf0_dec" * ] + } + ] + [ { "context-free reduction" * } { + [ @@"wcpr0_defs" * ] + [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ] + } + ] + } + ] + class "green" + [ { "unfold" * } { + [ { "iterated static type assignment" * } { + [ @@"sty1_defs" @@"sty1_props" * ] + } + ] + } + ] + class "grass" + [ { "static typing" * } { + [ { "static type assignment" * } { + [ @@"sty0_defs" @@"sty0_props" * ] + } + ] + [ { "context ref. for binary arity assignment" * } { + [ @@"csuba_defs" @@"csuba_props" * ] + } + ] + [ { "binary arity assignment" * } { + [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ] + } + ] + [ { "binary arity" * } { + [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ] + } + ] + [ { "parameters" * } { + [ @@"parameter_defs" * ] + } + ] + [ { "basic context ref." * } { + [ @@"csubv_defs" * ] + } + ] + } + ] + class "yellow" + [ { "multiple substitution" * } { + [ { "iterated context slicing" * } { + [ @@"drop1_defs" @@"drop1_props" * ] + } + ] + [ { "generic term relocation" * } { + [ @@"lift1_defs" @@"lift1_props" * ] + } + ] + } + ] + class "orange" + [ { "substitution" * } { + [ { "ordinary substitution" * } { + [ @@"subst_defs" @@"subst_props" * ] + [ @@"csubst1_defs" @@"csubst1_props" * ] + [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ] + } + ] + [ { "normal forms for ordinary strict substitution" * } { + [ "" @@"dnf_dec" * ] + } + ] + [ { "ordinary strict substitution" * } { + [ @@"fsubst0_defs" * ] + [ @@"csubst0_defs" * ] + [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ] + } + ] + [ { "basic local env. slicing" * } { + [ @@"getl_defs" @@"getl_props" * ] + [ @@"drop_defs" @@"drop_props" * ] + } + ] + [ { "basic term relocation" * } { + [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "closures" * } { + [ @@"flt_defs" * ] + } + ] + [ { "contexts" * } { + [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ] + } + ] + [ { "terms" * } { + [ @@"tlist_defs" * ] + [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ] + } + ] + } + ] +} + +class "top" { * } + +class "capitalize italic" { 0 } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl new file mode 100644 index 000000000..c87e8d037 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl @@ -0,0 +1,28 @@ +name "basic_1_sum" + +table { + class "gray" [ "category" + [ "objects" * ] + ] + class "cyan" [ "sizes" + [ "files" "120" ] + [ "characters" "198089" ] + [ "nodes" "1449099" ] + ] + class "green" [ "propositions" + [ "theorems" "81" ] + [ "lemmas" "618" ] + [ "total" "699" ] + ] + class "yellow" [ "concepts" + [ "declared" "39" ] + [ "defined" "47" ] + [ "total" "86" ] + ] +} + +class "capitalize italic" { 0 } + +class "italic" { 1 } { 3 } { 5 } + +class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml b/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml new file mode 100644 index 000000000..846fe7ce9 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml @@ -0,0 +1,33 @@ + + + + + + Summary of the Specification + Here is a numerical account of the specification's contents + and its timeline. + +
+ + + Update with backports from the abandoned specification of λδ version 2. + + + Specification is concluded. + + + Specification starts. + + + Logical Structure of the Specification + This table reports the specification's components and their planes. + +
+ +
+ diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl b/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl new file mode 100644 index 000000000..f8ce17263 --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl @@ -0,0 +1,50 @@ +name "ground_1_src" + +table uri "static/coq/lambdadelta/ground_1/" ext ".txt" { + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "grass" + [ { "multiple relocation" * } { + [ { "" * } { + [ @@"bg_plist" * ] + } + ] + } + ] + class "yellow" + [ { "extensions to the library" * } { + [ { "" * } { + [ @@"bg_hints" @@"bg_blt" * ] + } + ] + } + ] + class "orange" + [ { "generated logical decomposables" * } { + [ { "" * } { + [ @@"bg_types" @@"bg_props" * ] + } + ] + } + ] + class "red" + [ { "preamble" * } { + [ { "" * } { + [ @@"bg_require" @@"bg_rewrite" @@"bg_tactics" @@"bg_subst" * ] + } + ] + } + ] +} + +class "top" { * } + +class "capitalize italic" { 0 } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl b/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl new file mode 100644 index 000000000..88451619c --- /dev/null +++ b/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl @@ -0,0 +1,28 @@ +name "ground_1_sum" + +table { + class "gray" [ "category" + [ "objects" * ] + ] + class "cyan" [ "sizes" + [ "files" "10" ] + [ "characters" "15063" ] + [ "nodes" "14881" ] + ] + class "green" [ "propositions" + [ "theorems" "0" ] + [ "lemmas" "50" ] + [ "total" "50" ] + ] + class "yellow" [ "concepts" + [ "declared" "24" ] + [ "defined" "4" ] + [ "total" "28" ] + ] +} + +class "capitalize italic" { 0 } + +class "italic" { 1 } { 3 } { 5 } + +class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 602ed2c57..e4e4b3450 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 720fb0dee..9f7e234b6 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index f6b288778..78dd5c0f4 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -823,6 +823,6 @@

-
Last update: Tue, 31 May 2016 21:18:48 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5c8b09d63..42152ed06 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -811,6 +811,6 @@

-
Last update: Tue, 31 May 2016 21:18:48 +0200
+
Last update: Wed, 01 Jun 2016 16:23:07 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 0fedfb151..a687f7a62 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -183,7 +183,7 @@
- +
P2d. F. Guidi: Considerations on Automath in Light of the Grundlagen (2016-05). Presentation at University of Bologna (slides).F. Guidi: Considerations on Automath in Light of the Grundlagen (revised 2016-06). Presentation at University of Bologna (slides).
@@ -401,6 +401,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/download/ld_talk_9s.pdf b/helm/www/lambdadelta/download/ld_talk_9s.pdf index 3f7c2bee7..b7f3ca96c 100644 Binary files a/helm/www/lambdadelta/download/ld_talk_9s.pdf and b/helm/www/lambdadelta/download/ld_talk_9s.pdf differ diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index bf75563e5..1362fd68a 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -291,6 +291,6 @@

-
Last update: Tue, 31 May 2016 21:18:48 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index fc266948a..d982e3846 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -823,6 +823,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:23:06 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 6bf8c301f..6c8adae77 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -302,6 +302,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index b3e330c9f..ea9e12c41 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -186,7 +186,7 @@
Disclaimer [spacer]
- The systens of the λδ family are not related intentionally to + The systems of the λδ family are not related intentionally to any other system having (variations of) the symbols λ and δ in its name or syntax. Examples include (but are not limited to):
@@ -252,7 +252,7 @@
[Smiling face] - Moreover, the systens of the λδ family are not related intentionally to + Moreover, the systems of the λδ family are not related intentionally to Lady Lambdadelta, the Witch of Certainty of the sound novel Umineko no Naku Koro ni. @@ -283,6 +283,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 6101558d2..80e936a07 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -380,6 +380,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index ec0d85773..f67b59787 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -378,6 +378,6 @@

-
Last update: Tue, 31 May 2016 21:18:47 +0200
+
Last update: Wed, 01 Jun 2016 16:28:47 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 3e59b57e6..7b450ff46 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -48,7 +48,7 @@ table { "F. Guidi:" + @@("download/ld_talk_9s.pdf" "Considerations on Automath in Light of the Grundlagen") + - "(2016-05)." + + "(revised 2016-06)." + "Presentation at University of Bologna (slides)." * } ] diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index c5004f36a..a7e9b6702 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -86,7 +86,7 @@ Disclaimer - The systens of the λδ family related intentionally to + The systems of the λδ family related intentionally to any other system having (variations of) the symbols λ and δ in its name or syntax. Examples include (but are not limited to): @@ -146,7 +146,7 @@ - Moreover, the systens of the λδ family related intentionally to + Moreover, the systems of the λδ family related intentionally to Lady Lambdadelta, the Witch of Certainty of the sound novel Umineko no Naku Koro ni. diff --git a/helm/www/lambdadelta/web/home/osn.ldw.xml b/helm/www/lambdadelta/web/home/osn.ldw.xml index ef8580bb8..d83efaaaf 100644 --- a/helm/www/lambdadelta/web/home/osn.ldw.xml +++ b/helm/www/lambdadelta/web/home/osn.ldw.xml @@ -11,7 +11,7 @@ is an easy and flexible data-interchange text format intended for the lightweight representation of generic abstract syntax trees in the domain of formal systems. - In order to meet theese design goals, OSN pursues the following features. + In order to meet these design goals, OSN pursues the following features.