component | plane | files |
|
|
|
functional | reduction and type machine | rtm | rtm_step ( ? ⇨ ? ) |
|
|
| unfold | lift ( ↑[?,?] ? ) | subst ( [?←?] ? ) |
|
|
examples |
|
|
|
|
|
native typing |
| nty |
|
|
|
conversion | context-sensitive conversion | cpcs ( ? ⊢ ? ⬌* ? ) |
|
|
|
computation | strongly normalizing computation | csn ( ⬇* ? ) | csn_cr | csn_aaa |
|
| context-sensitive computation | cprs (? ⊢ ? ➡* ?) |
|
|
|
| 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 | context-sensitive reduction | lcpr ( ? ⊢ ➡ ? ) |
|
|
|
|
| cpr ( ? ⊢ ? ➡ ? ) | cpr_lift | cpr_ltpr | cpr_cpr |
| context-free normal forms | twhnf | tnf |
|
|
| context-free reduction | ltpr ( ? ➡ ? ) | ltpr_ldrop |
|
|
|
| tpr ( ? ➡ ? ) | tpr_lift | tpr_tpss | tpr_tpr |
| context-free reducible forms | trf |
|
|
|
static typing | static type assignment | sty | sty_lift | sty_sty |
|
| local env. ref. for atomic arity assignment | lsuba ( ? ÷⊑ ? ) |
|
|
|
| atomic arity assignment | aaa ( ? ⊢ ? ÷ ? ) | aaa_lift | aaa_lifts | aaa_aaa |
| parameters | sh |
|
|
|
unfold | term inverse relocation | delift ( ? ⊢ ? [?,?] ≡ ? ) | delift_lift |
|
|
| partial unfold | ltpss ( ? [?,?] ▶* ? ) | ltpss_ldrop | ltpss_tps | ltpss_ltpss |
|
| tpss ( ? ⊢ ? [?,?] ▶* ? ) | tpss_lift | tpss_tpss | tpss_ltps |
| 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_gr2 |
|
|
substitution | parallel substitution | ltps ( ? [?,?] ▶ ? ) | ltps_ldrop | ltps_tps | ltps_ltps |
|
| tps ( ? ⊢ ? [?,?] ▶ ? ) | tps_lift | tps_tps |
|
| global env. slicing | gdrop ( ⇩[?] ? ≡ ? ) | gdrop_gdrop |
|
|
| basic local env. slicing | ldrop ( ⇩[?,?] ? ≡ ? ) | ldrop_ldrop |
|
|
| basic term relocation | lift_vector ( ⇧[?,?] ? ≡ ? ) | lift_lift_vector |
|
|
|
| lift ( ⇧[?,?] ? ≡ ? ) | lift_lift |
|
|
grammar | local env. ref. for substitution | lsubs ( ? [?,?] ≼ ? ) | lsubs_lsubs |
|
|
| term hom. | thom | thom_thom |
|
|
| closures | cl_shift ( ? @ ? ) | cl_weight ( #[?,?] ) |
|
|
| internal syntax | genv |
|
|
|
|
| lenv | lenv_weight ( #[?] ) | lenv_length ( |?| ) |
|
|
| term | term_weight ( #[?] ) | term_simple | term_vector |
|
| item |
|
|
|
| external syntax | aarity |
|
|
|