\lambda\delta version 2

Here is a numerical acount of the specification's contents +

+
+

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ home +	+ news +	+ specification +	+ +	+ +	+ documentation +	+ implementation +	+ +
+ foreword +	+ milestones +	+ version 2 +	(background - core - applications)	+ +	+ version 2 +	+ helena +	+ Open Symbolic Notation (OSN) +
+ citations +	+ visibility +	+ version 1 +	(background - core)	(static HELM directory)	+ version 1 +	+ library +	(static LDDL directory)

+ +

Summary of the Specification $\lambda\delta butterfly$ +

Here is a numerical account of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78].

- - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +

category

objects

sizes

files

367

characters

431873

nodes

1830977

sizes

files

221

characters

212835

nodes

1046738

propositions

theorems

128

lemmas

1302

total

1430

propositions

theorems

lemmas

693

total

742

concepts

declared

defined

total

137

concepts

declared

defined

total

Stage "B"

- In progress. + Ongoing. Context-sensitive subject equivalence for native type assignment.

Stage "A2": "Extending the Applicability Condition"

+ 2017 February 19. + Generic candidates of reducibility. +

+ 2017 January 17. + Confluence for parallel r-transition on referred entries of local environments. +

+ 2016 September 15. + Confluence for context-sensitive parallel r-transition on terms. +

+ 2016 April 16. + Grammatical component reconstructed: + grammar, relocation, s_transition, s_computation, static + (anniversary milestone). +

+ 2016 March 25. + Relocation with reference transforming maps (rtmap). +

+ 2015 October 9. + Î»Î´ version 2A2 is started. +

Stage "A1": "Extending the Applicability Condition"

+ 2015 August 27. + Î»Î´ version 2A1 appears too complex and is dismissed. +

+ 2014 October 28. + Î»Î´ version 2A1 is released. +

+ 2014 September 9. + Iterated static type assignment defined (more elegantly) + as a primitive notion. +

- 2014 June 18. + 2014 June 18. Preservation of stratified native validity for context-sensitive computation on terms.

- 2014 June 9. - "Big tree" strong normalization + 2014 June 9. + Strong qrst-normalization for simply typed terms.

- 2014 April 16. - lazy equivalence on local environments - serves as irrelevant step in "big tree" computation on closures + 2014 April 16. + Lazy equivalence on local environments + added as q-step to rst-computation on closures (anniversary milestone).

- 2014 January 20. - Parametrized slicing for local environments + 2014 January 20. + Parametrized slicing of local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now).

- 2013 August 7. + 2013 August 7. Passive support for global environments.

- 2013 July 27. - Reaxiomatized Î²-reductum as in extended Î²-reduction + 2013 July 27. + Reaxiomatized Î²-reductum as in rt-reduction.

- 2013 July 20. - Context-sensitive extended strong normalization + 2013 July 20. + Context-sensitive strong rt-normalization for simply typed terms.

- 2013 April 16. + 2013 April 16. Reaxiomatized substitution and reduction commute with respect to subclosure (anniversary milestone).

- 2013 March 16. + 2013 March 16. Mutual recursive preservation of stratified native validity - for "big tree" computation on closures. + for rst-computation on closures.

- 2012 October 16. + 2012 October 16. Confluence for context-free parallel reduction on closures.

- 2012 July 26. + 2012 July 26. Term binders polarized to control Î¶-reduction (not released).

- 2012 April 16. + 2012 April 16. Context-sensitive subject equivalence for atomic arity assignment (anniversary milestone).

- 2012 March 15. + 2012 March 15. Context-sensitive strong normalization for simply typed terms.

- 2012 January 27. - Support for abstract candidates of reducibility. + 2012 January 27. + Generic candidates of reducibility.

- 2011 September 21. + 2011 September 21. Confluence for context-sensitive parallel reduction on terms.

- 2011 September 6. + 2011 September 6. Confluence for context-free parallel reduction on terms.

- 2011 April 17. - Specification starts. + 2011 April 17. + Î»Î´ version 2 is started.

Logical Structure of the Specification

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

Logical Structure of the Specification $\lambda\delta butterfly$ +

This table reports the specification's components and their planes.

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + - - - - - - + + + - - - - - - + + + + - - - - - - + + - - - - - - + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + + - - - - - - + + - - - - - - + + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + - - - - - - + + - - - - - - + + - - - - - - + - - - - - - - - - - - - - - + - - - - - - + + - - - - - - + - - - - - - + - - - - - - + - - - - - - - - - - - - - - + + - - - - - - + - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + +

component	plane	files	- -	- -	- -
examples	terms with special features	ex_cpr_omega	- -	- -	- -
-	-	-	- -	- -	- -
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? â«Â¡[?,?] ? )	lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv	- -	- -
- -	stratified native validity	hsnv ( â¦?,?â¦ â¢ ? Â¡[?,?,?] )	hsnv_aaa	- -	- -
- -	- -	snv ( â¦?,?â¦ â¢ ? Â¡[?,?] )	snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpes snv_preserve	- -	- -
equivalence	decomposed extended equivalence	cpes ( â¦?,?â¦ â¢ ? â¢â¬[?,?,?,?] ? )	cpes_aaa cpes_cpcs cpes_cpes	- -	- -
- -	context-sensitive equivalence	cpcs ( â¦?,?â¦ â¢ ? â¬* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs	- -	- -
conversion	context-sensitive conversion	cpc ( â¦?,?â¦ â¢ ? â¬ ? )	cpc_cpc	- -	- -
computation	evaluation for context-sensitive extended reduction	cpxe ( â¦?,?â¦ â¢ â¡*[?,?] ðâ¦?â¦ )	- -	- -	- -
- -	evaluation for context-sensitive reduction	cpre ( â¦?,?â¦ â¢ â¡* ðâ¦?â¦ )	cpre_cpre	- -	- -
- -	strongly normalizing "big tree" computation	fsb ( â¦?,?â¦ â¢ â¦¥[?,?] ? )	fsb_alt ( â¦?,?â¦ â¢ â¦¥â¦¥[?,?] ? )	fsb_aaa fsb_csx	- -
- -	strongly normalizing extended computation	lcosx ( ? â¢ ~â¬*[?,?,?] ? )	lcosx_cpx	- -	- -
- -	- -	lsx ( ? â¢ â¬*[?,?,?,?] ? )	lsx_alt ( ? â¢ â¬â¬*[?,?,?,?] ? )	lsx_drop lsx_lpx lsx_lpxs llsx_csx	- -
- -	- -	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_tstc_vector csx_aaa	- -	- -
- -	- -	csx ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_alt ( â¦?,?â¦ â¢ â¬â¬*[?,?] ? )	csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs	- -
- -	"big tree" parallel computation	fpbg ( â¦?,?,?â¦ >â¡[?,?] â¦?,?,?â¦ )	fpbg_lift fpbg_fleq fpbg_fpbg	- -	- -
- -	- -	fpbc ( â¦?,?,?â¦ â»â¡[?,?] â¦?,?,?â¦ )	fpbc_fleq fpbc_fpbs	- -	- -
- -	- -	fpbu ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	fpbu_lift fpbu_lleq	fpbu_fleq	- -
- -	- -	fpbs ( â¦?,?,?â¦ â¥[?,?] â¦?,?,?â¦ )	fpbs_alt ( â¦?,?,?â¦ â¥â¥[?,?] â¦?,?,?â¦ )	fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext	+	component	plane	files
- -	decomposed extended computation	cpds ( â¦?,?â¦ â¢ ? â¢â¡[?,?,?] ? )	cpds_lift cpds_aaa cpds_cpds	- -	+	rt-computation	uncounted context-sensitive rt-transition	cpxs ( â¦?,?â¦ â¢ ? â¬*[?] ? )
- -	context-sensitive extended computation	lpxs ( â¦?,?â¦ â¢ â¡*[?,?] ? )	lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs	- -	+	rt-transition	parallel qrst-rtransition	fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )
- -	- -	cpxs ( â¦?,?â¦ â¢ ? â¡*[?,?] ? )	cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs	- -	+		t-bound context-sensitive rt-transition	lfpr ( â¦?,?â¦ â¢ â¡[?,?] ? )	lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
- -	context-sensitive computation	lprs ( â¦?,?â¦ â¢ â¡* ? )	lprs_drop lprs_cprs lprs_lprs	+		+		cpr ( â¦?,?â¦ â¢ ? â¡[?] ? )	cpr_drops
+		- -	cprs ( â¦?,?â¦ â¢ ? â¡* ?)	cprs_lift cprs_cprs	- -	+		cpm ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
- -	local env. ref. for abstract candidates of reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drop lsubc_drops lsubc_lsuba	- -	+		uncounted context-sensitive rt-transition	cnx ( â¦?,?â¦ â¢ â¬[?,?] ðâ¦?â¦ )	cnx_simple cnx_drops
+		support for abstract computation properties	acp	acp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	acp_aaa	+		lfpx ( â¦?,?â¦ â¢ â¬[?,?] ? )	lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa
reduction	"big tree" parallel reduction	fpb ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ )	fpb_lift fpb_aaa	+		+		cpx ( â¦?,?â¦ â¢ ? â¬[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfdeq
- -	normal forms for context-sensitive extended reduction	cnx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )	cnx_lift cnx_crx cnx_cix	- -	+		counted context-sensitive rt-transition	cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
- -	context-sensitive extended reduction	lpx ( â¦?,?â¦ â¢ â¡[?,?] ? )	lpx_drop lpx_frees	lpx_lleq lpx_aaa	- -	static typing	generic reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drop lsubc_drops lsubc_lsubr lsubc_lsuba
- -	- -	cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix	+		+		gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	gcp_aaa
+		irreducible forms for context-sensitive extended reduction	cix ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )	cix_lift	+		+	gcp
- -	reducible forms for context-sensitive extended reduction	crx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )	crx_lift	- -	+		atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
- -	normal forms for context-sensitive reduction	cnr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )	cnr_lift cnr_crr cnr_cir	+		+		aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
- -	context-sensitive reduction	lpr ( â¦?,?â¦ â¢ â¡ ? )	lpr_drop lpr_lpr	- -	+		degree-based equivalence on referred entries	ffdeq ( â¦?,?,?â¦ â¡[?,?] â¦?,?,?â¦ )	ffdeq_fqup ffdeq_ffdeq
- -	- -	cpr ( â¦?,?â¦ â¢ ? â¡ ? )	cpr_lift cpr_llpx_sn cpr_cir	+		+		lfdeq ( ? â¡[?,?,?] ? )	lfdeq_length lfdeq_fqup lfdeq_lfdeq
- -	irreducible forms for context-sensitive reduction	cir ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )	cir_lift	- -	+		generic extension on referred entries	lfxs ( ? â¦»*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
- -	reducible forms for context-sensitive reduction	crr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )	crr_lift	- -	+		context-sensitive free variables	lsubf ( â¦?,?â¦ â«ð* â¦?,?â¦ )	lsubf_frees
unfold	unfold	unfold ( â¦?,?â¦ â¢ ? â§«* ? )	- -	+		+		frees ( ? â¢ ð*â¦?â¦ â¡ ? )	frees_weight frees_drops frees_fqup frees_frees
- -	iterated static type assignment	lstas ( â¦?,?â¦ â¢ ? â¢*[?,?] ? )	lstas_alt ( â¦?,?â¦ â¢ ? â¢â¢*[?,?] ? )	lstas_lift lstas_aaa lstas_da lstas_lstas	+		restricted ref. for local env.	lsubr ( ? â« ? )	lsubr_length lsubr_drops lsubr_lsubr
static typing	local env. ref. for degree assignment	lsubd ( ? â¢ ? â«âª[?,?] ? )	lsubd_da lsubd_lsubd	- -	- -	s-computation	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_weight fqus_drops fqus_fqup fqus_fqus
+		degree assignment	da ( â¦?,?â¦ â¢ ? âª[?,?] ? )	da_lift da_aaa da_sta da_da	- -	+		fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_weight fqup_drops fqup_fqup
- -	static type assignment	sta ( â¦?,?â¦ â¢ ? â¢[?] ? )	sta_lift sta_lpx_sn sta_aaa sta_sta	- -	- -	s-transition	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_length fquq_weight
- -	parameters	sh	sd	+		+		fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_length fqu_weight
- -	local env. ref. for atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_aaa lsuba_lsuba	- -	+	relocation	generic slicing for local environments	drops_vector ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )
- -	atomic arity assignment	aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa	+		+		drops ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )	drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
- -	restricted local env. ref.	lsubr ( ? â« ? )	lsubr_lsubr	- -	+		generic relocation for terms	lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lifts_vector
multiple substitution	lazy equivalence	fleq ( â¦?,?,?â¦ â¡[?] â¦?,?,?â¦ )	fleq_fleq	+		+		lifts ( â¬*[?] ? â¡ ? )	lifts_simple lifts_weight lifts_tdeq lifts_lifts
- -	- -	lleq ( ? â¡[?,?] ? )	lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq	- -	+		ranged equivalence for local environments	lreq ( ? â¡[?] ? )	lreq_length lreq_lreq
- -	lazy pointwise extension of a relation	llpx_sn	llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor	- -	+		generic entrywise extension	lexs ( ? â¦»*[?,?,?] ? )	lexs_length lexs_lexs
- -	pointwise union for local environments	llor ( ? â©[?,?] ? â¡ ? )	llor_alt llor_drop	- -	- -	syntax	append for local environments	append ( ? @@ ? )	append_length
- -	context-sensitive exclusion from free variables	frees ( ? â¢ ? Ïµ ð*[?]â¦?â¦ )	frees_append frees_leq frees_lift	- -	+		degree-based equivalence for terms	deq ( ? â¡[?,?] ? )	deq_deq
- -	contxt-sensitive extended multiple substitution	cpys ( â¦?,?â¦ â¢ ? â¶*[?,?] ? )	cpys_alt ( â¦?,?â¦ â¢ ? â¶â¶*[?,?] ? )	cpys_lift cpys_cpys	+		same top term structure	tsts ( ? â ? )	tsts_tsts tsts_vector
+		iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_alt fqus_fqus	- -	+	closures	cl_weight ( â¯{?,?,?} )
- -	+		fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_fqup	+		+	cl_restricted_weight ( â¯{?,?} )
+		iterated local env. slicing	drops ( â©*[?,?] ? â¡ ? )	drops_drop drops_drops	- -	+	global environments	genv
- -	generic term relocation	lifts_vector ( â§*[?] ? â¡ ? )	lifts_lift_vector	+		+	local environments	lenv_length ( \|?\| )
+		+		lifts ( â§*[?] ? â¡ ? )	lifts_lift lifts_lifts	- -	+	lenv_weight ( â¯{?} )
+		support for generic relocation	gr2 ( @â¦?,?â¦ â¡ ? )	gr2_plus ( ? + ? )	gr2_minus ( ? â ? â¡ ? )	gr2_gr2
substitution	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_alt ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )	+		+	lenv
- -	+		fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	- -	- -	+	terms	term_vector ( â¶?.? )
+		global env. slicing	gget ( â©[?] ? â¡ ? )	gget_gget	+		+	term_simple ( ðâ¦?â¦ )
+		contxt-sensitive extended ordinary substitution	cpy ( â¦?,?â¦ â¢ ? â¶[?,?] ? )	cpy_lift cpy_nlift cpy_cpy	+		+	term_weight ( â¯{?} )
+		local env. ref. for extended substitution	lsuby ( ? â[?,?] ? )	lsuby_lsuby	+		+	term
- -	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_leq drop_drop	+		+	items	item_sd
+		basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector	+		+	item_sh
- -	+		lift ( â§[?,?] ? â¡ ? )	lift_neq lift_lift	+		+	item
grammar	equivalence for local environments	leq ( ? â©¬[?,?] ? )	leq_leq	+		- -
- -	same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_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	- -	- -	+	atomic arities	aarity

- -

Physical Structure of the Specification

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

+ $\lambda\delta rainbow rule$

@@ -1316,6 +837,6 @@

Last update: Tue, 05 Aug 2014 23:07:40 +0200

- +

Last update: Sun, 19 Feb 2017 19:57:19 +0100