Stage "A": "Extending the Applicability Condition"
+ Stage "A2": "Extending the Applicability Condition"
+ -
+
- + 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. + +
-
+
- + 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 2A is released. + λδ version 2A1 is released.
-
@@ -287,7 +339,7 @@
- 2012 January 27. - Support for abstract candidates of reducibility. + Generic candidates of reducibility.
- 2011 April 17. - Specification starts. + λδ version 2 is started.
-
@@ -305,10 +357,10 @@
Logical Structure of the Specification
+ component
plane
files
-
-
-
-
-
-
- examples
- terms with special features
- ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
-
-
-
-
-
-
-
-
-
+ rt-computation
+ uncounted context-sensitive rt-computation
+ csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠)
+ csx_cnx_vector csx_csx_vector
-
-
-
-
-
-
-
+
-
+
+ csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠)
+ csx_simple csx_simple_theq csx_drops csx_lsubr csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_csx
- dynamic typing
- local env. ref. for stratified native validity
- lsubsv ( ? ⢠? â«Â¡[?,?] ? )
- lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv
-
+
-
+
+ lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? )
+ lfpxs_length lfpxs_fqup lfpxs_cpxs
-
+
- stratified native validity
- shnv ( �,?⦠⢠? ¡[?,?,?] )
-
-
-
-
-
-
-
+
+ cpxs ( â¦?,?⦠⢠? â¬*[?] ? )
+ cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_lsubr cpxs_lfpx cpxs_cnx cpxs_cpxs
-
-
-
-
-
-
- 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
-
-
-
-
-
-
+ rt-transition
+ parallel rst-transition
+ fpbq ( â¦?,?,?⦠â½[?] â¦?,?,?⦠)
+ fpbq_aaa
@@ -500,28 +424,16 @@
- lsx ( ? ⢠â¬*[?,?,?,?] ? )
- lsx_alt ( ? ⢠â¬â¬*[?,?,?,?] ? )
- lsx_drop lsx_lpx lsx_lpxs llsx_csx
-
-
-
+ fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠)
+ fpb_lfdeq
-
-
-
- csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? )
- csx_tsts_vector csx_aaa
-
-
-
-
-
-
+ t-bound context-sensitive rt-transition
+ lfpr ( â¦?,?⦠⢠â¡[?,?] ? )
+ lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr
@@ -530,26 +442,8 @@
- 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
-
-
-
-
-
-
+ cpr ( â¦?,?⦠⢠? â¡[?] ? )
+ cpr_drops
@@ -558,40 +452,16 @@
- fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠)
- fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠)
- fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs
-
-
-
-
-
-
-
-
- decomposed rt-computation
- scpds ( â¦?,?⦠⢠? â¢*â¡*[?,?,?] ? )
- scpds_lift scpds_aaa scpds_scpds
-
-
-
-
-
-
+ cpm ( â¦?,?⦠⢠? â¡[?,?] ? )
+ cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx
- context-sensitive rt-computation
- lpxs ( â¦?,?⦠⢠â¡*[?,?] ? )
- lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
-
-
-
-
-
-
+ uncounted context-sensitive rt-transition
+ cnx ( â¦?,?⦠⢠â¬[?,?] ðâ¦?⦠)
+ cnx_simple cnx_drops cnx_cnx
@@ -600,28 +470,8 @@
- 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
-
-
-
-
-
-
+ lfpx ( â¦?,?⦠⢠â¬[?,?] ? )
+ lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx
@@ -630,332 +480,144 @@
- cprs ( â¦?,?⦠⢠? â¡* ?)
- cprs_lift cprs_cprs
-
-
-
-
-
-
-
-
-
-
-
- local env. ref. for generic reducibility
- lsubc ( ? ⢠? â«[?] ? )
- lsubc_drop lsubc_drops lsubc_lsuba
-
-
-
-
-
-
+ cpx ( â¦?,?⦠⢠? â¬[?] ? )
+ cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs
- 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
-
-
-
-
-
-
+ counted context-sensitive rt-transition
+ cpg ( â¦?,?⦠⢠? â¬[?,?] ? )
+ cpg_simple cpg_drops cpg_lsubr
-
-
-
- reducible forms for context-sensitive rt-reduction
- crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠)
- crx_lift
-
-
-
+ iterated static typing
+ iterated extension on referred entries
+ tc_lfxs ( ? ⦻**[?,?] ? )
-
-
-
- normal forms for context-sensitive reduction
- cnr ( â¦?,?⦠⢠⡠ðâ¦?⦠)
- cnr_lift cnr_crr cnr_cir
-
-
-
-
-
-
+ static typing
+ generic reducibility
+ lsubc ( ? ⢠? â«[?] ? )
+ lsubc_drops lsubc_lsubr lsubc_lsuba
-
-
-
- context-sensitive reduction
- lpr ( �,?⦠⢠⡠? )
- lpr_drop lpr_lpr
-
+
-
+
+ gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã )
+ gcp_aaa
-
-
-
-
+
- cpr ( �,?⦠⢠? ⡠? )
- cpr_lift cpr_llpx_sn cpr_cir
-
+
-
+ gcp
+
-
-
-
- irreducible forms for context-sensitive reduction
- cir ( â¦?,?⦠⢠⡠ðâ¦?⦠)
- cir_lift
-
-
-
-
+
+ atomic arity assignment
+ lsuba ( ? ⢠? â«â ? )
+ lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba
-
+
- reducible forms for context-sensitive reduction
- crr ( â¦?,?⦠⢠⡠ðâ¦?⦠)
- crr_lift
-
-
-
-
+
+ aaa ( â¦?,?⦠⢠? â ? )
+ aaa_drops aaa_fqus aaa_lfdeq aaa_aaa
- unfold
- unfold
- unfold ( �,?⦠⢠? ⧫* ? )
-
-
-
-
-
-
-
+
+ degree-based equivalence on referred entries
+ ffdeq ( â¦?,?,?⦠â¡[?,?] â¦?,?,?⦠)
+ ffdeq_fqup ffdeq_ffdeq
- iterated static type assignment
- lstas ( â¦?,?⦠⢠? â¢*[?,?] ? )
- lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
-
-
-
-
+
+ lfdeq ( ? â¡[?,?,?] ? )
+ lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq
- static typing
- local env. ref. for degree assignment
- lsubd ( ? ⢠? â«âª[?,?] ? )
- lsubd_da lsubd_lsubd
-
-
-
-
+
+ generic extension on referred entries
+ lfxs ( ? ⦻*[?,?] ? )
+ lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs
-
-
-
- degree assignment
- da ( â¦?,?⦠⢠? âª[?,?] ? )
- da_lift da_aaa da_da
-
-
-
-
+
+ context-sensitive free variables
+ lsubf ( â¦?,?⦠â«ð
* �,?⦠)
+ lsubf_frees
-
-
-
- parameters
- sh
- sd
-
+
-
+
+ frees ( ? ⢠ð
*�⦠⡠? )
+ frees_drops frees_fqup frees_frees
-
-
-
- local env. ref. for atomic arity assignment
- lsuba ( ? ⢠? â«â ? )
- lsuba_aaa lsuba_lsuba
-
-
-
-
+
+ restricted ref. for local env.
+ lsubr ( ? â« ? )
+ lsubr_length lsubr_drops lsubr_lsubr
-
-
-
- atomic arity assignment
- aaa ( â¦?,?⦠⢠? â ? )
- aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
-
-
-
-
-
-
+ s-computation
+ iterated structural successor for closures
+ fqus ( â¦?,?,?⦠â* â¦?,?,?⦠)
+ fqus_weight fqus_drops fqus_fqup fqus_fqus
- restricted local env. ref.
- lsubr ( ? â« ? )
- lsubr_lsubr
-
-
-
-
+
+ fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠)
+ fqup_weight fqup_drops fqup_fqup
- multiple substitution
- lazy equivalence
- fleq ( â¦?,?,?⦠â¡[?] â¦?,?,?⦠)
- fleq_fleq
-
-
-
-
-
-
+ s-transition
+ structural successor for closures
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠)
+ fquq_length fquq_weight
@@ -964,291 +626,167 @@
- 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
-
-
-
-
-
-
+ fqu ( â¦?,?,?⦠â â¦?,?,?⦠)
+ fqu_length fqu_weight
-
-
-
- context-sensitive exclusion from free variables
- frees ( ? ⢠? ϵ ð
*[?]�⦠)
- frees_append frees_lreq frees_lift
-
-
-
-
+ relocation
+ generic slicing for local environments
+ drops_vector ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? )
+
-
+
- context-sensitive multiple rt-substitution
- cpys ( â¦?,?⦠⢠? â¶*[?,?] ? )
- cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? )
- cpys_lift cpys_cpys
-
+
+ drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? )
+ drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
-
-
-
- iterated structural successor for closures
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠)
- fqus_alt fqus_fqus
-
-
-
-
+
+ generic relocation for terms
+ lifts_vector ( â¬*[?] ? â¡ ? )
+ lifts_lifts_vector
-
-
-
-
-
-
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠)
- fqup_fqup
-
+
-
+
+ lifts ( â¬*[?] ? â¡ ? )
+ lifts_simple lifts_weight lifts_tdeq lifts_lifts
-
-
-
- iterated local env. slicing
- drops ( â¬*[?,?] ? â¡ ? )
- drops_drop drops_drops
-
-
-
-
+
+ ranged equivalence for local environments
+ lreq ( ? â¡[?] ? )
+ lreq_length lreq_lreq
-
-
-
- generic term relocation
- lifts_vector ( â¬*[?] ? â¡ ? )
- lifts_lift_vector
-
-
-
-
+
+ generic entrywise extension
+ lexs ( ? ⦻*[?,?,?] ? )
+ lexs_length lexs_lexs
-
-
-
-
-
-
- lifts ( â¬*[?] ? â¡ ? )
- lifts_lift lifts_lifts
-
-
-
-
-
-
+ syntax
+ append for local environments
+ append ( ? @@ ? )
+ append_length
-
+
- support for multiple relocation
- mr2 ( @�,?⦠⡠? )
- mr2_plus ( ? + ? )
- mr2_minus ( ? â ? â¡ ? )
- mr2_mr2
+ head equivalence for terms
+ theq ( ? ⩳[?,?] ? )
+ theq_simple theq_tdeq theq_theq theq_simple_vector
- substitution
- structural successor for closures
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠)
- fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠)
-
-
-
-
+
+ degree-based equivalence for terms
+ deq ( ? â¡[?,?] ? )
+ deq_deq
-
-
-
-
-
-
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠)
-
-
-
-
+
-
+ closures
+ cl_weight ( â¯{?,?,?} )
+
-
+
- global env. slicing
- gget ( â¬[?] ? â¡ ? )
- gget_gget
-
+
-
+ cl_restricted_weight ( â¯{?,?} )
+
-
-
-
- context-sensitive ordinary rt-substitution
- cpy ( â¦?,?⦠⢠? â¶[?,?] ? )
- cpy_lift cpy_nlift cpy_cpy
-
+
-
+ global environments
+ genv
+
-
-
-
- local env. ref. for rt-substitution
- lsuby ( ? â[?,?] ? )
- lsuby_lsuby
-
+
-
+ local environments
+ 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 ( â¬[?,?,?] ? â¡ ? )
- drop_append drop_lreq drop_drop
-
+
-
+ lenv
+
-
-
-
- basic term relocation
- lift_vector ( â¬[?,?] ? â¡ ? )
- lift_lift_vector
-
+
-
+ terms
+ term_vector ( �.? )
+
-
-
-
-
-
-
- lift ( â¬[?,?] ? â¡ ? )
- lift_neq lift_lift
-
-
-
-
+
-
-
- grammar
- equivalence for local environments
- lreq ( ? ⩬[?,?] ? )
- lreq_lreq
-
+
+ term_simple ( ðâ¦?⦠)
@@ -1257,12 +795,10 @@
- same top term structure
- tsts ( ? â ? )
- tsts_tsts tsts_vector
-
+
+ term_weight ( â¯{?} )
@@ -1271,12 +807,10 @@
- closures
- cl_weight ( â¯{?,?,?} )
- cl_restricted_weight ( â¯{?,?} )
-
+
+ term
@@ -1285,14 +819,8 @@
- internal syntax
- genv
-
-
-
-
-
-
+ items
+ item_sd
@@ -1304,22 +832,10 @@
- lenv
- lenv_weight ( â¯{?} )
- lenv_length ( |?| )
- lenv_append ( ? @@ ? )
-
-
-
-
-
-
+ item_sh
+
- term
- term_weight ( â¯{?} )
- term_simple ( ðâ¦?⦠)
- term_vector ( �.? )
@@ -1329,12 +845,6 @@
item
-
-
-
-
-
-
@@ -1343,14 +853,8 @@
- external syntax
+ atomic arities
aarity
-
-
-
-
-
-
@@ -1359,7 +863,7 @@
@@ -1384,6 +888,6 @@
-
Logical Structure of the Specification
This table reports the specification's components and their planes.
@@ -319,179 +371,51 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+
@@ -1384,6 +888,6 @@
Last update: Fri, 07 Aug 2015 14:21:47 +0200
+ Last update: Sat, 01 Apr 2017 16:50:39 +0200