X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=8e5745e167831a675faa3ae35b90f89649ebba45;hb=645b62762e9c86e343d4741541a2ddccfed8ebc7;hp=300521154b9879f4ebb0cb7bd257174491750384;hpb=548f2d3f410c05e2eb332f5c2d074f5e6c6985e1;p=helm.git
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 300521154..8e5745e16 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -58,29 +58,29 @@
sizes |
files |
- 328 |
+ 361 |
characters |
- 557560 |
+ 652919 |
nodes |
- 1522569 |
+ 1828390 |
propositions |
theorems |
- 103 |
+ 121 |
lemmas |
- 1136 |
+ 1299 |
total |
- 1239 |
+ 1420 |
concepts |
declared |
- 50 |
+ 54 |
defined |
- 77 |
+ 81 |
total |
- 127 |
+ 135 |
@@ -94,16 +94,23 @@
-
- In progress.
- Closure of native validity
- for context-sensitive extended computation.
+ 2014 June 18.
+ Preservation of stratified native validity
+ for context-sensitive computation on terms.
+
+
+
+ -
+ 2014 June 9.
+ "Big tree" strong normalization
+ for simply typed terms.
-
2014 April 16.
lazy equivalence on local environments
- serves as irrelevant step in "big tree" computation
+ serves as irrelevant step in "big tree" computation on closures
(anniversary milestone).
@@ -229,7 +236,7 @@
dynamic typing |
local env. ref. for stratified native validity |
lsubsv ( ? ⢠? ¡â«[?,?] ? ) |
- lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv |
+ lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv |
|
@@ -243,7 +250,7 @@
stratified native validity |
snv ( �,?⦠⢠? ¡[?,?] ) |
- snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs |
+ snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve |
|
@@ -352,7 +359,7 @@
lsx ( ? ⢠â¬*[?,?,?,?] ? ) |
lsx_alt ( ? ⢠â¬â¬*[?,?,?,?] ? ) |
- lsx_ldrop lsx_lpx lsx_lpxs llsx_csx |
+ lsx_drop lsx_lpx lsx_lpxs llsx_csx |
|
@@ -392,7 +399,7 @@
"big tree" parallel computation |
- fpbg ( â¦?,?,?⦠>â[?,?] â¦?,?,?⦠) |
+ fpbg ( â¦?,?,?⦠>â¡[?,?] â¦?,?,?⦠) |
fpbg_lift fpbg_fleq fpbg_fpbg |
@@ -408,7 +415,7 @@
|
|
- fpbc ( â¦?,?,?⦠â»â[?,?] â¦?,?,?⦠) |
+ fpbc ( â¦?,?,?⦠â»â¡[?,?] â¦?,?,?⦠) |
fpbc_fleq fpbc_fpbs |
@@ -465,7 +472,7 @@
|
context-sensitive extended computation |
lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
- lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
+ lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
@@ -495,7 +502,7 @@
context-sensitive computation |
lprs ( â¦?,?⦠⢠â¡* ? ) |
- lprs_ldrop lprs_cprs lprs_lprs |
+ lprs_drop lprs_cprs lprs_lprs |
|
@@ -525,7 +532,7 @@
local env. ref. for abstract candidates of reducibility |
lsubc ( ? ⢠? â«[?] ? ) |
- lsubc_ldrop lsubc_ldrops lsubc_lsuba |
+ lsubc_drop lsubc_drops lsubc_lsuba |
|
@@ -577,10 +584,8 @@
context-sensitive extended reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lpx_ldrop lpx_lleq lpx_aaa |
-
-
- |
+ lpx_drop lpx_frees |
+ lpx_lleq lpx_aaa |
|
@@ -649,7 +654,7 @@
context-sensitive reduction |
lpr ( �,?⦠⢠⡠? ) |
- lpr_ldrop lpr_lpr |
+ lpr_drop lpr_lpr |
|
@@ -720,18 +725,18 @@
iterated static type assignment |
- lsstas ( â¦?,?⦠⢠? â¢*[?,?,?] ? ) |
- lsstas_alt ( â¦?,?⦠⢠? â¢â¢*[?,?,?] ? ) |
- lsstas_lift lsstas_aaa lsstas_lsstas |
+ lstas ( â¦?,?⦠⢠? â¢*[?,?] ? ) |
+ lstas_alt ( â¦?,?⦠⢠? â¢â¢*[?,?] ? ) |
+ lstas_lift lstas_aaa lstas_da lstas_lstas |
|
static typing |
- local env. ref. for atomic arity assignment |
- lsuba ( ? ⢠? ââ« ? ) |
- lsuba_ldrop lsuba_aaa lsuba_lsuba |
+ local env. ref. for degree assignment |
+ lsubd ( ? ⢠? âªâ« ? ) |
+ lsubd_da lsubd_lsubd |
|
@@ -743,9 +748,9 @@
|
- atomic arity assignment |
- aaa ( â¦?,?⦠⢠? â ? ) |
- aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_da aaa_ssta aaa_aaa |
+ degree assignment |
+ da ( â¦?,?⦠⢠? âª[?,?] ? ) |
+ da_lift da_aaa da_sta da_da |
|
@@ -757,9 +762,9 @@
|
- stratified static type assignment |
- ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) |
- ssta_lift ssta_lpx_sn ssta_ssta |
+ static type assignment |
+ sta ( â¦?,?⦠⢠? â¢[?] ? ) |
+ sta_lift sta_lpx_sn sta_aaa sta_sta |
|
@@ -771,9 +776,9 @@
|
- local env. ref. for degree assignment |
- lsubd ( ? ⢠? âªâ« ? ) |
- lsubd_da lsubd_lsubd |
+ parameters |
+ sh |
+ sd |
|
@@ -785,9 +790,9 @@
|
- degree assignment |
- da ( â¦?,?⦠⢠? âª[?,?] ? ) |
- da_lift da_da |
+ local env. ref. for atomic arity assignment |
+ lsuba ( ? ⢠? ââ« ? ) |
+ lsuba_aaa lsuba_lsuba |
|
@@ -799,9 +804,9 @@
|
- parameters |
- sh |
- sd |
+ atomic arity assignment |
+ aaa ( â¦?,?⦠⢠? â ? ) |
+ aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa |
|
@@ -824,9 +829,9 @@
- substitution |
+ multiple substitution |
lazy equivalence |
- fleq ( â¦?,?,?⦠â[?] â¦?,?,?⦠) |
+ fleq ( â¦?,?,?⦠â¡[?] â¦?,?,?⦠) |
fleq_fleq |
@@ -842,8 +847,22 @@
|
|
- lleq ( ? â[?,?] ? ) |
- lleq_alt lleq_leq lleq_ldrop lleq_fqus lleq_lleq |
+ lleq ( ? â¡[?,?] ? ) |
+ lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ lazy pointwise extension of a relation |
+ llpx_sn |
+ llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor |
|
@@ -851,6 +870,46 @@
+
+
+
+ |
+ pointwise union for local environments |
+ llor ( ? â©[?,?] ? â¡ ? ) |
+ llor_alt llor_drop |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ context-sensitive exclusion from free variables |
+ frees ( ? ⢠? ϵ ð
*[?]�⦠) |
+ frees_append frees_leq frees_lift |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ contxt-sensitive extended multiple substitution |
+ cpys ( â¦?,?⦠⢠? â¶*[?,?] ? ) |
+ cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? ) |
+ cpys_lift cpys_cpys |
+
+
+ |
+
@@ -886,8 +945,8 @@
|
iterated local env. slicing |
- ldrops ( â©*[?,?] ? â¡ ? ) |
- ldrops_ldrop ldrops_ldrops |
+ drops ( â©*[?,?] ? â¡ ? ) |
+ drops_drop drops_drops |
|
@@ -936,7 +995,7 @@
gr2_gr2 |
- relocation |
+ substitution |
structural successor for closures |
fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
@@ -970,8 +1029,8 @@
global env. slicing |
- gdrop ( â©[?] ? â¡ ? ) |
- gdrop_gdrop |
+ gget ( â©[?] ? â¡ ? ) |
+ gget_gget |
|
@@ -983,11 +1042,9 @@
|
- pointwise union for local environments |
- llor ( ? â©[?] ? â¡ ? ) |
-
-
- |
+ contxt-sensitive extended ordinary substitution |
+ cpy ( â¦?,?⦠⢠? â¶[?,?] ? ) |
+ cpy_lift cpy_nlift cpy_cpy |
|
@@ -999,9 +1056,9 @@
|
- pointwise extension of a relation |
- llpx_sn |
- llpx_sn_alt llpx_sn_tc llpx_sn_leq llpx_sn_ldrop llpx_sn_lpx_sn |
+ local env. ref. for extended substitution |
+ lsuby ( ? âÃ[?,?] ? ) |
+ lsuby_lsuby |
|
@@ -1013,11 +1070,9 @@
|
-
-
- |
+ pointwise extension of a relation |
lpx_sn |
- lpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_sn |
+ lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn |
|
@@ -1030,8 +1085,8 @@
basic local env. slicing |
- ldrop ( â©[?,?,?] ? â¡ ? ) |
- ldrop_leq ldrop_ldrop |
+ drop ( â©[?,?,?] ? â¡ ? ) |
+ drop_append drop_leq drop_drop |
|
@@ -1072,7 +1127,7 @@
grammar |
equivalence for local environments |
- leq ( ? â[?,?] ? ) |
+ leq ( ? ⩬[?,?] ? ) |
leq_leq |
@@ -1086,7 +1141,7 @@
|
same top term constructor |
- tstc ( ? â ? ) |
+ tstc ( ? â ? ) |
tstc_tstc tstc_vector |
@@ -1217,6 +1272,6 @@
- Last update: Fri, 18 Apr 2014 21:10:22 +0200
+ Last update: Sat, 28 Jun 2014 20:29:31 +0200
|