From: Ferruccio Guidi Date: Thu, 15 Mar 2012 18:57:05 +0000 (+0000) Subject: some renaming (ld_ prefix removed from file names) X-Git-Tag: make_still_working~1849 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae7427e8d3c57ccc77931e27913d8605d385cbda;p=helm.git some renaming (ld_ prefix removed from file names) --- diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html new file mode 100644 index 000000000..0344bee55 --- /dev/null +++ b/helm/www/lambda_delta/apps_2.html @@ -0,0 +1,62 @@ + + + + + + + + + + applications of lambda_delta version 2 + + + + + +
[lambda_delta home]
cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)
[Spacer]
+
Contents of the Specification
+
This specification comprises a collection of checked + applications of λδ version 2. + In particular it contains the components below. +
+ + + +
Summary of the Specification
+
Here is a numerical acount of the specification's contents + and its timeline. +
+
categoryobjects




sizesfiles5bytes13091

propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
+ + + + +
Logical Structure of the Specification
+
The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses. +
+
+ +
Physical Structure of the Specification
+
The source files are grouped in directories, + one for each component. +
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-03-15+01:00
+ + diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html new file mode 100644 index 000000000..65a801e7e --- /dev/null +++ b/helm/www/lambda_delta/basic_2.html @@ -0,0 +1,73 @@ + + + + + + + + + + lambda_delta version 2 + + + + + +
[lambda_delta home]
cic:/matita/lambda_delta/basic_2/ (λδ version 2)
[Spacer]
+
System's Syntax and Behavior
+
This is a summary of the "block structure" + of the System's syntactic items and reductions. +
+
+
* In terms only. + ** In terms and local environments only. + *** In global environments only. + **** Sort level k in terms only. +
+ +
Summary of the Specification
+
Here is a numerical acount of the specification's contents + and its timeline. +
+
categoryobjects




sizesfiles113bytes422759

propositionstheorems45lemmas450total495
conceptsdeclared31defined39total70
+
  • In progress. + Context-sensitive subject equivalence + for native type assignment. +
+
  • In progress. + Context-sensitive subject equivalence + for atomic arity assignment. +
+
  • 2012 March 15. + Context-sensitive strong normalization + for simply typed terms. +
+
  • 2012 January 27. + Support for abstract candidates of reducibility. +
+
  • 2011 September 21. + Confluence for context-sensitive parallel reduction. +
+
  • 2011 September 6. + Confluence for context-free parallel reduction. +
+
  • 2011 April 17. + Specification starts. +
+ +
Logical Structure of the Specification
+
The source files are grouped in planes and components + according to the following table. + A notation file covering the whole specification is provided. + The notation for the relations or functions introduced in each file + is shown in parentheses. +
+
+ +
Physical Structure of the Specification
+
The source files are grouped in directories, + one for each component. +
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-03-15+01:00
+ + diff --git a/helm/www/lambda_delta/ld_apps_2.html b/helm/www/lambda_delta/ld_apps_2.html deleted file mode 100644 index e6634f9aa..000000000 --- a/helm/www/lambda_delta/ld_apps_2.html +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - - - - - applications of lambda_delta version 2 - - - - - -
[lambda_delta home]
cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)
[Spacer]
-
Contents of the Specification
-
This specification comprises a collection of checked - applications of λδ version 2. - In particular it contains the components below. -
-
  • MLTT1. - Martin-Löf's Type Theory with one universe - using λδ as the theory of expressions. -
-
  • Functional. - The validation algorithm for λδ as implemented in - Helena 0.8. -
- -
Summary of the Specification
-
Here is a numerical acount of the specification's contents - and its timeline. -
-
categoryobjects




sizesfiles5bytes13091

propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
-
  • 2012 February 24. - The Applications directory is started. -
-
  • 2011 December 20. - The Functional component is started - inside the specification of λδ version 2. -
-
  • 2011 December 12. - The MLTT1 component is started. -
- -
Logical Structure of the Specification
-
The source files are grouped in planes and components - according to the following table. - Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses. -
-
componentplanefiles
MLTT1
genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
- -
Physical Structure of the Specification
-
The source files are grouped in directories, - one for each component. -
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-03-15+01:00
- - diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html deleted file mode 100644 index 8d1fc3ea5..000000000 --- a/helm/www/lambda_delta/ld_basic_2.html +++ /dev/null @@ -1,73 +0,0 @@ - - - - - - - - - - lambda_delta version 2 - - - - - -
[lambda_delta home]
cic:/matita/lambda_delta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" - of the System's syntactic items and reductions. -
-
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
- -
Summary of the Specification
-
Here is a numerical acount of the specification's contents - and its timeline. -
-
categoryobjects




sizesfiles113bytes422759

propositionstheorems45lemmas450total495
conceptsdeclared31defined39total70
-
  • In progress. - Context-sensitive subject equivalence - for native type assignment. -
-
  • In progress. - Context-sensitive subject equivalence - for atomic arity assignment. -
-
  • 2012 March 15. - Context-sensitive strong normalization - for simply typed terms. -
-
  • 2012 January 27. - Support for abstract candidates of reducibility. -
-
  • 2011 September 21. - Confluence for context-sensitive parallel reduction. -
-
  • 2011 September 6. - Confluence for context-free parallel reduction. -
-
  • 2011 April 17. - Specification starts. -
- -
Logical Structure of the Specification
-
The source files are grouped in planes and components - according to the following table. - A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses. -
-
componentplanefiles





examples







native typing
nty





equivalencecontext-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )





conversioncontext-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc




computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa




csn ( ⬇* ? )csn_liftcsn_cprcsn_cprs ( ⬇** ? )csn_lcpr


context-sensitive computationlcprs ( ? ⊢ ➡* ? )lcprs_cprslcprs_lcprs





cprs (? ⊢ ? ➡* ?)cprs_liftcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba



support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa



reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift





context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_cpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr


context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif




context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps





tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr



context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )




static typingstatic type assignmentstysty_liftsty_sty




local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_aaa



parameterssh





unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift





partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss




tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps



generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops




generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector






lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts




support for generic relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2


substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps




tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps




global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop





basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop





basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector






lift ( ⇧[?,?] ? ≡ ? )lift_lift




grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs





same head term formtshf ( ? ≈ ? )tshf_tshf





same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector




closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )





internal syntaxgenv







lenvlenv_weight ( #[?] )lenv_length ( |?| )





termterm_weight ( #[?] )term_simple ( 𝐒[?] )term_vector




item






external syntaxaarity





- -
Physical Structure of the Specification
-
The source files are grouped in directories, - one for each component. -
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-03-15+01:00
- - diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html index 388833406..987949365 100644 --- a/helm/www/lambda_delta/news.html +++ b/helm/www/lambda_delta/news.html @@ -71,10 +71,10 @@ restarted in Matita 0.5.
    -
  • Here is a page about +
  • Here is a page about the topics related to the specification (Applications).
    • -
  • Here is a page about +
  • Here is a page about the specification (Core).
    • @@ -279,7 +279,7 @@ relocation functions: s,

    - Last update 2012-02-24 by Ferruccio Guidi
diff --git a/helm/www/lambda_delta/web/home/apps_2.ldw.xml b/helm/www/lambda_delta/web/home/apps_2.ldw.xml new file mode 100644 index 000000000..253fbdc87 --- /dev/null +++ b/helm/www/lambda_delta/web/home/apps_2.ldw.xml @@ -0,0 +1,52 @@ + + + +
Contents of the Specification
+ This specification comprises a collection of checked + applications of λδ version 2. + In particular it contains the components below. + + + Martin-Löf's Type Theory with one universe + using λδ as the theory of expressions. + + + The validation algorithm for λδ as implemented in + Helena 0.8. + + +
Summary of the Specification
+ Here is a numerical acount of the specification's contents + and its timeline. + + + + The Applications directory is started. + + + The Functional component is started + inside the specification of λδ version 2. + + + The MLTT1 component is started. + + +
Logical Structure of the Specification
+ The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses. + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each component. + +
+ diff --git a/helm/www/lambda_delta/web/home/apps_2_src.tbl b/helm/www/lambda_delta/web/home/apps_2_src.tbl new file mode 100644 index 000000000..df8a5602a --- /dev/null +++ b/helm/www/lambda_delta/web/home/apps_2_src.tbl @@ -0,0 +1,38 @@ +name "ld_apps_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "orange" + [ { "MLTT1" * } { + [ { "" * } { + [ "genv_primitive" "judgement" * ] + } + ] + } + ] + class "red" + [ { "functional" * } { + [ { "reduction and type machine" * } { + [ "rtm" "rtm_step ( ? ⇨ ? )" * ] + } + ] + [ { "unfold" * } { + [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] + } + ] + } + ] +} + +class "component" { 0 } + +class "plane" { 1 } + +class "file" { 2 * } diff --git a/helm/www/lambda_delta/web/home/basic_2.ldw.xml b/helm/www/lambda_delta/web/home/basic_2.ldw.xml new file mode 100644 index 000000000..6a1f30239 --- /dev/null +++ b/helm/www/lambda_delta/web/home/basic_2.ldw.xml @@ -0,0 +1,63 @@ + + + +
System's Syntax and Behavior
+ This is a summary of the "block structure" + of the System's syntactic items and reductions. + +
+ * In terms only. + ** In terms and local environments only. + *** In global environments only. + **** Sort level k in terms only. + + +
Summary of the Specification
+ Here is a numerical acount of the specification's contents + and its timeline. + +
+ + Context-sensitive subject equivalence + for native type assignment. + + + Context-sensitive subject equivalence + for atomic arity assignment. + + + Context-sensitive strong normalization + for simply typed terms. + + + Support for abstract candidates of reducibility. + + + Confluence for context-sensitive parallel reduction. + + + Confluence for context-free parallel reduction. + + + Specification starts. + + +
Logical Structure of the Specification
+ The source files are grouped in planes and components + according to the following table. + A notation file covering the whole specification is provided. + The notation for the relations or functions introduced in each file + is shown in parentheses. + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each component. + +
+ diff --git a/helm/www/lambda_delta/web/home/basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl new file mode 100644 index 000000000..8e3ada607 --- /dev/null +++ b/helm/www/lambda_delta/web/home/basic_2_blk.tbl @@ -0,0 +1,45 @@ +name "ld_basic_2_blk" + +table { + class "grey" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "wine" [ + [ "typed abstraction **" ] [ "Γ ⊢ λW" ] + [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] + ] + class "magenta" [ + [ "typed declaration ***" ] [ "Γ ⊢ pλW" ] + [ "no" ] [ "no" ] [ "no" ] [ "$p" ] + ] + class "prune" [ + [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ] + [ "no" ] [ "no" ] [ "yes" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "blue" [ + [ "local abbreviation **" ] [ "Γ ⊢ δV" ] + [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ] + ] + class "sky" [ + [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ] + [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ] + ] + } ] + [ { "no" * } { + class "cyan" [ + [ "sort ****" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "text" { 0 } { 2 * } + +class "plane" { 1 } + diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl new file mode 100644 index 000000000..4dfeb8017 --- /dev/null +++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl @@ -0,0 +1,197 @@ +name "ld_basic_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "prune" + [ { "examples" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] + class "blue" + [ { "native typing" * } { + [ { "" * } { + [ "nty" * ] + } + ] + } + ] + class "sky" + [ { "equivalence" * } { + [ { "context-sensitive equivalence" * } { + [ "cpcs ( ? ⊢ ? ⬌* ? )" * ] + } + ] + } + ] + class "cyan" + [ { "conversion" * } { + [ { "context-sensitive conversion" * } { + [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] + } + ] + } + ] + class "water" + [ { "computation" * } { + [ { "strongly normalizing computation" * } { + [ "csn_vector ( ⬇* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ] + [ "csn ( ⬇* ? )" "csn_lift" "csn_cpr" "csn_cprs ( ⬇** ? )" "csn_lcpr" * ] + } + ] + [ { "context-sensitive computation" * } { + [ "lcprs ( ? ⊢ ➡* ? )" "lcprs_cprs" "lcprs_lcprs" * ] + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ] + } + ] + [ { "local env. ref. for abstract candidates of reducibility" * } { + [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ] + } + ] + [ { "support for abstract computation properties" * } { + [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ] + } + ] + } + ] + class "green" + [ { "reducibility" * } { + [ { "context-sensitive normal forms" * } { + [ "cnf ( ? ⊢ 𝐍[?] )" "cnf_lift" * ] + } + ] + [ { "context-sensitive reduction" * } { + [ "lcpr ( ? ⊢ ➡ ? )" "lcpr_cpr" * ] + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpr" "cpr_cpr" * ] + } + ] + [ { "context-free normal forms" * } { + [ "twhnf ( 𝐖𝐇𝐍[?] )" "tnf ( 𝐍[?] )" "tnf_tif" * ] + } + ] + [ { "context-free reduction" * } { + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" * ] + [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] + } + ] + [ { "context-free reducible forms" * } { + [ "trf ( 𝐑[?] )" "tif ( 𝐈[?] )" * ] + } + ] + } + ] + class "grass" + [ { "static typing" * } { + [ { "static type assignment" * } { + [ "sty" "sty_lift" "sty_sty" * ] + } + ] + [ { "local env. ref. for atomic arity assignment" * } { + [ "lsuba ( ? ÷⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ] + } + ] + [ { "atomic arity assignment" * } { + [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_aaa" * ] + } + ] + [ { "parameters" * } { + [ "sh" * ] + } + ] + } + ] + class "yellow" + [ { "unfold" * } { + [ { "term inverse relocation" * } { + [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ] + } + ] + [ { "partial unfold" * } { + [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] + [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] + } + ] + [ { "generic local env. slicing" * } { + [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ] + } + ] + [ { "generic term relocation" * } { + [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ] + [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ] + } + ] + [ { "support for generic relocation" * } { + [ "gr2 ( @ [ ? ] ? ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ] + } + ] + } + ] + class "orange" + [ { "substitution" * } { + [ { "parallel substitution" * } { + [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ] + [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ] + } + ] + [ { "global env. slicing" * } { + [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] + } + ] + [ { "basic local env. slicing" * } { + [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ] + } + ] + [ { "basic term relocation" * } { + [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] + [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "local env. ref. for substitution" * } { + [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ] + } + ] + [ { "same head term form" * } { + [ "tshf ( ? ≈ ? )" "tshf_tshf" * ] + } + ] + [ { "same top term constructor" * } { + [ "tstc ( ? ≃ ? )" "tstc_tstc" "tstc_vector" * ] + } + ] + [ { "closures" * } { + [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ] + } + ] + [ { "internal syntax" * } { + [ "genv" * ] + [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ] + [ "term" "term_weight ( #[?] )" "term_simple ( 𝐒[?] )" "term_vector" * ] + [ "item" * ] + } + ] + [ { "external syntax" * } { + [ "aarity" * ] + } + ] + } + ] +} + +class "component" { 0 } + +class "plane" { 1 } + +class "file" { 2 * } diff --git a/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml deleted file mode 100644 index 5c6e7859e..000000000 --- a/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml +++ /dev/null @@ -1,52 +0,0 @@ - - - -
Contents of the Specification
- This specification comprises a collection of checked - applications of λδ version 2. - In particular it contains the components below. - - - Martin-Löf's Type Theory with one universe - using λδ as the theory of expressions. - - - The validation algorithm for λδ as implemented in - Helena 0.8. - - -
Summary of the Specification
- Here is a numerical acount of the specification's contents - and its timeline. - -
- - The Applications directory is started. - - - The Functional component is started - inside the specification of λδ version 2. - - - The MLTT1 component is started. - - -
Logical Structure of the Specification
- The source files are grouped in planes and components - according to the following table. - Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses. - -
- -
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. - -
- diff --git a/helm/www/lambda_delta/web/home/ld_apps_2_src.tbl b/helm/www/lambda_delta/web/home/ld_apps_2_src.tbl deleted file mode 100644 index df8a5602a..000000000 --- a/helm/www/lambda_delta/web/home/ld_apps_2_src.tbl +++ /dev/null @@ -1,38 +0,0 @@ -name "ld_apps_2_src" - -table { - class "grey" - [ { "component" * } { - [ { "plane" * } { - [ "files" * ] - } - ] - } - ] - class "orange" - [ { "MLTT1" * } { - [ { "" * } { - [ "genv_primitive" "judgement" * ] - } - ] - } - ] - class "red" - [ { "functional" * } { - [ { "reduction and type machine" * } { - [ "rtm" "rtm_step ( ? ⇨ ? )" * ] - } - ] - [ { "unfold" * } { - [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] - } - ] - } - ] -} - -class "component" { 0 } - -class "plane" { 1 } - -class "file" { 2 * } diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml deleted file mode 100644 index a542cc19a..000000000 --- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml +++ /dev/null @@ -1,63 +0,0 @@ - - - -
System's Syntax and Behavior
- This is a summary of the "block structure" - of the System's syntactic items and reductions. - -
- * In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. - - -
Summary of the Specification
- Here is a numerical acount of the specification's contents - and its timeline. - -
- - Context-sensitive subject equivalence - for native type assignment. - - - Context-sensitive subject equivalence - for atomic arity assignment. - - - Context-sensitive strong normalization - for simply typed terms. - - - Support for abstract candidates of reducibility. - - - Confluence for context-sensitive parallel reduction. - - - Confluence for context-free parallel reduction. - - - Specification starts. - - -
Logical Structure of the Specification
- The source files are grouped in planes and components - according to the following table. - A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses. - -
- -
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. - -
- diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl deleted file mode 100644 index 8e3ada607..000000000 --- a/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl +++ /dev/null @@ -1,45 +0,0 @@ -name "ld_basic_2_blk" - -table { - class "grey" [ { "domain" * } { - [ - [ "block" ] [ "leader" ] - [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] - ] - } ] - [ { "{X | Γ ⊢ X : W}" * } { - class "wine" [ - [ "typed abstraction **" ] [ "Γ ⊢ λW" ] - [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] - ] - class "magenta" [ - [ "typed declaration ***" ] [ "Γ ⊢ pλW" ] - [ "no" ] [ "no" ] [ "no" ] [ "$p" ] - ] - class "prune" [ - [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ] - [ "no" ] [ "no" ] [ "yes" ] [ "no" ] - ] - } ] - [ { "{X | Γ ⊢ X = V}" * } { - class "blue" [ - [ "local abbreviation **" ] [ "Γ ⊢ δV" ] - [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ] - ] - class "sky" [ - [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ] - [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ] - ] - } ] - [ { "no" * } { - class "cyan" [ - [ "sort ****" ] [ "Γ ⊢ ⋆k" ] - [ "no" ] [ "no" ] [ "no" ] [ "no" ] - ] - } ] -} - -class "text" { 0 } { 2 * } - -class "plane" { 1 } - diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl deleted file mode 100644 index 4dfeb8017..000000000 --- a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl +++ /dev/null @@ -1,197 +0,0 @@ -name "ld_basic_2_src" - -table { - class "grey" - [ { "component" * } { - [ { "plane" * } { - [ "files" * ] - } - ] - } - ] - class "prune" - [ { "examples" * } { - [ { "" * } { - [ "" * ] - } - ] - } - ] - class "blue" - [ { "native typing" * } { - [ { "" * } { - [ "nty" * ] - } - ] - } - ] - class "sky" - [ { "equivalence" * } { - [ { "context-sensitive equivalence" * } { - [ "cpcs ( ? ⊢ ? ⬌* ? )" * ] - } - ] - } - ] - class "cyan" - [ { "conversion" * } { - [ { "context-sensitive conversion" * } { - [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] - } - ] - } - ] - class "water" - [ { "computation" * } { - [ { "strongly normalizing computation" * } { - [ "csn_vector ( ⬇* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ] - [ "csn ( ⬇* ? )" "csn_lift" "csn_cpr" "csn_cprs ( ⬇** ? )" "csn_lcpr" * ] - } - ] - [ { "context-sensitive computation" * } { - [ "lcprs ( ? ⊢ ➡* ? )" "lcprs_cprs" "lcprs_lcprs" * ] - [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" "cprs_lcpr" "cprs_cprs" "cprs_lcprs" "cprs_tstc" "cprs_tstc_vector" * ] - } - ] - [ { "local env. ref. for abstract candidates of reducibility" * } { - [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ] - } - ] - [ { "support for abstract computation properties" * } { - [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ] - } - ] - } - ] - class "green" - [ { "reducibility" * } { - [ { "context-sensitive normal forms" * } { - [ "cnf ( ? ⊢ 𝐍[?] )" "cnf_lift" * ] - } - ] - [ { "context-sensitive reduction" * } { - [ "lcpr ( ? ⊢ ➡ ? )" "lcpr_cpr" * ] - [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpr" "cpr_cpr" * ] - } - ] - [ { "context-free normal forms" * } { - [ "twhnf ( 𝐖𝐇𝐍[?] )" "tnf ( 𝐍[?] )" "tnf_tif" * ] - } - ] - [ { "context-free reduction" * } { - [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" * ] - [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] - } - ] - [ { "context-free reducible forms" * } { - [ "trf ( 𝐑[?] )" "tif ( 𝐈[?] )" * ] - } - ] - } - ] - class "grass" - [ { "static typing" * } { - [ { "static type assignment" * } { - [ "sty" "sty_lift" "sty_sty" * ] - } - ] - [ { "local env. ref. for atomic arity assignment" * } { - [ "lsuba ( ? ÷⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ] - } - ] - [ { "atomic arity assignment" * } { - [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_aaa" * ] - } - ] - [ { "parameters" * } { - [ "sh" * ] - } - ] - } - ] - class "yellow" - [ { "unfold" * } { - [ { "term inverse relocation" * } { - [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ] - } - ] - [ { "partial unfold" * } { - [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] - [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] - } - ] - [ { "generic local env. slicing" * } { - [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ] - } - ] - [ { "generic term relocation" * } { - [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ] - [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ] - } - ] - [ { "support for generic relocation" * } { - [ "gr2 ( @ [ ? ] ? ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ] - } - ] - } - ] - class "orange" - [ { "substitution" * } { - [ { "parallel substitution" * } { - [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ] - [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ] - } - ] - [ { "global env. slicing" * } { - [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] - } - ] - [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ] - } - ] - [ { "basic term relocation" * } { - [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] - [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ] - } - ] - } - ] - class "red" - [ { "grammar" * } { - [ { "local env. ref. for substitution" * } { - [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ] - } - ] - [ { "same head term form" * } { - [ "tshf ( ? ≈ ? )" "tshf_tshf" * ] - } - ] - [ { "same top term constructor" * } { - [ "tstc ( ? ≃ ? )" "tstc_tstc" "tstc_vector" * ] - } - ] - [ { "closures" * } { - [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ] - } - ] - [ { "internal syntax" * } { - [ "genv" * ] - [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ] - [ "term" "term_weight ( #[?] )" "term_simple ( 𝐒[?] )" "term_vector" * ] - [ "item" * ] - } - ] - [ { "external syntax" * } { - [ "aarity" * ] - } - ] - } - ] -} - -class "component" { 0 } - -class "plane" { 1 } - -class "file" { 2 * } diff --git a/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl b/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl deleted file mode 100644 index c6ba91d7c..000000000 --- a/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl +++ /dev/null @@ -1,80 +0,0 @@ - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
- - -