lambdadelta version 2

+
+

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

domain

block

leader

applicator (with âÎ¸)*

reduction

âÎ¶ *

reference *

{X | Î â¢ X : W}

local typed abstraction *

Î â¢ +Î»W

âV

âÎ²

-
+

+ home

local typed declaration **

Î â¢ -Î»W

âV

âÎ²

+ news +

+ specification +

global typed declaration ***

Î â¢ pÎ»W

native type annotation *

Î â¢ âW

yes

{X | Î â¢ X = V}

local abbreviation *

Î â¢ +Î´V

local âÎ´

yes

+ documentation +

+ implementation +

local definition **

Î â¢ -Î´V

local âÎ´

+ foreword +

+ milestones +

+ version 2 +

(background - core - applications)

global definition ***

Î â¢ pÎ´V

global âÎ´

+ version 2 +

+ helena +

+ Open Symbolic Notation (OSN) +

sort ****

Î â¢ âk

+ citations +

+ visibility +

+ version 1 +

(background - core)

(static HELM directory)

+ version 1 +

+ library +

(static LDDL directory)

* In terms only. + +

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

247

characters

366699

nodes

1091471

sizes

files

265

characters

273408

nodes

1338125

propositions

theorems

lemmas

748

total

824

propositions

theorems

lemmas

930

total

1009

concepts

declared

defined

total

118

concepts

declared

defined

total

114

Stage "B"

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

Stage "A2": "Extending the Applicability Condition"

+ 2017 October 17. + Exclusion binder in local environments. + Syntactic component updated: + syntax, relocation, s_transition, s_computation, static, i_static. +

+ 2017 April 16. + Strong rt-normalization + for simply typed terms + (anniversary milestone). +

+ 2017 March 16. + First behavioral component reconstructed: + rt_transition. +

+ 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. +

- In progress. - Closure of context-sensitive extended computation - for native validity. + 2016 April 16. + Syntactic component reconstructed: + syntax, 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. + Preservation of stratified native validity + for context-sensitive computation on terms. +

+ 2014 June 9. + Strong qrst-normalization + for simply typed terms.

- 2013 August 7. + 2014 April 16. + Lazy equivalence on local environments + added as q-step to rst-computation on closures + (anniversary milestone). +

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

+ 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. - Reaxiomatized substitution and reduction + 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 hyper 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. - Term binders polarized to control Î¶-reduction. + 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. - 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). +

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

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

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

component	plane	files	- -	- -	+	component	plane	files
dynamic typing	"big tree" parallel computation	yprs ( ? â¢ â¦?,?,?â¦ â¥[?,?] â¦?,?,?â¦ )	yprs_yprs	ygt ( â¦?,?,?â¦ >[?,?] â¦?,?,?â¦ )	ygt_ygt	rt-conversion	context-sensitive r-conversion	cpc ( â¦?,?â¦ â¢ ? â¬[?] ? )	cpc_cpc
- -	"big tree" parallel reduction	ypr ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ )	ysc ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	- -	- -	rt-computation	uncounted context-sensitive rt-computation	lfpxs ( â¦?,?â¦ â¢ â¬*[?,?] ? )	lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs
+		local env. ref. for stratified native validity	lsubsv ( ? â¢ ? Â¡â[?,?] ? )	lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv	- -	+		cpxs ( â¦?,?â¦ â¢ ? â¬*[?] ? )	cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_lsubr cpxs_aaa cpxs_lfpx cpxs_cnx cpxs_cpxs
- -	stratified native validity	snv ( â¦?,?â¦ â¢ ? Â¡[?,?] )	snv_lift snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs	- -	- -	rt-transition	uncounted rst-transition	fpbq ( â¦?,?,?â¦ â½[?] â¦?,?,?â¦ )	fpbq_aaa
equivalence	context-sensitive equivalence	cpcs ( â¦?,?â¦ â¢ ? â¬* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs	+		+		fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	fpb_lfdeq
conversion	context-sensitive conversion	cpc ( â¦?,?â¦ â¢ ? â¬ ? )	cpc_cpc	- -	+		t-bound context-sensitive rt-transition	lfpr ( â¦?,?â¦ â¢ â¡[?,?] ? )	lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
computation	context-sensitive extended evaluation	cpxe ( â¦?,?â¦ â¢ â¡*[?,?] ðâ¦?â¦ )	+		+		+	cpr_ext ( â¦?,?â¦ â¢ ? â¡[?] ? )
+		context-sensitive evaluation	cpre ( â¦?,?â¦ â¢ â¡* ðâ¦?â¦ )	cpre_cpre	- -	+		cpr ( â¦?,?â¦ â¢ ? â¡[?] ? )	cpr_drops
+		strongly normalizing computation	csn_vector ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csn_tstc_vector csn_aaa	- -	+		cpm ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
+		+	uncounted context-sensitive rt-transition	cnx ( â¦?,?â¦ â¢ â¬[?,?] ðâ¦?â¦ )	cnx_simple cnx_drops cnx_cnx
	csn ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csn_alt ( â¦?,?â¦ â¢ â¬â¬*[?,?] ? )	csn_lift csn_lpx	+		lfpx ( â¦?,?â¦ â¢ â¬[?,?] ? )	lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx
+		decomposed extended computation	dxprs ( â¦?,?â¦ â¢ ? â¢â¡[?,?] ? )	dxprs_lift dxprs_aaa dxprs_dxprs	+		+	cpx_ext ( â¦?,?â¦ â¢ ? â¬[?] ? )
+		context-sensitive extended computation	lpxs ( â¦?,?â¦ â¢ â¡*[?,?] ? )	lpxs_alt ( â¦?,?â¦ â¢ â¡â¡*[?,?] ? )	lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs	+		cpx ( â¦?,?â¦ â¢ ? â¬[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
- -	- -	cpxs ( â¦?,?â¦ â¢ ? â¡*[?,?] ? )	cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs	- -	+		counted context-sensitive rt-transition	cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
- -	context-sensitive computation	lprs ( â¦?,?â¦ â¢ â¡* ? )	lprs_alt ( â¦?,?â¦ â¢ â¡â¡* ? )	lprs_ldrop lprs_cprs lprs_lprs	- -	iterated static typing	iterated extension on referred entries	tc_lfxs ( ? â¦»**[?,?] ? )	tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs
- -	- -	cprs ( â¦?,?â¦ â¢ ? â¡* ?)	cprs_lift cprs_cprs	+	static typing	generic reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drops lsubc_lsubr lsubc_lsuba
	+		gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	gcp_aaa
+		local env. ref. for abstract candidates of reducibility	lsubc ( ? â¢ ? â[?] ? )	lsubc_ldrop lsubc_ldrops lsubc_lsuba	+		+	gcp
- -	support for abstract computation properties	acp	acp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	acp_aaa	+		atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
reduction	context-sensitive extended normal forms	cnx ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	cnx_lift cnx_crx cnx_cix	+		+		aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
- -	context-sensitive extended reduction	lpx ( â¦?,?â¦ â¢ â¡[?,?] ? )	lpx_ldrop lpx_aaa	- -	+		degree-based equivalence on referred entries	ffdeq ( â¦?,?,?â¦ â¡[?,?] â¦?,?,?â¦ )	ffdeq_fqup ffdeq_ffdeq
+		- -	cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpx_lift cpx_cix	- -	+		lfdeq ( ? â¡[?,?,?] ? )	lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
- -	context-sensitive extended irreducible forms	cix ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	cix_append cix_lift	- -	+		generic extension on referred entries	lfxs ( ? â¦»*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
- -	context-sensitive extended reducible forms	crx ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	crx_append crx_lift	- -	+		context-sensitive free variables	lsubf ( â¦?,?â¦ â«ð* â¦?,?â¦ )	lsubf_lsubr lsubf_frees lsubf_lsubf
- -	context-sensitive normal forms	cnr ( â¦?,?â¦ â¢ ðâ¦?â¦ )	cnr_lift cnr_crr cnr_cir	+		+		frees ( ? â¢ ð*â¦?â¦ â¡ ? )	frees_drops frees_fqup frees_frees
- -	context-sensitive reduction	lpr ( â¦?,?â¦ â¢ â¡ ? )	lpr_ldrop lpr_lpr	- -	+		restricted ref. for local env.	lsubr ( ? â« ? )	lsubr_length lsubr_drops lsubr_lsubr
- -	- -	cpr ( â¦?,?â¦ â¢ ? â¡ ? )	cpr_lift cpr_cir	- -	- -	s-computation	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqus_weight fqus_drops fqus_fqup fqus_fqus
- -	context-sensitive irreducible forms	cir ( â¦?,?â¦ â¢ ðâ¦?â¦ )	cir_append cir_lift	+		+		fqup ( â¦?,?,?â¦ â+[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_weight fqup_drops fqup_fqup
- -	context-sensitive reducible forms	crr ( â¦?,?â¦ â¢ ðâ¦?â¦ )	crr_append crr_lift	- -	- -	s-transition	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸®[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_length fquq_weight
unfold	unfold	unfold ( â¦?,?â¦ â¢ ? â§«* ? )	+		- -	+		fqu ( â¦?,?,?â¦ â[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_length fqu_weight
- -	iterated stratified static type assignment	sstas ( â¦?,?â¦ â¢ ? â¢*[?] ? )	sstas_lift sstas_aaa sstas_sstas	- -	+	relocation	generic slicing for local environments	drops_vector ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )
static typing	stratified static type assignment	ssta ( â¦?,?â¦ â¢ ? â¢[?,?] â¦?,?â¦ )	ssta_lift ssta_aaa ssta_ssta	+		+		drops ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )	drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops
- -	local env. ref. for atomic arity assignment	lsuba ( ? â¢ ? ââ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba	- -	+		generic relocation	lifts_bind ( â¬*[?] ? â¡ ? )	lifts_weight_bind lifts_lifts_bind
+		atomic arity assignment	aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_lift aaa_lifts aaa_aaa	- -	+		lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lifts_vector
- -	parameters	sh	sd	+		+		lifts ( â¬*[?] ? â¡ ? )	lifts_simple lifts_weight lifts_tdeq lifts_lifts
substitution	restricted local env. ref.	lsubr ( ? â ? )	lsubr_lsubr	- -	+		ranged equivalence for local environments	lreq ( ? â¡[?] ? )	lreq_length lreq_lreq
+		iterated structural successor for closures	fsups ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fsups_fsups	- -	+	generic entrywise extension	lexs ( ? â¦»*[?,?,?] ? )	lexs_length lexs_lexs
syntax	append for local environments	append ( ? @@ ? )	append_length
	head equivalence for terms	theq ( ? â©³[?,?] ? )	theq_simple theq_tdeq theq_theq theq_simple_vector
+		+	degree-based equivalence	tdeq_ext ( ? â¡[?,?] ? ) ( ? â¢ ? â¡[?,?] ? )		fsupp ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fsupp_fsupp	+
	+		tdeq ( ? â¡[?,?] ? )	tdeq_tdeq
- -	generic local env. slicing	ldrops ( â©*[?] ? â¡ ? )	ldrops_ldrop ldrops_ldrops	+		+	closures	cl_weight ( â¯{?,?,?} )
+		generic term relocation	lifts_vector ( â§*[?] ? â¡ ? )	lifts_lift_vector	+		+	cl_restricted_weight ( â¯{?,?} )
- -	- -	lifts ( â§*[?] ? â¡ ? )	lifts_lift lifts_lifts	+		+	global environments	genv
+		support for generic relocation	gr2 ( @â¦?,?â¦ â¡ ? )	gr2_plus ( ? + ? )	gr2_minus ( ? â ? â¡ ? )	gr2_gr2
relocation	structural successor for closures	fsup ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fsupq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fsupq_alt ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )	+	local environments	lenv_ext2
+		global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop	+		+	lenv_length ( \|?\| )
+		basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_append ldrop_lpx_sn ldrop_ldrop	+		+	lenv_weight ( â¯{?} )
+		basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector	+		+	lenv
- -	+		lift ( â§[?,?] ? â¡ ? )	lift_lift	+	binders for local environments	ext2	ext2_ext2
	+		bind	bind_weight
grammar	pointwise extension of a relation	lpx_sn	lpx_sn_tc lpx_sn_lpx_sn	+		+	terms	term_vector ( â¶?.? )
+		same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_vector	+		+	term_simple ( ðâ¦?â¦ )
+		closures	cl_shift ( ? @@ ? )	cl_weight ( â¯{?,?,?} )	+		+	term_weight ( â¯{?} )
+		internal syntax	genv	+		- -	+	term
+		+	items	item_sd		lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )
+		+		term	term_weight ( â¯{?} )	term_simple ( ðâ¦?â¦ )	term_vector
+	item_sh		- -	item	+
	+		+	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$

@@ -1076,6 +964,6 @@

Last update: Wed, 07 Aug 2013 23:40:05 +0200

- +

Last update: Wed, 25 Oct 2017 21:44:35 +0200