]
class "cyan"
[ { "computation" * } {
- [ { "decomposed extended computation" * } {
- [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
+ [ { "context-sensitive extended evaluation" * } {
+ [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?] 𝐍⦃?⦄ )" * ]
}
]
- [ { "weakly normalizing computation" * } {
- [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
+ [ { "context-sensitive evaluation" * } {
+ [ "cpre ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
}
]
[ { "strongly normalizing computation" * } {
[ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpx" * ]
}
]
+ [ { "decomposed extended computation" * } {
+ [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
+ }
+ ]
[ { "context-sensitive extended computation" * } {
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ]
[ "crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ )" "crx_append" + "crx_lift" * ]
}
]
+ [ { "local env. ref. for extended reduction" * } {
+ [ "lsubx ( ? ⓝ⊑ ? )" "lsubx_lsubx" * ]
+ }
+ ]
[ { "context-sensitive normal forms" * } {
[ "cnr ( ? ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
class "yellow"
[ { "substitution" * } {
- [ { "parallel substitution" * } {
+ [ { "parallel substitution" * } {
[ "lpss ( ? ⊢ ▶* ? )" "lpss_ldrop" + "lpss_cpss" + "lpss_lpss" * ]
[ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
}