@@ -363,60 +376,164 @@
- rt-transition |
- t-bound context-sensitive rt-transition |
- lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
+ rt-computation |
+ uncounted context-sensitive rt-computation |
+ csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
+
+
+ |
-
+ |
|
-
+ |
|
- cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
- cpr_drops |
+ csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
+ csx_cnx csx_cpxs csx_csx |
-
+ |
|
-
+ |
|
- cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpm_simple cpm_drops cpm_lsubr cpm_cpx |
+ lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ lfpxs_length lfpxs_fqup lfpxs_cpxs |
-
+ |
+
+ |
+
|
- uncounted context-sensitive rt-transition |
- lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
- lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa |
+ 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 |
+
+
+
|
-
+ |
|
- cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
- cpx_simple cpx_drops cpx_lsubr |
+ 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 |
+
+
+ iterated static typing |
+ iterated extension on referred entries |
+ tc_lfxs ( ? ⦻**[?,?] ? ) |
+
|
- counted context-sensitive rt-transition |
- cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
- cpg_simple cpg_drops cpg_lsubr |
static typing |
- restricted ref. for atomic arity assignment |
+ generic reducibility |
+ lsubc ( ? ⢠? â«[?] ? ) |
+ lsubc_drops lsubc_lsubr lsubc_lsuba |
+
+
+
+
+ |
+
+
+ |
+ gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
+ gcp_aaa |
+
+
+
+
+ |
+
+
+ |
+ gcp |
+
+
+ |
+
+
+
+
+ |
+ atomic arity assignment |
lsuba ( ? ⢠? â«â ? ) |
lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
@@ -424,7 +541,9 @@
|
- atomic arity assignment |
+
+
+ |
aaa ( â¦?,?⦠⢠? â ? ) |
aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
@@ -432,7 +551,7 @@
|
- degree-based equivalence for closures on referred entries |
+ degree-based equivalence on referred entries |
ffdeq ( â¦?,?,?⦠â¡[?,?] â¦?,?,?⦠) |
ffdeq_fqup ffdeq_ffdeq |
@@ -440,9 +559,11 @@
|
- degree-based equivalence for local environments on referred entries |
+
+
+ |
lfdeq ( ? â¡[?,?,?] ? ) |
- lfdeq_length lfdeq_fqup lfdeq_lfdeq |
+ lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq |
@@ -456,7 +577,7 @@
|
|
- restricted ref. for context-sensitive free variables |
+ context-sensitive free variables |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
lsubf_frees |
@@ -464,9 +585,11 @@
|
- context-sensitive free variables |
+
+
+ |
frees ( ? ⢠ð
*�⦠⡠? ) |
- frees_weight frees_drops frees_fqup frees_frees |
+ frees_drops frees_fqup frees_frees |
@@ -542,7 +665,7 @@
|
lifts ( â¬*[?] ? â¡ ? ) |
- lifts_simple lifts_weight lifts_lifts |
+ lifts_simple lifts_weight lifts_tdeq lifts_lifts |
@@ -570,17 +693,17 @@
|
|
- degree-based equivalence for terms |
- deq ( ? â¡[?,?] ? ) |
- deq_deq |
+ same top term structure |
+ tsts ( ? ⩳[?,?] ? ) |
+ tsts_simple tsts_tdeq tsts_tsts tsts_simple_vector |
|
- same top term structure |
- tsts ( ? â ? ) |
- tsts_tsts tsts_vector |
+ degree-based equivalence for terms |
+ deq ( ? â¡[?,?] ? ) |
+ deq_deq |
@@ -767,6 +890,6 @@
- Last update: Tue, 24 Jan 2017 18:22:21 +0100
+ Last update: Thu, 16 Mar 2017 20:59:31 +0100
|