component |
plane |
files |
|
|
|
examples |
terms with special features |
ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta |
|
|
|
|
|
|
|
|
|
dynamic typing |
local env. ref. for stratified native validity |
lsubsv ( ? ⊢ ? ⫃¡[?,?] ? ) |
lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv |
|
|
|
stratified native validity |
shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) |
|
|
|
|
|
snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) |
snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve |
|
|
equivalence |
decomposed rt-equivalence |
scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) |
scpes_aaa scpes_cpcs scpes_scpes |
|
|
|
context-sensitive equivalence |
cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? ) |
cpcs_aaa cpcs_cprs cpcs_cpcs |
|
|
conversion |
context-sensitive conversion |
cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? ) |
cpc_cpc |
|
|
computation |
evaluation for context-sensitive rt-reduction |
cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) |
|
|
|
|
evaluation for context-sensitive reduction |
cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) |
cpre_cpre |
|
|
|
strongly normalizing qrst-computation |
fsb ( ⦥[?,?] ⦃?,?,?⦄ ) |
fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ ) |
fsb_aaa fsb_csx |
|
|
strongly normalizing rt-computation |
lcosx ( ? ⊢ ~⬊*[?,?,?] ? ) |
lcosx_cpx |
|
|
|
|
lsx ( ? ⊢ ⬊*[?,?,?,?] ? ) |
lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? ) |
lsx_drop lsx_lpx lsx_lpxs llsx_csx |
|
|
|
csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) |
csx_tsts_vector csx_aaa |
|
|
|
|
csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) |
csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) |
csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs |
|
|
parallel qrst-computation |
fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ ) |
fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg |
|
|
|
|
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) |
fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) |
fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs |
|
|
decomposed rt-computation |
scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) |
scpds_lift scpds_aaa scpds_scpds |
|
|
|
context-sensitive rt-computation |
lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) |
lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
|
|
|
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) |
cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
|
|
|
context-sensitive computation |
lprs ( ⦃?,?⦄ ⊢ ➡* ? ) |
lprs_drop lprs_cprs lprs_lprs |
|
|
|
|
cprs ( ⦃?,?⦄ ⊢ ? ➡* ?) |
cprs_lift cprs_cprs |
|
|
|
local env. ref. for generic reducibility |
lsubc ( ? ⊢ ? ⫃[?] ? ) |
lsubc_drop lsubc_drops lsubc_lsuba |
|
|
|
support for generic computation properties |
gcp |
gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) |
gcp_aaa |
|
reduction |
parallel qrst-reduction |
fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) |
fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ ) |
fpbq_lift fpbq_aaa |
|
|
|
fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) |
fpb_lift fpb_lleq fpb_fleq |
|
|
|
normal forms for context-sensitive rt-reduction |
cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) |
cnx_lift cnx_crx cnx_cix |
|
|
|
context-sensitive rt-reduction |
lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) |
lpx_drop lpx_frees lpx_lleq lpx_aaa |
|
|
|
|
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) |
cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix |
|
|
|
irreducible forms for context-sensitive rt-reduction |
cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) |
cix_lift |
|
|
|
reducible forms for context-sensitive rt-reduction |
crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) |
crx_lift |
|
|
|
normal forms for context-sensitive reduction |
cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ ) |
cnr_lift cnr_crr cnr_cir |
|
|
|
context-sensitive reduction |
lpr ( ⦃?,?⦄ ⊢ ➡ ? ) |
lpr_drop lpr_lpr |
|
|
|
|
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? ) |
cpr_lift cpr_llpx_sn cpr_cir |
|
|
|
irreducible forms for context-sensitive reduction |
cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ ) |
cir_lift |
|
|
|
reducible forms for context-sensitive reduction |
crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ ) |
crr_lift |
|
|
unfold |
unfold |
unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) |
|
|
|
|
iterated static type assignment |
lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? ) |
lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas |
|
|
static typing |
local env. ref. for degree assignment |
lsubd ( ? ⊢ ? ⫃▪[?,?] ? ) |
lsubd_da lsubd_lsubd |
|
|
|
degree assignment |
da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) |
da_lift da_aaa da_da |
|
|
|
parameters |
sh |
sd |
|
|
|
local env. ref. for atomic arity assignment |
lsuba ( ? ⊢ ? ⫃⁝ ? ) |
lsuba_aaa lsuba_lsuba |
|
|
|
atomic arity assignment |
aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) |
aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa |
|
|
|
restricted local env. ref. |
lsubr ( ? ⫃ ? ) |
lsubr_lsubr |
|
|
multiple substitution |
lazy equivalence |
fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ ) |
fleq_fleq |
|
|
|
|
lleq ( ? ≡[?,?] ? ) |
lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq |
|
|
|
lazy pointwise extension of a relation |
llpx_sn |
llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor |
|
|
|
pointwise union for local environments |
llor ( ? ⋓[?,?] ? ≡ ? ) |
llor_alt llor_drop |
|
|
|
context-sensitive exclusion from free variables |
frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ ) |
frees_append frees_lreq frees_lift |
|
|
|
contxt-sensitive multiple rt-substitution |
cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) |
cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) |
cpys_lift cpys_cpys |
|
|
iterated structural successor for closures |
fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) |
fqus_alt fqus_fqus |
|
|
|
|
fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) |
fqup_fqup |
|
|
|
iterated local env. slicing |
drops ( ⬇*[?,?] ? ≡ ? ) |
drops_drop drops_drops |
|
|
|
generic term relocation |
lifts_vector ( ⬆*[?] ? ≡ ? ) |
lifts_lift_vector |
|
|
|
|
lifts ( ⬆*[?] ? ≡ ? ) |
lifts_lift lifts_lifts |
|
|
|
support for multiple relocation |
mr2 ( @⦃?,?⦄ ≡ ? ) |
mr2_plus ( ? + ? ) |
mr2_minus ( ? ▭ ? ≡ ? ) |
mr2_mr2 |
substitution |
structural successor for closures |
fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) |
fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) |
|
|
|
|
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) |
|
|
|
|
global env. slicing |
gget ( ⬇[?] ? ≡ ? ) |
gget_gget |
|
|
|
contxt-sensitive ordinary rt-substitution |
cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) |
cpy_lift cpy_nlift cpy_cpy |
|
|
|
local env. ref. for rt-substitution |
lsuby ( ? ⊆[?,?] ? ) |
lsuby_lsuby |
|
|
|
pointwise extension of a relation |
lpx_sn |
lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn |
|
|
|
basic local env. slicing |
drop ( ⬇[?,?,?] ? ≡ ? ) |
drop_append drop_lreq drop_drop |
|
|
|
basic term relocation |
lift_vector ( ⬆[?,?] ? ≡ ? ) |
lift_lift_vector |
|
|
|
|
lift ( ⬆[?,?] ? ≡ ? ) |
lift_neq lift_lift |
|
|
grammar |
equivalence for local environments |
lreq ( ? ⩬[?,?] ? ) |
lreq_lreq |
|
|
|
same top term structure |
tsts ( ? ≂ ? ) |
tsts_tsts tsts_vector |
|
|
|
closures |
cl_weight ( ♯{?,?,?} ) |
cl_restricted_weight ( ♯{?,?} ) |
|
|
|
internal syntax |
genv |
|
|
|
|
|
lenv |
lenv_weight ( ♯{?} ) |
lenv_length ( |?| ) |
lenv_append ( ? @@ ? ) |
|
|
term |
term_weight ( ♯{?} ) |
term_simple ( 𝐒⦃?⦄ ) |
term_vector ( Ⓐ?.? ) |
|
|
item |
|
|
|
|
external syntax |
aarity |
|
|
|