From 3fb2d167ba8463e0fa80efe42ee9be1a15e282a0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Apr 2013 21:38:03 +0000 Subject: [PATCH] update in basic_2 and apps_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 34 ++- helm/www/lambdadelta/basic_2.html | 442 ++++++++++++++++-------------- 3 files changed, 260 insertions(+), 218 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 64faa2fde..e663b4adb 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Fri, 05 Apr 2013 14:24:37 +0200
+
Last update: Sun, 07 Apr 2013 23:37:37 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 183306020..9d03180c2 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -138,24 +138,32 @@ - MLTT1 - - genv_primitive - judgement + MLTT1 + + genv_primitive + judgement - functional - reduction and type machine - rtm - rtm_step ( ? ⇨ ? ) + functional + reduction and type machine + rtm + rtm_step ( ? ⇨ ? ) - + +
+ + unfold + lift ( ↑[?,?] ? ) + subst ( [?←?] ? ) + + + examples + + +
- unfold - lift ( ↑[?,?] ? ) - subst ( [?←?] ? ) @@ -191,6 +199,6 @@

-
Last update: Fri, 05 Apr 2013 14:24:38 +0200
+
Last update: Sun, 07 Apr 2013 23:37:36 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index a534b0a72..67fa00856 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -159,29 +159,29 @@ sizes files - 255 + 262 characters - 502802 + 527314 nodes - 1365444 + 1440935 propositions theorems - 89 + 95 lemmas - 1126 + 1170 total - 1215 + 1265 concepts declared - 48 + 49 defined - 82 + 87 total - 130 + 136 @@ -294,40 +294,72 @@ - dynamic typing - "big tree" parallel computation - yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) - yprs_yprs - ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) - ygt_ygt - + dynamic typing + "big tree" parallel computation + yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) + yprs_yprs + ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) + ygt_ygt +
- +
- "big tree" parallel reduction - ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) - ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) - + "big tree" parallel reduction + ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) + ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) +
- +
- +
- +
- local env. ref. for stratified native validity - lsubsv ( ? ⊢ ? ¡⊑[?] ? ) - lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv + local env. ref. for stratified native validity + lsubsv ( ? ⊢ ? ¡⊑[?] ? ) + lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv + +
+ + +
+ + +
+ + + + +
+ + stratified native validity + snv ( ⦃?,?⦄ ⊢ ? ¡[?] ) + snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs + +
+ + +
+ + +
+ + + + equivalence + focalized equivalence + lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ ) + lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs
@@ -342,9 +374,11 @@
- stratified native validity - snv ( ⦃?,?⦄ ⊢ ? ¡[?] ) - snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs + +
+ + fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ ) + fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs
@@ -356,29 +390,44 @@ - equivalence - focalized equivalence - lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ ) - lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs - +
- + local env. ref. for stratified static type assignment + lsubss ( ? •⊑[?] ? ) + lsubss_ldrop lsubss_ssta lsubss_cpcs +
- + +
+ +
- +
- + context-sensitive equivalence + cpcs ( ? ⊢ ? ⬌* ? ) + cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs + +
+ + +
+ +
- fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ ) - fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs + + + conversion + focalized conversion + lfpc ( ⦃?⦄ ⬌ ⦃?⦄ ) + lfpc_lfpc
@@ -393,9 +442,11 @@
- local env. ref. for stratified static type assignment - lsubss ( ? •⊑[?] ? ) - lsubss_ldrop lsubss_ssta lsubss_cpcs + +
+ + fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ ) + fpc_fpc
@@ -410,9 +461,9 @@
- context-sensitive equivalence - cpcs ( ? ⊢ ? ⬌* ? ) - cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs + context-sensitive conversion + cpc ( ? ⊢ ? ⬌ ? ) + cpc_cpc
@@ -424,10 +475,10 @@ - conversion - focalized conversion - lfpc ( ⦃?⦄ ⬌ ⦃?⦄ ) - lfpc_lfpc + computation + focalized computation + lfprs ( ⦃?⦄ ➡* ⦃?⦄ ) + lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs
@@ -445,8 +496,8 @@
- fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ ) - fpc_fpc + fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ ) + fprs_aaa fprs_fprs
@@ -461,9 +512,9 @@
- context-sensitive conversion - cpc ( ? ⊢ ? ⬌ ? ) - cpc_cpc + decomposed extended computation + dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) + dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs
@@ -475,114 +526,144 @@ - computation - focalized computation - lfprs ( ⦃?⦄ ➡* ⦃?⦄ ) - lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs - +
- + weakly normalizing computation + cpe ( ? ⊢ ➡* 𝐍⦃?⦄ ) + cpe_cpe +
- +
- - - +
- + + +
- fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ ) - fprs_aaa fprs_fprs - + strongly normalizing computation + csn_vector ( ? ⊢ ⬊* ? ) + csn_cpr_vector csn_tstc_vector csn_aaa +
- +
- +
- +
- decomposed extended computation - dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) - dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs - +
- + csn ( ? ⊢ ⬊* ? ) + csn_alt ( ? ⊢ ⬊⬊* ? ) + csn_lift csn_cpr csn_lfpr +
- +
- +
- weakly normalizing computation - cpe ( ? ⊢ ➡* 𝐍⦃?⦄ ) - cpe_cpe - + context-sensitive computation + cprs (? ⊢ ? ➡* ?) + cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector +
- +
- +
- +
- strongly normalizing computation - csn_vector ( ? ⊢ ⬊* ? ) - csn_cpr_vector csn_tstc_vector csn_aaa - + context-free computation + ltprs ( ? ➡* ? ) + ltprs_alt ( ? ➡➡* ? ) + ltprs_ldrop ltprs_ltprs +
- +
- + + + +
+ + +
+ + tprs ( ? ➡* ?) + tprs_lift tprs_tprs + +
+ + +
+ +
- +
- + local env. ref. for abstract candidates of reducibility + lsubc ( ? ⊑[?] ? ) + lsubc_ldrop lsubc_ldrops lsubc_lsuba +
- csn ( ? ⊢ ⬊* ? ) - csn_alt ( ? ⊢ ⬊⬊* ? ) - csn_lift csn_cpr csn_lfpr - +
- +
- + +
+ + support for abstract computation properties + acp + acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 ) + acp_aaa + +
+ +
- context-sensitive computation - cprs (? ⊢ ? ➡* ?) - cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector + + + reducibility + context-sensitive focalized reduction + cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ ) + cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr
@@ -597,10 +678,10 @@
- context-free computation - ltprs ( ? ➡* ? ) - ltprs_alt ( ? ➡➡* ? ) - ltprs_ldrop ltprs_ltprs + context-free focalized reduction + lfpr ( ⦃?⦄ ➡ ⦃?⦄ ) + lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ ) + lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr
@@ -615,8 +696,8 @@
- tprs ( ? ➡* ?) - tprs_lift tprs_tprs + fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ ) + fpr_cpr fpr_fpr
@@ -631,9 +712,9 @@
- local env. ref. for abstract candidates of reducibility - lsubc ( ? ⊑[?] ? ) - lsubc_ldrop lsubc_ldrops lsubc_lsuba + context-sensitive normal forms + cnf ( ? ⊢ 𝐍⦃?⦄ ) + cnf_lift cnf_cif
@@ -648,139 +729,92 @@
- support for abstract computation properties - acp - acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 ) - acp_aaa + context-sensitive reduction + cpr ( ? ⊢ ? ➡ ? ) + cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr
- -
- - - - reducibility - context-sensitive focalized reduction - cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ ) - cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr - -
- - +
- +
- -
- - context-free focalized reduction - lfpr ( ⦃?⦄ ➡ ⦃?⦄ ) - lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ ) - lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr - +
- + context-sensitive reducible forms + crf ( ? ⊢ 𝐑⦃?⦄ ) + crf_append + cif ( ? ⊢ 𝐈⦃?⦄ ) + cif_append +
- -
- - -
- - fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ ) - fpr_cpr fpr_fpr - -
- - -
- - +
- - - + context-free normal forms + thnf ( 𝐇𝐍⦃?⦄ ) +
- context-sensitive normal forms - cnf ( ? ⊢ 𝐍⦃?⦄ ) - cnf_lift cnf_cif - +
- +
- +
- -
- - context-sensitive reduction - cpr ( ? ⊢ ? ➡ ? ) - cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr - -
- - +
- + context-free reduction + ltpr ( ? ➡ ? ) + ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr +
- - - +
- context-sensitive reducible forms - crf ( ? ⊢ 𝐑⦃?⦄ ) - crf_append - cif ( ? ⊢ 𝐈⦃?⦄ ) - cif_append - +
- +
- context-free normal forms - thnf ( 𝐇𝐍⦃?⦄ ) - +
- + tpr ( ? ➡ ? ) + tpr_lift tpr_delift tpr_tpr +
- +
- +
- -
- - context-free reduction - ltpr ( ? ➡ ? ) - ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr + restricted computation + restricted parallel computation + lpqs ( ? ⊢ ➤* ? ) + lpqs_ldrop lpqs_cpqs lpqs_lpqs
@@ -798,8 +832,8 @@
- tpr ( ? ➡ ? ) - tpr_lift tpr_delift tpr_tpr + cpqs ( ? ⊢ ? ➤* ? ) + cpqs_lift
@@ -926,8 +960,8 @@
revised parallel substitution - lcpss ( ? ⊢ ▶* ? ) - lcpss_ldrop lcpss_cpss lcpss_lcpss + lpss ( ? ⊢ ▶* ? ) + lpss_ldrop lpss_cpss lpss_lpss
@@ -1146,7 +1180,7 @@ basic local env. slicing ldrop ( ⇩[?,?] ? ≡ ? ) - ldrop_append ldrop_lpx ldrop_lbotr ldrop_ldrop + ldrop_append ldrop_lpx ldrop_lpx_sn ldrop_lbotr ldrop_ldrop
@@ -1287,7 +1321,7 @@ lenv_weight ( ♯{?} ) lenv_length ( |?| ) lenv_append ( ? @@ ? ) - lenv_px lenv_px_bi + lenv_px lenv_px_sn lenv_px_bi @@ -1378,6 +1412,6 @@

-
Last update: Fri, 05 Apr 2013 14:24:38 +0200
+
Last update: Sun, 07 Apr 2013 23:37:37 +0200
-- 2.39.2