![[lambda_delta home]](http://lambda-delta.info/images/crux_32.png "lambda_delta home")
System's Syntax and Behavior
+ This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
- | category | objects | |||
| propositions | theorems | 39 | lemmas | 333 |
| concepts | declared | 33 | defined | 46 |
| domain | block | leader | applicator (with âθ)* | reduction | âζ * | reference * |
| {X | Π⢠X : W} | typed abstraction ** | Π⢠λW | âV | âβ | no | #i |
| typed declaration *** | Π⢠pλW | no | no | no | $p | |
| native type annotation * | Π⢠â£W | no | no | yes | no | |
| {X | Π⢠X = V} | local abbreviation ** | Π⢠δV | no | local âδ | yes | #i |
| global abbreviation *** | Π⢠pδV | no | global âδ | no | $p | |
| no | sort **** | Π⢠âk | no | no | no | no |
* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+
+
+ Summary of the Specification
+ Here is a numerical acount of the specification's contents
+ and its timeline.
+
+ | category | objects | |||||
| volume | files | 112 | ||||
| propositions | theorems | 45 | lemmas | 437 | total | 482 |
| concepts | declared | 32 | defined | 38 | total | 70 |
- In progress. + Context-sensitive strong normalization of simply typed terms. +
- 2012 January 27. - Support for abstract candidates of reducibility closed. + Support for abstract candidates of reducibility closed.
- 2011 September 21. - Confluence of context-sensitive parallel reduction closed. + Confluence of context-sensitive parallel reduction closed.
- 2011 September 6. - Confluence of context-free parallel reduction closed. + Confluence of context-free parallel reduction closed.
- 2011 April 17. - Specification started. + Specification started.
Logical structure of the contribution
+
+ Logical Structure of the Specification
The source files are grouped in planes and components
- according to the following table.
- The notation for the relations or functions introduced in each file
- is shown in parentheses.
+ according to the following table.
+ A notation file covering the whole specification is provided.
+ The notation for the relations or functions introduced in each file
+ is shown in parentheses.
- | component | plane | files | |||
| functional | reduction and type machine | rtm | rtm_step ( ? ⨠? ) | ||
| unfold | lift ( â[?,?] ? ) | subst ( [?â?] ? ) | |||
| examples | |||||
| native typing | nty | ||||
| conversion | context-sensitive conversion | cpcs ( ? ⢠? â¬* ? ) | |||
| computation | strongly normalizing computation | csn ( â¬* ? ) | csn_cr | csn_aaa | |
| context-sensitive computation | cprs (? ⢠? â¡* ?) | ||||
| 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 reduction | lcpr ( ? ⢠⡠? ) | |||
| cpr ( ? ⢠? ⡠? ) | cpr_lift | cpr_ltpr | cpr_cpr | ||
| context-free normal forms | twhnf ( ððð[?] ) | tnf ( ð[?] ) | tnf_tif | ||
| context-free reduction | ltpr ( ? â¡ ? ) | ltpr_ldrop | |||
| 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_lifts | 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 | ||
| term hom. | thom | thom_thom | |||
| 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 contribution
- The source files are grouped in directories, one for each
- component.
+
+
+ ![[Spacer]](http://lambda-delta.info/images/rainbow.png "lambda_delta rainbow rule")
![[Valid XHTML 1.1]](http://www.w3.org/Icons/valid-xhtml11-blue "Valid XHTML 1.1")
![[Valid CSS level 2]](http://www.w3.org/Icons/valid-css2-blue "Valid CSS level 2")
![[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")
| component | plane | files | ||||||
| examples | ||||||||
| native typing | nty | |||||||
| equivalence | context-sensitive equivalence | cpcs ( ? ⢠? â¬* ? ) | ||||||
| conversion | context-sensitive conversion | cpc ( ? ⢠? ⬠? ) | cpc_cpc | |||||
| computation | strongly normalizing computation | csn_vector ( â¬* ? ) | csn_lcpr_vector | csn_aaa | ||||
| csn ( â¬* ? ) | csn_lift | csn_cpr | csn_cprs ( â¬** ? ) | csn_lcpr | ||||
| context-sensitive computation | lcprs ( ? ⢠â¡* ? ) | lcprs_cprs | lcprs_lcprs | |||||
| cprs (? ⢠? â¡* ?) | cprs_lift | 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_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 | |||||
| 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_lifts | 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 |
Physical Structure of the Specification
+ The source files are grouped in directories,
+ one for each component.
- Last update: 2012-02-01+01:00
+ Last update: 2012-03-09+01:00