\lambda\delta home page

home	news	specification	specification log		documentation	implementation
foreword	milestones	version 2	(background - syntax - core - applications)		version 2	helena	Open Symbolic Notation (OSN)
citations	visibility	version 1	(background - core)	(static HELM directory)	version 1	library	(static LDDL directory)

This is a summary of available syntactic items and reductions (block structure).

domain	block	leader	→ζ *	annotator (with →ϵ *)	applicator (with →θ *)	reference *	reduction
{X \| Γ ⊢ ⊤}	exclusion	Γ ⊢ χ	yes	no	no	no	no
{X \| Γ ⊢ X : W}	typed abstraction	Γ ⊢ λW	no	<W>	(V)	#i	→β *
{X \| Γ ⊢ X = V}	abbreviation	Γ ⊢ δV	yes	no	no	#i	→δ
no	sort	Γ ⊢ ⋆k	no	no	no	no	no

* In terms only.

Here is a numerical account of the specification's contents and its timeline.

category	objects
sizes	files	120	characters	198089	nodes	1449099
propositions	theorems	81	lemmas	618	total	699
concepts	declared	39	defined	47	total	86

This table reports the specification's components and their planes.

component	plane	files
examples	terms with special features	levels_ex0 ty3_ex1 nf2_ex2

dynamic typing	well-formed contexts	wf3_defs	wf3_props
	context ref. for native type assignment	csubt_defs	csubt_props csubt_arity_props
	native type assignment	ty3_defs	ty3_props ty3_gen ty3_gen_context ty3_gen_nf2 ty3_lift ty3_subst0 ty3_arity_props ty3_nf2_gen ty3_sred ty3_sred_props ty3_dec
equivalence	context-sensitive equivalence	pc3_defs	pc3_props pc3_gen pc3_gen_context pc3_subst0
	context-free equivalence	pc1_defs	pc1_props

computation	context ref. for reducibility	csubc_defs	csubc_props
	reducibility	sc3_defs	sc3_props sc3_arity
	strongly normalizing computation	sn3_defs	sn3_gen sn3_props
	context-sensitive computation	pr3_defs	pr3_props pr3_gen pr3_gen_context pr3_iso pr3_subst1 pr3_confluence
	context-free computation	pr1_defs	pr1_props pr1_confluence
reduction	normal forms for context-sensitive reduction	nf2_defs	nf2_props nf2_gen nf2_dec
	context-sensitive reduction	pr2_defs	pr2_gen pr2_gen_context pr2_lift pr2_subst1 pr2_confluence
	normal forms for context-free reduction		nf0_dec
	context-free reduction	wcpr0_defs
		pr0_defs	pr0_gen pr0_lift pr0_subst0 pr0_subst1 pr0_confluence
unfold	iterated static type assignment	sty1_defs	sty1_props
static typing	static type assignment	sty0_defs	sty0_props
	context ref. for binary arity assignment	csuba_defs	csuba_props
	binary arity assignment	arity_defs	arity_props arity_gen arity_subst0 arity_sred
	binary arity	levels_defs llt_defs aprem_defs
	parameters	parameter_defs
	basic context ref.	csubv_defs
multiple substitution	iterated context slicing	drop1_defs	drop1_props
	generic term relocation	lift1_defs	lift1_props
substitution	ordinary substitution	subst_defs	subst_props
		csubst1_defs	csubst1_props
		subst1_defs	subst1_gen subst1_lift subst1_subst1 subst1_confluence
	normal forms for ordinary strict substitution		dnf_dec
	ordinary strict substitution	fsubst0_defs
		csubst0_defs
		subst0_defs	subst0_gen subst0_tlt subst0_lift subst0_subst0 subst0_confluence
	basic local env. slicing	getl_defs	getl_props
		drop_defs	drop_props
	basic term relocation	lift_defs	lift_props lift_gen lift_tlt
grammar	closures	flt_defs
	contexts	contexts_defs clt_defs ctail_defs app_defs cnt_defs
	terms	tlist_defs
		terms_defs tlt_defs iso_defs