\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].

@@ -58,1245 +144,675 @@ - + - + - + - + - + - + - + - + - +

sizes	files	359	221	characters	429770	212835	nodes	1856085	1046738
propositions	theorems	127	49	lemmas	1273	693	total	1400	742
concepts	declared	54	29	defined	83	62	total	137	91

- -

Stage "B"

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

Stage "A": "Weakening the Applicability Condition"

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

@@ -1321,6 +837,6 @@

Last update: Fri, 12 Sep 2014 20:28:32 +0200

- +

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