domain | block | leader | applicator (with →θ)* | reduction | →ζ * | reference * |
{X | Γ ⊢ X : W} | local typed abstraction * | Γ ⊢ +λW | ⓐV | →β | no | #i |
|
local typed declaration ** | Γ ⊢ -λW | ⓐV | →β | no | #i |
|
global typed declaration *** | Γ ⊢ pλW | no | no | no | $p |
|
native type annotation * | Γ ⊢ ⓝW | no | no | yes | no |
{X | Γ ⊢ X = V} | local abbreviation * | Γ ⊢ +δV | no | local →δ | yes | #i |
|
local definition ** | Γ ⊢ -δV | no | local →δ | no | #i |
|
global definition *** | Γ ⊢ pδV | no | global →δ | no | $p |
no | sort **** | Γ ⊢ ⋆k | no | no | no | no |
category | objects |
|
|
|
|
|
sizes | files | 247 | characters | 350287 | nodes | 1035865 |
propositions | theorems | 76 | lemmas | 748 | total | 824 |
concepts | declared | 41 | defined | 77 | total | 118 |
component | plane | files |
|
|
|
dynamic typing | "big tree" parallel computation | yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ ) | yprs_yprs | ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ ) | ygt_ygt |
|
"big tree" parallel reduction | ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ ) | ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ ) |
|
|
|
local env. ref. for stratified native validity | lsubsv ( ? ⊢ ? ¡⊑[?] ? ) | lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv |
|
|
|
stratified native validity | snv ( ⦃?,?⦄ ⊢ ? ¡[?] ) | snv_lift snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs |
|
|
equivalence | context-sensitive equivalence | cpcs ( ? ⊢ ? ⬌* ? ) | cpcs_aaa cpcs_cprs cpcs_cpcs |
|
|
conversion | context-sensitive conversion | cpc ( ? ⊢ ? ⬌ ? ) | cpc_cpc |
|
|
computation | context-sensitive extended evaluation | cpxe ( ⦃?,?⦄ ⊢ ➡*[?] 𝐍⦃?⦄ ) |
|
|
|
|
context-sensitive evaluation | cpre ( ? ⊢ ➡* 𝐍⦃?⦄ ) | cpre_cpre |
|
|
|
strongly normalizing computation | csn_vector ( ? ⊢ ⬊* ? ) | csn_tstc_vector csn_aaa |
|
|
|
|
csn ( ? ⊢ ⬊* ? ) | csn_alt ( ? ⊢ ⬊⬊* ? ) | csn_lift csn_lpx |
|
|
decomposed extended computation | dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) | dxprs_lift 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 |
|
|
|
context-sensitive computation | lprs ( ? ⊢ ➡* ? ) | lprs_alt ( ? ⊢ ➡➡* ? ) | lprs_ldrop lprs_cprs lprs_lprs |
|
|
|
cprs ( ? ⊢ ? ➡* ?) | cprs_lift cprs_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 |
|
reduction | context-sensitive extended normal forms | cnx ( ⦃?,?⦄ ⊢ 𝐍[?]⦃?⦄ ) | cnx_lift cnx_crx cnx_cix |
|
|
|
context-sensitive extended reduction | lpx ( ⦃?,?⦄ ⊢ ➡[?] ? ) | lpx_ldrop lpx_aaa |
|
|
|
|
cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) | cpx_lift cpx_cix |
|
|
|
context-sensitive extended irreducible forms | cix ( ⦃?,?⦄ ⊢ 𝐈[?]⦃?⦄ ) | cix_append cix_lift |
|
|
|
context-sensitive extended reducible forms | crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ ) | crx_append crx_lift |
|
|
|
context-sensitive normal forms | cnr ( ? ⊢ 𝐍⦃?⦄ ) | cnr_lift cnr_crr cnr_cir |
|
|
|
context-sensitive reduction | lpr ( ? ⊢ ➡ ? ) | lpr_ldrop lpr_lpr |
|
|
|
|
cpr ( ? ⊢ ? ➡ ? ) | cpr_lift cpr_cir |
|
|
|
context-sensitive irreducible forms | cir ( ? ⊢ 𝐈⦃?⦄ ) | cir_append cir_lift |
|
|
|
context-sensitive reducible forms | crr ( ? ⊢ 𝐑⦃?⦄ ) | crr_append crr_lift |
|
|
unfold | unfold | unfold ( ? ⊢ ? ⧫* ? ) |
|
|
|
|
iterated stratified static type assignment | sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? ) | sstas_lift sstas_aaa sstas_sstas |
|
|
static typing | stratified static type assignment | ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) | ssta_lift 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_aaa |
|
|
|
parameters | sh | sd |
|
|
substitution | restricted local env. ref. | lsubr ( ? ⊑ ? ) | lsubr_lsubr |
|
|
|
iterated structural successor for closures | fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ ) | fsups_fsups |
|
|
|
|
fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ ) | fsupp_fsupp |
|
|
|
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 |
relocation | structural successor for closures | fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) | fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ ) | fsupq_alt |
|
|
global env. slicing | gdrop ( ⇩[?] ? ≡ ? ) | gdrop_gdrop |
|
|
|
basic local env. slicing | ldrop ( ⇩[?,?] ? ≡ ? ) | ldrop_append ldrop_lpx_sn ldrop_ldrop |
|
|
|
basic term relocation | lift_vector ( ⇧[?,?] ? ≡ ? ) | lift_lift_vector |
|
|
|
|
lift ( ⇧[?,?] ? ≡ ? ) | lift_lift |
|
|
grammar | pointwise extension of a relation | lpx_sn | lpx_sn_tc lpx_sn_lpx_sn |
|
|
|
same top term constructor | tstc ( ? ≃ ? ) | tstc_tstc tstc_vector |
|
|
|
closures | cl_shift ( ? @@ ? ) | cl_weight ( ♯{?,?} ) |
|
|
|
internal syntax | genv |
|
|
|
|
|
lenv | lenv_weight ( ♯{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) |
|
|
term | term_weight ( ♯{?} ) | term_simple ( 𝐒⦃?⦄ ) | term_vector |
|
|
item |
|
|
|
|
external syntax | aarity |
|
|
|