From 640716b0624d2a7cd9f339b9ab975e85b3288a50 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 20 Apr 2013 19:34:58 +0000 Subject: [PATCH] update in basic_2 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 519 ++++++++++++++++-------------- 3 files changed, 272 insertions(+), 251 deletions(-) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index baeb99f9e..928de2d64 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Tue, 16 Apr 2013 21:51:34 +0200
+
Last update: Sat, 20 Apr 2013 21:34:40 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 3d494689d..340e2919d 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -199,6 +199,6 @@

-
Last update: Tue, 16 Apr 2013 21:51:34 +0200
+
Last update: Sat, 20 Apr 2013 21:34:40 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 2d407bee0..cd756f629 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -159,29 +159,29 @@ sizes files - 233 + 237 characters - 408114 + 420425 nodes - 1092089 + 1063117 propositions theorems 85 lemmas - 934 + 946 total - 1019 + 1031 concepts declared - 44 + 45 defined 80 total - 124 + 125 @@ -302,78 +302,12 @@ - dynamic typing - "big tree" parallel computation - yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) - yprs_yprs - ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) - ygt_ygt - -
- - - - -
- - "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 - -
- - -
- - -
- - - - -
- - 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 - -
- - -
- + dynamic typing + "big tree" parallel computation + yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) + yprs_yprs + ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) + ygt_ygt
@@ -382,11 +316,9 @@
- -
- - fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ ) - fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs + "big tree" parallel reduction + ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) + ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )
@@ -401,9 +333,9 @@
- local env. ref. for stratified static type assignment - lsubss ( ? •⊑[?] ? ) - lsubss_ldrop lsubss_ssta lsubss_cpcs + local env. ref. for stratified native validity + lsubsv ( ? ⊢ ? ¡⊑[?] ? ) + lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv
@@ -418,9 +350,9 @@
- context-sensitive equivalence - cpcs ( ? ⊢ ? ⬌* ? ) - cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs + 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
@@ -432,10 +364,10 @@ - conversion - focalized conversion - lfpc ( ⦃?⦄ ⬌ ⦃?⦄ ) - lfpc_lfpc + equivalence + focalized equivalence + lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ ) + lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs
@@ -453,8 +385,8 @@
- fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ ) - fpc_fpc + fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ ) + fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs
@@ -469,9 +401,9 @@
- context-sensitive conversion - cpc ( ? ⊢ ? ⬌ ? ) - cpc_cpc + local env. ref. for stratified static type assignment + lsubss ( ? •⊑[?] ? ) + lsubss_ldrop lsubss_ssta lsubss_cpcs
@@ -483,29 +415,27 @@ - computation - focalized computation - lfprs ( ⦃?⦄ ➡* ⦃?⦄ ) - lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs - -
- - +
- + context-sensitive equivalence + cpcs ( ? ⊢ ? ⬌* ? ) + cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs +
- - - +
- +
- fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ ) - fprs_aaa fprs_fprs + + + conversion + focalized conversion + lfpc ( ⦃?⦄ ⬌ ⦃?⦄ ) + lfpc_lfpc
@@ -520,9 +450,11 @@
- decomposed extended computation - dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) - dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs + +
+ + fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ ) + fpc_fpc
@@ -537,9 +469,9 @@
- weakly normalizing computation - cpe ( ? ⊢ ➡* 𝐍⦃?⦄ ) - cpe_cpe + context-sensitive conversion + cpc ( ? ⊢ ? ⬌ ? ) + cpc_cpc
@@ -551,127 +483,114 @@ - -
- - strongly normalizing computation - csn_vector ( ? ⊢ ⬊* ? ) - csn_cpr_vector csn_tstc_vector csn_aaa - + computation + focalized computation + lfprs ( ⦃?⦄ ➡* ⦃?⦄ ) + lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs +
- +
- +
- +
- +
- csn ( ? ⊢ ⬊* ? ) - csn_alt ( ? ⊢ ⬊⬊* ? ) - csn_lift csn_cpr csn_lfpr - + fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ ) + fprs_aaa fprs_fprs +
- + +
+ +
- +
- 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 - + decomposed extended computation + dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) + dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs +
- +
- +
- +
- context-free computation - ltprs ( ? ➡* ? ) - ltprs_alt ( ? ➡➡* ? ) - ltprs_ldrop ltprs_ltprs - + weakly normalizing computation + cpe ( ? ⊢ ➡* 𝐍⦃?⦄ ) + cpe_cpe +
- +
- - - +
- + + +
- tprs ( ? ➡* ?) - tprs_lift tprs_tprs - + strongly normalizing computation + csn_vector ( ? ⊢ ⬊* ? ) + csn_cpr_vector csn_tstc_vector csn_aaa +
- +
- +
- +
- 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 - -
- - +
- - - reducibility - context-sensitive focalized reduction - cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ ) - cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr + 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
@@ -686,10 +605,10 @@
- context-free focalized reduction - lfpr ( ⦃?⦄ ➡ ⦃?⦄ ) - lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ ) - lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr + context-free computation + ltprs ( ? ➡* ? ) + ltprs_alt ( ? ➡➡* ? ) + ltprs_ldrop ltprs_ltprs
@@ -704,8 +623,8 @@
- fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ ) - fpr_cpr fpr_fpr + tprs ( ? ➡* ?) + tprs_lift tprs_tprs
@@ -720,9 +639,9 @@
- context-sensitive normal forms - cnf ( ? ⊢ 𝐍⦃?⦄ ) - cnf_lift cnf_cif + local env. ref. for abstract candidates of reducibility + lsubc ( ? ⊑[?] ? ) + lsubc_ldrop lsubc_ldrops lsubc_lsuba
@@ -737,128 +656,175 @@
- revised context-sensitive reduction - lpr ( ? ⊢ ➡ ? ) - lpr_ldrop lpr_cpr lpr_lpr + support for abstract computation properties + acp + acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 ) + acp_aaa
- +
- + + + 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 +
- cpr ( ? ⊢ ? ➡ ? ) - cpr_lift - +
- + + +
- + +
+ + fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ ) + fpr_cpr fpr_fpr + +
+ + +
+ +
- +
- context-sensitive reduction - cpr ( ? ⊢ ? ➡ ? ) - cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr - + context-sensitive normal forms + cnf ( ? ⊢ 𝐍⦃?⦄ ) + cnf_lift cnf_cif +
- +
- +
- +
- context-sensitive reducible forms - crf ( ? ⊢ 𝐑⦃?⦄ ) - crf_append - cif ( ? ⊢ 𝐈⦃?⦄ ) - cif_append - + revised context-sensitive reduction + lpr ( ? ⊢ ➡ ? ) + lpr_ldrop lpr_cpr lpr_lpr + +
+ + +
+ +
- +
- context-free normal forms - thnf ( 𝐇𝐍⦃?⦄ ) - +
- + cpr ( ? ⊢ ? ➡ ? ) + cpr_lift +
- +
- +
- +
- context-free reduction - ltpr ( ? ➡ ? ) - ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr - + context-sensitive reduction + cpr ( ? ⊢ ? ➡ ? ) + cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr +
- +
- +
- +
- + context-sensitive reducible forms + crf ( ? ⊢ 𝐑⦃?⦄ ) + crf_append + cif ( ? ⊢ 𝐈⦃?⦄ ) + cif_append +
- tpr ( ? ➡ ? ) - tpr_lift tpr_delift tpr_tpr - + + +
- + context-free normal forms + thnf ( 𝐇𝐍⦃?⦄ ) +
- + +
+ + +
+ +
- restricted computation - restricted parallel computation - lpqs ( ? ⊢ ➤* ? ) - lpqs_ldrop lpqs_cpqs lpqs_lpqs + +
+ + context-free reduction + ltpr ( ? ➡ ? ) + ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr
@@ -876,8 +842,8 @@
- cpqs ( ? ⊢ ? ➤* ? ) - cpqs_lift + tpr ( ? ➡ ? ) + tpr_lift tpr_delift tpr_tpr
@@ -889,7 +855,62 @@ - unwind + unfold + restricted parallel computation + lpqs ( ? ⊢ ➤* ? ) + lpqs_ldrop lpqs_cpqs lpqs_lpqs + +
+ + +
+ + +
+ + + + +
+ + +
+ + cpqs ( ? ⊢ ? ➤* ? ) + cpqs_lift + +
+ + +
+ + +
+ + + + +
+ + unfold + unfold ( ? ⊢ ? ⧫* ? ) + +
+ + +
+ + +
+ + +
+ + + + +
+ iterated stratified static type assignment sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? ) sstas_lift sstas_lpss sstas_aaa sstas_sstas @@ -970,7 +991,7 @@ - unfold + substitution parallel substitution lpss ( ? ⊢ ▶* ? ) lpss_ldrop lpss_cpss lpss_lpss @@ -1106,7 +1127,7 @@ - substitution + relocation structural successor for closures fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) @@ -1377,6 +1398,6 @@

-
Last update: Tue, 16 Apr 2013 21:51:34 +0200
+
Last update: Sat, 20 Apr 2013 21:34:40 +0200
-- 2.39.2