- 2012 April 16. Context-sensitive subject equivalence for atomic arity assignment.
| component | plane | files | |||||||
| examples | |||||||||
| native typing | nty | ||||||||
| equivalence | context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) | cpcs_cprs | cpcs_cpcs | |||||
| conversion | context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc | ||||||
| computation | weakly normalizing computation | cpe ( ? ⢠? ⢠â¡* ð[?] ) | cpe_cpe | ||||||
| strongly normalizing computation | csn_vector ( â¬* ? ) | csn_cpr_vector | csn_tstc_vector | csn_aaa | |||||
| csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr | |||||
| context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_aaa | lcprs_cprs | lcprs_lcprs | |||||
| cprs (? ⢠? â¡* ?) | cprs_lift | cprs_ltpr | cprs_lcpr | cprs_cprs | cprs_lcprs | cprs_tstc | cprs_tstc_vector | ||
| 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 | context-sensitive normal forms | cnf ( ? ⢠ð[?] ) | cnf_lift | ||||||
| context-sensitive reduction | lcpr ( ? ⢠⡠? ) | lcpr_aaa | lcpr_cpr | ||||||
| cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_ltpss | cpr_ltpr | cpr_cpr | |||||
| context-free normal forms | twhnf ( ððð[?] ) | tnf ( ð[?] ) | tnf_tif | ||||||
| context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | ltpr_aaa | |||||
| tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_tpr | ||||||
| context-free reducible forms | trf ( ð[?] ) | tif ( ð[?] ) | |||||||
| static typing | static type assignment | sty | sty_lift | sty_sty | |||||
| local env. ref. for atomic arity assignment | lsuba ( ? ։ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | |||||
| atomic arity assignment | aaa ( ? ⢠? ÷ ? ) | aaa_lift | aaa_ltps | aaa_lifts | aaa_ltpss | aaa_aaa | |||
| parameters | sh | ||||||||
| unfold | term inverse relocation | delift ( ? ⢠? [?,?] ⡠? ) | delift_lift | ||||||
| partial unfold | ltpss ( ? [?,?] â¶* ? ) | ltpss_ldrop | ltpss_tps | ltpss_ltpss | |||||
| tpss ( ? ⢠? [?,?] â¶* ? ) | tpss_lift | tpss_tpss | tpss_ltps | ||||||
| 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 | ltps ( ? [?,?] ⶠ? ) | ltps_ldrop | ltps_tps | ltps_ltps | ||||
| tps ( ? ⢠? [?,?] ⶠ? ) | tps_lift | tps_tps | |||||||
| global env. slicing | gdrop ( â©[?] ? â¡ ? ) | gdrop_gdrop | |||||||
| basic local env. slicing | ldrop ( â©[?,?] ? â¡ ? ) | ldrop_ldrop | |||||||
| basic term relocation | lift_vector ( â§[?,?] ? â¡ ? ) | lift_lift_vector | |||||||
| lift ( â§[?,?] ? â¡ ? ) | lift_lift | ||||||||
| grammar | local env. ref. for substitution | lsubs ( ? [?,?] â¼ ? ) | lsubs_lsubs | ||||||
| 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 ( |?| ) | |||||||
| term | term_weight ( #[?] ) | term_simple ( ð[?] ) | term_vector | ||||||
| item | |||||||||
| external syntax | aarity |
| component | plane | files | ||||||||
| examples | ||||||||||
| dynamic typing | native type assignment | nta ( �,?⦠⢠? : ? ) | nta_alt ( �,?⦠⢠? :: ? ) | nta_lift | nta_delift | nta_sta | nta_nta | |||
| equivalence | context-sensitive equivalence | lcpcs ( ? ⢠â¬* ? ) | lcpcs_aaa | lcpcs_lcprs | lcpcs_lcpcs | |||||
| cpcs ( ? ⢠? â¬* ? ) | cpcs_delift | cpcs_cprs | cpcs_cpcs | |||||||
| conversion | context-sensitive conversion | lcpc ( ? ⢠⬠? ) | lcpc_lcpc | |||||||
| cpc ( ? ⢠? ⬠? ) | cpc_cpc | |||||||||
| computation | 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_lcpr | ||||||
| context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_aaa | lcprs_cprs | lcprs_lcprs | ||||||
| cprs (? ⢠? â¡* ?) | cprs_lift | cprs_delift | cprs_ltpr | cprs_lcpr | cprs_cprs | cprs_lcprs | cprs_tstc | cprs_tstc_vector | ||
| 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 | context-sensitive normal forms | cnf ( ? ⢠ð[?] ) | cnf_lift | |||||||
| context-sensitive reduction | lcpr ( ? ⢠⡠? ) | lcpr_aaa | lcpr_cpr | lcpr_lcpr | ||||||
| cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_ltpss | cpr_delift | cpr_ltpr | cpr_cpr | |||||
| context-free normal forms | twhnf ( ððð[?] ) | tnf ( ð[?] ) | tnf_tif | |||||||
| context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | ltpr_tps | ltpr_ltpss | ltpr_aaa | ltpr_ltpr | ||||
| tpr ( ? â¡ ? ) | tpr_lift | tpr_tpss | tpr_delift | tpr_tpr | ||||||
| context-free reducible forms | trf ( ð[?] ) | tif ( ð[?] ) | ||||||||
| static typing | static type assignment | sta ( �,?⦠⢠? ⢠? ) | sta_lift | sta_sta | ||||||
| local env. ref. for atomic arity assignment | lsuba ( ? ââ ? ) | lsuba_ldrop | lsuba_aaa | lsuba_lsuba | ||||||
| atomic arity assignment | aaa ( ? ⢠? â ? ) | aaa_lift | aaa_lifts | aaa_ltpss | aaa_aaa | |||||
| parameters | sh | |||||||||
| 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 ( ? â¶*[?,?] ? ) | ltpss_ldrop | ltpss_tps | ltpss_tpss | ltpss_ltpss | |||||
| 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_ldrop | ldrop_sfr | |||||||
| 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 ( |?| ) | ||||||||
| 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-03-30+02:00
+ Last update: 2012-05-16+02:00