cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
-
Logical structure of the contribution
+
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 ( â¬* ? )
csn_cr
csn_aaa
context-sensitive computation
cprs (? ⢠? â¡* ?)
local env. ref. for abstract candidates of reducibility