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 +

+ helena +

global definition ***

Î â¢ pÎ´V

global âÎ´

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

237

characters

420425

nodes

1063117

sizes

files

102

characters

69295

nodes

245853

propositions

theorems

lemmas

946

total

1031

propositions

theorems

lemmas

256

total

290

concepts

declared

defined

total

125

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

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

- In progress. - Closure of extended context-sensitive computation - for native validity. + 2013 July 27. + Reaxiomatized Î²-reductum as in rt-reduction.

- In progress. - Extended context-sensitive strong normalization + 2013 July 20. + Context-sensitive strong rt-normalization for simply typed terms.

- 2013 April 16. - Reaxiomatized substitution and reduction + 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. + 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 $\lambda\delta butterfly$ +

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

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

component

plane

files

-
-

dynamic typing

"big tree" parallel computation

yprs ( ? â¢ â¦?,?â¦ â¥[g] â¦?,?â¦ )

yprs_yprs

ygt ( ? â¢ â¦?,?â¦ >[g] â¦?,?â¦ )

ygt_ygt

-
-

"big tree" parallel reduction

ypr ( ? â¢ â¦?,?â¦ â½[g] â¦?,?â¦ )

ysc ( ? â¢ â¦?,?â¦ â»[g] â¦?,?â¦ )

-
-

local env. ref. for stratified native validity

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

lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv

-
-

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

-
-

equivalence

focalized equivalence

lfpcs ( â¦?â¦ â¬* â¦?â¦ )

lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs

-
-

fpcs ( â¦?,?â¦ â¬* â¦?,?â¦ )

fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs

-
-

local env. ref. for stratified static type assignment

lsubss ( ? â¢â[?] ? )

lsubss_ldrop lsubss_ssta lsubss_cpcs

-
-

context-sensitive equivalence

cpcs ( ? â¢ ? â¬* ? )

cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs

-
-

conversion

focalized conversion

lfpc ( â¦?â¦ â¬ â¦?â¦ )

lfpc_lfpc

component

plane

files

-
-

static typing

parameters

fpc ( â¦?,?â¦ â¬ â¦?,?â¦ )

fpc_fpc

-
-

context-sensitive conversion

cpc ( ? â¢ ? â¬ ? )

cpc_cpc

restricted ref. for local env.

lsubr ( ? â« ? )

lsubr_length lsubr_drops lsubr_lsubr

-
-

computation

focalized computation

lfprs ( â¦?â¦ â¡* â¦?â¦ )

lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs

ranged equivalence for closures

freq ( â¦?,?,?â¦ â¡ â¦?,?,?â¦ )

freq_freq

-
-

fprs ( â¦?,?â¦ â¡* â¦?,?â¦ )

fprs_aaa fprs_fprs

context-sensitive free variables

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

frees_weight frees_lreq frees_frees

-
-

s-computation

decomposed extended computation

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

dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxprs_dxprs

-
-

weakly normalizing computation

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

cpe_cpe

s-transition

structural successor for closures

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

fquq_length fquq_weight

-
-

strongly normalizing computation

csn_vector ( ? â¢ â¬* ? )

csn_cpr_vector csn_tstc_vector csn_aaa

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

fqu_length fqu_weight

-
-

relocation

generic slicing for local environments

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

csn ( ? â¢ â¬* ? )

csn_alt ( ? â¢ â¬â¬* ? )

csn_lift csn_cpr csn_lfpr

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

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

drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops

context-free computation

ltprs ( ? â¡* ? )

ltprs_alt ( ? â¡â¡* ? )

ltprs_ldrop ltprs_ltprs

generic relocation for terms

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

lifts_lifts_vector

tprs ( ? â¡* ?)

tprs_lift tprs_tprs

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

lifts_simple lifts_weight lifts_lifts

-
-

local env. ref. for abstract candidates of reducibility

lsubc ( ? â[?] ? )

lsubc_ldrop lsubc_ldrops lsubc_lsuba

ranged equivalence for local environments

lreq ( ? â¡[?] ? )

lreq_length lreq_lreq

support for abstract computation properties

acp

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

acp_aaa

generic entrywise extension of context-sensitive relations for terma

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

lexs_length lexs_lexs

reducibility

context-sensitive focalized reduction

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

cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr

grammar

append for local environments

append ( ? @@ ? )

append_length

-
-

context-free focalized reduction

lfpr ( â¦?â¦ â¡ â¦?â¦ )

lfpr_alt ( â¦?â¦ â¡â¡ â¦?â¦ )

lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr

context-sensitive equivalences for terms

ceq

ceq_ceq

-
-

fpr ( â¦?,?â¦ â¡ â¦?,?â¦ )

fpr_cpr fpr_fpr

same top term structure

tsts ( ? â ? )

tsts_tsts tsts_vector

-
-

context-sensitive normal forms

cnf ( ? â¢ ðâ¦?â¦ )

cnf_lift cnf_cif

closures

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

cl_restricted_weight ( â¯{?,?} )

revised context-sensitive reduction

lpr ( ? â¢ â¡ ? )

lpr_ldrop lpr_cpr lpr_lpr

internal syntax

genv

-
-

cpr ( ? â¢ ? â¡ ? )

cpr_lift

lenv

lenv_weight ( â¯{?} )

lenv_length ( |?| )

context-sensitive reduction

cpr ( ? â¢ ? â¡ ? )

cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr

-
-

term

term_weight ( â¯{?} )

term_simple ( ðâ¦?â¦ )

term_vector ( â¶?.? )

context-sensitive reducible forms

crf ( ? â¢ ðâ¦?â¦ )

crf_append

cif ( ? â¢ ðâ¦?â¦ )

cif_append

-
-

context-free normal forms

thnf ( ððâ¦?â¦ )

item

-
-

context-free reduction

ltpr ( ? â¡ ? )

ltpr_ldrop ltpr_tps ltpr_tpss ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr

-
-

tpr ( ? â¡ ? )

tpr_lift tpr_delift tpr_tpr

external syntax

aarity

unfold

restricted parallel computation

lpqs ( ? â¢ â¤* ? )

lpqs_ldrop lpqs_cpqs lpqs_lpqs

-
-

cpqs ( ? â¢ ? â¤* ? )

cpqs_lift

-
-

unfold

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

-
-

iterated stratified static type assignment

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

sstas_lift sstas_lpss sstas_aaa sstas_sstas

-
-

static typing

stratified static type assignment

ssta ( â¦?,?â¦ â¢ ? â¢[?,?] ? )

ssta_lift ssta_lpss ssta_aaa ssta_ssta

-
-

local env. ref. for atomic arity assignment

lsuba ( ? ââ ? )

lsuba_ldrop lsuba_aaa lsuba_lsuba

-
-

atomic arity assignment

aaa ( ? â¢ ? â ? )

aaa_lift aaa_lifts aaa_lpss aaa_aaa

-
-

parameters

-
-

substitution

parallel substitution

lpss ( ? â¢ â¶* ? )

lpss_ldrop lpss_cpss lpss_lpss

-
-

cpss ( ? â¢ ? â¶* ? )

cpss_lift

-
-

iterated structural successor for closures

fsups ( â¦?,?â¦ â* â¦?,?â¦ )

fsups_fsups

-
-

fsupp ( â¦?,?â¦ â+ â¦?,?â¦ )

fsupp_fsupp

-
-

generic local env. slicing

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

fsup ( â¦?,?â¦ â â¦?,?â¦ )

-
-

global env. slicing

gdrop_gdrop

-
-

basic local env. slicing

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

-
-

- -

Physical Structure of the Specification

The source files are grouped in directories, - one for each component. -

+ $\lambda\delta rainbow rule$

@@ -1398,6 +687,6 @@

Last update: Sat, 20 Apr 2013 21:34:40 +0200

- +

Last update: Thu, 07 Apr 2016 15:45:52 +0200