lambdadelta version 2

+
+

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

domain

block

leader

applicator (with âÎ¸)*

reduction

âÎ¶ *

reference *

{X | Î â¢ X : W}

local typed abstraction *

Î â¢ +Î»W

âV

âÎ²

+ home +

+ news +

+ specification +

local typed declaration **

Î â¢ -Î»W

âV

âÎ²

global typed declaration ***

Î â¢ pÎ»W

+ documentation +

+ implementation +

native type annotation *

Î â¢ âW

yes

{X | Î â¢ X = V}

local abbreviation *

Î â¢ +Î´V

local âÎ´

yes

+ foreword +

+ milestones +

+ version 2 +

(background - core - applications)

local definition **

Î â¢ -Î´V

local âÎ´

+ version 2 +

+ library +

(static LDDL directory)

+ citations +

+ visibility +

+ version 1 +

(background - core)

(static HELM directory)

+ version 1 +

+ helena +

global definition ***

Î â¢ pÎ´V

global âÎ´

sort ****

Î â¢ âk

* In terms only. + +

Summary of the Specification [spacer]

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

293

characters

441375

nodes

1286916

sizes

files

102

characters

69295

nodes

245853

propositions

theorems

lemmas

888

total

979

propositions

theorems

lemmas

256

total

290

concepts

declared

defined

total

134

concepts

declared

defined

total

Stage "B"

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

Stage "A2": "Extending the Applicability Condition"

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

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

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

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

+ 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. 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. - 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. + 2012 January 27. Support for abstract 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 [spacer]

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

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

component	plane	files	+	component	plane	files		+		+
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? Â¡â[?,?] ? )	lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv	+	static typing	parameters	sh	sd		+
+		stratified native validity	snv ( â¦?,?â¦ â¢ ? Â¡[?,?] )	snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs	+	restricted ref. for local env.	lsubr ( ? â« ? )	lsubr_length lsubr_drops lsubr_lsubr		+
equivalence	decomposed extended equivalence	cpes ( â¦?,?â¦ â¢ ? â¢â¬[?,?] ? )	cpes_cpds	+		- -
- -	context-sensitive equivalence	cpcs ( â¦?,?â¦ â¢ ? â¬* ? )	cpcs_aaa cpcs_cprs cpcs_cpcs	- -	- -
conversion	context-sensitive conversion	cpc ( â¦?,?â¦ â¢ ? â¬ ? )	cpc_cpc	+	ranged equivalence for closures	freq ( â¦?,?,?â¦ â¡ â¦?,?,?â¦ )	freq_freq		+
computation	context-sensitive extended evaluation	cpxe ( â¦?,?â¦ â¢ â¡*[?,?] ðâ¦?â¦ )	+		+	context-sensitive free variables	frees ( ? â¢ ð*â¦?â¦ â¡ ? )	frees_weight frees_lreq frees_frees		+
+	s-computation	+		context-sensitive evaluation	cpre ( â¦?,?â¦ â¢ â¡* ðâ¦?â¦ )	cpre_cpre	+		+
- -	strongly normalizing "big tree" computation	fsb ( â¦?,?â¦ â¢ â¦¥[?,?] ? )	fsb_alt ( â¦?,?â¦ â¢ â¦¥â¦¥[?,?] ? )	fsb_fleq fsb_csx	+
- -	strongly normalizing extended computation	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_tstc_vector csx_aaa	+	s-transition	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_length fquq_weight		+
+		- -	csx ( â¦?,?â¦ â¢ â¬*[?,?] ? )	csx_alt ( â¦?,?â¦ â¢ â¬â¬*[?,?] ? )	csx_lift csx_lpx	- -
+		parallel computation for "big tree" normal forms	fpns ( â¦?,?,?â¦ â¢ ââ¡*[?,?] â¦?,?,?â¦ )	fpns_fpns	+	fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_length fqu_weight		+
+	relocation	generic slicing for local environments	drops_vector ( â¬*[?,?] ? â¡ ? )		"big tree" parallel computation	fpbr ( â¦?,?,?â¦ ââ¥[?,?] â¦?,?,?â¦ )	fpbr_fpbr	+		+
+		+		fpbg ( â¦?,?,?â¦ >[?,?] â¦?,?,?â¦ )	fpbg_lift fpbg_fpbg	+	drops ( â¬*[?,?] ? â¡ ? )	drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops		+
+		+	generic relocation for terms	lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lifts_vector		fpbs ( â¦?,?,?â¦ â¥[?,?] â¦?,?,?â¦ )	fpbs_alt ( â¦?,?,?â¦ â¥â¥[?,?] â¦?,?,?â¦ )	fpbs_lift fpbs_fleq fpbs_fpbs	+
+		decomposed extended computation	cpds ( â¦?,?â¦ â¢ ? â¢â¡[?,?] ? )	cpds_lift cpds_aaa cpds_cpds	+		+	lifts ( â¬*[?] ? â¡ ? )	lifts_simple lifts_weight lifts_lifts
- -	context-sensitive extended computation	lpxs ( â¦?,?â¦ â¢ â¡*[?,?] ? )	lpxs_alt ( â¦?,?â¦ â¢ â¡â¡*[?,?] ? )	lpxs_ldrop lpxs_aaa lpxs_cpxs lpxs_lpxs	+
- -	+		cpxs ( â¦?,?â¦ â¢ ? â¡*[?,?] ? )	cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_aaa cpxs_cpxs	+	ranged equivalence for local environments	lreq ( ? â¡[?] ? )	lreq_length lreq_lreq		+
+		context-sensitive computation	lprs ( â¦?,?â¦ â¢ â¡* ? )	lprs_alt ( â¦?,?â¦ â¢ â¡â¡* ? )	lprs_ldrop lprs_cprs lprs_lprs	+	generic entrywise extension of context-sensitive relations for terma	lexs ( ? â¦»*[?,?,?] ? )	lexs_length lexs_lexs
- -	- -	cprs ( â¦?,?â¦ â¢ ? â¡* ?)	cprs_lift cprs_cprs	- -	- -
- -	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	+
reduction	"big tree" parallel reduction	fpbc ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	fpbc_lift	+	grammar	append for local environments	append ( ? @@ ? )	append_length		+
- -	+		fpb ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ )	fpb_lift	+	context-sensitive equivalences for terms	ceq	ceq_ceq		+
+		context-sensitive extended normal forms	cnx ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	cnx_lift cnx_crx cnx_cix	+	same top term structure	tsts ( ? â ? )	tsts_tsts tsts_vector		+
+		context-sensitive extended reduction	lpx ( â¦?,?â¦ â¢ â¡[?,?] ? )	lpx_ldrop lpx_aaa lpx_lpx	+	closures	cl_weight ( â¯{?,?,?} )	cl_restricted_weight ( â¯{?,?} )		+
+		+	internal syntax	genv		cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpx_lift cpx_cix cpx_cpx	+		+
+		context-sensitive extended irreducible forms	cix ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	cix_append cix_lift	+		+	lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )
- -	context-sensitive extended reducible forms	crx ( â¦?,?â¦ â¢ ð[?,?]â¦?â¦ )	crx_append crx_lift	+		+		term	term_weight ( â¯{?} )	term_simple ( ðâ¦?â¦ )	term_vector ( â¶?.? )
+		context-sensitive normal forms	cnr ( â¦?,?â¦ â¢ ðâ¦?â¦ )	cnr_lift cnr_crr cnr_cir	+		+	item
+		context-sensitive reduction	lpr ( â¦?,?â¦ â¢ â¡ ? )	lpr_ldrop lpr_lpr	- -	- -
- -	- -	cpr ( â¦?,?â¦ â¢ ? â¡ ? )	cpr_lift cpr_cir	- -	+
- -	context-sensitive irreducible forms	cir ( â¦?,?â¦ â¢ ðâ¦?â¦ )	cir_append cir_lift	- -	- -
- -	context-sensitive reducible forms	crr ( â¦?,?â¦ â¢ ðâ¦?â¦ )	crr_append crr_lift	- -	+
unfold	unfold	unfold ( â¦?,?â¦ â¢ ? â§«* ? )	- -	- -	- -
- -	iterated static type assignment	lsstas ( â¦?,?â¦ â¢ ? â¢*[?,?,?] ? )	lsstas_alt ( â¦?,?â¦ â¢ ? â¢â¢*[?,?,?] ? )	lsstas_lift lsstas_aaa lsstas_lsstas	- -
static typing	local env. ref. for atomic arity assignment	lsuba ( ? â¢ ? ââ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba	- -	- -
- -	atomic arity assignment	aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_lift aaa_lifts aaa_da aaa_ssta aaa_aaa	- -	- -
- -	stratified static type assignment	ssta ( â¦?,?â¦ â¢ ? â¢[?,?] ? )	ssta_lift ssta_ssta	- -	- -
- -	local env. ref. for degree assignment	lsubd ( ? â¢ ? âªâ ? )	lsubd_da lsubd_lsubd	- -	- -
+	external syntax	aarity		degree assignment	da ( â¦?,?â¦ â¢ ? âª[?,?] ? )	da_lift da_da	+		- -
- -	parameters	sh	sd	- -	- -
substitution	restricted local env. ref.	lsubr ( ? â ? )	lsubr_lsubr	- -	- -
- -	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_alt fqus_fqus	- -	- -
- -	- -	fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_fqup	- -	- -
- -	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
relocation	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_alt ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )	fquq_fquq	- -
- -	- -	fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_fqu	- -	- -
- -	lazy equivalence for local environments	lleq ( ? â[?] ? )	lleq_fleq	- -	- -
- -	global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop	- -	- -
- -	basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_append ldrop_lpx_sn ldrop_ldrop	- -	- -
- -	basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector	- -	- -
- -	- -	lift ( â§[?,?] ? â¡ ? )	lift_lift	- -	- -
grammar	pointwise extension of a relation	lpx_sn	lpx_sn_tc lpx_sn_lpx_sn	- -	- -
- -	same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_vector	- -	- -
- -	closures	cl_shift ( ? @@ ? )	cl_weight ( â¯{?,?,?} )	- -	- -
- -	internal syntax	genv	- -	- -	- -
- -	- -	lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )
- -	- -	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. -

@@ -1222,6 +687,6 @@

Last update: Mon, 25 Nov 2013 15:44:49 +0100

- +

Last update: Fri, 01 Apr 2016 23:30:53 +0200