-
2014 January 20.
- Parametrized slicing of local environments
+ Parametrized slicing on local environments
comprises both versions of this operation
(one from basic_1, the other used in basic_2 till now).
@@ -375,120 +391,8 @@
-
- rt-computation |
- uncounted context-sensitive rt-computation |
- csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
-
-
- |
-
-
-
-
- |
-
-
- |
- csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
- csx_cnx csx_cpxs csx_csx |
-
-
-
-
- |
-
-
- |
- lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- lfpxs_length lfpxs_fqup lfpxs_cpxs |
-
-
-
-
- |
-
-
- |
- cpxs ( â¦?,?⦠⢠? â¬*[?] ? ) |
- cpxs_tdeq cpxs_tsts cpxs_tsts_vector cpxs_drops cpxs_lsubr cpxs_lfpx cpxs_cnx cpxs_cpxs |
-
rt-transition |
- parallel rst-transition |
- fpbq ( â¦?,?,?⦠â½[?] â¦?,?,?⦠) |
- fpbq_aaa |
-
-
-
-
- |
-
-
- |
- fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
- fpb_lfdeq |
-
-
-
-
- |
- t-bound context-sensitive rt-transition |
- lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
-
-
-
-
- |
-
-
- |
- cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
- cpr_drops |
-
-
-
-
- |
-
-
- |
- cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx |
-
-
-
-
- |
- uncounted context-sensitive rt-transition |
- cnx ( â¦?,?⦠⢠â¬[?,?] ðâ¦?⦠) |
- cnx_simple cnx_drops cnx_cnx |
-
-
-
-
- |
-
-
- |
- lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
- lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx |
-
-
-
-
- |
-
-
- |
- cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
- cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs |
-
-
-
-
- |
counted context-sensitive rt-transition |
cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
cpg_simple cpg_drops cpg_lsubr |
@@ -497,9 +401,7 @@
iterated static typing |
iterated extension on referred entries |
tc_lfxs ( ? ⦻**[?,?] ? ) |
-
-
- |
+ tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
static typing |
@@ -579,7 +481,7 @@
context-sensitive free variables |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
- lsubf_frees |
+ lsubf_lsubr lsubf_frees lsubf_lsubf |
@@ -602,7 +504,7 @@
|
s-computation |
iterated structural successor for closures |
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus ( â¦?,?,?⦠â*[?] â¦?,?,?⦠) ( â¦?,?,?⦠â* â¦?,?,?⦠) |
fqus_weight fqus_drops fqus_fqup fqus_fqus |
@@ -612,13 +514,13 @@
|
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
fqup_weight fqup_drops fqup_fqup |
s-transition |
structural successor for closures |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_length fquq_weight |
@@ -628,7 +530,7 @@
|
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) |
fqu_length fqu_weight |
@@ -647,13 +549,23 @@
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
+ drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops |
+
+
+
+
+ |
+ generic relocation |
+ lifts_bind ( â¬*[?] ? â¡ ? ) |
+ lifts_weight_bind lifts_lifts_bind |
|
- generic relocation for terms |
+
+
+ |
lifts_vector ( â¬*[?] ? â¡ ? ) |
lifts_lifts_vector |
@@ -693,17 +605,29 @@
|
- same top term structure |
- tsts ( ? ⩳[?,?] ? ) |
- tsts_simple tsts_tdeq tsts_tsts tsts_simple_vector |
+ head equivalence for terms |
+ theq ( ? ⩳[?,?] ? ) |
+ theq_simple theq_tdeq theq_theq theq_simple_vector |
|
- degree-based equivalence for terms |
- deq ( ? â¡[?,?] ? ) |
- deq_deq |
+ degree-based equivalence |
+ tdeq_ext ( ? â¡[?,?] ? ) |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ tdeq ( ? â¡[?,?] ? ) |
+ tdeq_tdeq |
@@ -742,6 +666,18 @@
|
local environments |
+ lenv_ext2 |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
lenv_length ( |?| ) |
@@ -771,6 +707,24 @@
|
+
+
+
+ |
+ binders for local environments |
+ ext2 |
+ ext2_ext2 |
+
+
+
+
+ |
+
+
+ |
+ bind |
+ bind_weight |
+
@@ -890,6 +844,6 @@
- Last update: Thu, 16 Mar 2017 20:59:31 +0100
+ Last update: Tue, 17 Oct 2017 20:34:24 +0200
|