Here is a numerical account of the specification's contents
and its timeline.
@@ -137,29 +144,29 @@
sizes
files
- 360
+ 102
characters
- 433402
+ 69295
nodes
- 1874774
+ 245853
propositions
theorems
- 130
+ 34
lemmas
- 1286
+ 256
total
- 1416
+ 290
concepts
declared
- 54
+ 21
defined
- 89
+ 29
total
- 143
+ 50
@@ -172,11 +179,24 @@
for native type assignment.
-
Stage "A": "Extending the Applicability Condition"
+ 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 2A is released. + λδ version 2A1 is released.
-
@@ -204,7 +224,7 @@
- 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).
- 2011 April 17. - Specification starts. + λδ version 2 is started.
Logical Structure of the Specification ![[spacer]](http://lambdadelta.info/images/b4.png "lambdadelta butterfly")
@@ -323,518 +343,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
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- cpx ( â¦?,?⦠⢠? â¡[?,?] ? )
- cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix
-
-
-
-
-
-
-
-
-
-
-
- irreducible forms for context-sensitive rt-reduction
- cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠)
- cix_lift
-
-
-
-
-
-
-
-
-
-
-
- reducible forms for context-sensitive rt-reduction
- crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠)
- crx_lift
-
-
-
-
-
-
-
-
-
-
-
- normal forms for context-sensitive reduction
- cnr ( â¦?,?⦠⢠⡠ðâ¦?⦠)
- cnr_lift cnr_crr cnr_cir
-
-
-
-
-
-
-
-
-
-
-
- context-sensitive reduction
- lpr ( �,?⦠⢠⡠? )
- lpr_drop lpr_lpr
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- cpr ( �,?⦠⢠? ⡠? )
- cpr_lift cpr_llpx_sn cpr_cir
-
-
-
-
-
-
-
-
-
-
-
- irreducible forms for context-sensitive reduction
- cir ( â¦?,?⦠⢠⡠ðâ¦?⦠)
- cir_lift
-
-
-
-
-
-
-
-
-
-
-
- reducible forms for context-sensitive reduction
- crr ( â¦?,?⦠⢠⡠ðâ¦?⦠)
- crr_lift
-
-
-
-
-
-
-
-
- unfold
- unfold
- unfold ( �,?⦠⢠? ⧫* ? )
-
-
-
+ static typing
+ parameters
+ sh
+ sd
@@ -846,9 +358,9 @@
- 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
@@ -857,80 +369,42 @@
- static typing
- local env. ref. for degree assignment
- lsubd ( ? ⢠? â«âª[?,?] ? )
- lsubd_da lsubd_lsubd
-
-
-
-
-
-
-
-
-
-
-
- degree assignment
- da ( â¦?,?⦠⢠? âª[?,?] ? )
- da_lift da_aaa da_da
-
-
-
-
-
-
-
-
-
+
- parameters
- sh
- sd
-
+ ranged equivalence for closures
+ freq ( �,?,?⦠⡠�,?,?⦠)
+ freq_freq
+
-
+
-
+
- local env. ref. for atomic arity assignment
- lsuba ( ? ⢠? â«â ? )
- lsuba_aaa lsuba_lsuba
-
+ context-sensitive free variables
+ frees ( ? ⢠ð
*�⦠⡠? )
+ frees_weight frees_lreq frees_frees
+
-
+
-
+ s-computation
+
- atomic arity assignment
- aaa ( â¦?,?⦠⢠? â ? )
- aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
-
-
-
-
-
-
-
-
- restricted local env. ref.
- lsubr ( ? â« ? )
- lsubr_lsubr
@@ -939,94 +413,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
+ s-transition
+ structural successor for closures
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠)
+ fquq_length fquq_weight
@@ -1041,8 +431,8 @@
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠)
- fqup_fqup
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠)
+ fqu_length fqu_weight
@@ -1051,64 +441,12 @@
-
-
-
- iterated local env. slicing
- drops ( â¬*[?,?] ? â¡ ? )
- drops_drop drops_drops
-
-
-
-
-
-
-
-
-
-
-
- generic term relocation
- lifts_vector ( â¬*[?] ? â¡ ? )
- lifts_lift_vector
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- lifts ( â¬*[?] ? â¡ ? )
- lifts_lift lifts_lifts
-
-
-
-
-
-
-
-
-
+ 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 ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠)
@@ -1123,10 +461,8 @@
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠)
-
-
-
+ drops ( â¬*[?,?] ? â¡ ? )
+ drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
@@ -1138,9 +474,9 @@
- global env. slicing
- gget ( â¬[?] ? â¡ ? )
- gget_gget
+ generic relocation for terms
+ lifts_vector ( â¬*[?] ? â¡ ? )
+ lifts_lifts_vector
@@ -1152,23 +488,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
@@ -1180,9 +504,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
@@ -1194,9 +518,9 @@
- basic local env. slicing
- drop ( â¬[?,?,?] ? â¡ ? )
- drop_append drop_lreq drop_drop
+ generic entrywise extension of context-sensitive relations for terma
+ lexs ( ? ⦻*[?,?,?] ? )
+ lexs_length lexs_lexs
@@ -1205,40 +529,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
@@ -1300,7 +608,9 @@
lenv
lenv_weight ( â¯{?} )
lenv_length ( |?| )
- lenv_append ( ? @@ ? )
+
+
+
@@ -1377,6 +687,6 @@
-
@@ -323,518 +343,10 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
Last update: Thu, 15 Jan 2015 16:54:45 +0100
+ Last update: Fri, 01 Apr 2016 23:30:53 +0200