@@ -316,19 +316,9 @@
dynamic typing |
- "big tree" parallel computation |
- yprs ( ? ⢠â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
- yprs_yprs |
- ygt ( �,?,?⦠>[?,?] �,?,?⦠) |
- ygt_ygt |
-
-
-
-
- |
- "big tree" parallel reduction |
- ypr ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
- ysc ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ local env. ref. for stratified native validity |
+ lsubsv ( ? ⢠? ¡â[?,?] ? ) |
+ lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv |
|
@@ -340,9 +330,9 @@
|
- 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_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs |
|
@@ -351,21 +341,21 @@
-
-
- |
- stratified native validity |
- snv ( �,?⦠⢠? ¡[?,?] ) |
- snv_lift snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs |
-
+ | equivalence |
+ decomposed extended equivalence |
+ cpes ( â¦?,?⦠⢠? â¢*â¬*[?,?] ? ) |
+ cpes_cpds |
+
|
-
+ |
|
- equivalence |
+
+
+ |
context-sensitive equivalence |
cpcs ( â¦?,?⦠⢠? â¬* ? ) |
cpcs_aaa cpcs_cprs cpcs_cpcs |
@@ -420,9 +410,49 @@
|
- strongly normalizing computation |
- csn_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- csn_tstc_vector csn_aaa |
+ strongly normalizing "big tree" computation |
+ fsb ( �,?⦠⢠⦥[?,?] ? ) |
+ fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
+ fsb_fleq fsb_csx |
+
+
+ |
+
+
+
+
+ |
+ strongly normalizing extended computation |
+ csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ csx_tstc_vector csx_aaa |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ csx ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ csx_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
+ csx_lift csx_lpx |
+
+
+ |
+
+
+
+
+ |
+ "big tree" parallel computation |
+ fpbr ( â¦?,?,?⦠ââ¥[?,?] â¦?,?,?⦠) |
+ fpbr_fpbr |
|
@@ -437,9 +467,25 @@
|
- csn ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- csn_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
- csn_lift csn_lpx |
+ fpbg ( �,?,?⦠>[?,?] �,?,?⦠) |
+ fpbg_lift fpbg_fpbg |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
+ fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
+ fpbs_lift fpbs_fleq fpbs_fpbs |
|
@@ -449,8 +495,8 @@
decomposed extended computation |
- dxprs ( â¦?,?⦠⢠? â¢*â¡*[?,?] ? ) |
- dxprs_lift dxprs_aaa dxprs_dxprs |
+ cpds ( â¦?,?⦠⢠? â¢*â¡*[?,?] ? ) |
+ cpds_lift cpds_aaa cpds_cpds |
|
@@ -542,6 +588,36 @@
reduction |
+ "big tree" parallel reduction |
+ fpbc ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpbc_lift |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
+ fpb_lift |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
context-sensitive extended normal forms |
cnx ( â¦?,?⦠⢠ð[?,?]â¦?⦠) |
cnx_lift cnx_crx cnx_cix |
@@ -700,21 +776,47 @@
|
- iterated stratified static type assignment |
- sstas ( â¦?,?⦠⢠? â¢*[?] ? ) |
- sstas_lift sstas_aaa sstas_sstas |
-
-
- |
+ iterated static type assignment |
+ lsstas ( â¦?,?⦠⢠? â¢*[?,?,?] ? ) |
+ lsstas_alt ( â¦?,?⦠⢠? â¢â¢*[?,?,?] ? ) |
+ lsstas_lift lsstas_aaa lsstas_lsstas |
|
static typing |
+ local env. ref. for atomic arity assignment |
+ lsuba ( ? ⢠? ââ ? ) |
+ lsuba_ldrop lsuba_aaa lsuba_lsuba |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
+ atomic arity assignment |
+ aaa ( â¦?,?⦠⢠? â ? ) |
+ aaa_lift aaa_lifts aaa_da aaa_ssta aaa_aaa |
+
+
+ |
+
+
+ |
+
+
+
+
+ |
stratified static type assignment |
- ssta ( â¦?,?⦠⢠? â¢[?,?] â¦?,?⦠) |
- ssta_lift ssta_aaa ssta_ssta |
+ ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) |
+ ssta_lift ssta_ssta |
|
@@ -726,9 +828,9 @@
|
- 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 |
|
@@ -740,9 +842,9 @@
|
- atomic arity assignment |
- aaa ( â¦?,?⦠⢠? â ? ) |
- aaa_lift aaa_lifts aaa_aaa |
+ degree assignment |
+ da ( â¦?,?⦠⢠? âª[?,?] ? ) |
+ da_lift da_da |
|
@@ -781,8 +883,8 @@
iterated structural successor for closures |
- fsups ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fsups_fsups |
+ fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus_alt fqus_fqus |
|
@@ -797,8 +899,8 @@
|
- fsupp ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fsupp_fsupp |
+ fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup_fqup |
|
@@ -863,9 +965,23 @@
relocation |
structural successor for closures |
- fsup ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fsupq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
- fsupq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+
+
+ |
+
+
+
+
+ |
+ lazy equivalence for closures |
+ fleq ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fleq_fleq |
+
+
+ |
|
@@ -1076,6 +1192,6 @@
- Last update: Wed, 07 Aug 2013 23:40:05 +0200
+ Last update: Sun, 27 Oct 2013 22:23:38 +0100