component | plane | files |
|
|
|
|
|
|
|
|
dynamic typing | stratified native validity | snv ( ⦃?,?⦄ ⊩ ? :[?] ) | snv_lift | snv_aaa |
|
|
|
|
|
|
equivalence | context-sensitive equivalence | lcpcs ( ? ⊢ ⬌* ? ) | lcpcs_aaa | lcpcs_lcprs | lcpcs_lcpcs |
|
|
|
|
|
|
| cpcs ( ? ⊢ ? ⬌* ? ) | cpcs_ltpss | cpcs_delift | cpcs_ltpr | cpcs_cprs | cpcs_cpcs |
|
|
|
conversion | context-sensitive conversion | lcpc ( ? ⊢ ⬌ ? ) | lcpc_lcpc |
|
|
|
|
|
|
|
|
| cpc ( ? ⊢ ? ⬌ ? ) | cpc_cpc |
|
|
|
|
|
|
|
computation | extended computation | xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? ) | xprs_lift | xprs_aaa | xprs_cprs |
|
|
|
|
|
| weakly normalizing computation | cpe ( ? ⊢ ➡* 𝐍⦃?⦄ ) | cpe_cpe |
|
|
|
|
|
|
|
| strongly normalizing computation | csn_vector ( ? ⊢ ⬊* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa |
|
|
|
|
|
|
| csn ( ? ⊢ ⬊* ? ) | csn_alt ( ? ⊢ ⬊⬊* ? ) | csn_lift | csn_cpr | csn_lcpr |
|
|
|
|
| context-sensitive computation | lcprs ( ? ⊢ ➡* ? ) | lcprs_aaa | lcprs_cprs | lcprs_lcprs |
|
|
|
|
|
|
| cprs (? ⊢ ? ➡* ?) | cprs_lift | cprs_delift | cprs_ltpr | cprs_lcpr | cprs_cprs | cprs_lcprs | cprs_tstc | cprs_tstc_vector |
| context-free computation | ltprs ( ? ➡* ? ) | ltprs_alt ( ? ➡➡* ? ) | ltprs_ldrop | ltprs_ltprs |
|
|
|
|
|
|
| tprs ( ? ➡* ?) | tprs_lift | tprs_tprs |
|
|
|
|
|
|
| local env. ref. for abstract candidates of reducibility | lsubc ( ? ⊑[?] ? ) | lsubc_ldrop | lsubc_ldrops | lsubc_lsuba |
|
|
|
|
|
| support for abstract computation properties | acp | acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 ) | acp_aaa |
|
|
|
|
|
|
reducibility | extended reduction | xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? ) | xpr_lift | xpr_aaa |
|
|
|
|
|
|
| context-sensitive normal forms | cnf ( ? ⊢ 𝐍⦃?⦄ ) | cnf_lift |
|
|
| cnf_cif |
|
|
|
| context-sensitive reduction | lcpr ( ? ⊢ ➡ ? ) | lcpr_aaa | lcpr_cpr | lcpr_lcpr |
|
|
|
|
|
|
| cpr ( ? ⊢ ? ➡ ? ) | cpr_lift | cpr_ltpss | cpr_delift | cpr_ltpr | cpr_cpr |
|
|
|
| context-sensitive reducible forms | crf ( ? ⊢ 𝐑⦃?⦄ ) | crf_append | cif ( ? ⊢ 𝐈⦃?⦄ ) | cif_append |
|
|
|
|
|
| focalized reduction | lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ ) |
|
|
|
|
|
|
|
|
|
| fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ ) |
|
|
|
|
|
|
|
|
| context-free normal forms | thnf ( 𝐇𝐍⦃?⦄ ) |
|
|
|
|
|
|
|
|
| context-free reduction | ltpr ( ? ➡ ? ) | ltpr_ldrop | ltpr_tps | ltpr_ltpss_dx | ltpr_ltpss_sn | ltpr_aaa | ltpr_ltpr |
|
|
|
| tpr ( ? ➡ ? ) | tpr_lift | tpr_tpss | tpr_delift | tpr_tpr |
|
|
|
|
unwind |
|
|
|
|
|
|
|
|
|
|
static typing | local env. ref. for stratified static type assignment | lsubss ( ? ⁝⊑ ? ) | lsubss_ldrop | lsubss_ssta | lsubss_lsubss |
|
|
|
|
|
| stratified static type assignment | ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) | ssta_lift | ssta_ltpss_dx | ssta_ltpss_sn | ssta_aaa | ssta_ssta |
|
|
|
| local env. ref. for atomic arity assignment | lsuba ( ? ⁝⊑ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba |
|
|
|
|
|
| atomic arity assignment | aaa ( ? ⊢ ? ⁝ ? ) | aaa_lift | aaa_lifts | aaa_ltpss_dx | aaa_ltpss_sn | aaa_aaa |
|
|
|
| parameters | sh | sd |
|
|
|
|
|
|
|
unfold | basic local env. thinning | thin ( ? ▼*[?,?] ≡ ? ) | thin_ldrop | thin_delift |
|
|
|
|
|
|
| inverse basic term relocation | delift ( ? ⊢ ? ▼*[?,?] ≡ ? ) | delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? ) | delift_lift | delift_tpss | delift_ltpss | delift_delift |
|
|
|
| partial unfold | ltpss_sn ( ? ⊢ ▶*[?,?] ? ) | ltpss_sn_ldrop | ltpss_sn_tps | ltpss_sn_tpss | ltpss_sn_ltpss_sn | ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? ) |
|
|
|
|
| ltpss_dx ( ? ▶*[?,?] ? ) | ltpss_dx_ldrop | ltpss_dx_tps | ltpss_dx_tpss | ltpss_dx_ltpss_dx |
|
|
|
|
|
| tpss ( ? ⊢ ? ▶*[?,?] ? ) | tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? ) | tpss_lift | tpss_tpss |
|
|
|
|
|
| generic local env. slicing | ldrops ( ⇩*[?] ? ≡ ? ) | ldrops_ldrop | ldrops_ldrops |
|
|
|
|
|
|
| generic term relocation | lifts_vector ( ⇧*[?] ? ≡ ? ) | lifts_lift_vector |
|
|
|
|
|
|
|
|
| lifts ( ⇧*[?] ? ≡ ? ) | lifts_lift | lifts_lifts |
|
|
|
|
|
|
| support for generic relocation | gr2 ( @⦃?,?⦄ ≡ ? ) | gr2_plus ( ? + ? ) | gr2_minus ( ? ▭ ? ≡ ? ) | gr2_gr2 |
|
|
|
|
|
substitution | parallel substitution | tps ( ? ⊢ ? ▶[?,?] ? ) | tps_lift | tps_tps |
|
|
|
|
|
|
| global env. slicing | gdrop ( ⇩[?] ? ≡ ? ) | gdrop_gdrop |
|
|
|
|
|
|
|
| basic local env. slicing | ldrop ( ⇩[?,?] ? ≡ ? ) | ldrop_append | ldrop_lpx | ldrop_sfr | ldrop_ldrop |
|
|
|
|
| local env. ref. for substitution | lsubs ( ? ≼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( ≽[?,?] ? ) |
|
|
|
|
|
|
| basic term relocation | lift_vector ( ⇧[?,?] ? ≡ ? ) | lift_lift_vector |
|
|
|
|
|
|
|
|
| lift ( ⇧[?,?] ? ≡ ? ) | lift_lift |
|
|
|
|
|
|
|
grammar | same head term form | tshf ( ? ≈ ? ) | (tshf_tshf) |
|
|
|
|
|
|
|
| same top term constructor | tstc ( ? ≃ ? ) | tstc_tstc | tstc_vector |
|
|
|
|
|
|
| closures | cl_shift ( ? @@ ? ) | cl_weight ( #{?,?} ) |
|
|
|
|
|
|
|
| internal syntax | genv |
|
|
|
|
|
|
|
|
|
| lenv | lenv_weight ( #{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) | lenv_px | lenv_px_bi |
|
|
|
|
| term | term_weight ( #{?} ) | term_simple ( 𝐒⦃?⦄ ) | term_vector |
|
|
|
|
|
|
| item |
|
|
|
|
|
|
|
|
| external syntax | aarity |
|
|
|
|
|
|
|
|