cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
Logical structure of the contribution
The source files are grouped in planes and components
according to the following table.
The notation for the relation or function 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 (? ⊢ ? ➡* ?) |
|
|
|
| support for abstract computation properties | lsubc ( ? [?] ⊑ ? ) | lsubc_ldrop | lsubc_ldrops |
|
|
| acp | acp_cr ( ⦃?,?⦄ ϵ 〚?〛 ) | acp_aaa |
|
| reducibility | context-sensitive reduction | lcpr ( ? ⊢ ➡ ? ) |
|
|
|
|
| cpr ( ? ⊢ ? ➡ ? ) | cpr_lift | cpr_ltpr | cpr_cpr |
| context-free normal forms | twhnf | tnf |
|
|
| context-free reduction | ltpr ( ? ➡ ? ) | ltpr_ldrop |
|
|
|
| tpr ( ? ➡ ? ) | tpr_lift | tpr_tpss | tpr_tpr |
| context-free reducible forms | trf |
|
|
|
| static typing | static type ass. | sty | sty_lift | sty_sty |
|
| atomic arity ass. | aaa ( ? ⊢ ? ÷ ? ) | aaa_lift | 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_ldrops |
|
|
| generic relocation | lifts ( ⇧*[?] ? ≡ ? ) | lifts_lifts | lifts_vector |
|
| substitution | parallel substitution | ltps ( ? [?,?] ▶ ? ) | ltps_ldrop | ltps_tps | ltps_ltps |
|
| tps ( ? ⊢ ? [?,?] ▶ ? ) | tps_lift | tps_tps |
|
| global env. slicing | gdrop ( ⇩[?] ? ≡ ? ) | gdrop_gdrop |
|
|
| local env. slicing | ldrop ( ⇩[?,?] ? ≡ ? ) | ldrop_ldrop |
|
|
| term relocation | lift ( ⇧[?,?] ? ≡ ? ) | lift_lift | lift_vector |
|
| 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.
Last update: 2012-01-08+01:00
![[lambda_delta home]](http://lambda-delta.info/images/crux_32.png "lambda_delta home")
![[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")