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 |
|
|
|
propositions | theorems | 46 | lemmas | 405 |
concepts | declared | 35 | defined | 49 |
- In progress.
Context-sensitive strong normalization of simply typed terms.
- 2012 January 27.
Support for abstract candidates of reducibility closed.
- 2011 September 21.
Confluence of context-sensitive parallel reduction closed.
- 2011 September 6.
Confluence of context-free parallel reduction closed.
- 2011 April 17.
Specification started.
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.
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_vector ( ⬇* ? ) | csn_cr | csn_aaa |
|
|
|
| csn ( ⬇* ? ) | csn_lift | csn_cpr | csn_cprs ( ⬇** ? ) | csn_lcpr |
| context-sensitive computation | cprs (? ⊢ ? ➡* ?) | cprs_lcpr | cprs_cprs | cprs_tstc |
|
| 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 |
|
|
|
| term hom. | thom ( ? ≈ ? ) | thom_thom |
|
|
|
| same top term constructor | tstc ( ? ≃ ? ) | tstc_tstc |
|
|
|
| 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-20+01:00