cic:/matita/lambda_delta/basic_2/ (λδ version 2)
System's Syntax and Behavior
This is a summary of the "block structure"
of the System's syntactic items and reductions.
| 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 |
|
|
|
|
|
| sizes | files | 116 | bytes | 428758 |
|
|
| propositions | theorems | 46 | lemmas | 453 | total | 499 |
| concepts | declared | 31 | defined | 40 | total | 71 |
- In progress.
Context-sensitive subject equivalence
for native type assignment.
- In progress.
Context-sensitive subject equivalence
for atomic arity assignment.
- 2012 March 15.
Context-sensitive strong normalization
for simply typed terms.
- 2012 January 27.
Support for abstract candidates of reducibility.
- 2011 September 21.
Confluence for context-sensitive parallel reduction.
- 2011 September 6.
Confluence for context-free parallel reduction.
- 2011 April 17.
Specification starts.
Logical Structure of the Specification
The source files are grouped in planes and components
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 (? are placeholders).
| component | plane | files |
|
|
|
|
|
|
|
| examples |
|
|
|
|
|
|
|
|
|
| native typing |
| nty |
|
|
|
|
|
|
|
| equivalence | context-sensitive equivalence | 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_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_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-03-17+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")