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.

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

category

objects

sizes

files

262

characters

527314

nodes

1440935

sizes

files

238

characters

249398

nodes

1213337

propositions

theorems

lemmas

1170

total

1265

propositions

theorems

lemmas

838

total

901

concepts

declared

defined

total

136

concepts

declared

defined

total

100

Stage "B"

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

Stage "A2": "Extending the Applicability Condition"

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

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

- In progress. - Closure of extended context-sensitive computation - for native validity. + 2016 March 25. + Relocation with reference transforming maps (rtmap).

- In progress. - Extended context-sensitive strong normalization + 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. +

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

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

+ 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 ( ? â¢ â¦?,?â¦ â¥[g] â¦?,?â¦ )	yprs_yprs	ygt ( ? â¢ â¦?,?â¦ >[g] â¦?,?â¦ )	ygt_ygt	- -	rt-computation	uncounted context-sensitive rt-computation	csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ðâ¦?â¦ )	csx_cnx_vector csx_csx_vector
- -	"big tree" parallel reduction	ypr ( ? â¢ â¦?,?â¦ â½[g] â¦?,?â¦ )	ysc ( ? â¢ â¦?,?â¦ â»[g] â¦?,?â¦ )	+		- -	+		csx ( â¦?,?â¦ â¢ â¬*[?,?] ðâ¦?â¦ )	csx_simple csx_simple_theq csx_drops csx_lsubr csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_csx
- -	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? Â¡â[?] ? )	lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv	+		- -	+		lfpxs ( â¦?,?â¦ â¢ â¬*[?,?] ? )	lfpxs_length lfpxs_fqup lfpxs_cpxs
- -	stratified native validity	snv ( â¦?,?â¦ â¢ ? Â¡[?] )	snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs	- -	+		+		cpxs ( â¦?,?â¦ â¢ ? â¬*[?] ? )	cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_lsubr cpxs_lfpx cpxs_cnx cpxs_cpxs
equivalence	focalized equivalence	lfpcs ( â¦?â¦ â¬* â¦?â¦ )	lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs	- -	- -	- -	rt-transition	parallel rst-transition	fpbq ( â¦?,?,?â¦ â½[?] â¦?,?,?â¦ )	fpbq_aaa
- -	- -	fpcs ( â¦?,?â¦ â¬* â¦?,?â¦ )	fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs	- -	+		+		fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )	fpb_lfdeq
- -	local env. ref. for stratified static type assignment	lsubss ( ? â¢â[?] ? )	lsubss_ldrop lsubss_ssta lsubss_cpcs	- -	- -	+		t-bound context-sensitive rt-transition	lfpr ( â¦?,?â¦ â¢ â¡[?,?] ? )	lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
+		context-sensitive equivalence	cpcs ( ? â¢ ? â¬* ? )	cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs	- -	- -	+		cpr ( â¦?,?â¦ â¢ ? â¡[?] ? )	cpr_drops
conversion	focalized conversion	lfpc ( â¦?â¦ â¬ â¦?â¦ )	lfpc_lfpc	+		- -	+		cpm ( â¦?,?â¦ â¢ ? â¡[?,?] ? )	cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
- -	- -	fpc ( â¦?,?â¦ â¬ â¦?,?â¦ )	fpc_fpc	- -	- -	+		uncounted context-sensitive rt-transition	cnx ( â¦?,?â¦ â¢ â¬[?,?] ðâ¦?â¦ )	cnx_simple cnx_drops cnx_cnx
+		context-sensitive conversion	cpc ( ? â¢ ? â¬ ? )	cpc_cpc	- -	- -	+		lfpx ( â¦?,?â¦ â¢ â¬[?,?] ? )	lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx
computation	focalized computation	lfprs ( â¦?â¦ â¡* â¦?â¦ )	lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs	+		- -	+		cpx ( â¦?,?â¦ â¢ ? â¬[?] ? )	cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
- -	- -	fprs ( â¦?,?â¦ â¡* â¦?,?â¦ )	fprs_aaa fprs_fprs	- -	- -	+		counted context-sensitive rt-transition	cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? )	cpg_simple cpg_drops cpg_lsubr
- -	decomposed extended computation	dxprs ( â¦?,?â¦ â¢ ? â¢â¡[?] ? )	dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs	- -	- -	+	iterated static typing	iterated extension on referred entries	tc_lfxs ( ? â¦»**[?,?] ? )
- -	weakly normalizing computation	cpe ( ? â¢ â¡* ðâ¦?â¦ )	cpe_cpe	- -	- -	- -	static typing	generic reducibility	lsubc ( ? â¢ ? â«[?] ? )	lsubc_drops lsubc_lsubr lsubc_lsuba
+		strongly normalizing computation	csn_vector ( ? â¢ â¬* ? )	csn_cpr_vector csn_tstc_vector csn_aaa	- -	- -	+		gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )	gcp_aaa
+		+		csn ( ? â¢ â¬* ? )	csn_alt ( ? â¢ â¬â¬* ? )	csn_lift csn_cpr csn_lfpr	- -	+	gcp
- -	context-sensitive computation	cprs (? â¢ ? â¡* ?)	cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector	- -	- -	+		atomic arity assignment	lsuba ( ? â¢ ? â«â ? )	lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
+		context-free computation	ltprs ( ? â¡* ? )	ltprs_alt ( ? â¡â¡* ? )	ltprs_ldrop ltprs_ltprs	- -	+		aaa ( â¦?,?â¦ â¢ ? â ? )	aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
- -	- -	tprs ( ? â¡* ?)	tprs_lift tprs_tprs	- -	- -	+		degree-based equivalence on referred entries	ffdeq ( â¦?,?,?â¦ â¡[?,?] â¦?,?,?â¦ )	ffdeq_fqup ffdeq_ffdeq
+		local env. ref. for abstract candidates of reducibility	lsubc ( ? â[?] ? )	lsubc_ldrop lsubc_ldrops lsubc_lsuba	- -	- -	+		lfdeq ( ? â¡[?,?,?] ? )	lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
- -	support for abstract computation properties	acp	acp_cr ( â¦?,?â¦ Ïµ[?] ã?ã )	acp_aaa	- -	+		generic extension on referred entries	lfxs ( ? â¦»*[?,?] ? )	lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
reducibility	context-sensitive focalized reduction	cfpr ( ? â¢ â¦?,?â¦ â¡ â¦?,?â¦ )	cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr	- -	- -	+		context-sensitive free variables	lsubf ( â¦?,?â¦ â«ð* â¦?,?â¦ )	lsubf_frees
- -	context-free focalized reduction	lfpr ( â¦?â¦ â¡ â¦?â¦ )	lfpr_alt ( â¦?â¦ â¡â¡ â¦?â¦ )	lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr	+		+		frees ( ? â¢ ð*â¦?â¦ â¡ ? )	frees_drops frees_fqup frees_frees
- -	- -	fpr ( â¦?,?â¦ â¡ â¦?,?â¦ )	fpr_cpr fpr_fpr	- -	- -	+		restricted ref. for local env.	lsubr ( ? â« ? )	lsubr_length lsubr_drops lsubr_lsubr
- -	context-sensitive normal forms	cnf ( ? â¢ ðâ¦?â¦ )	cnf_lift cnf_cif	- -	- -	- -	s-computation	iterated structural successor for closures	fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )	fqus_weight fqus_drops fqus_fqup fqus_fqus
- -	context-sensitive reduction	cpr ( ? â¢ ? â¡ ? )	cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr	+		- -	+		fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )	fqup_weight fqup_drops fqup_fqup
- -	context-sensitive reducible forms	crf ( ? â¢ ðâ¦?â¦ )	crf_append	cif ( ? â¢ ðâ¦?â¦ )	cif_append	- -	s-transition	structural successor for closures	fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )	fquq_length fquq_weight
- -	context-free normal forms	thnf ( ððâ¦?â¦ )	- -	+		- -	+		fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )	fqu_length fqu_weight
- -	context-free reduction	ltpr ( ? â¡ ? )	ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr	- -	- -	+	relocation	generic slicing for local environments	drops_vector ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )
+		- -	tpr ( ? â¡ ? )	tpr_lift tpr_delift tpr_tpr	- -	- -	+		drops ( â¬[?,?] ? â¡ ? ) ( â¬[?] ? â¡ ? )	drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
restricted computation	restricted parallel computation	lpqs ( ? â¢ â¤* ? )	lpqs_ldrop lpqs_cpqs lpqs_lpqs	- -	- -	+		generic relocation for terms	lifts_vector ( â¬*[?] ? â¡ ? )	lifts_lifts_vector
- -	- -	cpqs ( ? â¢ ? â¤* ? )	cpqs_lift	+		- -	+		lifts ( â¬*[?] ? â¡ ? )	lifts_simple lifts_weight lifts_tdeq lifts_lifts
unwind	iterated stratified static type assignment	sstas ( â¦?,?â¦ â¢ ? â¢*[?] ? )	sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_sstas	- -	- -	+		ranged equivalence for local environments	lreq ( ? â¡[?] ? )	lreq_length lreq_lreq
static typing	stratified static type assignment	ssta ( â¦?,?â¦ â¢ ? â¢[?,?] ? )	ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta	- -	- -	+		generic entrywise extension	lexs ( ? â¦»*[?,?,?] ? )	lexs_length lexs_lexs
- -	local env. ref. for atomic arity assignment	lsuba ( ? ââ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba	- -	- -	- -	syntax	append for local environments	append ( ? @@ ? )	append_length
- -	atomic arity assignment	aaa ( ? â¢ ? â ? )	aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa	- -	- -	+		head equivalence for terms	theq ( ? â©³[?,?] ? )	theq_simple theq_tdeq theq_theq theq_simple_vector
- -	parameters	sh	sd	- -	- -	- -
unfold	basic local env. thinning	thin ( ? â¼*[?,?] â¡ ? )	thin_ldrop thin_delift	- -	- -	+		degree-based equivalence for terms	deq ( ? â¡[?,?] ? )	deq_deq
+		inverse basic term relocation	delift ( ? â¢ ? â¼*[?,?] â¡ ? )	delift_alt ( ? â¢ ? â¼â¼*[?,?] â¡ ? )	delift_lift delift_tpss delift_ltpss delift_delift	- -	+	closures	cl_weight ( â¯{?,?,?} )
- -	revised parallel substitution	lpss ( ? â¢ â¶* ? )	lpss_ldrop lpss_cpss lpss_lpss	+		+		+	cl_restricted_weight ( â¯{?,?} )
+		- -	cpss ( ? â¢ ? â¶* ? )	cpss_lift	- -	- -	+	global environments	genv
- -	partial unfold	ltpss_sn ( ? â¢ â¶*[?,?] ? )	ltpss_sn_alt ( ? â¢ â¶â¶*[?,?] ? )	ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn	+		+	local environments	lenv_length ( \|?\| )
- -	+		ltpss_dx ( ? â¶*[?,?] ? )	ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx	+		- -	+	lenv_weight ( â¯{?} )
+		+		tpss ( ? â¢ ? â¶*[?,?] ? )	tpss_alt ( ? â¢ ? â¶â¶*[?,?] ? )	tpss_lift	tpss_tpss	+	lenv
- -	iterated structural successor for closures	fsupp ( â¦?,?â¦ â+ â¦?,?â¦ )	fsupp_fsupp	+		- -	+	terms	term_vector ( â¶?.? )
- -	generic local env. slicing	ldrops ( â©*[?] ? â¡ ? )	ldrops_ldrop ldrops_ldrops	+		+		+	term_simple ( ðâ¦?â¦ )
+		generic term relocation	lifts_vector ( â§*[?] ? â¡ ? )	lifts_lift_vector	+		- -	+	term_weight ( â¯{?} )
- -	- -	lifts ( â§*[?] ? â¡ ? )	lifts_lift lifts_lifts	- -	- -	+
+		support for generic relocation	gr2 ( @â¦?,?â¦ â¡ ? )	gr2_plus ( ? + ? )	gr2_minus ( ? â ? â¡ ? )	gr2_gr2	+	term
substitution	parallel substitution	tps ( ? â¢ ? â¶[?,?] ? )	tps_lift tps_tps	- -	+		+	items	item_sd
- -	structural successor for closures	fsup ( â¦?,?â¦ â â¦?,?â¦ )	- -	+		+		+	item_sh
- -	global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop	+		+		+	item
- -	basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_append ldrop_lpx ldrop_lpx_sn ldrop_lbotr ldrop_ldrop	- -	+		- -
- -	local env. ref. for substitution	lsubr ( ? â[?,?] ? )	(lsubr_lsubr)	lsubr_lbotr ( â[?,?] ? )	- -	- -
- -	basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector	- -	- -	- -
- -	- -	lift ( â§[?,?] ? â¡ ? )	lift_lift	- -	- -	- -
grammar	same head term form	tshf ( ? â ? )	(tshf_tshf)	- -	- -	- -
- -	same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_vector	- -	- -	- -
- -	closures	cl_shift ( ? @@ ? )	cl_weight ( â¯{?,?} )	- -	- -	- -
- -	internal syntax	genv	- -	- -	- -	- -
- -	- -	lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )	lenv_px lenv_px_sn lenv_px_bi
- -	- -	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$

@@ -1412,6 +888,6 @@

Last update: Sun, 07 Apr 2013 23:37:37 +0200

- +

Last update: Sat, 01 Apr 2017 16:50:39 +0200