\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].

- + @@ -56,397 +142,374 @@ - - - - - - - + + + + + + + - + - + - + - - - - - - - + + + + + + +

category	objects	units
sizes	files	359	characters	429628	nodes	1855731	sizes	characters (files)	315581 (309)	nodes (objects)	1458870 (1431)	intrinsic loss factor	4.6
propositions	theorems	127	92	lemmas	1276	1085	total	1403	1177
concepts	declared	54	defined	85	total	139	concepts	declared	34	defined	93	total	127

- -

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

- 2014 September 9. + 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 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.

+ - - - - - - - - + + + + + - - - + + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - - - - - - - - + + - - - - - - + + + - - - - - - + + + + + - - - - - - - - - - - - + + + - - - - - + + + + - - - - - - - - - - - + + @@ -455,116 +518,51 @@ - - - - - - - - - - - - + + + - - - - - + + + + - - - - - + + + + - - - - - - - - - - - - + + + - - - - - - - - - - - + + @@ -573,14 +571,11 @@ - - - - + + @@ -589,598 +584,411 @@ - - - - - + + + - - - - - + + + + - - - - - - + + + + + - - - - - - + + + + + - - - - - - + + + - - - - - - + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + + - - - - - - + + + + - - - - - - + + + - - - - - + + + + - - - - - - + + + + + - - - - - - - - - - - - + + + - - - - - - + + + + + - - - - - - + + + - - - - - - + + + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + - - - - - - + + - - - - - - + + - - - - - - - - - - - - - - + - - - - - - + + - - - - - - + + + - - - - - - + - - - - - - + - - - - - - + - - - - - - + - - - - - - + + + - - - - - - + + - - - - - + + @@ -1189,12 +997,11 @@ - - - - + @@ -1203,12 +1010,11 @@ - - - - + @@ -1217,14 +1023,11 @@ - - - - + @@ -1233,40 +1036,35 @@ - + + - - - - - + + - - - - - + - - @@ -1275,14 +1073,9 @@ - + + - - @@ -1290,13 +1083,8 @@

component

section

plane

files

-
-

examples

terms with special features

ex_sta_ldec ex_cpr_omega

-
-

rt-conversion

context-sensitive parallel r-conversion

for terms

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

cpc_cpc

-
-

rt-computation

uncounted context-sensitive parallel rt-computation

refinement for lenvs

lsubsx ( ? â¢ ? ââ§[?,?,?] ? )

lsubsx_lfsx lsubsx_lsubsx

dynamic typing

local env. ref. for stratified native validity

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

lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv

strongly normalizing for lenvs on referred entries

lfsx ( ? â¢ â¬*[?,?,?] ðâ¦?â¦ )

lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx

-
-

stratified native validity

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

-
-

strongly normalizing for term vectors

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

csx_cnx_vector csx_csx_vector

-
-

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

snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve

-
-

strongly normalizing for terms

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

csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx

equivalence

decomposed extended equivalence

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

scpes_aaa scpes_cpcs scpes_scpes

for lenvs on referred entries

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

lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs

-
-

context-sensitive equivalence

cpcs ( â¦?,?â¦ â¢ ? â¬* ? )

cpcs_aaa cpcs_cprs cpcs_cpcs

-
-

conversion

context-sensitive conversion

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

cpc_cpc

for lenvs on all entries

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

computation

evaluation for context-sensitive extended reduction

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

-
-

for terms

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

cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs

-
-

evaluation for context-sensitive reduction

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

cpre_cpre

-
-

rt-transition

uncounted parallel rst-transition

for closures

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

fpbq_aaa

strongly normalizing "big tree" computation

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

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

fsb_aaa fsb_csx

-
-

strongly normalizing extended computation

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

lcosx_cpx

-
-

proper for closures

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

fpb_lfdeq

-
-

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

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

lsx_drop lsx_lpx lsx_lpxs llsx_csx

-
-

context-sensitive parallel r-transition

for lenvs on referred entries

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

lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr

-
-

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

csx_tsts_vector csx_aaa

-
-

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

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

csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs

for binders

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

"big tree" parallel computation

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

fpbg_lift fpbg_fleq fpbg_fpbg

-
-

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

fpbc_fleq fpbc_fpbs

-
-

for terms

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

cpr_drops

-
-

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

fpbu_lift fpbu_lleq fpbu_fleq

-
-

t-bound context-sensitive parallel rt-transition

for terms

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

cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx

-
-

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

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

fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext

-
-

uncounted context-sensitive parallel rt-transition

normal form for terms

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

cnx_simple cnx_drops cnx_cnx

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

-
-

for lenvs on referred entries

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

lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx

-
-

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

cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs

-
-

context-sensitive computation

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

lprs_drop lprs_cprs lprs_lprs

-
-

for lenvs on all entries

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

-
-

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

cprs_lift cprs_cprs

for binders

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

local env. ref. for generic reducibility

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

lsubc_drop lsubc_drops lsubc_lsuba

-
-

for terms

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

cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq

support for generic computation properties

gcp

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

gcp_aaa

-
-

counted context-sensitive parallel rt-transition

for terms

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

cpg_simple cpg_drops cpg_lsubr

reduction

"big tree" parallel reduction

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

fpb_lift fpb_aaa

-
-

iterated static typing

iterated generic extension of a context-sensitive relation

for lenvs on referred entries

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

tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs

-
-

normal forms for context-sensitive extended reduction

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

cnx_lift cnx_crx cnx_cix

-
-

static typing

generic reducibility

restricted refinement for lenvs

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

lsubc_drops lsubc_lsubr lsubc_lsuba

-
-

context-sensitive extended reduction

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

lpx_drop lpx_frees lpx_lleq lpx_aaa

candidates

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

gcp_aaa

-
-

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

cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix

computation properties

gcp

-
-

irreducible forms for context-sensitive extended reduction

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

cix_lift

-
-

atomic arity assignment

restricted refinement for lenvs

lsuba ( ? â¢ ? â«â ? )

lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba

-
-

reducible forms for context-sensitive extended reduction

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

crx_lift

for terms

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

aaa_drops aaa_fqus aaa_lfdeq aaa_aaa

-
-

normal forms for context-sensitive reduction

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

cnr_lift cnr_crr cnr_cir

-
-

degree-based equivalence

for closures on referred entries

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

ffdeq_fqup ffdeq_ffdeq

-
-

context-sensitive reduction

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

lpr_drop lpr_lpr

for lenvs on referred entries

lfdeq ( ? â[?,?,?] ? )

lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq

-
-

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

cpr_lift cpr_llpx_sn cpr_cir

-
-

syntactic equivalence

for lenvs on referred entries

lfeq ( ? â¡[?] ? )

lfeq_fqup lfeq_lfeq

-
-

irreducible forms for context-sensitive reduction

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

cir_lift

-
-

generic extension of a context-sensitive relation

for lenvs 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

restricted refinement for lenvs

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

lsubf_lsubr lsubf_frees lsubf_lsubf

unfold

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

-
-

for terms

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

frees_drops frees_fqup frees_frees

iterated static type assignment

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

lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas

-
-

local environments

restricted refinement

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

-
-

parameters

-
-

proper for closures

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

fqup_weight fqup_drops fqup_fqup

-
-

local env. ref. for atomic arity assignment

lsuba ( ? â¢ ? â«â ? )

lsuba_aaa lsuba_lsuba

-
-

s-transition

structural successor

for closures

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

fquq_length fquq_weight

-
-

atomic arity assignment

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

aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa

proper for closures

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

fqu_length fqu_weight

-
-

restricted local env. ref.

lsubr ( ? â« ? )

lsubr_lsubr

-
-

relocation

generic slicing

for lenvs

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

drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector

multiple substitution

lazy equivalence

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

fleq_fleq

-
-

generic relocation

for binders

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

lifts_weight_bind lifts_lifts_bind

-
-

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

lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq

for term vectors

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

for terms

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

lifts_simple lifts_weight lifts_tdeq lifts_lifts

-
-

pointwise union for local environments

llor_alt llor_drop

-
-

syntactic equivalence

for lenvs on selected entries

lreq ( ? â¡[?] ? )

lreq_length lreq_lreq

-
-

context-sensitive exclusion from free variables

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

frees_append frees_leq frees_lift

-
-

generic entrywise extension

for lenvs of one contex-sensitive relation

lex ( ? â¦»[?] ? )

lex_tc

contxt-sensitive extended multiple substitution

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

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

cpys_lift cpys_cpys

for lenvs of two contex-sensitive relations

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

lexs_tc lexs_length lexs_lexs

-
-

iterated structural successor for closures

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

fqus_alt fqus_fqus

-
-

syntax

append for local environments

append ( ? @@ ? )

append_length

-
-

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

fqup_fqup

-
-

head equivalence for terms

theq_simple theq_tdeq theq_theq theq_simple_vector

-
-

iterated local env. slicing

drops_drop drops_drops

degree-based equivalence

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

-
-

generic term relocation

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

lifts_lift_vector

tdeq ( ? â[?,?] ? )

tdeq_tdeq

-
-

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

lifts_lift lifts_lifts

closures

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

support for multiple relocation

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

mr2_plus ( ? + ? )

mr2_minus ( ? â ? â¡ ? )

mr2_mr2

substitution

structural successor for closures

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

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

cl_restricted_weight ( â¯{?,?} )

-
-

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

-
-

global environments

genv

-
-

global env. slicing

gget_gget

-
-

local environments

ceq_ext

ceq_ext_ceq_ext

contxt-sensitive extended ordinary substitution

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

cpy_lift cpy_nlift cpy_cpy

cext2

local env. ref. for extended substitution

lsuby ( ? â[?,?] ? )

lsuby_lsuby

lenv_length ( |?| )

pointwise extension of a relation

lpx_sn

lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn

lenv_weight ( â¯{?} )

basic local env. slicing

drop_append drop_leq drop_drop

lenv

-
-

basic term relocation

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

lift_lift_vector

-
-

binders for local environments

ext2

ext2_tc ext2_ext2

-
-

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

lift_neq lift_lift

bind

bind_weight

grammar

equivalence for local environments

leq_leq

terms

term_vector ( â¶?.? )

same top term structure

tsts ( ? â ? )

tsts_tsts tsts_vector

term_simple ( ðâ¦?â¦ )

closures

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

cl_restricted_weight ( â¯{?,?} )

term_weight ( â¯{?} )

internal syntax

genv

-
-

term

items

item_sd

lenv

lenv_weight ( â¯{?} )

lenv_length ( |?| )

lenv_append ( ? @@ ? )

+
+

item_sh

term

term_weight ( â¯{?} )

term_simple ( ðâ¦?â¦ )

term_vector ( â¶?.? )

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

Last update: Sun, 14 Sep 2014 23:26:35 +0200

- +

Last update: Fri, 24 Nov 2017 21:00:01 +0100