+ $[\lambda\delta home]$

-

+ $\lambda\delta rainbow rule$

@@ -31,23 +31,23 @@ - home + home news - - documentation - - + specification - +
- +
+ + documentation + implementation @@ -57,47 +57,47 @@ - foreword + foreword milestones - - version 2 - - + version 2 - (background - core - applications) - + (background - core - applications) +
+ + version 2 + - library + helena + + + Open Symbolic Notation (OSN) - (static LDDL directory) - citations + citations visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 - - (core) - (static HELM directory) - - helena - - -
+ library + (static LDDL directory) @@ -114,9 +114,9 @@ **** Sort level k in terms only. --> -

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.

@@ -144,29 +144,29 @@ sizes files - 360 + 150 characters - 433402 + 128505 nodes - 1874774 + 646562 propositions theorems - 130 + 45 lemmas - 1286 + 476 total - 1416 + 521 concepts declared - 54 + 23 defined - 89 + 37 total - 143 + 60 @@ -179,11 +179,38 @@ for native type assignment. -

Stage "A": "Extending the Applicability Condition"

+

Stage "A2": "Extending the Applicability Condition"

+

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

@@ -305,10 +332,10 @@

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.

@@ -330,388 +357,10 @@ - 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 - -
- - - - reduction - parallel qrst-reduction - fpbq ( â¦?,?,?â¦ â½[?,?] â¦?,?,?â¦ ) - fpbq_alt ( â¦?,?,?â¦ â½â½[?,?] â¦?,?,?â¦ ) - fpbq_lift fpbq_aaa - -
- - - - -
- - -
- - fpb ( â¦?,?,?â¦ â»[?,?] â¦?,?,?â¦ ) - fpb_lift fpb_lleq fpb_fleq - -
- - -
- - - - -
- - normal forms for context-sensitive rt-reduction - cnx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ ) - cnx_lift cnx_crx cnx_cix - -
- - -
- - - - -
- - context-sensitive rt-reduction - lpx ( â¦?,?â¦ â¢ â¡[?,?] ? ) - lpx_drop lpx_frees lpx_lleq lpx_aaa + rt-transition + uncounted context-sensitive rt-transition + lfpx ( â¦?,?â¦ â¢ â¬[?,?] ? ) + lfpx_length lfpx_drops lfpx_fqup
@@ -726,22 +375,8 @@
- cpx ( â¦?,?â¦ â¢ ? â¡[?,?] ? ) - cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix - -
- - -
- - - - -
- - irreducible forms for context-sensitive rt-reduction - cix ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ ) - cix_lift + cpx ( â¦?,?â¦ â¢ ? â¬[?] ? ) + cpx_simple cpx_drops cpx_lsubr
@@ -753,9 +388,9 @@
- reducible forms for context-sensitive rt-reduction - crx ( â¦?,?â¦ â¢ â¡[?,?] ðâ¦?â¦ ) - crx_lift + counted context-sensitive rt-transition + cpg ( â¦?,?â¦ â¢ ? â¬[?,?] ? ) + cpg_simple cpg_drops cpg_lsubr
@@ -764,84 +399,66 @@ - -
- - normal forms for context-sensitive reduction - cnr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ ) - cnr_lift cnr_crr cnr_cir - -
- - -
- - - - -
- - context-sensitive reduction - lpr ( â¦?,?â¦ â¢ â¡ ? ) - lpr_drop lpr_lpr - + static typing + parameters + sh + sd +
- +
- -
- - +
- cpr ( â¦?,?â¦ â¢ ? â¡ ? ) - cpr_lift cpr_llpx_sn cpr_cir - + restricted ref. for atomic arity assignment + lsuba ( ? â¢ ? â«â ? ) + lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba +
- +
- +
- irreducible forms for context-sensitive reduction - cir ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ ) - cir_lift - + atomic arity assignment + aaa ( â¦?,?â¦ â¢ ? â ? ) + aaa_drops aaa_fqus aaa_lfeq aaa_aaa +
- +
- +
- reducible forms for context-sensitive reduction - crr ( â¦?,?â¦ â¢ â¡ ðâ¦?â¦ ) - crr_lift - + restricted ref. for local env. + lsubr ( ? â« ? ) + lsubr_length lsubr_drops lsubr_lsubr +
- +
- unfold - unfold - unfold ( â¦?,?â¦ â¢ ? â§«* ? ) - +
+ equivalence for closures on referred entries + ffeq ( â¦?,?,?â¦ â¡ â¦?,?,?â¦ ) + ffeq_freq
@@ -853,9 +470,9 @@
- iterated static type assignment - lstas ( â¦?,?â¦ â¢ ? â¢*[?,?] ? ) - lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas + equivalence for local environments on referred entries + lfeq ( ? â¡[?] ? ) + lfeq_length lfeq_lreq lfeq_fqup lfeq_lfeq
@@ -864,52 +481,38 @@ - static typing - local env. ref. for degree assignment - lsubd ( ? â¢ ? â«âª[?,?] ? ) - lsubd_da lsubd_lsubd - -
- - -
- - - - +
- degree assignment - da ( â¦?,?â¦ â¢ ? âª[?,?] ? ) - da_lift da_aaa da_da - + generic extension on referred entries + lfxs ( ? â¦»*[?,?] ? ) + lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs +
- +
- +
- parameters - sh - sd - + context-sensitive free variables + frees ( ? â¢ ð*â¦?â¦ â¡ ? ) + frees_weight frees_lreq frees_drops frees_frees +
- +
- -
- - 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
@@ -921,23 +524,11 @@
- 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
@@ -946,138 +537,10 @@ - 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
@@ -1092,8 +555,8 @@
- lifts ( â¬*[?] ? â¡ ? ) - lifts_lift lifts_lifts + fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ ) + fqu_length fqu_weight
@@ -1102,20 +565,12 @@ - + 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 ( â¦?,?,?â¦ âââ¸® â¦?,?,?â¦ )
@@ -1130,10 +585,8 @@
- fqu ( â¦?,?,?â¦ â â¦?,?,?â¦ ) - -
- + drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) + drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
@@ -1145,9 +598,9 @@
- global env. slicing - gget ( â¬[?] ? â¡ ? ) - gget_gget + generic relocation for terms + lifts_vector ( â¬*[?] ? â¡ ? ) + lifts_lifts_vector
@@ -1159,23 +612,11 @@
- 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
@@ -1187,9 +628,9 @@
- 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
@@ -1201,9 +642,9 @@
- basic local env. slicing - drop ( â¬[?,?,?] ? â¡ ? ) - drop_append drop_lreq drop_drop + generic entrywise extension + lexs ( ? â¦»*[?,?,?] ? ) + lexs_length lexs_lexs
@@ -1212,40 +653,24 @@ - -
- - 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_lreq + context-sensitive equivalences for terms + ceq + ceq_ceq
@@ -1307,7 +732,9 @@ lenv lenv_weight ( â¯{?} ) lenv_length ( |?| ) - lenv_append ( ? @@ ? ) + +
+ @@ -1359,7 +786,7 @@

-

+ $\lambda\delta rainbow rule$

@@ -1384,6 +811,6 @@

-

Last update: Mon, 19 Jan 2015 23:52:52 +0100

+

Last update: Fri, 22 Jul 2016 19:34:08 +0200