@@ -31,73 +31,95 @@ - home + home news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - - foreword + foreword milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 + helena - (background - core - applications) - - library + + Open Symbolic Notation (OSN) - citations + citations visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - -
- - - helena + library + (static LDDL directory)

- - -

Summary of the Specification

+ +

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical acount of the specification's contents +

Here is a numerical account of the specification's contents and its timeline.

@@ -122,80 +144,117 @@ - + - + - + - + - + - + - + - + - +

sizes	files	360	177	characters	433402	181483	nodes	1874774	952913
propositions	theorems	130	49	lemmas	1286	633	total	1416	682
concepts	declared	54	24	defined	89	42	total	143	66

- -

Stage "B"

Ongoing. Context-sensitive subject equivalence for native type assignment.

Stage "A": "Extending the Applicability Condition"

Stage "A2": "Extending the Applicability Condition"

+ 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 2A is released. + Î»Î´ 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 - addded as q-step to rst-computation on closures + added as q-step to rst-computation on closures (anniversary milestone).

2014 January 20. Parametrized slicing of local environments @@ -203,26 +262,26 @@ (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 @@ -230,26 +289,26 @@ (anniversary milestone).

2013 March 16. Mutual recursive preservation of stratified native validity for rst-computation on closures.

2012 October 16. Confluence for context-free parallel reduction on closures.

2012 July 26. Term binders polarized to control Î¶-reduction (not released).

2012 April 16. Context-sensitive subject equivalence @@ -257,43 +316,42 @@ (anniversary milestone).

2012 March 15. Context-sensitive strong normalization for simply typed terms.

2012 January 27. Support for abstract candidates of reducibility.

2011 September 21. Confluence for context-sensitive parallel reduction on terms.

2011 September 6. Confluence for context-free parallel reduction on terms.

2011 April 17. - Specification starts. + Î»Î´ version 2 is started.

Logical Structure of the Specification [spacer]

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

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

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

@@ -311,347 +369,13 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - - - - - - - @@ -663,8 +387,8 @@ - - + + @@ -676,9 +400,11 @@ - - - + + + @@ -690,9 +416,9 @@ - - - + + + @@ -707,8 +433,8 @@ - - + + @@ -720,9 +446,9 @@ - - - + + + @@ -731,98 +457,80 @@ - - - - - - - - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - + + + @@ -834,9 +542,9 @@ - - - + + + @@ -845,52 +553,38 @@ - - - - - - - - - - - - - + + + - - - - - - + + + - - - - - + + + + @@ -902,23 +596,11 @@ - - - - - - - - - - - + + @@ -927,138 +609,10 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + @@ -1073,8 +627,8 @@ - - + + @@ -1083,20 +637,12 @@ - + + + - - - - - - - - - - - @@ -1111,10 +657,8 @@ - - + + @@ -1126,9 +670,9 @@ - - - + + + @@ -1140,23 +684,11 @@ - - - - - - - - - - - + + @@ -1168,9 +700,9 @@ - - - + + + @@ -1182,9 +714,9 @@ - - - + + + @@ -1193,40 +725,24 @@ - - - - - + + + + - - - - - - - - - - - - - + + + @@ -1288,7 +804,9 @@ - +

examples

terms with special features

ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta

-
-

dynamic typing

local env. ref. for stratified native validity

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

lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv

-
-

stratified native validity

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

-
-

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

snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve

-
-

equivalence

decomposed rt-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 rt-reduction

cpxe ( â¦?,?â¦ â¢ â¡*[?,?] ðâ¦?â¦ )

-
-

evaluation for context-sensitive reduction

cpre ( â¦?,?â¦ â¢ â¡* ðâ¦?â¦ )

cpre_cpre

-
-

strongly normalizing qrst-computation

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

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

fsb_aaa fsb_csx

-
-

strongly normalizing rt-computation

lcosx ( ? â¢ ~â¬*[?,?,?] ? )

lcosx_cpx

-
-

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

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

lsx_drop lsx_lpx lsx_lpxs llsx_csx

-
-

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

csx_tsts_vector csx_aaa

-
-

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

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

csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs

-
-

parallel qrst-computation

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

fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg

-
-

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

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

fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs

-
-

decomposed rt-computation

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

scpds_lift scpds_aaa scpds_scpds

-
-

context-sensitive rt-computation

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

lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs

-
-

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

cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs

-
-

context-sensitive computation

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

lprs_drop lprs_cprs lprs_lprs

-
-

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

cprs_lift cprs_cprs

-
-

local env. ref. for generic reducibility

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

lsubc_drop lsubc_drops lsubc_lsuba

-
-

support for generic computation properties

gcp

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

gcp_aaa

rt-transition

t-bound context-sensitive rt-transition

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

lfpr_length lfpr_drops lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr

reduction

parallel qrst-reduction

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

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

fpbq_lift fpbq_aaa

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

fpb_lift fpb_lleq fpb_fleq

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

cpr_drops

normal forms for context-sensitive rt-reduction

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

cnx_lift cnx_crx cnx_cix

+
+

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

cpm_simple cpm_drops cpm_lsubr cpm_cpx

context-sensitive rt-reduction

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

lpx_drop lpx_frees lpx_lleq lpx_aaa

uncounted context-sensitive rt-transition

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

lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_aaa

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

cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix

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

cpx_simple cpx_drops cpx_lsubr

irreducible forms for context-sensitive rt-reduction

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

cix_lift

counted context-sensitive rt-transition

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

cpg_simple cpg_drops cpg_lsubr

-
-

reducible forms for context-sensitive rt-reduction

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

crx_lift

-
-

normal forms for context-sensitive reduction

cnr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )

cnr_lift cnr_crr cnr_cir

static typing

parameters

context-sensitive reduction

lpr ( â¦?,?â¦ â¢ â¡ ? )

lpr_drop lpr_lpr

restricted ref. for atomic arity assignment

lsuba ( ? â¢ ? â«â ? )

lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba

-
-

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

cpr_lift cpr_llpx_sn cpr_cir

atomic arity assignment

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

aaa_drops aaa_fqus aaa_lfeq aaa_aaa

irreducible forms for context-sensitive reduction

cir ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )

cir_lift

equivalence for closures on referred entries

ffeq ( â¦?,?,?â¦ â¡ â¦?,?,?â¦ )

ffeq_freq

reducible forms for context-sensitive reduction

crr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ )

crr_lift

equivalence for local environments on referred entries

lfeq ( ? â¡[?] ? )

lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq

unfold

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

generic extension on referred entries

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

lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs

iterated static type assignment

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

lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas

restricted ref. for context-sensitive free variables

lsubf ( â¦?,?â¦ â«ð* â¦?,?â¦ )

lsubf_frees

static typing

local env. ref. for degree assignment

lsubd ( ? â¢ ? â«âª[?,?] ? )

lsubd_da lsubd_lsubd

-
-

degree assignment

da ( â¦?,?â¦ â¢ ? âª[?,?] ? )

da_lift da_aaa da_da

context-sensitive free variables

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

frees_weight frees_lreq frees_drops frees_fqup frees_frees

parameters

restricted ref. for local env.

lsubr ( ? â« ? )

lsubr_length lsubr_drops lsubr_lsubr

-
-

local env. ref. for atomic arity assignment

lsuba ( ? â¢ ? â«â ? )

lsuba_aaa lsuba_lsuba

s-computation

iterated structural successor for closures

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

fqus_weight fqus_drops fqus_fqup fqus_fqus

atomic arity assignment

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

aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa

-
-

restricted local env. ref.

lsubr ( ? â« ? )

lsubr_lsubr

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

fqup_weight fqup_drops fqup_fqup

multiple substitution

lazy equivalence

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

fleq_fleq

-
-

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

lleq_alt lleq_alt_rec lleq_lreq 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_lreq 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_lreq frees_lift

-
-

contxt-sensitive multiple rt-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

s-transition

structural successor for closures

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

fquq_length fquq_weight

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

lifts_lift lifts_lifts

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

fqu_length fqu_weight

relocation

generic slicing for local environments

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

support for multiple relocation

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

mr2_plus ( ? + ? )

mr2_minus ( ? â ? â¡ ? )

mr2_mr2

substitution

structural successor for closures

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

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

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

-
-

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

drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops

global env. slicing

gget ( â¬[?] ? â¡ ? )

gget_gget

generic relocation for terms

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

lifts_lifts_vector

contxt-sensitive ordinary rt-substitution

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

cpy_lift cpy_nlift cpy_cpy

-
-

local env. ref. for rt-substitution

lsuby ( ? â[?,?] ? )

lsuby_lsuby

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

lifts_simple lifts_weight lifts_lifts

pointwise extension of a relation

lpx_sn

lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn

ranged equivalence for local environments

lreq ( ? â¡[?] ? )

lreq_length lreq_lreq

basic local env. slicing

drop ( â¬[?,?,?] ? â¡ ? )

drop_append drop_lreq drop_drop

generic entrywise extension

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

lexs_length lexs_lexs

-
-

basic term relocation

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

lift_lift_vector

grammar

append for local environments

append ( ? @@ ? )

append_length

-
-

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

lift_neq lift_lift

-
-

grammar

equivalence for local environments

lreq_lreq

context-sensitive equivalences for terms

ceq

ceq_ceq

lenv

lenv_weight ( â¯{?} )

lenv_length ( |?| )

lenv_append ( ? @@ ? )

+
+

@@ -1339,9 +857,8 @@

- -

+ $\lambda\delta rainbow rule$

@@ -1366,6 +883,6 @@

Last update: Tue, 04 Nov 2014 16:28:52 +0100

- +

Last update: Sat, 21 Jan 2017 15:35:26 +0100