lambda_delta version 2

This is a summary of the "block structure" of the System's syntactic items and reductions.

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

* In terms only. ** In terms and local environments only. *** In global environments only. **** Sort level k in terms only.

Here is a numerical acount of the specification's contents and its timeline.

category	objects
sizes	files	199	bytes	739801
propositions	theorems	70	lemmas	880	total	950
concepts	declared	40	defined	72	total	112

The source files are grouped in planes and components according to the following table. A notation file covering the whole specification is provided. The notation for the relations or functions introduced in each file is shown in parentheses (? are placeholders).

component	plane	files
dynamic typing	stratified native validity	snv ( ⦃?,?⦄ ⊩ ? :[?] )	snv_lift	snv_aaa
equivalence	context-sensitive equivalence	lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )	lfpcs_aaa	lfpcs_lfprs	lfpcs_lfpcs
		cpcs ( ? ⊢ ? ⬌* ? )	cpcs_ltpss	cpcs_delift	cpcs_aaa	cpcs_ltpr	cpcs_cprs	cpcs_cpcs
conversion	context-sensitive conversion	lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )	lfpc_lfpc
		cpc ( ? ⊢ ? ⬌ ? )	cpc_cpc
computation	extended computation	xprs ( ⦃?,?⦄ ⊢ ? ➸*[?] ? )	xprs_lift	xprs_aaa	xprs_cprs
	weakly normalizing computation	cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )	cpe_cpe
	strongly normalizing computation	csn_vector ( ? ⊢ ⬊* ? )	csn_cpr_vector	csn_tstc_vector	csn_aaa
		csn ( ? ⊢ ⬊* ? )	csn_alt ( ? ⊢ ⬊⬊* ? )	csn_lift	csn_cpr	csn_lfpr
	context-sensitive computation	lfprs ( ⦃?⦄ ➡* ⦃?⦄ )	lfprs_aaa	lfprs_cprs	lfprs_lfprs
		cprs (? ⊢ ? ➡* ?)	cprs_lift	cprs_delift	cprs_aaa	cprs_ltpr	cprs_lfpr	cprs_cprs	cprs_lfprs	cprs_tstc	cprs_tstc_vector
	context-free computation	ltprs ( ? ➡* ? )	ltprs_alt ( ? ➡➡* ? )	ltprs_ldrop	ltprs_ltprs
		tprs ( ? ➡* ?)	tprs_lift	tprs_tprs
	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
reducibility	extended reduction	xpr ( ⦃?,?⦄ ⊢ ? ➸[?] ? )	xpr_lift	xpr_aaa
	context-sensitive focalized reduction	cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )	cnfpr_ltpss	cfpr_aaa	cfpr_cpr
	context-free focalized reduction	lfpr ( ⦃?⦄ ➡ ⦃?⦄ )	lfpr_aaa	lfpr_cpr	lfpr_fpr	lfpr_lfpr	lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )
		fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )	fpr_cpr
	context-sensitive normal forms	cnf ( ? ⊢ 𝐍⦃?⦄ )	cnf_lift	cnf_cif
	context-sensitive reduction	cpr ( ? ⊢ ? ➡ ? )	cpr_lift	cpr_tpss	cpr_ltpss	cpr_delift	cpr_aaa	cpr_ltpr	cpr_cpr
	context-sensitive reducible forms	crf ( ? ⊢ 𝐑⦃?⦄ )	crf_append	cif ( ? ⊢ 𝐈⦃?⦄ )	cif_append
	context-free normal forms	thnf ( 𝐇𝐍⦃?⦄ )
	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
unwind
static typing	local env. ref. for stratified static type assignment	lsubss ( ? ⁝⊑ ? )	lsubss_ldrop	lsubss_ssta	lsubss_lsubss
	stratified static type assignment	ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )	ssta_lift	ssta_ltpss_dx	ssta_ltpss_sn	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_ltpss_dx	aaa_ltpss_sn	aaa_aaa
	parameters	sh	sd
unfold	basic local env. thinning	thin ( ? ▼*[?,?] ≡ ? )	thin_ldrop	thin_delift
	inverse basic term relocation	delift ( ? ⊢ ? ▼*[?,?] ≡ ? )	delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )	delift_lift	delift_tpss	delift_ltpss	delift_delift
	partial unfold	ltpss_sn ( ? ⊢ ▶*[?,?] ? )	ltpss_sn_ldrop	ltpss_sn_tps	ltpss_sn_tpss	ltpss_sn_ltpss_sn	ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )
		ltpss_dx ( ? ▶*[?,?] ? )	ltpss_dx_ldrop	ltpss_dx_tps	ltpss_dx_tpss	ltpss_dx_ltpss_dx
		tpss ( ? ⊢ ? ▶*[?,?] ? )	tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )	tpss_lift	tpss_tpss
	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
substitution	parallel substitution	tps ( ? ⊢ ? ▶[?,?] ? )	tps_lift	tps_tps
	global env. slicing	gdrop ( ⇩[?] ? ≡ ? )	gdrop_gdrop
	basic local env. slicing	ldrop ( ⇩[?,?] ? ≡ ? )	ldrop_append	ldrop_lpx	ldrop_sfr	ldrop_ldrop
	local env. ref. for substitution	lsubs ( ? ≼[?,?] ? )	(lsubs_lsubs)	lsubs_sfr ( ≽[?,?] ? )
	basic term relocation	lift_vector ( ⇧[?,?] ? ≡ ? )	lift_lift_vector
		lift ( ⇧[?,?] ? ≡ ? )	lift_lift
grammar	same head term form	tshf ( ? ≈ ? )	(tshf_tshf)
	same top term constructor	tstc ( ? ≃ ? )	tstc_tstc	tstc_vector
	closures	cl_shift ( ? @@ ? )	cl_weight ( #{?,?} )
	internal syntax	genv
		lenv	lenv_weight ( #{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )	lenv_px	lenv_px_bi
		term	term_weight ( #{?} )	term_simple ( 𝐒⦃?⦄ )	term_vector
		item
	external syntax	aarity

The source files are grouped in directories, one for each component.