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}	typed abstraction **	Î â¢ Î»W	âV	âÎ²	no	#i
	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
	global abbreviation ***	Î â¢ 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
propositions	theorems	43	lemmas	409	total	452
concepts	declared	32	defined	35	total	67

The source files are grouped in planes and components - according to the following table. - The notation for the relations or functions introduced in each file - is shown in parentheses. + 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.

component	plane	files
functional	reduction and type machine	rtm	rtm_step ( ? â¨ ? )
	unfold	lift ( â[?,?] ? )	subst ( [?â?] ? )
examples
native typing		nty
conversion	context-sensitive conversion	cpcs ( ? â¢ ? â¬* ? )
computation	strongly normalizing computation	csn ( â¬* ? )	csn_cr	csn_aaa
	context-sensitive computation	cprs (? â¢ ? â¡* ?)
	support for abstract computation properties	lsubc ( ? [?] â ? )	lsubc_ldrop	lsubc_ldrops	lsubc_lsuba
		acp	acp_cr ( â¦?,?â¦ Ïµ ã?ã )	acp_aaa
reducibility	context-sensitive reduction	lcpr ( ? â¢ â¡ ? )
		cpr ( ? â¢ ? â¡ ? )	cpr_lift	cpr_ltpr	cpr_cpr
	context-free normal forms	twhnf	tnf
	context-free reduction	ltpr ( ? â¡ ? )	ltpr_ldrop
		tpr ( ? â¡ ? )	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf
static typing	static type ass.	sty	sty_lift	sty_sty
	atomic arity ass.	lsuba ( ? Ã·â ? )
		aaa ( ? â¢ ? Ã· ? )	aaa_lift	aaa_aaa
	parameters	sh
unfold	term inverse relocation	delift ( ? â¢ ? [?,?] â¡ ? )	delift_lift
	partial unfold	ltpss ( ? [?,?] â¶* ? )	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss ( ? â¢ ? [?,?] â¶* ? )	tpss_lift	tpss_tpss	tpss_ltps
	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_gr2
substitution	parallel substitution	ltps ( ? [?,?] â¶ ? )	ltps_ldrop	ltps_tps	ltps_ltps
		tps ( ? â¢ ? [?,?] â¶ ? )	tps_lift	tps_tps
	global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop
	basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_ldrop
	basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector
		lift ( â§[?,?] ? â¡ ? )	lift_lift
grammar	local env. ref. for substitution	lsubs ( ? [?,?] â¼ ? )	lsubs_lsubs
	term hom.	thom	thom_thom
	closures	cl_shift ( ? @ ? )	cl_weight ( #[?,?] )
	internal syntax	genv
		lenv	lenv_weight ( #[?] )	lenv_length ( \|?\| )
		term	term_weight ( #[?] )	term_simple	term_vector
		item
	external syntax	aarity

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

component	plane	files
examples
native typing		nty
conversion	context-sensitive conversion	cpcs ( ? â¢ ? â¬* ? )
computation	strongly normalizing computation	csn_vector ( â¬* ? )	csn_lcpr_vector	csn_aaa
		csn ( â¬* ? )	csn_lift	csn_cpr	csn_cprs ( â¬** ? )	csn_lcpr
	context-sensitive computation	cprs (? â¢ ? â¡* ?)	cprs_lcpr	cprs_cprs	cprs_tstc	cprs_tstc_vector
	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	context-sensitive normal forms	cnf ( ? â¢ ð[?] )	cnf_lift
	context-sensitive reduction	lcpr ( ? â¢ â¡ ? )	lcpr_cpr
		cpr ( ? â¢ ? â¡ ? )	cpr_lift	cpr_ltpss	cpr_ltpr	cpr_cpr
	context-free normal forms	twhnf ( ððð[?] )	tnf ( ð[?] )	tnf_tif
	context-free reduction	ltpr ( ? â¡ ? )	ltpr_ldrop	ltpr_tps
		tpr ( ? â¡ ? )	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf ( ð[?] )	tif ( ð[?] )
static typing	static type assignment	sty	sty_lift	sty_sty
	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
unfold	term inverse relocation	delift ( ? â¢ ? [?,?] â¡ ? )	delift_lift
	partial unfold	ltpss ( ? [?,?] â¶* ? )	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss ( ? â¢ ? [?,?] â¶* ? )	tpss_lift	tpss_tpss	tpss_ltps
	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	ltps ( ? [?,?] â¶ ? )	ltps_ldrop	ltps_tps	ltps_ltps
		tps ( ? â¢ ? [?,?] â¶ ? )	tps_lift	tps_tps
	global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop
	basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_ldrop
	basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector
		lift ( â§[?,?] ? â¡ ? )	lift_lift
grammar	local env. ref. for substitution	lsubs ( ? [?,?] â¼ ? )	lsubs_lsubs
	same head term form	tshf ( ? â ? )	tshf_tshf
	same top term constructor	tstc ( ? â ? )	tstc_tstc
	closures	cl_shift ( ? @ ? )	cl_weight ( #[?,?] )
	internal syntax	genv
		lenv	lenv_weight ( #[?] )	lenv_length ( \|?\| )
		term	term_weight ( #[?] )	term_simple ( ð[?] )	term_vector
		item
	external syntax	aarity

+ +

Physical Structure of the Specification

+

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

-

Last update: 2012-01-21+01:00

+

Last update: 2012-02-24+01:00