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 | 169 | characters | 345703 | nodes | 964553 |
propositions | theorems | 75 | lemmas | 710 | total | 785 |
concepts | declared | 42 | defined | 66 | total | 108 |
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_lpss snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs |
|
|
equivalence | local env. ref. for stratified static type assignment | lsubss ( ? •⊑[?] ? ) | lsubss_ldrop lsubss_ssta lsubss_cpcs |
|
|
|
context-sensitive equivalence | cpcs ( ? ⊢ ? ⬌* ? ) | cpcs_lpss cpcs_aaa cpcs_cprs cpcs_cpcs |
|
|
conversion | context-sensitive conversion | cpc ( ? ⊢ ? ⬌ ? ) | cpc_cpc |
|
|
computation | decomposed extended computation | dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? ) | dxprs_lift dxprs_lpss dxprs_aaa dxprs_dxprs |
|
|
|
weakly normalizing computation | cpe ( ? ⊢ ➡* 𝐍⦃?⦄ ) | cpe_cpe |
|
|
|
strongly normalizing computation | csn_vector ( ? ⊢ ⬊* ? ) | csn_tstc_vector csn_aaa |
|
|
|
|
csn ( ? ⊢ ⬊* ? ) | csn_alt ( ? ⊢ ⬊⬊* ? ) | csn_lift csn_lpr |
|
|
context-sensitive computation | lprs ( ? ⊢ ➡* ? ) | lprs_alt ( ? ⊢ ➡➡* ? ) | lprs_ldrop lprs_lpss lprs_aaa lprs_cprs lprs_lprs |
|
|
|
cprs ( ? ⊢ ? ➡* ?) | cprs_tstc cprs_tstc_vector cprs_lift cprs_lpss cprs_aaa 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 normal forms | cnf ( ? ⊢ 𝐍⦃?⦄ ) | cnf_liftt cnf_crf cnf_cif |
|
|
|
context-sensitive reduction | lpr ( ? ⊢ ➡ ? ) | lpr_ldrop lpr_lpss lpr_aaa lpr_lpr |
|
|
|
|
cpr ( ? ⊢ ? ➡ ? ) | cpr_lift cpr_cif |
|
|
|
context-sensitive reducible forms | crf ( ? ⊢ 𝐑⦃?⦄ ) | crf_append | cif ( ? ⊢ 𝐈⦃?⦄ ) | cif_append |
unfold | restricted parallel computation | lpqs ( ? ⊢ ➤* ? ) | lpqs_ldrop lpqs_cpqs lpqs_lpqs |
|
|
|
|
cpqs ( ? ⊢ ? ➤* ? ) | cpqs_lift |
|
|
|
unfold | unfold ( ? ⊢ ? ⧫* ? ) |
|
|
|
|
iterated stratified static type assignment | sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? ) | sstas_lift sstas_lpss sstas_aaa sstas_sstas |
|
|
static typing | stratified static type assignment | ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) | ssta_lift ssta_lpss 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_lpss aaa_aaa |
|
|
|
parameters | sh | sd |
|
|
substitution | parallel substitution | lpss ( ? ⊢ ▶* ? ) | lpss_ldrop lpss_cpss lpss_lpss |
|
|
|
|
cpss ( ? ⊢ ? ▶* ? ) | cpss_lift |
|
|
|
local env. ref. for substitution | 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 ( ⦃?,?⦄ ⊃ ⦃?,?⦄ ) |
|
|
|
|
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 |
|
|
|