From 1d7c90aaa2a5d5dadb3bca87d56bf717efab4361 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 1 Jun 2012 12:36:29 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambda_delta/apps_2.html | 4 ++-- helm/www/lambda_delta/basic_2.html | 8 ++++---- helm/www/lambda_delta/web/home/basic_2_blk.tbl | 2 +- helm/www/lambda_delta/web/home/basic_2_src.tbl | 14 +++++++++----- 4 files changed, 16 insertions(+), 12 deletions(-) diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html index eb4a0265e..f5095dc8e 100644 --- a/helm/www/lambda_delta/apps_2.html +++ b/helm/www/lambda_delta/apps_2.html @@ -32,7 +32,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles5bytes13113

propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
+
categoryobjects




sizesfiles5bytes13121

propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
@@ -57,6 +57,6 @@
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-05-30+02:00
+
[Spacer]

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

Last update: 2012-06-01+02:00
diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 4e79e60ec..ad4d2327b 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -18,7 +18,7 @@
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
+
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. @@ -29,7 +29,7 @@
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles154bytes578506

propositionstheorems60lemmas634total694
conceptsdeclared36defined47total83
+
categoryobjects




sizesfiles157bytes588107

propositionstheorems60lemmas641total701
conceptsdeclared37defined47total84
-
componentplanefiles







examples









dynamic typingnative type assignmentnta ( ⦃?,?⦄ ⊢ ? : ? )nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )nta_liftnta_ltpssnta_thinnta_stanta_nta

equivalencecontext-sensitive equivalencelcpcs ( ? ⊢ ⬌* ? )lcpcs_aaalcpcs_lcprslcpcs_lcpcs






cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_ltprcpcs_cprscpcs_cpcs


conversioncontext-sensitive conversionlcpc ( ? ⊢ ⬌ ? )lcpc_lcpc








cpc ( ? ⊢ ? ⬌ ? )cpc_cpc






computationweakly normalizing computationcpe ( ? ⊢ ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe







strongly normalizing computationcsn_vector ( ⬇* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa






csn ( ⬇* ? )csn_alt ( ⬇⬇* ? )csn_liftcsn_cprcsn_lcpr




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






cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_ltprcprs_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_aaalcpr_cprlcpr_lcpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_deliftcpr_ltprcpr_cpr



context-free normal formstwhnf ( 𝐖𝐇𝐍⦃?⦄ )tnf ( 𝐍⦃?⦄ )tnf_tif






context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpssltpr_aaaltpr_ltpr




tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr




context-free reducible formstrf ( 𝐑⦃?⦄ )tif ( 𝐈⦃?⦄ )






static typingstatic type assignmentsta ( ⦃?,?⦄ ⊢ ? • ? )sta_liftsta_sta






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





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpssaaa_aaa




parameterssh







unfoldbasic local env. thinningthin ( ? [?,?] ≡ ? )thin_ldropthin_delift






inverse basic term relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_alt ( ? ⊢ ? [?,?] ≡≡ ? )delift_liftdelift_tpssdelift_ltpssdelift_delift



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





tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss





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 substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lifttps_tps






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







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






local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )lsubs_lsubslsubs_sfr ( ≼[?,?] ? )






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








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






grammarsame 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







+
componentplanefiles







examples









dynamic typinglocal env. ref. for native type assignmentlsubn ( ? ⊢ ? :⊑ ? )lsubn_ldroplsubn_nta






native type assignmentnta ( ⦃?,?⦄ ⊢ ? : ? )nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )nta_liftnta_ltpssnta_thinnta_stanta_nta

equivalencecontext-sensitive equivalencelcpcs ( ? ⊢ ⬌* ? )lcpcs_aaalcpcs_lcprslcpcs_lcpcs






cpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpsscpcs_deliftcpcs_ltprcpcs_cprscpcs_cpcs


conversioncontext-sensitive conversionlcpc ( ? ⊢ ⬌ ? )lcpc_lcpc








cpc ( ? ⊢ ? ⬌ ? )cpc_cpc






computationweakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe







strongly normalizing computationcsn_vector ( ? ⊢ ⬇* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa






csn ( ? ⊢ ⬇* ? )csn_alt ( ? ⊢ ⬇⬇* ? )csn_liftcsn_cprcsn_lcpr




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






cprs (? ⊢ ? ➡* ?)cprs_liftcprs_deliftcprs_ltprcprs_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_aaalcpr_cprlcpr_lcpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_deliftcpr_ltprcpr_cpr



context-free normal formstwhnf ( 𝐖𝐇𝐍⦃?⦄ )tnf ( 𝐍⦃?⦄ )tnf_tif






context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tpsltpr_ltpssltpr_aaaltpr_ltpr




tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_delifttpr_tpr




context-free reducible formstrf ( 𝐑⦃?⦄ )tif ( 𝐈⦃?⦄ )






static typingstatic type assignmentsta ( ⦃?,?⦄ ⊢ ? • ? )sta_liftsta_sta






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





atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_liftaaa_liftsaaa_ltpssaaa_aaa




parameterssh







unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldropthin_delift






inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_liftdelift_tpssdelift_ltpssdelift_delift



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





tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss





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 substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lifttps_tps






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







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






local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )lsubs_lsubslsubs_sfr ( ≼[?,?] ? )






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








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






grammarsame 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-05-30+02:00
+
[Spacer]

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

Last update: 2012-06-01+02:00
diff --git a/helm/www/lambda_delta/web/home/basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl index 01a4d1c2a..8c4ee4827 100644 --- a/helm/www/lambda_delta/web/home/basic_2_blk.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_blk.tbl @@ -17,7 +17,7 @@ table { [ "no" ] [ "no" ] [ "no" ] [ "$p" ] ] class "prune" [ - [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ] + [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ] [ "no" ] [ "no" ] [ "yes" ] [ "no" ] ] } ] diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl index d93513b2b..82980f767 100644 --- a/helm/www/lambda_delta/web/home/basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl @@ -19,6 +19,10 @@ table { ] class "blue" [ { "dynamic typing" * } { + [ { "local env. ref. for native type assignment" * } { + [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_nta" * ] + } + ] [ { "native type assignment" * } { [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_sta" "nta_nta" * ] } @@ -46,12 +50,12 @@ table { class "water" [ { "computation" * } { [ { "weakly normalizing computation" * } { - [ "cpe ( ? ⊢ ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ] + [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ] } ] [ { "strongly normalizing computation" * } { - [ "csn_vector ( ⬇* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ] - [ "csn ( ⬇* ? )" "csn_alt ( ⬇⬇* ? )" "csn_lift" "csn_cpr" "csn_lcpr" * ] + [ "csn_vector ( ? ⊢ ⬇* ? )" "csn_cpr_vector" "csn_tstc_vector" "csn_aaa" * ] + [ "csn ( ? ⊢ ⬇* ? )" "csn_alt ( ? ⊢ ⬇⬇* ? )" "csn_lift" "csn_cpr" "csn_lcpr" * ] } ] [ { "context-sensitive computation" * } { @@ -118,11 +122,11 @@ table { class "yellow" [ { "unfold" * } { [ { "basic local env. thinning" * } { - [ "thin ( ? [?,?] ≡ ? )" "thin_ldrop" "thin_delift" * ] + [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" "thin_delift" * ] } ] [ { "inverse basic term relocation" * } { - [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_alt ( ? ⊢ ? [?,?] ≡≡ ? )" "delift_lift" "delift_tpss" "delift_ltpss" "delift_delift" * ] + [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" "delift_tpss" "delift_ltpss" "delift_delift" * ] } ] [ { "partial unfold" * } { -- 2.39.2