\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,354 +144,280 @@ - + - + - + - + - + - + - + - + - +

sizes	files	358	265	characters	429611	273408	nodes	1856046	1338125
propositions	theorems	126	79	lemmas	1273	930	total	1399	1009
concepts	declared	54	33	defined	83	81	total	137	114

- -

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

+ 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 September 9. - Interated static type assignment defined (more elegantly) + 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 on 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.

- - - - - - - - + + + + - - - + + + + - - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - - - - + + - - - - - + + + - - - - - - - - - - - + @@ -472,14 +456,8 @@ - - - - + + - - - - + + - - - - - - - - - - - - - - - - - - - - - + + + - - - - + + - - - - + @@ -576,611 +506,363 @@ - - - - + + - - - - - + + + - - - - - - + + + + - - - - - - + + + + - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - + + + - - - - - - + + + + - - - - - + + - - - - - - + + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + - - - - - - + + - - - - - - + + - - - - - - - - - + - - - - - - - - - - - + + - - - - - - + + - - - - - - + - - - - - - + - - - - - - + - - - - - - + + + - - - - - - + + - - - - - - + + - - - - - - - - - - - - - + @@ -1189,12 +871,10 @@ - - - - + @@ -1203,12 +883,10 @@ - - - - + @@ -1217,14 +895,8 @@ - - - - + + @@ -1236,22 +908,10 @@ - - - - - - - - + - - - - - - @@ -1275,14 +929,8 @@ - + - - @@ -1290,13 +938,8 @@

component

plane

files

-
-

examples

terms with special features

ex_cpr_omega

-
-

rt-conversion

context-sensitive r-conversion

cpc ( â¦?,?â¦ â¢ ? â¬[?] ? )

cpc_cpc

-
-

rt-computation

uncounted context-sensitive rt-computation

lfpxs ( â¦?,?â¦ â¢ â¬*[?,?] ? )

lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs

dynamic typing

local env. ref. for stratified native validity

lsubsv ( ? â¢ ? â«Â¡[?,?] ? )

lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds 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

shnv ( â¦?,?â¦ â¢ ? Â¡[?,?,?] )

-
-

snv ( â¦?,?â¦ â¢ ? Â¡[?,?] )

snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve

-
-

equivalence

decomposed extended equivalence

scpes ( â¦?,?â¦ â¢ ? â¢*â¬*[?,?,?,?] ? )

scpes_aaa scpes_cpcs scpes_scpes

-
-

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

-
-

rt-transition

uncounted rst-transition

fpbq ( â¦?,?,?â¦ â½[?] â¦?,?,?â¦ )

fpbq_aaa

@@ -414,28 +426,16 @@

lsx ( ? â¢ â¬*[?,?,?,?] ? )

lsx_alt ( ? â¢ â¬â¬*[?,?,?,?] ? )

lsx_drop lsx_lpx lsx_lpxs llsx_csx

-
-

fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )

fpb_lfdeq

-
-

csx_vector ( â¦?,?â¦ â¢ â¬*[?,?] ? )

csx_tsts_vector csx_aaa

-
-

t-bound context-sensitive rt-transition

lfpr ( â¦?,?â¦ â¢ â¡[?,?] ? )

lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr

@@ -444,23 +444,7 @@

csx ( â¦?,?â¦ â¢ â¬*[?,?] ? )

csx_alt ( â¦?,?â¦ â¢ â¬â¬*[?,?] ? )

csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs

-
-

"big tree" parallel computation

fpbg ( â¦?,?,?â¦ >â¡[?,?] â¦?,?,?â¦ )

fpbg_lift fpbg_fleq fpbg_fpbg

-
-

cpr_ext ( â¦?,?â¦ â¢ ? â¡[?] ? )

fpbc ( â¦?,?,?â¦ â»â¡[?,?] â¦?,?,?â¦ )

fpbc_fleq fpbc_fpbs

-
-

cpr ( â¦?,?â¦ â¢ ? â¡[?] ? )

cpr_drops

@@ -488,56 +466,16 @@

fpbu ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ )

fpbu_lift fpbu_lleq fpbu_fleq

-
-

cpm ( â¦?,?â¦ â¢ ? â¡[?,?] ? )

cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx

-
-

fpbs ( â¦?,?,?â¦ â¥[?,?] â¦?,?,?â¦ )

fpbs_alt ( â¦?,?,?â¦ â¥â¥[?,?] â¦?,?,?â¦ )

fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext

-
-

decomposed extended computation

scpds ( â¦?,?â¦ â¢ ? â¢*â¡*[?,?,?] ? )

scpds_lift scpds_aaa scpds_scpds

-
-

context-sensitive extended computation

lpxs ( â¦?,?â¦ â¢ â¡*[?,?] ? )

lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs

-
-

uncounted context-sensitive rt-transition

cnx ( â¦?,?â¦ â¢ â¬[?,?] ðâ¦?â¦ )

cnx_simple cnx_drops cnx_cnx

@@ -546,25 +484,17 @@

cpxs ( â¦?,?â¦ â¢ ? â¡*[?,?] ? )

cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs

-
-

lfpx ( â¦?,?â¦ â¢ â¬[?,?] ? )

lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx

context-sensitive computation

lprs ( â¦?,?â¦ â¢ â¡* ? )

lprs_drop lprs_cprs lprs_lprs

cpx_ext ( â¦?,?â¦ â¢ ? â¬[?] ? )

cprs ( â¦?,?â¦ â¢ ? â¡* ?)

cprs_lift cprs_cprs

-
-

cpx ( â¦?,?â¦ â¢ ? â¬[?] ? )

cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs

local env. ref. for generic reducibility

lsubc ( ? â¢ ? â«[?] ? )

lsubc_drop lsubc_drops lsubc_lsuba

-
-

counted context-sensitive rt-transition

cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? )

cpg_simple cpg_drops cpg_lsubr

-
-

support for generic computation properties

gcp

gcp_cr ( â¦?,?,?â¦ Ïµ[?] ã?ã )

gcp_aaa

-
-

iterated static typing

iterated extension on referred entries

tc_lfxs ( ? â¦»**[?,?] ? )

tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs

reduction

"big tree" parallel reduction

fpb ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ )

fpb_lift fpb_aaa

-
-

static typing

generic reducibility

lsubc ( ? â¢ ? â«[?] ? )

lsubc_drops lsubc_lsubr lsubc_lsuba

-
-

normal forms for context-sensitive extended reduction

cnx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ )

cnx_lift cnx_crx cnx_cix

-
-

context-sensitive extended reduction

lpx ( â¦?,?â¦ â¢ â¡[?,?] ? )

lpx_drop lpx_frees lpx_lleq lpx_aaa

-
-

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_drops lfdeq_fqup lfdeq_fqus 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_lsubr lsubf_frees lsubf_lsubf

unfold

unfold ( â¦?,?â¦ â¢ ? â§«* ? )

-
-

frees ( ? â¢ ð*â¦?â¦ â¡ ? )

frees_drops frees_fqup frees_frees

iterated static type assignment

lstas ( â¦?,?â¦ â¢ ? â¢*[?,?] ? )

lstas_lift lstas_llpx_sn.ma 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_da

-
-

fqup ( â¦?,?,?â¦ â+[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )

fqup_weight fqup_drops fqup_fqup

-
-

parameters

-
-

s-transition

structural successor for closures

fquq ( â¦?,?,?â¦ ââ¸®[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )

fquq_length fquq_weight

-
-

local env. ref. for atomic arity assignment

lsuba ( ? â¢ ? â«â ? )

lsuba_aaa lsuba_lsuba

fqu ( â¦?,?,?â¦ â[?] â¦?,?,?â¦ ) ( â¦?,?,?â¦ â â¦?,?,?â¦ )

fqu_length fqu_weight

-
-

atomic arity assignment

aaa ( â¦?,?â¦ â¢ ? â ? )

aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa

-
-

relocation

generic slicing for local environments

drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? )

-
-

restricted local env. ref.

lsubr ( ? â« ? )

lsubr_lsubr

drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? )

drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops

multiple substitution

lazy equivalence

fleq ( â¦?,?,?â¦ â¡[?] â¦?,?,?â¦ )

fleq_fleq

-
-

generic relocation

lifts_bind ( â¬*[?] ? â¡ ? )

lifts_weight_bind lifts_lifts_bind

-
-

lleq ( ? â¡[?,?] ? )

lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq

lifts_vector ( â¬*[?] ? â¡ ? )

lifts_lifts_vector

-
-

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

lifts ( â¬*[?] ? â¡ ? )

lifts_simple lifts_weight lifts_tdeq lifts_lifts

-
-

pointwise union for local environments

llor ( ? â©[?,?] ? â¡ ? )

llor_alt llor_drop

-
-

ranged equivalence for local environments

lreq ( ? â¡[?] ? )

lreq_length lreq_lreq

-
-

context-sensitive exclusion from free variables

frees ( ? â¢ ? Ïµ ð*[?]â¦?â¦ )

frees_append frees_leq frees_lift

-
-

generic entrywise extension

lexs ( ? â¦»*[?,?,?] ? )

lexs_length lexs_lexs

-
-

contxt-sensitive extended multiple substitution

cpys ( â¦?,?â¦ â¢ ? â¶*[?,?] ? )

cpys_alt ( â¦?,?â¦ â¢ ? â¶â¶*[?,?] ? )

cpys_lift cpys_cpys

-
-

syntax

append for local environments

append ( ? @@ ? )

append_length

-
-

iterated structural successor for closures

fqus ( â¦?,?,?â¦ â* â¦?,?,?â¦ )

fqus_alt fqus_fqus

-
-

head equivalence for terms

theq_simple theq_tdeq theq_theq theq_simple_vector

-
-

fqup ( â¦?,?,?â¦ â+ â¦?,?,?â¦ )

fqup_fqup

degree-based equivalence

tdeq_ext ( ? â¡[?,?] ? ) ( ? â¢ ? â¡[?,?] ? )

-
-

iterated local env. slicing

drops_drop drops_drops

tdeq ( ? â¡[?,?] ? )

tdeq_tdeq

-
-

generic term relocation

lifts_vector ( â§*[?] ? â¡ ? )

lifts_lift_vector

closures

cl_weight ( â¯{?,?,?} )

-
-

lifts ( â§*[?] ? â¡ ? )

lifts_lift lifts_lifts

cl_restricted_weight ( â¯{?,?} )

support for multiple relocation

mr2 ( @â¦?,?â¦ â¡ ? )

mr2_plus ( ? + ? )

mr2_minus ( ? â ? â¡ ? )

mr2_mr2

substitution

structural successor for closures

fquq ( â¦?,?,?â¦ ââ¸® â¦?,?,?â¦ )

fquq_alt ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )

global environments

genv

-
-

fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ )

-
-

local environments

lenv_ext2

global env. slicing

gget_gget

lenv_length ( |?| )

contxt-sensitive extended ordinary substitution

cpy ( â¦?,?â¦ â¢ ? â¶[?,?] ? )

cpy_lift cpy_nlift cpy_cpy

lenv_weight ( â¯{?} )

local env. ref. for extended substitution

lsuby ( ? â[?,?] ? )

lsuby_lsuby

lenv

-
-

pointwise extension of a relation

lpx_sn

lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn

-
-

binders for local environments

ext2

ext2_ext2

-
-

basic local env. slicing

drop_append drop_leq drop_drop

bind

bind_weight

-
-

basic term relocation

lift_vector ( â§[?,?] ? â¡ ? )

lift_lift_vector

terms

term_vector ( â¶?.? )

-
-

lift ( â§[?,?] ? â¡ ? )

lift_neq lift_lift

-
-

grammar

equivalence for local environments

leq_leq

term_simple ( ðâ¦?â¦ )

same top term structure

tsts ( ? â ? )

tsts_tsts tsts_vector

term_weight ( â¯{?} )

closures

cl_weight ( â¯{?,?,?} )

cl_restricted_weight ( â¯{?,?} )

term

internal syntax

genv

-
-

items

item_sd

lenv

lenv_weight ( â¯{?} )

lenv_length ( |?| )

lenv_append ( ? @@ ? )

-
-

item_sh

term

term_weight ( â¯{?} )

term_simple ( ðâ¦?â¦ )

term_vector ( â¶?.? )

@@ -1261,12 +921,6 @@

item

-
-

external syntax

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 +964,6 @@

Last update: Wed, 10 Sep 2014 14:46:05 +0200

- +

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