]
*)
[ { "stratified native validity" * } {
- [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" * ]
+ [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" + "snv_ssta" * ]
}
]
}
[ { "equivalence" * } {
[ { "focalized equivalence" * } {
[ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
+ [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
+ }
+ ]
+ [ { "local env. ref. for context-sensitive equivalence" * } {
+ [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ]
}
]
[ { "context-sensitive equivalence" * } {
class "sky"
[ { "conversion" * } {
[ { "focalized conversion" * } {
- [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
+ [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
+ [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ]
}
]
[ { "context-sensitive conversion" * } {
]
class "cyan"
[ { "computation" * } {
+(*
+ [ { "hyper computation" * } {
+ [ "ysteps ( ? ⊢ ⦃?,?⦄ •⭃*[g] ⦃?,?⦄ )" "ysteps_csups" * ]
+ [ "yprs ( ? ⊢ ⦃?,?⦄ •⥸*[g] ⦃?,?⦄ )" "yprs_csups" + "yprs_xprs" + "yprs_yprs" * ]
+ }
+ ]
+*)
[ { "extended computation" * } {
- [ "xprs ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¸*[?] ? )" "xprs_lift" + "xprs_aaa" + "xprs_cprs" * ]
+ [ "xprs ( â¦\83?,?â¦\84 â\8a¢ ? â\80¢â\9e¡*[?] ? )" "xprs_lift" + "xprs_aaa" + "xpr_lsubss" + "xprs_cprs" + "xprs_xprs" * ]
}
]
[ { "weakly normalizing computation" * } {
]
[ { "focalized computation" * } {
[ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_cprs" + "lfprs_lfprs" * ]
+ [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
}
]
[ { "context-sensitive computation" * } {
]
class "water"
[ { "reducibility" * } {
+(*
+ [ { "hyper reduction" * } {
+ [ "ypr ( ? ⊢ ⦃?,?⦄ •⥸[g] ⦃?,?⦄ )" * ]
+ }
+ ]
+*)
[ { "extended reduction" * } {
- [ "xpr ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¸[?] ? )" "xpr_lift" + "xpr_aaa" * ]
+ [ "xpr ( â¦\83?,?â¦\84 â\8a¢ ? â\80¢â\9e¡[?] ? )" "xpr_lift" + "xpr_aaa" + "xpr_lsubss" * ]
}
]
[ { "context-sensitive focalized reduction" * } {
- [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" * ]
+ [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
}
]
[ { "context-free focalized reduction" * } {
[ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" "lfpr_aaa" + "lfpr_cpr" + "lfpr_fpr" + "lfpr_lfpr" * ]
- [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" * ]
+ [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
}
]
[ { "context-sensitive normal forms" * } {
]
[ { "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" * ]
+ [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
}
]
}
class "grass"
[ { "static typing" * } {
[ { "local env. ref. for stratified static type assignment" * } {
- [ "lsubss ( ? â\81\9dâ\8a\91 ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
+ [ "lsubss ( ? â\80¢â\8a\91[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
}
]
[ { "stratified static type assignment" * } {
[ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
}
]
+ [ { "iterated restricted structural predecessor for closures" * } {
+ [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ]
+ [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ]
+ }
+ ]
[ { "generic term relocation" * } {
[ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
[ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
[ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
}
]
+ [ { "restricted structural predecessor for closures" * } {
+ [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ]
+ }
+ ]
[ { "basic term relocation" * } {
[ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
[ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]