applications of lambda_delta version 2

From: Ferruccio Guidi Date: Fri, 24 Feb 2012 16:27:56 +0000 (+0000) Subject: - we added a web page (Apps_2) for the checked applications of Basic_2 X-Git-Tag: make_still_working~1939 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ff11fcced84c3e18f0f73be101bc7b2086fc0a52;p=helm.git - we added a web page (Apps_2) for the checked applications of Basic_2 - we added some files to Basic_2 - we improved the Makefiles --- diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile b/helm/www/lambda_delta/bin/xhtbl/Makefile index 79a056af5..df0833cca 100644 --- a/helm/www/lambda_delta/bin/xhtbl/Makefile +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile @@ -17,18 +17,20 @@ LDSRCDIR = ../../etc/lambda_delta/ HOMEDIR = ../../ TBLDIRS = $(SRCDIR) $(LDSRCDIR) +LDWS = $(shell find $(SRCDIR) -name "*.ldw.xml") TBLS = $(shell find $(TBLDIRS) -name "*.tbl") XSLS = xhtbl.xsl $(patsubst %.tbl, %.xsl, $(notdir $(TBLS))) +HTMLS = $(patsubst %.ldw.xml, $(HOMEDIR)%.html, $(notdir $(LDWS))) LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl -%.html: BASEURL = --stringparam baseurl $(LDURL) +$(HOMEDIR)%.html: BASEURL = --stringparam baseurl $(LDURL) -www: $(HOMEDIR)ld_basic_2.html +www: $(HTMLS) $(XSLS:%=$(XSLDIR)%): $(TBLS) $(XHTBL) @echo " XHTBL *.tbl" $(H)$(XHTBL) -O $(XSLDIR) $(TBLS) -$(HOMEDIR)ld_basic_2.html: $(SRCDIR)ld_basic_2.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%) +$(HOMEDIR)%.html: $(SRCDIR)%.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%) @echo " XSLT $(notdir $<)" $(H)$(XSLT) -o $@ $(BASEURL) $(XSLDIR)ld_web.xsl $< diff --git a/helm/www/lambda_delta/ld_apps_2.html b/helm/www/lambda_delta/ld_apps_2.html new file mode 100644 index 000000000..8558d5862 --- /dev/null +++ b/helm/www/lambda_delta/ld_apps_2.html @@ -0,0 +1,62 @@ + + + + + + + + + + applications of lambda_delta version 2 + + + + + +

cic:/matita/lambda_delta/Apps_2/ (applications of Î»Î´ version 2)

Contents of the Specification

This specification comprises a collection of checked + applications of Î»Î´ version 2. + In particular it contains the components below. +

MLTT1. + Martin-LÃ¶f's Type Theory with one universe + using Î»Î´ as the theory of expressions. +

Functional. + The validation algorithm for Î»Î´ as implemented in + Helena 0.8. +

+ +

Summary of the Specification

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

category	objects
propositions	theorems	4	lemmas	1	total	5
concepts	declared	3	defined	10	total	13

2012 February 24. + The Applications directory is started. +

2011 December 20. + The Functional component is started + inside the specification of Î»Î´ version 2. +

2011 December 12. + The MLTT1 component is started. +

+ +

Logical Structure of the Specification

The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses. +

component	plane	files
MLTT1		genv_primitive	judgement
functional	reduction and type machine	rtm	rtm_step ( ? â¨ ? )
	unfold	lift ( â[?,?] ? )	subst ( [?â?] ? )

+ +

Physical Structure of the Specification

The source files are grouped in directories, + one for each component. +

Last update: 2012-02-24+01:00

+ + diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 030109a2f..5d9118e0d 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -16,48 +16,49 @@

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. + 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. + ** 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. + and its timeline.

category	objects
propositions	theorems	46	lemmas	405
concepts	declared	35	defined	49

category	objects
propositions	theorems	43	lemmas	409	total	452
concepts	declared	32	defined	35	total	67

In progress. - Context-sensitive strong normalization of simply typed terms. + Context-sensitive strong normalization of simply typed terms.

2012 January 27. - Support for abstract candidates of reducibility closed. + Support for abstract candidates of reducibility closed.

2011 September 21. - Confluence of context-sensitive parallel reduction closed. + Confluence of context-sensitive parallel reduction closed.

2011 September 6. - Confluence of context-free parallel reduction closed. + Confluence of context-free parallel reduction closed.

2011 April 17. - Specification started. + 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. + 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
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

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_lcpr	cprs_cprs	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
	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. +

The source files are grouped in directories, + one for each component.

Last update: 2012-02-20+01:00

Last update: 2012-02-24+01:00

diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html index a1c4024ec..aecc87973 100644 --- a/helm/www/lambda_delta/news.html +++ b/helm/www/lambda_delta/news.html @@ -61,11 +61,14 @@ December 2012.

April 2011. The -specification of Î»Î´ version 2 is restarted in Matita 0.5.

Here is a page about the -specification.
+specification (Core).
+
Here is a page about the +topics related to the specification (Applications).

@@ -90,10 +93,7 @@ started.

June 2009. Helena, a validator for Î»Î´ version 2, is + href="implementation.html#helena">validator for Î»Î´ version 2, is available as a @@ -253,7 +253,7 @@ gives this site as the first result.

Ferruccio +Last update 2012-02-24 by

Ferruccio Guidi

diff --git a/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml new file mode 100644 index 000000000..425421933 --- /dev/null +++ b/helm/www/lambda_delta/web/home/ld_apps_2.ldw.xml @@ -0,0 +1,52 @@ + + + +

Contents of the Specification

+ This specification comprises a collection of checked + applications of Î»Î´ version 2. + In particular it contains the components below. + + + Martin-LÃ¶f's Type Theory with one universe + using Î»Î´ as the theory of expressions. + + + The validation algorithm for Î»Î´ as implemented in + Helena 0.8. + + +

Summary of the Specification

+ Here is a numerical acount of the specification's contents + and its timeline. + + + + The Applications directory is started. + + + The Functional component is started + inside the specification of Î»Î´ version 2. + + + The MLTT1 component is started. + + +

Logical Structure of the Specification

+ The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses. + +

+ +

Physical Structure of the Specification

+ The source files are grouped in directories, + one for each component. + +

+ * 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. - - - - Context-sensitive strong normalization of simply typed terms. - - - Support for abstract candidates of reducibility closed. - - - Confluence of context-sensitive parallel reduction closed. - - - Confluence of context-free parallel reduction closed. - - - Specification started. - +

Summary of the Specification

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

+ + Context-sensitive strong normalization of simply typed terms. + + + Support for abstract candidates of reducibility closed. + + + Confluence of context-sensitive parallel reduction closed. + + + Confluence of context-free parallel reduction closed. + + + 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. - - +

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. + +

- Physical Structure of the Specification - The source files are grouped in directories, one for each - component. - - - +

Physical Structure of the Specification

+ The source files are grouped in directories, + one for each component. + + + + @@ -22,6 +24,8 @@ + + @@ -29,7 +33,9 @@ - + + +

objects
theorems	0	lemmas	23	total	23
declared	22	defined	8	8	total	30

diff --git a/helm/www/lambda_delta/xslt/ld_web_root.xsl b/helm/www/lambda_delta/xslt/ld_web_root.xsl index 1375316f8..2920bc657 100644 --- a/helm/www/lambda_delta/xslt/ld_web_root.xsl +++ b/helm/www/lambda_delta/xslt/ld_web_root.xsl @@ -20,6 +20,12 @@ + + + + + +