component |
+ section |
plane |
files |
-
+ |
|
-
+ |
+
+ rt-conversion |
+ context-sensitive parallel r-conversion |
+ for terms |
+ cpc ( â¦?,?⦠⢠? â¬[?] ? ) |
+ cpc_cpc |
+
+
+ rt-computation |
+ uncounted context-sensitive parallel rt-computation |
+ refinement for lenvs |
+ lsubsx ( ? ⢠? ââ§[?,?,?] ? ) |
+ lsubsx_lfsx lsubsx_lsubsx |
+
+
+
+
+ |
+
|
+ strongly normalizing for lenvs on referred entries |
+ lfsx ( ? ⢠â¬*[?,?,?] ðâ¦?⦠) |
+ lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx |
- rt-computation |
- uncounted context-sensitive rt-transition |
- cpxs ( â¦?,?⦠⢠? â¬*[?] ? ) |
-
+ |
|
-
+ |
|
+ strongly normalizing for term vectors |
+ csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
+ csx_cnx_vector csx_csx_vector |
-
+ |
|
- generic reducibility |
- lsubc ( ? ⢠? â«[?] ? ) |
- lsubc_drop lsubc_drops lsubc_lsubr lsubc_lsuba |
-
+ |
|
+ strongly normalizing for terms |
+ csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
+ csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx |
-
+ |
|
-
+ |
|
- gcp |
- gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
- gcp_aaa |
+ for lenvs on referred entries |
+ lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs |
- rt-transition |
- parallel qrst-rtransition |
- fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
-
+ |
|
-
+ |
+
+ |
+ for lenvs on all entries |
+ lpxs ( â¦?,?⦠⢠â¬*[?] ? ) |
+
|
-
+ |
|
- t-bound context-sensitive rt-transition |
- lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
-
+ |
|
+ for terms |
+ cpxs ( â¦?,?⦠⢠? â¬*[?] ? ) |
+ cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs |
-
+ | rt-transition |
+ uncounted parallel rst-transition |
+ for closures |
+ fpbq ( â¦?,?,?⦠â½[?] â¦?,?,?⦠) |
+ fpbq_aaa |
+
+
+
|
-
+ |
|
- cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
- cpr_drops |
-
+ | proper for closures |
+ fpb ( â¦?,?,?⦠â»[?] â¦?,?,?⦠) |
+ fpb_lfdeq |
+
+
+
|
+ context-sensitive parallel r-transition |
+ for lenvs on referred entries |
+ lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
+ lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
-
+ |
|
-
+ |
|
- cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx |
-
+ | for binders |
+ cpr_ext ( â¦?,?⦠⢠? â¡[?] ? ) |
+
|
-
+ |
|
- uncounted context-sensitive rt-transition |
- cnx ( â¦?,?⦠⢠â¬[?,?] ðâ¦?⦠) |
- cnx_simple cnx_drops |
-
+ |
|
+ for terms |
+ cpr ( â¦?,?⦠⢠? â¡[?] ? ) |
+ cpr_drops |
-
+ |
|
-
+ | t-bound context-sensitive parallel rt-transition |
+ for terms |
+ cpm ( â¦?,?⦠⢠? â¡[?,?] ? ) |
+ cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx |
+
+
+
+
+ |
+ uncounted context-sensitive parallel rt-transition |
+ normal form for terms |
+ cnx ( â¦?,?⦠⢠â¬[?,?] ðâ¦?⦠) |
+ cnx_simple cnx_drops cnx_cnx |
+
+
+
|
- lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
- lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa |
-
+ |
|
+ for lenvs on referred entries |
+ lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
+ lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx |
-
+ |
|
-
+ |
|
- cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
- cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfdeq |
-
+ | for lenvs on all entries |
+ lpx ( â¦?,?⦠⢠â¬[?] ? ) |
+
|
-
+ |
|
- counted context-sensitive rt-transition |
- cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
- cpg_simple cpg_drops cpg_lsubr |
-
+ |
|
-
-
- static typing |
- atomic arity assignment |
- lsuba ( ? ⢠? â«â ? ) |
- lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
-
+ | for binders |
+ cpx_ext ( â¦?,?⦠⢠? â¬[?] ? ) |
+
|
-
+ |
|
-
+ |
|
- aaa ( â¦?,?⦠⢠? â ? ) |
- aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
-
+ | for terms |
+ cpx ( â¦?,?⦠⢠? â¬[?] ? ) |
+ cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq |
+
+
+
|
+ counted context-sensitive parallel rt-transition |
+ for terms |
+ cpg ( â¦?,?⦠⢠? â¬[?,?] ? ) |
+ cpg_simple cpg_drops cpg_lsubr |
+
+
+ iterated static typing |
+ iterated generic extension of a context-sensitive relation |
+ for lenvs on referred entries |
+ tc_lfxs ( ? ⦻**[?,?] ? ) |
+ tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
+
+
+ static typing |
+ generic reducibility |
+ restricted refinement for lenvs |
+ lsubc ( ? ⢠? â«[?] ? ) |
+ lsubc_drops lsubc_lsubr lsubc_lsuba |
|
- degree-based equivalence on referred entries |
- ffdeq ( â¦?,?,?⦠â¡[?,?] â¦?,?,?⦠) |
- ffdeq_fqup ffdeq_ffdeq |
-
+ |
|
+ candidates |
+ gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
+ gcp_aaa |
|
-
+ |
|
- lfdeq ( ? â¡[?,?,?] ? ) |
- lfdeq_length lfdeq_fqup lfdeq_lfdeq |
+ computation properties |
+ gcp |
|
@@ -544,178 +642,215 @@
|
- generic extension on referred entries |
- lfxs ( ? ⦻*[?,?] ? ) |
- lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
-
-
- |
+ atomic arity assignment |
+ restricted refinement for lenvs |
+ lsuba ( ? ⢠? â«â ? ) |
+ lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
|
- context-sensitive free variables |
- lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
- lsubf_frees |
-
+ |
|
+ for terms |
+ aaa ( â¦?,?⦠⢠? â ? ) |
+ aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
|
-
-
- |
- frees ( ? ⢠ð
*�⦠⡠? ) |
- frees_weight frees_drops frees_fqup frees_frees |
-
-
- |
+ degree-based equivalence |
+ for closures on referred entries |
+ ffdeq ( â¦?,?,?⦠â[?,?] â¦?,?,?⦠) |
+ ffdeq_fqup ffdeq_ffdeq |
|
- restricted ref. for local env. |
- lsubr ( ? â« ? ) |
- lsubr_length lsubr_drops lsubr_lsubr |
-
+ |
|
+ for lenvs on referred entries |
+ lfdeq ( ? â[?,?,?] ? ) |
+ lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq |
- s-computation |
- iterated structural successor for closures |
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fqus_weight fqus_drops fqus_fqup fqus_fqus |
-
+ |
|
+ syntactic equivalence |
+ for lenvs on referred entries |
+ lfeq ( ? â¡[?] ? ) |
+ lfeq_fqup lfeq_lfeq |
-
-
- |
-
-
- |
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fqup_weight fqup_drops fqup_fqup |
-
+ |
|
+ generic extension of a context-sensitive relation |
+ for lenvs on referred entries |
+ lfxs ( ? ⦻*[?,?] ? ) |
+ lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
- s-transition |
- structural successor for closures |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
- fquq_length fquq_weight |
-
+ |
|
+ context-sensitive free variables |
+ restricted refinement for lenvs |
+ lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
+ lsubf_lsubr lsubf_frees lsubf_lsubf |
-
+ |
|
-
+ |
|
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
- fqu_length fqu_weight |
-
+ | for terms |
+ frees ( ? ⢠ð
*�⦠⡠? ) |
+ frees_drops frees_fqup frees_frees |
+
+
+
|
+ local environments |
+ restricted refinement |
+ lsubr ( ? â« ? ) |
+ lsubr_length lsubr_drops lsubr_lsubr |
- relocation |
- generic slicing for local environments |
- drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
-
+ | s-computation |
+ iterated structural successor |
+ for closures |
+ fqus ( â¦?,?,?⦠â*[?] â¦?,?,?⦠) ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus_weight fqus_drops fqus_fqup fqus_fqus |
+
+
+
|
-
+ |
|
+ proper for closures |
+ fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup_weight fqup_drops fqup_fqup |
-
+ | s-transition |
+ structural successor |
+ for closures |
+ fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq_length fquq_weight |
+
+
+
|
-
+ |
|
+ proper for closures |
+ fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu_length fqu_weight |
+
+
+ relocation |
+ generic slicing |
+ for lenvs |
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
-
+ | drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector |
+
+
+
|
+ generic relocation |
+ for binders |
+ lifts_bind ( â¬*[?] ? â¡ ? ) |
+ lifts_weight_bind lifts_lifts_bind |
|
- generic relocation for terms |
- lifts_vector ( â¬*[?] ? â¡ ? ) |
- lifts_lifts_vector |
-
+ |
|
+ for term vectors |
+ lifts_vector ( â¬*[?] ? â¡ ? ) |
+ lifts_lifts_vector |
|
-
+ |
|
+ for terms |
lifts ( â¬*[?] ? â¡ ? ) |
- lifts_simple lifts_weight lifts_tdeq lifts_lifts |
-
-
- |
+ lifts_simple lifts_weight lifts_tdeq lifts_lifts |
|
- ranged equivalence for local environments |
+ syntactic equivalence |
+ for lenvs on selected entries |
lreq ( ? â¡[?] ? ) |
- lreq_length lreq_lreq |
-
+ | lreq_length lreq_lreq |
+
+
+
|
+ generic entrywise extension |
+ for lenvs of one contex-sensitive relation |
+ lex ( ? ⦻[?] ? ) |
+ lex_tc |
|
- generic entrywise extension |
- lexs ( ? ⦻*[?,?,?] ? ) |
- lexs_length lexs_lexs |
-
+ |
|
+ for lenvs of two contex-sensitive relations |
+ lexs ( ? ⦻*[?,?,?] ? ) |
+ lexs_tc lexs_length lexs_lexs |
syntax |
- append for local environments |
+ append for local environments |
+ |
append ( ? @@ ? ) |
- append_length |
-
+ | append_length |
+
+
+
|
+ 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 ( ? â[?,?] ? ) ( ? ⢠? â[?,?] ? ) |
|
@@ -724,22 +859,20 @@
|
- same top term structure |
- tsts ( ? â ? ) |
- tsts_tsts tsts_vector |
-
+ |
|
+ |
+ tdeq ( ? â[?,?] ? ) |
+ tdeq_tdeq |
|
- closures |
+ closures |
+ |
cl_weight ( â¯{?,?,?} ) |
-
-
- |
|
@@ -748,13 +881,22 @@
|
-
+ |
|
+ |
cl_restricted_weight ( â¯{?,?} ) |
-
+ |
|
+
+
+
+
+ |
+ global environments |
+ |
+ genv |
|
@@ -763,11 +905,20 @@
|
- global environments |
- genv |
-
+ | local environments |
+ |
+ ceq_ext |
+ ceq_ext_ceq_ext |
+
+
+
+
+ |
+
|
+ |
+ cext2 |
|
@@ -776,11 +927,11 @@
|
- local environments |
- lenv_length ( |?| ) |
-
+ |
|
+ |
+ lenv_length ( |?| ) |
|
@@ -789,13 +940,11 @@
|
-
+ |
|
+ |
lenv_weight ( â¯{?} ) |
-
-
- |
|
@@ -804,26 +953,42 @@
|
-
+ |
|
+ |
lenv |
-
+ |
|
-
+ |
+
+
|
+ binders for local environments |
+ |
+ ext2 |
+ ext2_tc ext2_ext2 |
|
- terms |
- term_vector ( �.? ) |
-
+ |
|
+ |
+ bind |
+ bind_weight |
+
+
+
+
+ |
+ terms |
+ |
+ term_vector ( �.? ) |
|
@@ -832,13 +997,11 @@
|
-
+ |
|
+ |
term_simple ( ðâ¦?⦠) |
-
-
- |
|
@@ -847,13 +1010,11 @@
|
-
+ |
|
+ |
term_weight ( â¯{?} ) |
-
-
- |
|
@@ -862,13 +1023,11 @@
|
-
+ |
|
+ |
term |
-
-
- |
|
@@ -877,11 +1036,9 @@
|
- items |
+ items |
+ |
item_sd |
-
-
- |
|
@@ -890,13 +1047,11 @@
|
-
+ |
|
+ |
item_sh |
-
-
- |
|
@@ -905,13 +1060,11 @@
|
-
+ |
|
+ |
item |
-
-
- |
|
@@ -920,11 +1073,9 @@
|
- atomic arities |
+ atomic arities |
+ |
aarity |
-
-
- |
|
@@ -958,6 +1109,6 @@
- Last update: Sun, 19 Feb 2017 16:24:37 +0100
+ Last update: Fri, 24 Nov 2017 21:00:01 +0100