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.
-
component
plane
files
examples
native typing
nty
conversion
context-sensitive
cpcs
computation
strongly normalizing
csn
context-sensitive
cprs
reducibility
context-sensitive reduction
lcpr
cpr
cpr_lift
cpr_ltpr
cpr_cpr
context-free normal forms
tnf
context-free reduction
ltpr
ltpr_ldrop
tpr
tpr_lift
tpr_tpss
tpr_tpr
context-free reducible forms
trf
static typing
atomic arity ass.
aaa
aaa_lift
aaa_aaa
static type ass.
sty
sty_lift
sty_sty
unfold
partial
ltpss
ltpss_ldrop
ltpss_tps
ltpss_ltpss
tpss
tpss_lift
tpss_tpss
tpss_ltps
substitution
parallel
ltps
ltps_ldrop
ltps_tps
ltps_ltps
tps
tps_lift
tps_tps
local env. dropping
ldrop
ldrop_ldrop
term relocation
lift
lift_lift
grammar
local env. ref. for substitution
lsubs
lsubs_lsubs
term hom.
thom
thom_thom
closures
cl_shift
cl_weight
internal syntax
lenv
lenv_weight
lenv_length
term
term_weight
term_simple
item
external syntax
aarity
parameters
sh
-
Physical structure of the contribution
-
The source files are grouped in directories, one for each component.
-
+
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
43
lemmas
422
total
465
concepts
declared
32
defined
35
total
67
+
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.
+ 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
examples
native typing
nty
conversion
context-sensitive conversion
cpcs ( ? ⢠? â¬* ? )
computation
strongly normalizing computation
csn_vector ( â¬* ? )
csn_lcpr_vector
csn_aaa
csn ( â¬* ? )
csn_lift
csn_cpr
csn_cprs ( â¬** ? )
csn_lcpr
context-sensitive computation
cprs (? ⢠? â¡* ?)
cprs_lift
cprs_lcpr
cprs_cprs
cprs_tstc
cprs_tstc_vector
local env. ref. for abstract candidates of reducibility