--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ logo = "crux"
+ head = "cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)"
+>
+ <sitemap name="sitemap"/>
+
+ <section6 name="blocks">Abstract Syntax and Behavior</section6>
+ <body>This is a summary of available syntactic items and reductions (block structure).
+ </body>
+ <table name="basic_1_blk"/>
+ <body>* In terms only.
+ </body>
+
+ <section6 name="summary">Summary of the Specification</section6>
+ <body>Here is a numerical account of the specification's contents
+ and its timeline.
+ </body>
+ <table name="basic_1_sum"/>
+
+ <news class="delta" date="January 2015.">
+ Update with backports from the abandoned specification of λδ version 2.
+ </news>
+ <news class="delta" date="May 2008.">
+ Specification is concluded.
+ </news>
+ <news class="gamma" date="November 2006.">
+ Decidability of native type assignment, λδ version 1 is released.
+ </news>
+ <news class="beta" date="December 2005.">
+ Preservation of native type by reduction, λδ version 1 is announced.
+ </news>
+ <news class="alpha" date="May 2004.">
+ Specification starts.
+ </news>
+
+ <section6 name="structure">Logical Structure of the Specification</section6>
+ <body>This table reports the specification's components and their planes.
+ </body>
+ <table name="basic_1_src"/>
+
+ <footer/>
+</page>
--- /dev/null
+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 }
--- /dev/null
+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 }
--- /dev/null
+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 }
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "\lambda\delta home page"
+ title = "\lambda\delta home page"
+ logo = "crux"
+ head = "cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)"
+>
+ <sitemap name="sitemap"/>
+
+ <section6 name="summary">Summary of the Specification</section6>
+ <body>Here is a numerical account of the specification's contents
+ and its timeline.
+ </body>
+ <table name="ground_1_sum"/>
+
+ <news class="delta" date="January 2015.">
+ Update with backports from the abandoned specification of λδ version 2.
+ </news>
+ <news class="delta" date="May 2008.">
+ Specification is concluded.
+ </news>
+ <news class="alpha" date="May 2004.">
+ Specification starts.
+ </news>
+
+ <section6 name="structure">Logical Structure of the Specification</section6>
+ <body>This table reports the specification's components and their planes.
+ </body>
+ <table name="ground_1_src"/>
+
+ <footer/>
+</page>
--- /dev/null
+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 }
--- /dev/null
+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 }
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:23:06 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:23:06 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:23:06 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:23:07 +0200</div>
</body>
</html>
<td class="snns top" id="ldP2d">
<span class="emph alpha">P2d.</span>
</td>
- <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_9s.pdf">Considerations on Automath in Light of the Grundlagen</a> (<span class="emph beta">2016-05</span>). Presentation at University of Bologna (slides).</td>
+ <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_9s.pdf">Considerations on Automath in Light of the Grundlagen</a> (revised <span class="emph gamma">2016-06</span>). Presentation at University of Bologna (slides).</td>
</tr>
<tr>
<td class="nnns top" />
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:28:47 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:48 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:23:06 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:23:06 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:28:47 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[spacer]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b9.png" />
</div>
<div xmlns:ld="http://lambdadelta.info/" class="text">
- The systens of the λδ family <span class="emph alpha">are not</span> related intentionally to
+ The systems of the λδ family <span class="emph alpha">are not</span> related intentionally to
any other system having (variations of) the symbols λ and δ in its name or syntax.
Examples include (but are not limited to):
</div>
</ul>
<div xmlns:ld="http://lambdadelta.info/" class="text">
<img class="icon32" alt="[Smiling face]" title="Smile!" src="http://lambdadelta.info/images/smile.png" />
- Moreover, the systens of the λδ family <span class="emph alpha">are not</span> related intentionally to
+ Moreover, the systems of the λδ family <span class="emph alpha">are not</span> related intentionally to
<a href="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</a>,
the Witch of Certainty of the sound novel
<a href="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</a>.
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:28:47 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:28:47 +0200</div>
</body>
</html>
<div xmlns:ld="http://lambdadelta.info/" class="spacer">
<br />
</div>
- <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 31 May 2016 21:18:47 +0200</div>
+ <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 01 Jun 2016 16:28:47 +0200</div>
</body>
</html>
"F. Guidi:" +
@@("download/ld_talk_9s.pdf"
"Considerations on Automath in Light of the Grundlagen") +
- "(<span class=\"emph beta\">2016-05</span>)." +
+ "(revised <span class=\"emph gamma\">2016-06</span>)." +
"Presentation at University of Bologna (slides)."
* }
]
<section9 name="disclaimer">Disclaimer</section9>
<body>
- The systens of the λδ family <notice class="alpha" text="are not"/> related intentionally to
+ The systems of the λδ family <notice class="alpha" text="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):
</body>
<body>
<img logo="smile"/>
- Moreover, the systens of the λδ family <notice class="alpha" text="are not"/> related intentionally to
+ Moreover, the systems of the λδ family <notice class="alpha" text="are not"/> related intentionally to
<link to="http://umineko.wikia.com/wiki/Lambdadelta">Lady Lambdadelta</link>,
the Witch of Certainty of the sound novel
<link to="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</link>.
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.
</body>
<list><style class="red-mark"><item><style class="alpha">
<link to="https://en.wikipedia.org/wiki/S-expression">Symbolic expressions</link>
contrary to <link to="http://www.w3.org/TR/2008/REC-xml-20081126/#sec-origin-goals">XML design goal 10</link>.
Compared to other data-interchange formats based on symbolic expressions,
like <link to="http://people.csail.mit.edu/rivest/Sexp.txt">canonical symbolic expressions</link>,
- representing arbitrary data in binary format is a secondary concern in the designn of OSN,
+ representing arbitrary data in binary format is a secondary concern in the design of OSN,
as well as the support for canonicalization.
- Apparently, theese features fall outside the scope of OSN,
+ Apparently, these features fall outside the scope of OSN,
which targets the data structures of <notice text="formal systems"/>.
</style></item></style>
<newline/>
projects / helm.git / commitdiff