| component | plane | files | |||||||||
| dynamic typing | stratified native validity | snv ( �,?⦠⩠? :[?] ) | snv_lift | snv_aaa | |||||||
| equivalence | context-sensitive equivalence | lfpcs ( â¦?⦠â¬* â¦?⦠) | lfpcs_aaa | lfpcs_lfprs | lfpcs_lfpcs | ||||||
| cpcs ( ? ⢠? â¬* ? ) | cpcs_ltpss | cpcs_delift | cpcs_aaa | cpcs_ltpr | cpcs_cprs | cpcs_cpcs | |||||
| conversion | context-sensitive conversion | lfpc ( �⦠⬠�⦠) | lfpc_lfpc | ||||||||
| cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||||||||
| computation | extended computation | xprs ( â¦?,?⦠⢠? â¸*[?] ? ) | xprs_lift | xprs_aaa | xprs_cprs | ||||||
| weakly normalizing computation | cpe ( ? ⢠â¡* ðâ¦?⦠) | cpe_cpe | |||||||||
| strongly normalizing computation | csn_vector ( ? ⢠â¬* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa | |||||||
| csn ( ? ⢠â¬* ? ) | csn_alt ( ? ⢠â¬â¬* ? ) | csn_lift | csn_cpr | csn_lfpr | |||||||
| context-sensitive computation | lfprs ( â¦?⦠â¡* â¦?⦠) | lfprs_aaa | lfprs_cprs | lfprs_lfprs | |||||||
| cprs (? ⢠? â¡* ?) | cprs_lift | cprs_delift | cprs_aaa | cprs_ltpr | cprs_lfpr | cprs_cprs | cprs_lfprs | cprs_tstc | cprs_tstc_vector | ||
| context-free computation | ltprs ( ? â¡* ? ) | ltprs_alt ( ? â¡â¡* ? ) | ltprs_ldrop | ltprs_ltprs | |||||||
| tprs ( ? â¡* ?) | tprs_lift | tprs_tprs | |||||||||
| local env. ref. for abstract candidates of reducibility | lsubc ( ? â[?] ? ) | lsubc_ldrop | lsubc_ldrops | lsubc_lsuba | |||||||
| support for abstract computation properties | acp | acp_cr ( â¦?,?⦠ϵ[?] ã?ã ) | acp_aaa | ||||||||
| reducibility | extended reduction | xpr ( â¦?,?⦠⢠? â¸[?] ? ) | xpr_lift | xpr_aaa | |||||||
| context-sensitive focalized reduction | cfpr ( ? ⢠�,?⦠⡠�,?⦠) | cnfpr_ltpss | cfpr_aaa | cfpr_cpr | |||||||
| context-free focalized reduction | lfpr ( â¦?⦠⡠â¦?⦠) | lfpr_aaa | lfpr_cpr | lfpr_fpr | lfpr_lfpr | lfpr_alt ( â¦?⦠â¡â¡ â¦?⦠) | |||||
| fpr ( �,?⦠⡠�,?⦠) | fpr_cpr | ||||||||||
| context-sensitive normal forms | cnf ( ? ⢠ðâ¦?⦠) | cnf_lift | cnf_cif | ||||||||
| context-sensitive reduction | cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_tpss | cpr_ltpss | cpr_delift | cpr_aaa | cpr_ltpr | cpr_cpr | |||
| context-sensitive reducible forms | crf ( ? ⢠ðâ¦?⦠) | crf_append | cif ( ? ⢠ðâ¦?⦠) | cif_append | |||||||
| context-free normal forms | thnf ( ððâ¦?⦠) | ||||||||||
| context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | ltpr_ltpss_dx | ltpr_ltpss_sn | ltpr_aaa | ltpr_ltpr | ||||
| tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_delift | tpr_tpr | |||||||
| unwind | |||||||||||
| static typing | local env. ref. for stratified static type assignment | lsubss ( ? ââ ? ) | lsubss_ldrop | lsubss_ssta | lsubss_lsubss | ||||||
| stratified static type assignment | ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) | ssta_lift | ssta_ltpss_dx | ssta_ltpss_sn | 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_ltpss_dx | aaa_ltpss_sn | aaa_aaa | |||||
| parameters | sh | sd | |||||||||
| unfold | basic local env. thinning | thin ( ? â¼*[?,?] â¡ ? ) | thin_ldrop | thin_delift | |||||||
| inverse basic term relocation | delift ( ? ⢠? â¼*[?,?] â¡ ? ) | delift_alt ( ? ⢠? â¼â¼*[?,?] â¡ ? ) | delift_lift | delift_tpss | delift_ltpss | delift_delift | |||||
| partial unfold | ltpss_sn ( ? ⢠â¶*[?,?] ? ) | ltpss_sn_ldrop | ltpss_sn_tps | ltpss_sn_tpss | ltpss_sn_ltpss_sn | ltpss_sn_alt ( ? ⢠â¶â¶*[?,?] ? ) | |||||
| ltpss_dx ( ? â¶*[?,?] ? ) | ltpss_dx_ldrop | ltpss_dx_tps | ltpss_dx_tpss | ltpss_dx_ltpss_dx | |||||||
| tpss ( ? ⢠? â¶*[?,?] ? ) | tpss_alt ( ? ⢠? â¶â¶*[?,?] ? ) | tpss_lift | tpss_tpss | ||||||||
| generic local env. slicing | ldrops ( â©*[?] ? â¡ ? ) | 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 | |||||||
| substitution | parallel substitution | tps ( ? ⢠? â¶[?,?] ? ) | tps_lift | tps_tps | |||||||
| global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | |||||||||
| basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_append | ldrop_lpx | ldrop_sfr | ldrop_ldrop | ||||||
| local env. ref. for substitution | lsubs ( ? â¼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( â½[?,?] ? ) | ||||||||
| 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_bi | ||||||
| term | term_weight ( #{?} ) | term_simple ( ðâ¦?⦠) | term_vector | ||||||||
| item | |||||||||||
| external syntax | aarity |
| component | plane | files | ||||
| dynamic typing | stratified native validity | snv ( �,?⦠⩠? :[?] ) | snv_lift snv_aaa | |||
| equivalence | focalized equivalence | lfpcs ( â¦?⦠â¬* â¦?⦠) | lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs | |||
| context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) | cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs | ||||
| conversion | focalized conversion | lfpc ( �⦠⬠�⦠) | lfpc_lfpc | |||
| context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||
| computation | extended computation | xprs ( â¦?,?⦠⢠? â¸*[?] ? ) | xprs_lift xprs_aaa xprs_cprs | |||
| weakly normalizing computation | cpe ( ? ⢠â¡* ðâ¦?⦠) | cpe_cpe | ||||
| strongly normalizing computation | csn_vector ( ? ⢠â¬* ? ) | csn_cpr_vector csn_tstc_vector csn_aaa | ||||
| csn ( ? ⢠â¬* ? ) | csn_alt ( ? ⢠â¬â¬* ? ) | csn_lift csn_cpr csn_lfpr | ||||
| focalized computation | lfprs ( â¦?⦠â¡* â¦?⦠) | lfprs_aaa lfprs_cprs lfprs_lfprs | ||||
| context-sensitive computation | cprs (? ⢠? â¡* ?) | cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector | ||||
| context-free computation | ltprs ( ? â¡* ? ) | ltprs_alt ( ? â¡â¡* ? ) | ltprs_ldrop ltprs_ltprs | |||
| tprs ( ? â¡* ?) | tprs_lift tprs_tprs | |||||
| local env. ref. for abstract candidates of reducibility | lsubc ( ? â[?] ? ) | lsubc_ldrop lsubc_ldrops lsubc_lsuba | ||||
| support for abstract computation properties | acp | acp_cr ( â¦?,?⦠ϵ[?] ã?ã ) | acp_aaa | |||
| reducibility | extended reduction | xpr ( â¦?,?⦠⢠? â¸[?] ? ) | xpr_lift xpr_aaa | |||
| context-sensitive focalized reduction | cfpr ( ? ⢠�,?⦠⡠�,?⦠) | cnfpr_ltpss cfpr_aaa cfpr_cpr | ||||
| context-free focalized reduction | lfpr ( â¦?⦠⡠â¦?⦠) | lfpr_alt ( â¦?⦠â¡â¡ â¦?⦠) | lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr | |||
| fpr ( �,?⦠⡠�,?⦠) | fpr_cpr | |||||
| context-sensitive normal forms | cnf ( ? ⢠ðâ¦?⦠) | cnf_lift cnf_cif | ||||
| context-sensitive reduction | cpr ( ? ⢠? ⡠? ) | cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr | ||||
| context-sensitive reducible forms | crf ( ? ⢠ðâ¦?⦠) | crf_append | cif ( ? ⢠ðâ¦?⦠) | cif_append | ||
| context-free normal forms | thnf ( ððâ¦?⦠) | |||||
| context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr | ||||
| tpr ( ? â¡ ? ) | tpr_lift tpr_tpss tpr_delift tpr_tpr | |||||
| unwind | ||||||
| static typing | local env. ref. for stratified static type assignment | lsubss ( ? ââ ? ) | lsubss_ldrop lsubss_ssta lsubss_lsubss | |||
| stratified static type assignment | ssta ( â¦?,?⦠⢠? â¢[?,?] ? ) | ssta_lift ssta_ltpss_dx ssta_ltpss_sn 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_ltpss_dx aaa_ltpss_sn aaa_aaa | ||||
| parameters | sh | sd | ||||
| unfold | basic local env. thinning | thin ( ? â¼*[?,?] â¡ ? ) | thin_ldrop thin_delift | |||
| inverse basic term relocation | delift ( ? ⢠? â¼*[?,?] â¡ ? ) | delift_alt ( ? ⢠? â¼â¼*[?,?] â¡ ? ) | delift_lift delift_tpss delift_ltpss delift_delift | |||
| partial unfold | ltpss_sn ( ? ⢠â¶*[?,?] ? ) | ltpss_sn_alt ( ? ⢠â¶â¶*[?,?] ? ) | ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn | |||
| ltpss_dx ( ? â¶*[?,?] ? ) | ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx | |||||
| tpss ( ? ⢠? â¶*[?,?] ? ) | tpss_alt ( ? ⢠? â¶â¶*[?,?] ? ) | tpss_lift | tpss_tpss | |||
| generic local env. slicing | ldrops ( â©*[?] ? â¡ ? ) | 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 | ||
| substitution | parallel substitution | tps ( ? ⢠? â¶[?,?] ? ) | tps_lift tps_tps | |||
| global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | ||||
| basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop | ||||
| local env. ref. for substitution | lsubs ( ? â¼[?,?] ? ) | (lsubs_lsubs) | lsubs_sfr ( â½[?,?] ? ) | |||
| 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_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.
- ![[Spacer]](http://lambda-delta.info/images/rainbow.png "lambda_delta rainbow rule")
![[Generated from XML via XSL]](http://lambda-delta.info/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://lambda-delta.info/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")
Last update: 2012-10-13T23:29:26+02:00
+ Last update: 2012-10-15T17:11:10+02:00