- 2011 April 17. - Specification starts. + λδ version 2 is started.
Logical Structure of the Specification ![[spacer]](http://lambdadelta.info/images/b4.png "lambdadelta butterfly")
@@ -330,626 +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 ( �,?⦠⢠? ⧫* ? )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- iterated static type assignment
- lstas ( â¦?,?⦠⢠? â¢*[?,?] ? )
- lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
-
-
-
-
-
-
-
-
- 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
-
-
-
-
-
-
-
-
-
-
-
- local env. ref. for atomic arity assignment
- lsuba ( ? ⢠? â«â ? )
- lsuba_aaa lsuba_lsuba
-
-
-
-
-
-
-
-
-
-
-
- atomic arity assignment
- aaa ( â¦?,?⦠⢠? â ? )
- aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
-
-
-
-
-
-
-
-
-
-
-
- restricted local env. ref.
- lsubr ( ? â« ? )
- lsubr_lsubr
-
-
-
-
-
-
-
-
- multiple substitution
- lazy equivalence
- fleq ( â¦?,?,?⦠â¡[?] â¦?,?,?⦠)
- fleq_fleq
+ relocation
+ ranged equivalence for closures
+ freq ( �,?,?⦠⡠�,?,?⦠)
+ freq_freq
@@ -961,11 +358,9 @@
-
-
-
- lleq ( ? â¡[?,?] ? )
- lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq
+ context-sensitive free variables
+ frees ( ? ⢠ð
*�⦠⡠? )
+ frees_weight frees_lreq frees_frees
@@ -977,63 +372,11 @@
- 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
+ generic slicing for local environments
+ drops_vector ( â¬*[?,?] ? â¡ ? )
-
-
-
-
-
-
-
-
- pointwise union for local environments
- llor ( ? â[?,?] ? â¡ ? )
- llor_alt llor_drop
-
-
-
-
-
-
-
-
-
-
-
- context-sensitive exclusion from free variables
- frees ( ? ⢠? ϵ ð
*[?]�⦠)
- frees_append frees_lreq frees_lift
-
-
-
-
-
-
-
-
-
-
-
- context-sensitive multiple rt-substitution
- cpys ( â¦?,?⦠⢠? â¶*[?,?] ? )
- cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? )
- cpys_lift cpys_cpys
-
-
-
-
-
-
-
-
- iterated structural successor for closures
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠)
- fqus_alt fqus_fqus
@@ -1048,22 +391,8 @@
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠)
- fqup_fqup
-
-
-
-
-
-
-
-
-
-
-
- iterated local env. slicing
drops ( â¬*[?,?] ? â¡ ? )
- drops_drop drops_drops
+ drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops
@@ -1075,7 +404,7 @@
- generic term relocation
+ generic relocation for terms
lifts_vector ( â¬*[?] ? â¡ ? )
lifts_lift_vector
@@ -1093,7 +422,7 @@
lifts ( â¬*[?] ? â¡ ? )
- lifts_lift lifts_lifts
+ lifts_simple lifts_weight lifts_lifts
@@ -1105,135 +434,39 @@
- support for multiple relocation
- mr2 ( @�,?⦠⡠? )
- mr2_plus ( ? + ? )
- mr2_minus ( ? â ? â¡ ? )
- mr2_mr2
-
-
- substitution
- structural successor for closures
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠)
- fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- global env. slicing
- gget ( â¬[?] ? â¡ ? )
- gget_gget
-
-
-
-
-
-
-
-
-
-
-
- context-sensitive ordinary rt-substitution
- cpy ( â¦?,?⦠⢠? â¶[?,?] ? )
- cpy_lift cpy_nlift cpy_cpy
-
-
-
-
-
-
-
-
-
-
-
- local env. ref. for rt-substitution
- lsuby ( ? â[?,?] ? )
- lsuby_lsuby
-
-
-
-
-
-
-
-
-
-
-
- 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
+
-
+
-
+
- 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
+
-
+
-
+
- basic term relocation
- lift_vector ( â¬[?,?] ? â¡ ? )
- lift_lift_vector
-
-
-
-
-
-
-
-
-
-
-
- lift ( â¬[?,?] ? â¡ ? )
- lift_neq lift_lift
@@ -1243,9 +476,9 @@
grammar
- equivalence for local environments
- lreq ( ? ⩬[?,?] ? )
- lreq_lreq
+ context-sensitive equivalences for terms
+ ceq
+ ceq_ceq
@@ -1384,6 +617,6 @@
-
@@ -330,626 +343,10 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
Last update: Sun, 06 Sep 2015 21:40:58 +0200
+ Last update: Sun, 27 Mar 2016 18:42:29 +0200