BTM

This table shows how the first 45 positive integers + +

cic:/matita/BTM/

Character classes

This table shows how the first 45 positive integers are distributed in the four classes.

class	contents
p		1	4	7	10	13	16	19	22	25	28	31	34	37	40	43
q		5	11	15	17	23	29	33	35	41	45
s		2	6	8	14	18	20	24	26	32	38	42	44
t		3	9	12	21	27	30	36	39

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

class	contents	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +	+ +
p	+ +	1	4	7	10	13	16	19	22	25	28	31	34	37	40	43
q	+ +	5	11	15	17	23	29	33	35	41	45	+ +	+ +	+ +	+ +	+ +
s	+ +	2	6	8	14	18	20	24	26	32	38	42	44	+ +	+ +	+ +
t	+ +	3	9	12	21	27	30	36	39	+ +	+ +	+ +	+ +	+ +	+ +	+ +

Last update: 2013-03-09T23:27:52+01:00

+
+

+ +

+ + +

+ +

+
+

Last update: Mon, 11 Mar 2013 13:47:08 +0100

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 0da13bb38..3a34b41d8 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -6,7 +6,6 @@ TAGS = www up \ install-jed install-bib \ LDURL = http://lambdadelta.info/ -LDDLURL = $(LDURL)static/lddl HOMEDIR = . ETCDIR = etc @@ -44,10 +43,25 @@ XMLS = brg_si/grundlagen/l/not.ld.xml \ LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl XMLLINT = xmllint --noout -XSLT = xsltproc +XSLT = xalan XHTBL = $(XHTBLDIR)/xhtbl.native -%.html: BASEURL = --stringparam baseurl $(LDURL) +ifeq ($(XSLT), xsltproc) + XSLT_PARAM := --param + XSLT_OUT := -o + XSLT_XSL := + XSLT_IN := +endif + +ifeq ($(XSLT), xalan) + XSLT_PARAM := -param + XSLT_OUT := -out + XSLT_XSL := -xsl + XSLT_IN := -in + XSLT += -indent 2 +endif + +XSLT += $(XSLT_PARAM) baseurl '"$(LDURL)"' $(XSLT_PARAM) date '"$(shell date -R)"' define HTML_TEMPLATE HTML_$(2) = $$(HOMEDIR)/$(2).html @@ -55,7 +69,7 @@ define HTML_TEMPLATE $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%) @echo " XSLT $$(notdir $$<)" - $$(H)$$(XSLT) -o $$@ $$(BASEURL) $$(XSLTDIR)/ld_web.xsl $$< + $$(H)$$(XSLT) $$(XSLT_OUT) $$@ $$(XSLT_XSL) $$(XSLTDIR)/ld_web.xsl $$(XSLT_IN) $$< endef ifeq ($(MAKECMDGOALS), www) @@ -114,12 +128,10 @@ up: @echo " UPDATE $(REMOTE):$(RDIR)" $(H)ssh $(REMOTE) "svn up $(RDIR)" -%.ld: BASEURL = --stringparam baseurl $(LDDLURL) - %.ld: @echo " XSLT $@" $(H)mkdir -p $(HTMLDIR)/$(@D) - $(H)$(XSLT) -o $(HTMLDIR)/$@.html $(BASEURL) $(XSLTDIR)/lddl.xsl $(XMLDIR)/$@.xml + $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml %.ldc: @echo " SKIP $@" diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 20e4c26bd..975779b5b 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,62 +1,196 @@ - + - - - - - + + + + + applications of lambdadelta version 2 - - - - + + + + -

cic:/matita/lambdadelta/apps_2/ (applications of Î»Î´ version 2)

Contents of the Specification

This specification comprises a collection of checked + +

+ +

cic:/matita/lambdadelta/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. + In particular it contains the components below.

MLTT1. +
- + MLTT1. Martin-LÃ¶f's Type Theory with one universe - using Î»Î´ as theory of expressions. -
-
- Functional. + using Î»Î´ as 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 + Helena 0.8. +

+ +

Summary of the Specification

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

category	objects
sizes	files	5	characters	5613	nodes	9842
propositions	theorems	4	lemmas	1	total	5
concepts	declared	3	defined	10	total	13

2012 February 24. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	5	characters	5613	nodes	+
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. +

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

2011 December 12. + 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 +

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 (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).

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

+ + + + + + + + + + + + + + + + + + + + + + + + + + +

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

Physical Structure of the Specification

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

Last update: 2013-03-09T23:27:52+01:00

+
+

+ +

+ + +

+ +

+
+

Last update: Mon, 11 Mar 2013 13:47:08 +0100

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3955a0574..eb181a3ee 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,1374 @@ - + - - - - - + + + + + lambdadelta version 2 - - - - + + + + -

cic:/matita/lambdadelta/basic_2/ (Î»Î´ version 2)

System's Syntax and Behavior

This is a summary of the "block structure" + +

+ +

cic:/matita/lambdadelta/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}	local typed abstraction *	Î â¢ +Î»W	âV	âÎ²	no	#i
	local typed declaration **	Î â¢ -Î»W	âV	âÎ²	no	#i
	global 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
	local definition **	Î â¢ -Î´V	no	local âÎ´	no	#i
	global definition ***	Î â¢ pÎ´V	no	global âÎ´	no	$p
no	sort ****	Î â¢ âk	no	no	no	no

* In terms only. - ** In terms and local environments only. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

domain	block	leader	applicator (with âÎ¸)*	reduction	âÎ¶ *	reference *
{X \| Î â¢ X : W}	local typed abstraction *	Î â¢ +Î»W	âV	âÎ²	no	#i
+ +	local typed declaration **	Î â¢ -Î»W	âV	âÎ²	no	#i
+ +	global 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
+ +	local definition **	Î â¢ -Î´V	no	local âÎ´	no	#i
+ +	global definition ***	Î â¢ 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. + **** Sort level k in terms only.

- -

Summary of the Specification

Here is a numerical acount of the specification's contents + +

Summary of the Specification

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

category	objects
sizes	files	252	characters	483454	nodes	1296744
propositions	theorems	85	lemmas	1119	total	1204
concepts	declared	46	defined	82	total	128

In progress. +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

category	objects	+ +	+ +	+ +	+ +	+ +
sizes	files	252	characters	483453	nodes	+
propositions	theorems	85	lemmas	1119	total	1204
concepts	declared	46	defined	82	total	128

+ In progress. Context-sensitive subject equivalence - for native type assignment. -

In progress. + for native type assignment. +

+ In progress. Closure of extended context-sensitive computation - for native validity. -

In progress. + for native validity. +

+ In progress. Extended context-sensitive strong normalization - for simply typed terms. -

2012 October 16. + for simply typed terms. +

+ 2012 October 16. Confluence for context-free parallel reduction on closures. -

2012 July 26. +

+ 2012 July 26. Term binders polarized to control Î¶ reduction. -

2012 April 16. +

+ 2012 April 16. Context-sensitive subject equivalence - for atomic arity assignment - (anniversary milestone). -

2012 March 15. + for atomic arity assignment + (anniversary milestone). +

+ 2012 March 15. Context-sensitive strong normalization - for simply typed terms. -

2012 January 27. + for simply typed terms. +

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

2011 September 21. +

+ 2011 September 21. Confluence for context-sensitive parallel reduction on terms. -

2011 September 6. +

+ 2011 September 6. Confluence for context-free parallel reduction on terms. -

2011 April 17. +

+ 2011 April 17. Specification starts. -

Logical Structure of the Specification

The source files are grouped in planes and components +

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 (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).

component	plane	files
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? â©:â[?] ? )	lsubsv_ldrop	lsubsv_snv
	stratified native validity	snv ( â¦?,?â¦ â© ? :[?] )	snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs
equivalence	focalized equivalence	lfpcs ( â¦?â¦ â¬* â¦?â¦ )	lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs
		fpcs ( â¦?,?â¦ â¬* â¦?,?â¦ )	fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs
	local env. ref. for context-sensitive equivalence	lsubse ( ? â¢â¢â[?] ? )	lsubse_ldrop lsubse_ssta lsubse_cpcs
	context-sensitive equivalence	cpcs ( ? â¢ ? â¬* ? )	cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs
conversion	focalized conversion	lfpc ( â¦?â¦ â¬ â¦?â¦ )	lfpc_lfpc
		fpc ( â¦?,?â¦ â¬ â¦?,?â¦ )	fpc_fpc
	context-sensitive conversion	cpc ( ? â¢ ? â¬ ? )	cpc_cpc
computation	focalized computation	lfprs ( â¦?â¦ â¡* â¦?â¦ )	lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs
		fprs ( â¦?,?â¦ â¡* â¦?,?â¦ )	fprs_aaa fprs_fprs
	"big tree" parallel computation	yprs ( ? â¢ â¦?,?â¦ â¥[g] â¦?,?â¦ )	yprs_yprs	ygt ( ? â¢ â¦?,?â¦ >[g] â¦?,?â¦ )	ygt_ygt
	decomposed extended computation	dxprs ( â¦?,?â¦ â¢ ? â¢â¡[?] ? )	dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs
	weakly normalizing computation	cpe ( ? â¢ â¡* ðâ¦?â¦ )	cpe_cpe
	strongly normalizing computation	csn_vector ( ? â¢ â¬* ? )	csn_cpr_vector csn_tstc_vector csn_aaa
		csn ( ? â¢ â¬* ? )	csn_alt ( ? â¢ â¬â¬* ? )	csn_lift csn_cpr csn_lfpr
	context-sensitive computation	cprs (? â¢ ? â¡* ?)	cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector
	context-free computation	ltprs ( ? â¡* ? )	ltprs_alt ( ? â¡â¡* ? )	ltprs_ldrop ltprs_ltprs
		tprs ( ? â¡* ?)	tprs_lift tprs_tprs
	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 focalized reduction	cfpr ( ? â¢ â¦?,?â¦ â¡ â¦?,?â¦ )	cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr
	context-free focalized reduction	lfpr ( â¦?â¦ â¡ â¦?â¦ )	lfpr_alt ( â¦?â¦ â¡â¡ â¦?â¦ )	lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr
		fpr ( â¦?,?â¦ â¡ â¦?,?â¦ )	fpr_cpr fpr_fpr
	"big tree" parallel reduction	ypr ( ? â¢ â¦?,?â¦ â½[g] â¦?,?â¦ )	ysc ( ? â¢ â¦?,?â¦ â»[g] â¦?,?â¦ )
	context-sensitive normal forms	cnf ( ? â¢ ðâ¦?â¦ )	cnf_lift cnf_cif
	context-sensitive reduction	cpr ( ? â¢ ? â¡ ? )	cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr
	context-sensitive reducible forms	crf ( ? â¢ ðâ¦?â¦ )	crf_append	cif ( ? â¢ ðâ¦?â¦ )	cif_append
	context-free normal forms	thnf ( ððâ¦?â¦ )
	context-free reduction	ltpr ( ? â¡ ? )	ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr
		tpr ( ? â¡ ? )	tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr
unwind	iterated stratified static type assignment	sstas ( â¦?,?â¦ â¢ ? â¢*[?] ? )	sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas
static typing	local env. ref. for stratified static type assignment	lsubss ( ? â¢â[?] ? )	lsubss_ldrop lsubss_ssta lsubss_lsubss
	stratified static type assignment	ssta ( â¦?,?â¦ â¢ ? â¢[?,?] ? )	ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta
	local env. ref. for atomic arity assignment	lsuba ( ? ââ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba
	atomic arity assignment	aaa ( ? â¢ ? â ? )	aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa
	parameters	sh	sd
unfold	basic local env. thinning	thin ( ? â¼*[?,?] â¡ ? )	thin_ldrop thin_delift
	inverse basic term relocation	delift ( ? â¢ ? â¼*[?,?] â¡ ? )	delift_alt ( ? â¢ ? â¼â¼*[?,?] â¡ ? )	delift_lift delift_tpss delift_ltpss delift_delift
	partial unfold	ltpss_sn ( ? â¢ â¶*[?,?] ? )	ltpss_sn_alt ( ? â¢ â¶â¶*[?,?] ? )	ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn
		ltpss_dx ( ? â¶*[?,?] ? )	ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx
		tpss ( ? â¢ ? â¶*[?,?] ? )	tpss_alt ( ? â¢ ? â¶â¶*[?,?] ? )	tpss_lift	tpss_tpss
	generic local env. slicing	ldrops ( â©*[?] ? â¡ ? )	ldrops_ldrop ldrops_ldrops
	iterated restricted structural predecessor for closures	frsups ( â¦?,?â¦ â§* â¦?,?â¦ )	frsups_frsups
		frsupp ( â¦?,?â¦ â§+ â¦?,?â¦ )	frsupp_frsupp
	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	tps ( ? â¢ ? â¶[?,?] ? )	tps_lift tps_tps
	global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop
	basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop
	local env. ref. for substitution	lsubs ( ? â¼[?,?] ? )	(lsubs_lsubs)	lsubs_sfr ( â½[?,?] ? )
	restricted structural predecessor for closures	frsup ( â¦?,?â¦ â§ â¦?,?â¦ )
	basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector
		lift ( â§[?,?] ? â¡ ? )	lift_lift
grammar	same head term form	tshf ( ? â ? )	(tshf_tshf)
	same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_vector
	closures	cl_shift ( ? @@ ? )	cl_weight ( â¯{?,?} )
	internal syntax	genv
		lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )	lenv_px lenv_px_bi
		term	term_weight ( â¯{?} )	term_simple ( ðâ¦?â¦ )	term_vector
		item
	external syntax	aarity

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

component	plane	files	+ +	+ +	+ +	+ +
dynamic typing	local env. ref. for stratified native validity	lsubsv ( ? â¢ ? â©:â[?] ? )	lsubsv_ldrop	lsubsv_snv	+ +	+ +
+ +	stratified native validity	snv ( â¦?,?â¦ â© ? :[?] )	snv_lift snv_ltpss_dx snv_ltpss_sn snv_aaa snv_ssta snv_sstas snv_ssta_ltpr snv_ltpr snv_cpcs	+ +	+ +	+ +
equivalence	focalized equivalence	lfpcs ( â¦?â¦ â¬* â¦?â¦ )	lfpcs_aaa lfpcs_fpcs lfpcs_lfprs lfpcs_lfpcs	+ +	+ +	+ +
+ +	+ +	fpcs ( â¦?,?â¦ â¬* â¦?,?â¦ )	fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs	+ +	+ +	+ +
+ +	local env. ref. for context-sensitive equivalence	lsubse ( ? â¢â¢â[?] ? )	lsubse_ldrop lsubse_ssta lsubse_cpcs	+ +	+ +	+ +
+ +	context-sensitive equivalence	cpcs ( ? â¢ ? â¬* ? )	cpcs_ltpss_dx cpcs_ltpss_sn cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs	+ +	+ +	+ +
conversion	focalized conversion	lfpc ( â¦?â¦ â¬ â¦?â¦ )	lfpc_lfpc	+ +	+ +	+ +
+ +	+ +	fpc ( â¦?,?â¦ â¬ â¦?,?â¦ )	fpc_fpc	+ +	+ +	+ +
+ +	context-sensitive conversion	cpc ( ? â¢ ? â¬ ? )	cpc_cpc	+ +	+ +	+ +
computation	focalized computation	lfprs ( â¦?â¦ â¡* â¦?â¦ )	lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs	+ +	+ +	+ +
+ +	+ +	fprs ( â¦?,?â¦ â¡* â¦?,?â¦ )	fprs_aaa fprs_fprs	+ +	+ +	+ +
+ +	"big tree" parallel computation	yprs ( ? â¢ â¦?,?â¦ â¥[g] â¦?,?â¦ )	yprs_yprs	ygt ( ? â¢ â¦?,?â¦ >[g] â¦?,?â¦ )	ygt_ygt	+ +
+ +	decomposed extended computation	dxprs ( â¦?,?â¦ â¢ ? â¢â¡[?] ? )	dxprs_lift dxprs_ltpss_dx dxprs_ltpss_sn dxprs_aaa dxpr_lsubss dxprs_dxprs	+ +	+ +	+ +
+ +	weakly normalizing computation	cpe ( ? â¢ â¡* ðâ¦?â¦ )	cpe_cpe	+ +	+ +	+ +
+ +	strongly normalizing computation	csn_vector ( ? â¢ â¬* ? )	csn_cpr_vector csn_tstc_vector csn_aaa	+ +	+ +	+ +
+ +	+ +	csn ( ? â¢ â¬* ? )	csn_alt ( ? â¢ â¬â¬* ? )	csn_lift csn_cpr csn_lfpr	+ +	+ +
+ +	context-sensitive computation	cprs (? â¢ ? â¡* ?)	cprs_lift cprs_tpss cprs_ltpss_dx cprs_ltpss_sn cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector	+ +	+ +	+ +
+ +	context-free computation	ltprs ( ? â¡* ? )	ltprs_alt ( ? â¡â¡* ? )	ltprs_ldrop ltprs_ltprs	+ +	+ +
+ +	+ +	tprs ( ? â¡* ?)	tprs_lift tprs_tprs	+ +	+ +	+ +
+ +	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 focalized reduction	cfpr ( ? â¢ â¦?,?â¦ â¡ â¦?,?â¦ )	cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr	+ +	+ +	+ +
+ +	context-free focalized reduction	lfpr ( â¦?â¦ â¡ â¦?â¦ )	lfpr_alt ( â¦?â¦ â¡â¡ â¦?â¦ )	lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr	+ +	+ +
+ +	+ +	fpr ( â¦?,?â¦ â¡ â¦?,?â¦ )	fpr_cpr fpr_fpr	+ +	+ +	+ +
+ +	"big tree" parallel reduction	ypr ( ? â¢ â¦?,?â¦ â½[g] â¦?,?â¦ )	ysc ( ? â¢ â¦?,?â¦ â»[g] â¦?,?â¦ )	+ +	+ +	+ +
+ +	context-sensitive normal forms	cnf ( ? â¢ ðâ¦?â¦ )	cnf_lift cnf_cif	+ +	+ +	+ +
+ +	context-sensitive reduction	cpr ( ? â¢ ? â¡ ? )	cpr_lift cpr_tpss cpr_ltpss_dx cpr_ltpss_sn cpr_delift cpr_aaa cpr_ltpr cpr_cpr	+ +	+ +	+ +
+ +	context-sensitive reducible forms	crf ( ? â¢ ðâ¦?â¦ )	crf_append	cif ( ? â¢ ðâ¦?â¦ )	cif_append	+ +
+ +	context-free normal forms	thnf ( ððâ¦?â¦ )	+ +	+ +	+ +	+ +
+ +	context-free reduction	ltpr ( ? â¡ ? )	ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr	+ +	+ +	+ +
+ +	+ +	tpr ( ? â¡ ? )	tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr	+ +	+ +	+ +
unwind	iterated stratified static type assignment	sstas ( â¦?,?â¦ â¢ ? â¢*[?] ? )	sstas_lift sstas_ltpss_dx sstas_ltpss_sn sstas_aaa sstas_lsubss sstas_sstas	+ +	+ +	+ +
static typing	local env. ref. for stratified static type assignment	lsubss ( ? â¢â[?] ? )	lsubss_ldrop lsubss_ssta lsubss_lsubss	+ +	+ +	+ +
+ +	stratified static type assignment	ssta ( â¦?,?â¦ â¢ ? â¢[?,?] ? )	ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta	+ +	+ +	+ +
+ +	local env. ref. for atomic arity assignment	lsuba ( ? ââ ? )	lsuba_ldrop lsuba_aaa lsuba_lsuba	+ +	+ +	+ +
+ +	atomic arity assignment	aaa ( ? â¢ ? â ? )	aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa	+ +	+ +	+ +
+ +	parameters	sh	sd	+ +	+ +	+ +
unfold	basic local env. thinning	thin ( ? â¼*[?,?] â¡ ? )	thin_ldrop thin_delift	+ +	+ +	+ +
+ +	inverse basic term relocation	delift ( ? â¢ ? â¼*[?,?] â¡ ? )	delift_alt ( ? â¢ ? â¼â¼*[?,?] â¡ ? )	delift_lift delift_tpss delift_ltpss delift_delift	+ +	+ +
+ +	partial unfold	ltpss_sn ( ? â¢ â¶*[?,?] ? )	ltpss_sn_alt ( ? â¢ â¶â¶*[?,?] ? )	ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn	+ +	+ +
+ +	+ +	ltpss_dx ( ? â¶*[?,?] ? )	ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx	+ +	+ +	+ +
+ +	+ +	tpss ( ? â¢ ? â¶*[?,?] ? )	tpss_alt ( ? â¢ ? â¶â¶*[?,?] ? )	tpss_lift	tpss_tpss	+ +
+ +	generic local env. slicing	ldrops ( â©*[?] ? â¡ ? )	ldrops_ldrop ldrops_ldrops	+ +	+ +	+ +
+ +	iterated restricted structural predecessor for closures	frsups ( â¦?,?â¦ â§* â¦?,?â¦ )	frsups_frsups	+ +	+ +	+ +
+ +	+ +	frsupp ( â¦?,?â¦ â§+ â¦?,?â¦ )	frsupp_frsupp	+ +	+ +	+ +
+ +	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	tps ( ? â¢ ? â¶[?,?] ? )	tps_lift tps_tps	+ +	+ +	+ +
+ +	global env. slicing	gdrop ( â©[?] ? â¡ ? )	gdrop_gdrop	+ +	+ +	+ +
+ +	basic local env. slicing	ldrop ( â©[?,?] ? â¡ ? )	ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop	+ +	+ +	+ +
+ +	local env. ref. for substitution	lsubs ( ? â¼[?,?] ? )	(lsubs_lsubs)	lsubs_sfr ( â½[?,?] ? )	+ +	+ +
+ +	restricted structural predecessor for closures	frsup ( â¦?,?â¦ â§ â¦?,?â¦ )	+ +	+ +	+ +	+ +
+ +	basic term relocation	lift_vector ( â§[?,?] ? â¡ ? )	lift_lift_vector	+ +	+ +	+ +
+ +	+ +	lift ( â§[?,?] ? â¡ ? )	lift_lift	+ +	+ +	+ +
grammar	same head term form	tshf ( ? â ? )	(tshf_tshf)	+ +	+ +	+ +
+ +	same top term constructor	tstc ( ? â ? )	tstc_tstc tstc_vector	+ +	+ +	+ +
+ +	closures	cl_shift ( ? @@ ? )	cl_weight ( â¯{?,?} )	+ +	+ +	+ +
+ +	internal syntax	genv	+ +	+ +	+ +	+ +
+ +	+ +	lenv	lenv_weight ( â¯{?} )	lenv_length ( \|?\| )	lenv_append ( ? @@ ? )	lenv_px lenv_px_bi
+ +	+ +	term	term_weight ( â¯{?} )	term_simple ( ðâ¦?â¦ )	term_vector	+ +
+ +	+ +	item	+ +	+ +	+ +	+ +
+ +	external syntax	aarity	+ +	+ +	+ +	+ +

Physical Structure of the Specification

The source files are grouped in directories, +

Physical Structure of the Specification

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

Last update: 2013-03-09T23:27:52+01:00

+
+

+ +

+ + +

+ +

+
+

Last update: Mon, 11 Mar 2013 13:47:08 +0100

diff --git a/helm/www/lambdadelta/xslt/ld_web.xsl b/helm/www/lambdadelta/xslt/ld_web.xsl index 288973806..dd091dcd3 100644 --- a/helm/www/lambdadelta/xslt/ld_web.xsl +++ b/helm/www/lambdadelta/xslt/ld_web.xsl @@ -5,6 +5,7 @@ > + diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 7c36784c9..e82b2784b 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -2,10 +2,8 @@ @@ -53,7 +51,7 @@

- +

@@ -62,7 +60,7 @@ - + diff --git a/helm/www/lambdadelta/xslt/lddl_library.xsl b/helm/www/lambdadelta/xslt/lddl_library.xsl index 9eccd5b85..ccd977990 100644 --- a/helm/www/lambdadelta/xslt/lddl_library.xsl +++ b/helm/www/lambdadelta/xslt/lddl_library.xsl @@ -144,9 +144,14 @@ + + + + + - +

.html

@@ -249,7 +254,7 @@ - +

-- 2.39.2