--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambdadelta.info">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="BTM"/>
+ <title>BTM</title>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css"/>
+ <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico"/>
+ </head>
+ <body lang="en-US"><div class="spacer"><a href="http://lambdadelta.info/"><img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/BTM/</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div>
+ <div class="head2">Character classes</div>
+ <div class="text">This table shows how the first 45 positive integers
+ are distributed in the four classes.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">class</td><td class="snns text grey">contents</td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn number grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component orange">p</td><td class="snns text orange"><br/></td><td class="snnn number orange">1</td><td class="snnn number orange">4</td><td class="snnn number orange">7</td><td class="snnn number orange">10</td><td class="snnn number orange">13</td><td class="snnn number orange">16</td><td class="snnn number orange">19</td><td class="snnn number orange">22</td><td class="snnn number orange">25</td><td class="snnn number orange">28</td><td class="snnn number orange">31</td><td class="snnn number orange">34</td><td class="snnn number orange">37</td><td class="snnn number orange">40</td><td class="ssnn number orange">43</td></tr><tr><td class="snns component green">q</td><td class="snns text green"><br/></td><td class="snnn number green">5</td><td class="snnn number green">11</td><td class="snnn number green">15</td><td class="snnn number green">17</td><td class="snnn number green">23</td><td class="snnn number green">29</td><td class="snnn number green">33</td><td class="snnn number green">35</td><td class="snnn number green">41</td><td class="snnn number green">45</td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="snnn number green"><br/></td><td class="ssnn number green"><br/></td></tr><tr><td class="snns component sky">s</td><td class="snns text sky"><br/></td><td class="snnn number sky">2</td><td class="snnn number sky">6</td><td class="snnn number sky">8</td><td class="snnn number sky">14</td><td class="snnn number sky">18</td><td class="snnn number sky">20</td><td class="snnn number sky">24</td><td class="snnn number sky">26</td><td class="snnn number sky">32</td><td class="snnn number sky">38</td><td class="snnn number sky">42</td><td class="snnn number sky">44</td><td class="snnn number sky"><br/></td><td class="snnn number sky"><br/></td><td class="ssnn number sky"><br/></td></tr><tr><td class="snss component magenta">t</td><td class="snss text magenta"><br/></td><td class="snsn number magenta">3</td><td class="snsn number magenta">9</td><td class="snsn number magenta">12</td><td class="snsn number magenta">21</td><td class="snsn number magenta">27</td><td class="snsn number magenta">30</td><td class="snsn number magenta">36</td><td class="snsn number magenta">39</td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="snsn number magenta"><br/></td><td class="sssn number magenta"><br/></td></tr></tbody></table></div>
+
+ <div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-12-01T17:55:33+01:00</div>
+</body>
+</html>
--- /dev/null
+H=@
+
+TAGS = www up \
+ lint-xml index lddl install-xml \
+ test-html html install-html \
+ install-jed install-bib \
+
+LDDLURL = http://lambdadelta.info/static/lddl
+
+ETCDIR = etc
+DOWNDIR = download
+XSLTDIR = xslt
+XMLDIR = xml
+HTMLDIR = $(HOME)/public_html/lddl
+JEDDIR = $(HOME)/mps/jed
+BIBDIR = $(HOME)/texmf/bibtex/bib
+XHTBLDIR = bin/xhtbl
+
+REMOTE = helm.cs.unibo.it
+RDIR = /projects/helm/public_html/lambdadelta
+RXMLDIR = $(REMOTE):$(RDIR)/xml
+RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl
+
+SLS = helena.sl automath.sl
+BIB = lambdadelta.bib
+
+XMLS = brg_si/grundlagen/l/not.ld.xml \
+ brg_si/grundlagen/l/et.ld.xml \
+ brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+ brg_si/grundlagen/l/e/pairis1.ld.xml \
+ brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+ crg_si/grundlagen/l/not.ld.xml \
+ crg_si/grundlagen/l/et.ld.xml \
+ crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+ crg_si/grundlagen/l/e/pairis1.ld.xml \
+ crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
+ brg_si/grundlagen/ccs.ldc.xml
+
+XMLLINT = xmllint --noout
+XSLT = xsltproc
+
+all: www
+
+lint-xml: $(XMLS:%=$(XMLDIR)/%)
+ @echo XMLLINT --valid
+ $(H)$(XMLLINT) --valid $^
+
+$(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index:
+ @echo " GENERATE INDEXES"
+ $(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt
+ $(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh
+
+lddl: $(ETCDIR)/exclude.txt index
+ @echo " GENERATE lddl.tar.bz2"
+ $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR)
+
+install-xml: $(XMLDIR)/index.txt
+ @echo " INSTALL xml"
+ $(H)scp -r $< $(XMLDIR)/brg_si/ $(XMLDIR)/crg_si/ $(RXMLDIR)
+
+test-html:
+ @$(MAKE) --no-print-directory $(XMLS:%.xml=%)
+
+html: $(ETCDIR)/make_html.sh
+ @echo " MAKE */*.ld"
+ $(H). $<
+
+install-html: $(ETCDIR)/make_html.sh
+ @echo " INSTALL html"
+ $(H)scp -r $(HTMLDIR)/* $(RHTMLDIR)
+
+install-jed: $(SLS:%=$(JEDDIR)/%)
+ @echo " INSTALL $(SLS)"
+ $(H)scp $^ $(DOWNDIR)
+
+install-bib: $(BIB:%=$(BIBDIR)/%)
+ @echo " INSTALL $(BIB)"
+ $(H)scp $< $(DOWNDIR)
+ $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt)
+
+www:
+ $(H)$(MAKE) --no-print-directory -C $(XHTBLDIR) www
+
+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
+
+%.ldc:
+ @echo " SKIP $@"
+
+.PHONY: $(TAGS)
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambdadelta.info">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="applications of lambdadelta version 2"/>
+ <title>applications of lambdadelta version 2</title>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css"/>
+ <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico"/>
+ </head>
+ <body lang="en-US"><div class="spacer"><a href="http://lambdadelta.info/"><img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div>
+ <div class="head2">Contents of the Specification</div>
+ <div class="text">This specification comprises a collection of checked
+ applications of λδ version 2.
+ In particular it contains the components below.
+ </div>
+ <ul><li><span class="date">MLTT1.</span>
+ Martin-Löf's Type Theory with one universe
+ using λδ as theory of expressions.
+ </li></ul>
+ <ul><li><span class="date">Functional.</span>
+ The validation algorithm for λδ as implemented in
+ <a href="http://lambdadelta.info/implementation.html#helena">Helena 0.8</a>.
+ </li></ul>
+
+ <div class="head2">Summary of the Specification</div>
+ <div class="text">Here is a numerical acount of the specification's contents
+ and its timeline.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">5</td><td class="snns plane cyan">bytes</td><td class="snnn number cyan">13143</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">4</td><td class="snns plane green">lemmas</td><td class="snnn number green">1</td><td class="snns plane green">total</td><td class="ssnn number green">5</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">3</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">10</td><td class="snss plane yellow">total</td><td class="sssn number yellow">13</td></tr></tbody></table></div>
+ <ul><li><span class="date">2012 February 24.</span>
+ The Applications directory is started.
+ </li></ul>
+ <ul><li><span class="date">2011 December 20.</span>
+ The Functional component is started
+ inside the specification of λδ version 2.
+ </li></ul>
+ <ul><li><span class="date">2011 December 12.</span>
+ The MLTT1 component is started.
+ </li></ul>
+
+ <div class="head2">Logical Structure of the Specification</div>
+ <div class="text">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).
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component orange">MLTT1</td><td class="snns plane orange"/><td class="snns file orange">genv_primitive</td><td class="ssnn file orange">judgement</td></tr><tr><td class="snns component red">functional</td><td class="snns plane red">reduction and type machine</td><td class="snns file red">rtm</td><td class="ssnn file red">rtm_step ( ? ⇨ ? )</td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">unfold</td><td class="snss file red">lift ( ↑[?,?] ? )</td><td class="sssn file red">subst ( [?←?] ? )</td></tr></tbody></table></div>
+
+ <div class="head2">Physical Structure of the Specification</div>
+ <div class="text">The source files are grouped in directories,
+ one for each component.
+ </div>
+ <div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-12-01T17:55:33+01:00</div>
+</body>
+</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" xmlns:ld="http://lambdadelta.info">
+ <head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="lambdadelta version 2"/>
+ <title>lambdadelta version 2</title>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css"/>
+ <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css"/>
+ <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico"/>
+ </head>
+ <body lang="en-US"><div class="spacer"><a href="http://lambdadelta.info/"><img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambdadelta/basic_2/ (λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div>
+ <div class="head2">System's Syntax and Behavior</div>
+ <div class="text">This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns text grey">domain</td><td class="snns plane grey">block</td><td class="snns text grey">leader</td><td class="snns text grey">applicator (with →θ)*</td><td class="snns text grey">reduction</td><td class="snns text grey">→ζ *</td><td class="ssns text grey">reference *</td></tr><tr><td class="snns text">{X | Γ ⊢ X : W}</td><td class="snns plane wine">local typed abstraction *</td><td class="snns text wine">Γ ⊢ +λW</td><td class="snns text wine">ⓐV</td><td class="snns text wine">→β</td><td class="snns text wine">no</td><td class="ssns text wine">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane magenta">local typed declaration **</td><td class="snns text magenta">Γ ⊢ -λW</td><td class="snns text magenta">ⓐV</td><td class="snns text magenta">→β</td><td class="snns text magenta">no</td><td class="ssns text magenta">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane prune">global typed declaration ***</td><td class="snns text prune">Γ ⊢ pλW</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="snns text prune">no</td><td class="ssns text prune">$p</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane blue">native type annotation *</td><td class="snns text blue">Γ ⊢ ⓝW</td><td class="snns text blue">no</td><td class="snns text blue">no</td><td class="snns text blue">yes</td><td class="ssns text blue">no</td></tr><tr><td class="snns text">{X | Γ ⊢ X = V}</td><td class="snns plane sky">local abbreviation *</td><td class="snns text sky">Γ ⊢ +δV</td><td class="snns text sky">no</td><td class="snns text sky">local →δ</td><td class="snns text sky">yes</td><td class="ssns text sky">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane cyan">local definition **</td><td class="snns text cyan">Γ ⊢ -δV</td><td class="snns text cyan">no</td><td class="snns text cyan">local →δ</td><td class="snns text cyan">no</td><td class="ssns text cyan">#i</td></tr><tr><td class="nnns text"><br/></td><td class="snns plane water">global definition ***</td><td class="snns text water">Γ ⊢ pδV</td><td class="snns text water">no</td><td class="snns text water">global →δ</td><td class="snns text water">no</td><td class="ssns text water">$p</td></tr><tr><td class="snss text">no</td><td class="snss plane green">sort ****</td><td class="snss text green">Γ ⊢ ⋆k</td><td class="snss text green">no</td><td class="snss text green">no</td><td class="snss text green">no</td><td class="ssss text green">no</td></tr></tbody></table></div>
+ <div class="text">* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </div>
+
+ <div class="head2">Summary of the Specification</div>
+ <div class="text">Here is a numerical acount of the specification's contents
+ and its timeline.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component cyan">sizes</td><td class="snns plane cyan">files</td><td class="snnn number cyan">226</td><td class="snns plane cyan">characters</td><td class="snnn number cyan">427252</td><td class="snns plane cyan"><br/></td><td class="ssnn number cyan"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">82</td><td class="snns plane green">lemmas</td><td class="snnn number green">981</td><td class="snns plane green">total</td><td class="ssnn number green">1063</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">43</td><td class="snss plane yellow">defined</td><td class="snsn number yellow">76</td><td class="snss plane yellow">total</td><td class="sssn number yellow">119</td></tr></tbody></table></div>
+ <ul><li><span class="date">In progress.</span>
+ Context-sensitive subject equivalence
+ for native type assignment.
+ </li></ul>
+ <ul><li><span class="date">In progress.</span>
+ Closure of extended context-sensitive computation
+ for native validity.
+ </li></ul>
+ <ul><li><span class="date">In progress.</span>
+ Extended context-sensitive strong normalization
+ for simply typed terms.
+ </li></ul>
+ <ul><li><span class="date">2012 October 16.</span>
+ Confluence for context-free parallel reduction on closures.
+ </li></ul>
+ <ul><li><span class="date">2012 July 26.</span>
+ Term binders polarized to control ζ reduction.
+ </li></ul>
+ <ul><li><span class="date">2012 April 16.</span>
+ Context-sensitive subject equivalence
+ for atomic arity assignment
+ (anniversary milestone).
+ </li></ul>
+ <ul><li><span class="date">2012 March 15.</span>
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </li></ul>
+ <ul><li><span class="date">2012 January 27.</span>
+ Support for abstract candidates of reducibility.
+ </li></ul>
+ <ul><li><span class="date">2011 September 21.</span>
+ Confluence for context-sensitive parallel reduction on terms.
+ </li></ul>
+ <ul><li><span class="date">2011 September 6.</span>
+ Confluence for context-free parallel reduction on terms.
+ </li></ul>
+ <ul><li><span class="date">2011 April 17.</span>
+ Specification starts.
+ </li></ul>
+
+ <div class="head2">Logical Structure of the Specification</div>
+ <div class="text">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).
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">dynamic typing</td><td class="snns plane prune">stratified native validity</td><td class="snns file prune">snv ( ⦃?,?⦄ ⊩ ? :[?] )</td><td class="snnn file prune">snv_lift snv_aaa snv_ssta</td><td class="snnn file prune"><br/></td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">equivalence</td><td class="snns plane blue">focalized equivalence</td><td class="snns file blue">lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )</td><td class="snnn file blue">lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="nnns plane blue"><br/></td><td class="snns file blue">fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )</td><td class="snnn file blue">fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="snns plane blue">local env. ref. for context-sensitive equivalence</td><td class="snns file blue">lsubse ( ? ⊢•⊑[?] ? )</td><td class="snnn file blue">lsubse_ldrop lsubse_ssta lsubse_cpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="nnns component blue"><br/></td><td class="snns plane blue">context-sensitive equivalence</td><td class="snns file blue">cpcs ( ? ⊢ ? ⬌* ? )</td><td class="snnn file blue">cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs</td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">conversion</td><td class="snns plane sky">focalized conversion</td><td class="snns file sky">lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )</td><td class="snnn file sky">lfpc_lfpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="nnns component sky"><br/></td><td class="nnns plane sky"><br/></td><td class="snns file sky">fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )</td><td class="snnn file sky">fpc_fpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="nnns component sky"><br/></td><td class="snns plane sky">context-sensitive conversion</td><td class="snns file sky">cpc ( ? ⊢ ? ⬌ ? )</td><td class="snnn file sky">cpc_cpc</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">computation</td><td class="snns plane cyan">extended computation</td><td class="snns file cyan">xprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )</td><td class="snnn file cyan">xprs_lift xprs_aaa xpr_lsubss xprs_cprs xprs_xprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">weakly normalizing computation</td><td class="snns file cyan">cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )</td><td class="snnn file cyan">cpe_cpe</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">strongly normalizing computation</td><td class="snns file cyan">csn_vector ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_cpr_vector csn_tstc_vector csn_aaa</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">csn ( ? ⊢ ⬊* ? )</td><td class="snnn file cyan">csn_alt ( ? ⊢ ⬊⬊* ? )</td><td class="snnn file cyan">csn_lift csn_cpr csn_lfpr</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">focalized computation</td><td class="snns file cyan">lfprs ( ⦃?⦄ ➡* ⦃?⦄ )</td><td class="snnn file cyan">lfprs_aaa lfprs_cprs lfprs_lfprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )</td><td class="snnn file cyan">fprs_aaa fprs_fprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-sensitive computation</td><td class="snns file cyan">cprs (? ⊢ ? ➡* ?)</td><td class="snnn file cyan">cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">context-free computation</td><td class="snns file cyan">ltprs ( ? ➡* ? )</td><td class="snnn file cyan">ltprs_alt ( ? ➡➡* ? )</td><td class="snnn file cyan">ltprs_ldrop ltprs_ltprs</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="nnns plane cyan"><br/></td><td class="snns file cyan">tprs ( ? ➡* ?)</td><td class="snnn file cyan">tprs_lift tprs_tprs</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td><td class="snns file cyan">lsubc ( ? ⊑[?] ? )</td><td class="snnn file cyan">lsubc_ldrop lsubc_ldrops lsubc_lsuba</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="nnns component cyan"><br/></td><td class="snns plane cyan">support for abstract computation properties</td><td class="snns file cyan">acp</td><td class="snnn file cyan">acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )</td><td class="snnn file cyan">acp_aaa</td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">reducibility</td><td class="snns plane water">extended reduction</td><td class="snns file water">xpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )</td><td class="snnn file water">xpr_lift xpr_aaa xpr_lsubss</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive focalized reduction</td><td class="snns file water">cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free focalized reduction</td><td class="snns file water">lfpr ( ⦃?⦄ ➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )</td><td class="snnn file water">lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr</td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )</td><td class="snnn file water">fpr_cpr fpr_fpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive normal forms</td><td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td><td class="snnn file water">cnf_lift cnf_cif</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reduction</td><td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td><td class="snnn file water">cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive reducible forms</td><td class="snns file water">crf ( ? ⊢ 𝐑⦃?⦄ )</td><td class="snnn file water">crf_append</td><td class="snnn file water">cif ( ? ⊢ 𝐈⦃?⦄ )</td><td class="snnn file water">cif_append</td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free normal forms</td><td class="snns file water">thnf ( 𝐇𝐍⦃?⦄ )</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-free reduction</td><td class="snns file water">ltpr ( ? ➡ ? )</td><td class="snnn file water">ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="nnns plane water"><br/></td><td class="snns file water">tpr ( ? ➡ ? )</td><td class="snnn file water">tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">unwind</td><td class="snns plane green"/><td class="snns file green"/><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">local env. ref. for stratified static type assignment</td><td class="snns file grass">lsubss ( ? •⊑[?] ? )</td><td class="snnn file grass">lsubss_ldrop lsubss_ssta lsubss_lsubss</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">stratified static type assignment</td><td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td><td class="snnn file grass">ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ⁝⊑ ? )</td><td class="snnn file grass">lsuba_ldrop lsuba_aaa lsuba_lsuba</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⊢ ? ⁝ ? )</td><td class="snnn file grass">aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass">sd</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">basic local env. thinning</td><td class="snns file yellow">thin ( ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">thin_ldrop thin_delift</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">inverse basic term relocation</td><td class="snns file yellow">delift ( ? ⊢ ? ▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )</td><td class="snnn file yellow">delift_lift delift_tpss delift_ltpss delift_delift</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss_sn ( ? ⊢ ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">ltpss_dx ( ? ▶*[?,?] ? )</td><td class="snnn file yellow">ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⊢ ? ▶*[?,?] ? )</td><td class="snnn file yellow">tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td><td class="snnn file yellow">ldrops_ldrop ldrops_ldrops</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">iterated restricted structural predecessor for closures</td><td class="snns file yellow">frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )</td><td class="snnn file yellow">frsups_frsups</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )</td><td class="snnn file yellow">frsupp_frsupp</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td><td class="snnn file yellow">lifts_lift lifts_lifts</td><td class="snnn file yellow"><br/></td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td><td class="snnn file yellow">gr2_gr2</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">tps ( ? ⊢ ? ▶[?,?] ? )</td><td class="snnn file orange">tps_lift tps_tps</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td><td class="snnn file orange">ldrop_append ldrop_lpx ldrop_sfr ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">local env. ref. for substitution</td><td class="snns file orange">lsubs ( ? ≼[?,?] ? )</td><td class="snnn file orange">(lsubs_lsubs)</td><td class="snnn file orange">lsubs_sfr ( ≽[?,?] ? )</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">restricted structural predecessor for closures</td><td class="snns file orange">frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">same head term form</td><td class="snns file red">tshf ( ? ≈ ? )</td><td class="snnn file red">(tshf_tshf)</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">same top term constructor</td><td class="snns file red">tstc ( ? ≃ ? )</td><td class="snnn file red">tstc_tstc tstc_vector</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @@ ? )</td><td class="snnn file red">cl_weight ( #{?,?} )</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #{?} )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="snnn file red">lenv_append ( ? @@ ? )</td><td class="ssnn file red">lenv_px lenv_px_bi</td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #{?} )</td><td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td><td class="snnn file red">term_vector</td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
+
+ <div class="head2">Physical Structure of the Specification</div>
+ <div class="text">The source files are grouped in directories,
+ one for each component.
+ </div>
+ <div class="spacer"><img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-12-01T17:55:33+01:00</div>
+</body>
+</html>
--- /dev/null
+let f = "0123456789abcdef"
+
+let r, g, b = 1.0, 0.5, 0.0
+
+let h = 1. /. 2.
+
+let mk_h x = x +. (1. -. x) *. h
+
+let rr, gg, bb = mk_h r, mk_h g, mk_h b
+
+let mk_f x =
+ let x = int_of_float x in
+ print_char f.[x / 16]; print_char f.[x mod 16]
+
+let _ =
+ mk_f (rr *. 255.); mk_f (gg *. 255.); mk_f (bb *. 255.);
+ print_newline ()
--- /dev/null
+EXEC = xhtbl
+VERSION=0.1.1
+
+REQUIRES = str
+
+YACCFLAGS = -v
+
+include Makefile.common
+
+XSLT = xsltproc
+XHTBL = ./xhtbl.native
+
+LDURL = http://lambdadelta.info/
+XSLDIR = ../../xslt/
+SRCDIR = ../../web/home/
+ETCDIR = ../../etc/
+HOMEDIR = ../../
+TBLDIRS = $(SRCDIR) $(ETCDIR)
+
+LDWS = $(shell find $(SRCDIR) -name "*.ldw.xml")
+TBLS = $(shell find -L $(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
+
+$(HOMEDIR)%.html: BASEURL = --stringparam baseurl $(LDURL)
+
+www: $(HTMLS)
+
+$(XSLS:%=$(XSLDIR)%): $(TBLS) $(XHTBL)
+ @echo " XHTBL *.tbl"
+ $(H)$(XHTBL) -O $(XSLDIR) $(TBLS)
+
+$(HOMEDIR)%.html: $(SRCDIR)%.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%)
+ @echo " XSLT $(notdir $<)"
+ $(H)$(XSLT) -o $@ $(BASEURL) $(XSLDIR)ld_web.xsl $<
--- /dev/null
+H=@
+
+include ../../etc/Makefile.defs
+
+DIST=$(EXEC)---$(VERSION)
+DATE=$(shell date +%y%m%d)
+
+OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\"
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS)
+OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS)
+
+all: $(EXEC).native
+
+$(EXEC).native: $(wildcard *.ml) $(wildcard *.mli) $(wildcard *.mly) $(wildcard *.mll)
+ @echo " OCAMLBUILD $(EXEC).native"
+ $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" -yaccflags "$(YACCFLAGS)" $(EXEC).native
+
+clean:
+ ocamlbuild -clean
+ rm -rf $(DIST) $(DIST).tgz
+
+dist:
+ mkdir -p $(DIST)/Sources
+ cp ReadMe $(DIST)
+ cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources
+ cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC)
+ tar -cvzf $(DIST).tgz $(DIST)
--- /dev/null
+module L = List
+
+module T = Table
+
+(* true for a row specification *)
+type atom = T.css * bool * int option * int option
+
+type atoms = atom list
+
+let get_css a y x =
+ let map y x (c, b, x1, x2) = match b, x1, x2 with
+ | _ , None, None -> c
+ | false, None, Some c2 -> if x <= c2 then c else []
+ | false, Some c1, None -> if x >= c1 then c else []
+ | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else []
+ | true , None, Some r2 -> if y <= r2 then c else []
+ | true , Some r1, None -> if y >= r1 then c else []
+ | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else []
+ in
+ L.concat (L.map (map y x) a)
--- /dev/null
+module T = Table
+
+type 'a fold_cb = {
+ open_table : 'a -> T.table -> 'a;
+ close_table: 'a -> T.table -> 'a;
+ map_key : 'a -> T.key -> 'a;
+ open_line : bool -> 'a -> 'a;
+ close_line : bool -> 'a -> 'a;
+ open_entry : bool -> 'a -> 'a;
+ close_entry: bool -> 'a -> 'a -> 'a;
+}
+
+let map h g f a b = h a (g (f a) b)
+
+let rec fold_table cb a t =
+ let a = cb.open_table a t in
+ let a = fold_entry cb a t.T.te in
+ cb.close_table a t
+
+and fold_entry cb a = function
+ | T.Key k -> cb.map_key a k
+ | T.Line (r, ts) ->
+ let a = cb.open_line r a in
+ let a = List.fold_left (map (cb.close_entry r) (fold_table cb) (cb.open_entry r)) a ts in
+ cb.close_line r a
--- /dev/null
+module A = Array
+
+module T = Table
+
+type cell = {
+ ck: string list; (* contents *)
+ cc: T.css; (* css classes *)
+ cb: T.border; (* border *)
+}
+
+type matrix = {
+ r: int; (* rows *)
+ c: int; (* columns *)
+ m: cell array array; (* matrix *)
+}
+
+let empty = {
+ ck = []; cc = []; cb = T.border false;
+}
+
+let make ts = {
+ r = ts.T.rf; c = ts.T.cf;
+ m = A.make_matrix ts.T.rf ts.T.cf empty;
+}
+
+let set_key m y x kl =
+ m.m.(y).(x) <- {m.m.(y).(x) with ck = kl}
+
+let set_css m y x c =
+ m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc}
+
+let set_west m y x b =
+ let c = m.m.(y).(x) in
+ let cb = {c.cb with T.w = c.cb.T.w || b.T.w} in
+ m.m.(y).(x) <- {c with cb = cb}
+
+let set_north m y x b =
+ let c = m.m.(y).(x) in
+ let cb = {c.cb with T.n = c.cb.T.n || b.T.n} in
+ m.m.(y).(x) <- {c with cb = cb}
+
+let set_east m y x b =
+ if x < pred m.c then set_west m y (succ x) {b with T.w = b.T.e} else
+ let c = m.m.(y).(x) in
+ let cb = {c.cb with T.e = c.cb.T.e || b.T.e} in
+ m.m.(y).(x) <- {c with cb = cb}
+
+let set_south m y x b =
+ if y < pred m.r then set_north m (succ y) x {b with T.n = b.T.s} else
+ let c = m.m.(y).(x) in
+ let cb = {c.cb with T.s = c.cb.T.s || b.T.s} in
+ m.m.(y).(x) <- {c with cb = cb}
--- /dev/null
+let output_dir_default = ""
+
+let debug_lexer_default = false
+
+let debug_pass_default = false
+
+let pass_default = false
+
+let output_dir = ref output_dir_default
+
+let debug_lexer = ref debug_lexer_default
+
+let d0 = ref debug_pass_default
+
+let d1 = ref debug_pass_default
+
+let d2 = ref debug_pass_default
+
+let e1 = ref debug_pass_default
+
+let e2 = ref debug_pass_default
+
+let p0 = ref pass_default
+
+let p1 = ref pass_default
+
+let p2 = ref pass_default
+
+let clear () =
+ output_dir := output_dir_default;
+ debug_lexer := debug_lexer_default;
+ d0 := debug_pass_default; d1 := debug_pass_default; d2 := debug_pass_default;
+ e1 := debug_pass_default; e2 := debug_pass_default;
+ p0 := pass_default; p1 := pass_default; p2 := pass_default
--- /dev/null
+module L = List
+
+module T = Table
+module F = Fold
+
+type status = {
+ ts: T.size; (* current dimensions *)
+ tc: T.css; (* current class *)
+}
+
+let empty = {
+ ts = T.no_size; tc = [];
+}
+
+let init b ts =
+ if b then
+ {ts with T.ri = max_int; T.ci = 0}
+ else
+ {ts with T.ri = 0; T.ci = max_int}
+
+let combine b ts1 ts2 =
+ if b then
+ {ts1 with
+ T.rf = max ts1.T.rf ts2.T.rf; T.ri = min ts1.T.ri ts2.T.ri;
+ T.cf = ts1.T.cf + ts2.T.cf; T.ci = ts1.T.ci + ts2.T.ci;
+ }
+ else
+ {ts1 with
+ T.cf = max ts1.T.cf ts2.T.cf; T.ci = min ts1.T.ci ts2.T.ci;
+ T.rf = ts1.T.rf + ts2.T.rf; T.ri = ts1.T.ri + ts2.T.ri;
+ }
+
+let deinit ts = {ts with
+ T.ri = if ts.T.ri = max_int then 0 else ts.T.ri;
+ T.ci = if ts.T.ci = max_int then 0 else ts.T.ci;
+}
+
+(****************************************************************************)
+
+let open_table st t =
+ t.T.tc <- t.T.tc @ st.tc;
+ {st with tc = t.T.tc}
+
+let close_table st t =
+ t.T.ts <- st.ts; st
+
+let map_key st k =
+ let ts = match k, st.ts.T.p with
+ | T.Text _ , _ ->
+ {st.ts with T.rf = 1; T.cf = 1; T.ri = 0; T.ci = 0}
+ | T.Glue None , _ ->
+ {st.ts with T.rf = 0; T.cf = 0; T.ri = 1; T.ci = 1}
+ | T.Glue Some g, Some false ->
+ {st.ts with T.rf = g; T.cf = 0; T.ri = 0; T.ci = 1}
+ | T.Glue Some g, Some true ->
+ {st.ts with T.rf = 0; T.cf = g; T.ri = 1; T.ci = 0}
+ | T.Glue Some g, None ->
+ {st.ts with T.rf = g; T.cf = g; T.ri = 0; T.ci = 0}
+ in
+ {st with ts = ts}
+
+let open_line b st =
+ let ts = init b st.ts in
+ let ts = {ts with T.rf = 0; T.cf = 0} in
+ {st with ts = ts}
+
+let open_entry b st =
+ let ts = {st.ts with T.p = Some b} in
+ {st with ts = ts}
+
+let close_entry b st sst =
+ {st with ts = combine b st.ts sst.ts}
+
+let close_line b st =
+ {st with ts = deinit st.ts}
+
+let cb = {
+ F.open_table = open_table; F.close_table = close_table;
+ F.open_line = open_line; F.close_line = close_line;
+ F.open_entry = open_entry; F.close_entry = close_entry;
+ F.map_key = map_key;
+}
+
+let process t =
+ let st = F.fold_table cb empty t in
+ st.ts
--- /dev/null
+module O = Options
+module T = Table
+module M = Matrix
+module F = Fold
+
+type status = {
+ ts: T.size; (* current dimensions *)
+ tm: M.matrix; (* current matrix *)
+}
+
+let initial t m = {
+ ts = {t.T.ts with T.ri = 0; T.ci = 0};
+ tm = m;
+}
+
+let resize b sts tts =
+ if b then begin (* parent is a row *)
+ if tts.T.rf < sts.T.rf && tts.T.ri = 0 then
+ failwith "underful column";
+ {tts with T.rf = sts.T.rf; T.cf = tts.T.cf + sts.T.ci * tts.T.ci}
+ end else begin (* parent is a column *)
+ if tts.T.cf < sts.T.cf && tts.T.ci = 0 then
+ failwith "underful row";
+ {tts with T.cf = sts.T.cf; T.rf = tts.T.rf + sts.T.ri * tts.T.ri}
+ end
+
+let fill b sts tts =
+ if b then (* parent is a row *)
+ {sts with T.ri =
+ let rf, ri = sts.T.rf - tts.T.rf, tts.T.ri in
+ if ri = 0 then 0 else
+ if rf mod ri = 0 then rf / ri else
+ failwith "fracted column"
+ }
+ else (* parent is a column *)
+ {sts with T.ci =
+ let cf, ci = sts.T.cf - tts.T.cf, tts.T.ci in
+ if ci = 0 then 0 else
+ if cf mod ci = 0 then cf / ci else
+ failwith "fracted row"
+ }
+
+let place b sts tts =
+ if b then (* parent is a row *)
+ {sts with T.x = sts.T.x + tts.T.cf}
+ else (* parent is a column *)
+ {sts with T.y = sts.T.y + tts.T.rf}
+
+let set_key st t = match t.T.te with
+ | T.Key (T.Text sl) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x sl
+ | _ -> ()
+
+let set_css st t =
+ let rec aux y x =
+ if y >= t.T.ts.T.rf then () else
+ if x >= t.T.ts.T.cf then aux (succ y) 0 else begin
+ M.set_css st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc;
+ aux y (succ x)
+ end
+ in
+ match t.T.te with
+ | T.Key _ -> aux 0 0
+ | _ -> ()
+
+let set_borders st t =
+ let rec aux_we y =
+ if y >= t.T.ts.T.rf then () else begin
+ M.set_west st.tm (t.T.ts.T.y + y) t.T.ts.T.x t.T.tb;
+ if t.T.ts.T.cf > 0 then
+ M.set_east st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + pred t.T.ts.T.cf) t.T.tb;
+ aux_we (succ y)
+ end
+ in
+ let rec aux_ns x =
+ if x >= t.T.ts.T.cf then () else begin
+ M.set_north st.tm t.T.ts.T.y (t.T.ts.T.x + x) t.T.tb;
+ if t.T.ts.T.rf > 0 then
+ M.set_south st.tm (t.T.ts.T.y + pred t.T.ts.T.rf) (t.T.ts.T.x + x) t.T.tb;
+ aux_ns (succ x)
+ end
+ in
+ match t.T.te with
+ | T.Line (true, _) -> aux_we 0; aux_ns 0
+ | _ -> ()
+
+let print st t =
+ if !O.e2 then
+ Printf.printf "#%u: (%u+%u, %u+%u) - (%u+%u, %u+%u)\n"
+ t.T.ti
+ t.T.ts.T.rf t.T.ts.T.ri
+ t.T.ts.T.cf t.T.ts.T.ci
+ st.ts.T.rf st.ts.T.ri
+ st.ts.T.cf st.ts.T.ci
+
+(****************************************************************************)
+
+let open_table st t =
+ print st t;
+ let ts = match t.T.ts.T.p with
+ | None ->
+ let ts = fill false st.ts t.T.ts in
+ let ts = fill true ts t.T.ts in
+ t.T.ts <- resize false st.ts t.T.ts;
+ t.T.ts <- resize true st.ts t.T.ts;
+ ts
+ | Some b ->
+ let ts = fill b st.ts t.T.ts in
+ t.T.ts <- resize b st.ts t.T.ts;
+ ts
+ in
+ t.T.ts <- {t.T.ts with T.ri = 0; T.ci = 0; T.x = st.ts.T.x; T.y = st.ts.T.y};
+ let ts = {ts with T.rf = t.T.ts.T.rf; T.cf = t.T.ts.T.cf} in
+ let st = {st with ts = ts} in
+ print st t; st
+
+let close_table st t =
+ set_key st t; set_css st t; set_borders st t; st
+
+let map_key st k = st
+
+let open_line b st = st
+
+let open_entry b st = st
+
+let close_entry b st sst =
+ let ts = place b st.ts sst.ts in
+ {st with ts = ts}
+
+let close_line b st = st
+
+let cb = {
+ F.open_table = open_table; F.close_table = close_table;
+ F.open_line = open_line; F.close_line = close_line;
+ F.open_entry = open_entry; F.close_entry = close_entry;
+ F.map_key = map_key;
+}
+
+let process t m =
+ let _ = F.fold_table cb (initial t m) t in ()
--- /dev/null
+module A = Array
+
+module M = Matrix
+module C = Css
+
+type status = {
+ m: M.matrix;
+ a: C.atoms;
+}
+
+let initial a m = {
+ m = m; a = a;
+}
+
+let process_cell st y x c =
+ M.set_css st.m y x (C.get_css st.a y x)
+
+let process_row st y row =
+ A.iteri (process_cell st y) row
+
+let process css matrix =
+ let st = initial css matrix in
+ A.iteri (process_row st) matrix.M.m
--- /dev/null
+type css = string list
+
+type size = {
+ y : int; (* first row *)
+ x : int; (* first column *)
+ rf: int; (* finite rows *)
+ cf: int; (* finite columns *)
+ ri: int; (* infinite rows *)
+ ci: int; (* infinite columns *)
+ p : bool option; (* parent kind *)
+}
+
+type border = {
+ n: bool; (* north *)
+ s: bool; (* south *)
+ e: bool; (* east *)
+ w: bool; (* west *)
+}
+
+type key = Text of string list
+ | Glue of int option
+
+type table = {
+ mutable tc: css; (* css classes *)
+ mutable ts: size; (* dimension *)
+ tb: border; (* border *)
+ te: entry; (* contents *)
+ ti: int; (* table identifier *)
+}
+
+and entry = Key of key
+ | Line of bool * table list (* true for a row *)
+
+let id =
+ let current = ref 0 in
+ fun () -> incr current; !current
+
+let no_size = {
+ y = 0; x = 0; rf = 0; cf = 0; ri = 0; ci = 0; p = None;
+}
+
+let border b = {
+ n = b; s = b; e = b; w = b;
+}
+
+let mk_key k tc = {
+ ts = no_size; tb = border false; te = Key k; tc = tc;
+ ti = id ();
+}
+
+let mk_line b tl tc = {
+ ts = no_size; tb = border b; te = Line (b, tl); tc = tc;
+ ti = id ();
+}
--- /dev/null
+{
+ module S = String
+ module O = Options
+ module TP = TextParser
+
+ let trim s = S.sub s 1 (S.length s - 2)
+
+ let out s = if !O.debug_lexer then prerr_endline s
+}
+
+let SPC = ['\r' '\n' '\t' ' ']+
+let QT = '"'
+let STR = QT [^'"']* QT
+let NUM = ['0'-'9']+
+
+rule token = parse
+ | SPC { token lexbuf }
+ | STR as s { out s; TP.TEXT (trim s) }
+ | NUM as s { out s; TP.NUM (int_of_string s) }
+ | "{" { out "{"; TP.OC }
+ | "}" { out "}"; TP.CC }
+ | "[" { out "["; TP.OB }
+ | "]" { out "]"; TP.CB }
+ | "*" { out "*"; TP.SR }
+ | "+" { out "+"; TP.PS }
+ | "name" { out "name"; TP.NAME }
+ | "table" { out "table"; TP.TABLE }
+ | "class" { out "class"; TP.CSS }
+ | "(*" { block lexbuf; token lexbuf }
+ | eof { TP.EOF }
+and block = parse
+ | "*)" { () }
+ | "(*" { block lexbuf; block lexbuf }
+ | STR { block lexbuf }
+ | _ { block lexbuf }
--- /dev/null
+%{
+
+module S = Str
+module L = List
+module T = Table
+
+let split s =
+ S.split (S.regexp "[ \r\n\t]+") s
+
+let mk_atom s rs =
+ let map c (b, (x1, x2)) = c, b, x1, x2 in
+ L.map (map (split s)) rs
+
+%}
+
+%token <int> NUM
+%token <string> TEXT
+%token NAME TABLE CSS SR OC CC OB CB PS EOF
+
+%start script
+%type <(string * Table.table * Css.atoms) list> script
+
+%%
+
+text:
+ | TEXT { $1 }
+
+texts:
+ | text { [$1] }
+ | text PS texts { $1 :: $3 }
+;
+
+key:
+ | texts { T.Text $1 }
+ | SR { T.Glue None }
+ | NUM { T.Glue (Some $1) }
+;
+
+css:
+ | { [] }
+ | CSS TEXT { split $2 }
+;
+
+table:
+ | css key { T.mk_key $2 $1 }
+ | css OC tables CC { T.mk_line false $3 $1 }
+ | css OB tables CB { T.mk_line true $3 $1 }
+;
+
+tables:
+ | { [] }
+ | table tables { $1 :: $2 }
+;
+
+name:
+ | { "" }
+ | NAME TEXT { $2 }
+;
+
+interval:
+ | NUM { Some $1, Some $1 }
+ | SR { None, None }
+ | NUM NUM { Some $1, Some $2 }
+ | NUM SR { Some $1, None }
+ | SR NUM { None, Some $2 }
+ | SR SR { None, None }
+;
+
+range:
+ | OB interval CB { true, $2 }
+ | OC interval CC { false, $2 }
+;
+
+ranges:
+ | { [] }
+ | range ranges { $1 :: $2 }
+;
+
+atom:
+ | CSS TEXT ranges { mk_atom $2 $3 }
+;
+
+atoms:
+ | { [] }
+ | atom atoms { $1 @ $2 }
+;
+
+directive:
+ | name TABLE table atoms { $1, $3, $4 }
+;
+
+script:
+ | EOF { [] }
+ | directive script { $1 :: $2 }
+;
--- /dev/null
+module L = List
+module P = Printf
+module S = String
+
+module T = Table
+module F = Fold
+
+type status = {
+ i: int; (* indentation *)
+ out: string -> unit; (* output function *)
+}
+
+let home = {
+ i = 0; out = print_string
+}
+
+let indent st =
+ S.make st.i ' '
+
+let add st = {st with i = st.i + 3}
+
+let sub st = {st with i = st.i - 3}
+
+let parent = function
+ | None -> "key"
+ | Some false -> "col"
+ | Some true -> "row"
+
+let size ts =
+ P.sprintf "(%u, %u); (%u+%u, %u+%u); %s"
+ ts.T.y ts.T.x ts.T.rf ts.T.ri ts.T.cf ts.T.ci (parent ts.T.p)
+
+let border tb =
+ let str = S.make 4 ' ' in
+ if tb.T.w then str.[0] <- 'W';
+ if tb.T.n then str.[1] <- 'N';
+ if tb.T.e then str.[2] <- 'E';
+ if tb.T.s then str.[3] <- 'S';
+ str
+
+let css tc =
+ P.sprintf "\"%s\"" (S.concat " " tc)
+
+let key = function
+ | T.Text sl ->
+ let map s = P.sprintf "\"%s\"" s in
+ S.concat " + " (L.map map sl)
+ | T.Glue None -> "*"
+ | T.Glue (Some i) -> P.sprintf "%u" i
+
+let entry = function
+ | false -> "column"
+ | true -> "row"
+
+(****************************************************************************)
+
+let open_table st t =
+ let str =
+ P.sprintf "%s[{#%u: %s; %s; %s}\n"
+ (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc)
+ in
+ st.out str; add st
+
+let close_table st t =
+ let st = sub st in
+ let str = P.sprintf "%s]\n" (indent st) in
+ st.out str; st
+
+let map_key st k =
+ let str = P.sprintf "%s%s\n" (indent st) (key k) in
+ st.out str; st
+
+let open_line b st =
+ let str = P.sprintf "%s%s\n" (indent st) (entry b) in
+ st.out str; st
+
+let close_line b st = st
+
+let open_entry b st = st
+
+let close_entry b st sst = st
+
+let cb = {
+ F.open_table = open_table; F.close_table = close_table;
+ F.open_line = open_line; F.close_line = close_line;
+ F.open_entry = open_entry; F.close_entry = close_entry;
+ F.map_key = map_key;
+}
+
+let debug t =
+ let _ = F.fold_table cb home t in ()
--- /dev/null
+module A = Arg
+module F = Filename
+module L = List
+
+module O = Options
+module TP = TextParser
+module TL = TextLexer
+module TU = TextUnparser
+module P1 = Pass1
+module P2 = Pass2
+module P3 = Pass3
+module M = Matrix
+module XU = XmlUnparser
+
+let help = ""
+let help_L = ""
+let help_O = ""
+let help_X = ""
+let help_d0 = ""
+let help_d1 = ""
+let help_d2 = ""
+let help_e1 = ""
+let help_e2 = ""
+let help_p0 = ""
+let help_p1 = ""
+let help_p2 = ""
+
+let hook = "xhtbl"
+
+let includes, tables = ref [], ref []
+
+let set_output_dir s = O.output_dir := s
+
+let process_directive och bname (name, table, css) =
+ tables := name :: !tables;
+ if !O.d0 then TU.debug table;
+ if not !O.p0 then begin
+ let size = P1.process table in
+ if !O.d1 then TU.debug table;
+ if not !O.p1 then begin
+ let matrix = M.make size in
+ let _ = P2.process table matrix in
+ if !O.d2 then TU.debug table;
+ if not !O.p2 then P3.process css matrix;
+ let name = if name = "" then bname else name in
+ XU.output och name matrix
+ end
+ end
+
+let process_file fname =
+ let bname = F.chop_extension (F.basename fname) in
+ let ich = open_in fname in
+ let lexbuf = Lexing.from_channel ich in
+ let ds = TP.script TL.token lexbuf in
+ close_in ich; includes := bname :: !includes;
+ let och = XU.open_out true bname in
+ L.iter (process_directive och bname) ds;
+ XU.close_out och
+
+let main () =
+ A.parse [
+ "-L", A.Set O.debug_lexer, help_L;
+ "-O", A.String set_output_dir, help_O;
+ "-X", A.Unit O.clear, help_X;
+ "-d0", A.Set O.d0, help_d0;
+ "-d1", A.Set O.d1, help_d1;
+ "-d2", A.Set O.d2, help_d2;
+ "-e1", A.Set O.e1, help_e1;
+ "-e2", A.Set O.e2, help_e2;
+ "-p0", A.Set O.p0, help_p0;
+ "-p1", A.Set O.p1, help_p1;
+ "-p2", A.Set O.p2, help_p2;
+ ] process_file help;
+ XU.write_hook hook !includes !tables
+
+let _ = main ()
--- /dev/null
+module A = Array
+module F = Filename
+module L = List
+module P = Printf
+module S = String
+
+module O = Options
+module T = Table
+module M = Matrix
+
+let i = 0
+
+let myself = F.basename (Sys.argv.(0))
+
+let msg = P.sprintf "This file was generated by %s, do not edit" myself
+
+let border cell =
+ let str = S.make 4 'n' in
+ if cell.M.cb.T.n then str.[0] <- 's';
+ if cell.M.cb.T.e then str.[1] <- 's';
+ if cell.M.cb.T.s then str.[2] <- 's';
+ if cell.M.cb.T.w then str.[3] <- 's';
+ str :: cell.M.cc
+
+let key cell =
+ if cell.M.ck = [] then "<br/>" else S.concat " " cell.M.ck
+
+let ind i = S.make (2 * i) ' '
+
+let out_cell och cell =
+ let cc = border cell in
+ P.fprintf och "%s<td class=\"%s\">%s</td>\n"
+ (ind (i+4)) (S.concat " " cc) (key cell)
+
+let out_row och row =
+ P.fprintf och "%s<tr>\n" (ind (i+3));
+ A.iter (out_cell och) row;
+ P.fprintf och "%s</tr>\n" (ind (i+3))
+
+(****************************************************************************)
+
+let open_out html name =
+ let fname = F.concat !O.output_dir (P.sprintf "%s.xsl" name) in
+ let och = open_out fname in
+ P.fprintf och "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n\n";
+ P.fprintf och "<!-- %s -->\n\n" msg;
+ P.fprintf och "<xsl:stylesheet version=\"1.0\"\n";
+ P.fprintf och " xmlns:xsl=\"http://www.w3.org/1999/XSL/Transform\"\n";
+ if html then P.fprintf och " xmlns=\"http://www.w3.org/1999/xhtml\"\n";
+ P.fprintf och ">\n\n";
+ och
+
+let output och name matrix =
+ P.fprintf och "<xsl:template name=\"%s\">\n" name;
+ P.fprintf och "%s<table cellpadding=\"4\" cellspacing=\"0\">\n" (ind (i+1));
+ P.fprintf och "%s<tbody>\n" (ind (i+2));
+ A.iter (out_row och) matrix.M.m;
+ P.fprintf och "%s</tbody>\n" (ind (i+2));
+ P.fprintf och "%s</table>\n" (ind (i+1));
+ P.fprintf och "</xsl:template>\n\n"
+
+let close_out och =
+ P.fprintf och "</xsl:stylesheet>\n";
+ close_out och
+
+let map_incs och name =
+ P.fprintf och "<xsl:include href=\"%s.xsl\"/>\n" name
+
+let map_tbls och name =
+ P.fprintf och "%s<xsl:when test=\"@name='%s'\">\n" (ind (i+2)) name;
+ P.fprintf och "%s<xsl:call-template name=\"%s\"/>\n" (ind (i+3)) name;
+ P.fprintf och "%s</xsl:when>\n" (ind (i+2))
+
+let write_hook name incs tbls =
+ let och = open_out false name in
+ L.iter (map_incs och) incs;
+ P.fprintf och "\n<xsl:template name=\"%s\">\n" name;
+ P.fprintf och "%s<xsl:choose>\n" (ind (i+1));
+ L.iter (map_tbls och) tbls;
+ P.fprintf och "%s</xsl:choose>\n" (ind (i+1));
+ P.fprintf och "</xsl:template>\n\n";
+ close_out och
--- /dev/null
+@charset "UTF-8";
+
+/* general ******************************************************************/
+
+body {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+ margin: 2.5%;
+}
+
+a:link, a:visited {
+ text-decoration: underline;
+}
+
+a:active, a:hover, a:focus {
+ background: rgb(192, 192, 192);
+}
+
+/* blocks *******************************************************************/
+
+div.spacer {
+ text-align: center;
+}
+
+div.head1 {
+ margin: 0.5em 0;
+ text-align: center;
+ font-weight: bold;
+ font-size: xx-large;
+}
+
+div.head2 {
+ margin: 0.5em 0;
+ text-align: left;
+ font-weight: bold;
+ font-size: x-large;
+}
+
+div.text {
+ margin: 1em 0;
+ text-align: left;
+}
+
+span.date {
+ font-weight: bold;
+}
+
+/* inline decorations *******************************************************/
+
+img.icon32 {
+ border: 0;
+ width: 32px;
+ height: 32px;
+}
+
+img.rule {
+ border: 0;
+ height: 4px;
+ width: 100%;
+}
+
+img.w3c {
+ margin: 0 0.5em;
+ border: 0;
+ width: 88px;
+ height: 32px; /* this should be 31px */
+}
+
+/* background colors ********************************************************/
+
+.grey {
+ background-color:#dfdfdf; /* + 7/8 */
+}
+
+.wine {
+ background-color:#ffbfdf; /* + 3/4 */
+}
+
+.magenta {
+ background-color:#ffccff; /* + 4/5 */
+}
+
+.prune {
+ background-color:#e5ccff; /* + 4/5 */
+}
+
+.blue {
+ background-color:#ccccff; /* + 4/5 */
+}
+
+.sky {
+ background-color:#bfdfff; /* + 3/4 */
+}
+
+.cyan {
+ background-color:#bfffff; /* + 3/4 */
+}
+
+.water {
+ background-color:#ccffe5; /* + 4/5 */
+}
+
+.green {
+ background-color:#bfffbf; /* + 3/4 */
+}
+
+.grass {
+ background-color:#dfffbf; /* + 3/4 */
+}
+
+.yellow {
+ background-color:#ffffbf; /* + 3/4 */
+}
+
+.orange {
+ background-color:#ffdfbf; /* + 3/4 */
+}
+
+.red {
+ background-color:#ffbfbf; /* + 3/4 */
+}
--- /dev/null
+@charset "UTF-8";
+
+/* terms ********************************************************************/
+
+.separator {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
+
+.sort {
+ background: rgb(255, 255, 255);
+ color: rgb(128, 0, 255);
+}
+
+.lref {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
+
+.gref {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 255);
+}
+
+.appl {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
+
+.cast {
+ background: rgb(255, 255, 255);
+ color: rgb(255, 0, 0);
+}
+
+.local {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 160, 0);
+}
+
+.global {
+ background: rgb(255, 255, 255);
+ color: rgb(0, 0, 0);
+}
--- /dev/null
+@charset "UTF-8";
+
+/* positioning **************************************************************/
+
+table {
+ margin-left: auto;
+ margin-right: auto;
+ width: 100%;
+}
+
+td {
+ border-color:#000000;
+ border-width:1px;
+ color:#000000;
+}
+
+/* content types ************************************************************/
+
+.text {
+ font-style: normal;
+}
+
+.component {
+ font-style: italic;
+ text-transform: capitalize;
+}
+
+.plane {
+ font-style: italic;
+ text-transform: lowercase;
+}
+
+.file {
+ font-style: normal;
+ text-transform: lowercase;
+}
+
+.number {
+ text-align: right;
+ font-style: italic;
+ text-transform: lowercase;
+}
+
+/* cell borders *************************************************************/
+
+td.nnnn {
+ border-style:none none none none;
+}
+
+td.nnns {
+ border-style:none none none solid;
+}
+
+td.nnsn {
+ border-style:none none solid none;
+}
+
+td.nnss {
+ border-style:none none solid solid;
+}
+
+td.nsnn {
+ border-style:none solid none none;
+}
+
+td.nsns {
+ border-style:none solid none solid;
+}
+
+td.nssn {
+ border-style:none solid solid none;
+}
+
+td.nsss {
+ border-style:none solid solid solid;
+}
+
+td.snnn {
+ border-style:solid none none none;
+}
+
+td.snns {
+ border-style:solid none none solid;
+}
+
+td.snsn {
+ border-style:solid none solid none;
+}
+
+td.snss {
+ border-style:solid none solid solid;
+}
+
+td.ssnn {
+ border-style:solid solid none none;
+}
+
+td.ssns {
+ border-style:solid solid none solid;
+}
+
+td.sssn {
+ border-style:solid solid solid none;
+}
+
+td.ssss {
+ border-style:solid solid solid solid;
+}
--- /dev/null
+<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html>
+ <head>
+ <meta content="text/html; charset=UTF-8" http-equiv="content-type">
+ <title>lambdadelta home page</title>
+ <meta content="Ferruccio Guidi" name="author">
+ <meta content="The formal system lambdadelta" name="description">
+ <link rel="shortcut icon" href="download/crux_16.ico">
+ </head>
+ <body>
+ <div style="text-align: center;">
+ <br>
+ <a href="http://lambdadelta.info"><img alt="[Crux Logo]"
+ title="The Crux" src="download/crux_32.png" style="border: 0px
+ solid ; width: 32px; height: 32px;"></a>
+ <h1>The Formal System λδ (lambdadelta)<br>
+ </h1>
+ <h2>Towards the unification of terms, types, environments and
+ contexts</h2>
+ <img style="width: 95%; height: 4px;" alt="[Separator]"
+ title="Separator" src="download/rainbow.png"><br>
+ <table style="text-align: left; width: 95%; margin-left: auto;
+ margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
+ <tbody>
+ <tr>
+ <td style="vertical-align: top;">
+ <ul>
+ <li><a href="index.html">Foreword</a></li>
+ </ul>
+ <ul>
+ <li><a href="news.html">News</a></li>
+ </ul>
+ <ul>
+ <li>Papers</li>
+ </ul>
+ <ul>
+ <li><a href="implementation.html">Resources</a><br>
+ </li>
+ </ul>
+ </td>
+ <td style="vertical-align: top; text-align: left;">
+ <h3 style="text-align: right;">Documentation <img
+ style="width: 37px; height: 37px;" alt="[Butterfly]"
+ title="Butterfly" src="download/b5.png"></h3>
+ Currently the <span style="font-weight: bold;">main
+ source of
+ information</span> on λδ (version 1) is <span
+ style="font-weight: bold;">Resource
+ 1.1</span> below.<br>
+ A <span style="font-weight: bold;">summary</span> of
+ basic λδ (version
+ 1) is found in <span style="font-weight: bold;">Resource
+ 1.5</span>
+ below.<br>
+ <h3><img style="width: 32px; height: 32px;" alt="[Basic
+ lambdadelta Logo]" title="Basic lambdadelta"
+ src="download/basic_32.png"> Basic λδ version 2 (in
+ progress):</h3>
+ <table style="text-align: left; width: 100%;" border="0"
+ cellpadding="2" cellspacing="2">
+ <tbody>
+ <tr>
+ <td style="vertical-align: top;">2.1.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldp7"></a>F.
+ Guidi: <a href="download/cie_2010.pdf"><span
+ style="font-style: italic;">An
+ Efficient
+ Validation Procedure for the Formal System </span><span
+ style="font-style: italic;">λδ</span></a><span
+ style="font-style: italic;"></span>
+ (<span style="font-weight: bold;">2010-07</span>).
+ In <span style="font-style: italic;">CiE 2010
+ Local Proceedings</span>.
+ University of Azores, CMATI Booklet, pp. 204-213.
+ <a href="implementation.html#bibtex">BibTeX entry</a>.<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">2.2.<br>
+ </td>
+ <td style="vertical-align: top;"> <a name="ldp6"></a>F.
+Guidi:
+
+
+
+
+
+
+
+
+
+
+
+ <a
+href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2009.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2009-16"><span
+ style="font-style: italic;">Landau's
+ "Grundlagen der Analysis" from Automath to
+ lambdadelta</span></a> (<span
+ style="font-weight: bold;">2009-09)</span>.
+ University of
+ Bologna, technical report UBLCS-2009-16. <a
+ href="implementation.html#bibtex">BibTeX entry</a>.<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">2.3.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt7"></a>F.
+ Guidi: <a href="download/ld_talk_7s.pdf"><span
+ style="font-style: italic;">An
+ Efficient
+ Validation Procedure for the Formal System λδ</span></a>
+ (<span style="font-weight: bold;">2010-07</span>).
+ Presentation
+ at
+ CiE
+ 2010
+ (slides).<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">2.4.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt6"></a>F.
+ Guidi: <a href="download/ld_talk_6s.pdf"><span
+ style="font-style: italic;">A
+ Validator
+ for the Formal System λδ</span></a> (revised <span
+ style="font-weight: bold;">2010-02</span>).
+ Presentation
+ at
+ the
+ University
+ of
+ Bologna
+ (slides). </td>
+ </tr>
+ </tbody>
+ </table>
+ <h3><img style="width: 32px; height: 32px;" alt="[Basic
+ lambdadelta Logo]" title="Basic lambdadelta"
+ src="download/basic_32.png"> Basic λδ version 1
+ (dismissed):</h3>
+ <table style="text-align: left; width: 100%;" border="0"
+ cellpadding="2" cellspacing="2">
+ <tbody>
+ <tr>
+ <td style="vertical-align: top;">1.1.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldp5"></a>F.
+Guidi:
+ <a
+ href="http://doi.acm.org/10.1145/1614431.1614436"><span
+ style="font-style: italic;">The Formal System
+ λδ</span></a> (<span style="font-weight:
+ bold;">2009-10</span>). In ACM ToCL 11(1),
+ Article
+ No. 5 (<a
+ href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
+ <span style="font-weight: bold;">2008-07</span>).
+ CoRR
+ identifier <a
+ href="http://arxiv.org/abs/cs/0611040"><span
+ style="font-style: italic;"></span>cs/0611040</a>
+ [v10] (revised <span style="font-weight: bold;">2008-09</span>).
+ <a href="implementation.html#bibtex">BibTeX
+ entry</a>.<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.2.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldp4"></a>F.
+ Guidi: <a href="download/cie_2007.pdf"><span
+ style="font-style: italic;">Lambda
+ Types on the Lambda Calculus with
+ Abbreviations</span></a> (<span
+ style="font-weight: bold;">2007-06</span>).
+ In <span style="font-style: italic;">CiE 2007
+ Local Proceedings</span>.
+ University
+ of
+ Siena,
+ technical
+ report
+ 487,
+ p.
+ 387
+ (abstract
+ of
+ a
+ presentation). <a
+ href="implementation.html#bibtex">BibTeX
+ entry</a>.<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.3.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldp3"></a>F.
+ Guidi: <a
+href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-25"><span
+ style="font-style: italic;">Lambda Types on
+ the Lambda Calculus with
+ Abbreviations</span></a> (<span
+ style="font-weight: bold;">2006-11</span>).
+ University
+ of
+ Bologna,
+ technical
+ report
+ UBLCS-2006-25. <a
+ href="implementation.html#bibtex">BibTeX
+ entry</a>.<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.4.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldp2"></a>F.
+ Guidi: <a style="font-style: italic;"
+href="http://www.cs.unibo.it/pub/TR/UBLCS/ABSTRACTS/2006.bib?ncstrl.cabernet//BOLOGNA-UBLCS-2006-01">Lambda
+ Types
+ on
+ the
+ Lambda
+ Calculus
+ with
+ Abbreviations:
+ a
+ Certified
+ Specification</a> (<span style="font-weight:
+ bold;">2006-01</span>).
+ University of
+ Bologna, technical report UBLCS-2006-01. <a
+ href="implementation.html#bibtex">BibTeX entry</a>.<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.5.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt5"></a>F.
+ Guidi: <a style="font-style: italic;"
+ href="download/ld_talk_5s.pdf">The
+ Formal
+ System lambdadelta</a>
+ (<span style="font-weight: bold;">2008-10</span>).
+ Presentation at
+ "Advances in Constructive Topology and Logical
+ Foundations" (slides).<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.6.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt4"></a>F.
+ Guidi: <a href="download/ld_talk_4s.pdf"><span
+ style="font-style: italic;">Towards
+ the Unification of Terms, Types
+ and Contexts</span></a> (<span
+ style="font-weight: bold;">2008-03</span>).
+ Presentation
+ at
+ Types
+ 2008
+ (slides).<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.7.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt3"></a>F.
+ Guidi: <a href="download/ld_talk_3s.pdf"><span
+ style="font-style: italic;">Lambda
+ Types on the Lambda Calculus with
+ Abbreviations</span></a> (<span
+ style="font-weight: bold;">2007-06</span>).
+ Presentation
+ at
+ CiE
+ 2007
+ (slides).<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.8.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt2"></a>F.
+ Guidi: <a href="download/ld_talk_2s.pdf"><span
+ style="font-style: italic;">Lambda
+ Tipi sul Lambda Calcolo con
+ Abbreviazioni</span></a> (<span
+ style="font-weight: bold;">2007-01</span>).
+ Presentation
+ at
+ the
+ University
+ of
+ Padova
+ (slides <span style="font-weight: bold;">in
+ Italian</span>).<br>
+ <br>
+ </td>
+ </tr>
+ <tr>
+ <td style="vertical-align: top;">1.9.<br>
+ </td>
+ <td style="vertical-align: top;"><a name="ldt1"></a>F.
+Guidi:
+ <a href="download/ld_talk_1s.pdf"><span
+ style="font-style: italic;">Lambda Tipi sul
+ Lambda Calcolo con
+ Abbreviazioni: una Specifica Certificata</span></a>
+ (<span style="font-weight: bold;">2005-12</span>).
+ Presentation at
+ the University of Bologna (slides <span
+ style="font-weight: bold;">in
+ Italian</span>).<br>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ <br>
+ <a href="http://validator.w3.org/check?uri=referer"><img
+ alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
+ Transitional" src="http://www.w3.org/Icons/valid-html401"
+ style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
+ href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
+ Browser Here]" title="Use Any Browser Here"
+ src="download/globe_trans.png" style="border: 0px solid ;
+ width: 147px; height: 42px;"></a> <img style="width: 88px;
+ height: 31px;" alt="[PNG Used Here]" title="PNG Used Here]"
+ src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png"><br>
+ <br>
+ Last update 2012-12-01 by <a
+ href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+ Guidi</a><br>
+ </div>
+ </body>
+</html>
--- /dev/null
+$1 = "Automath";
+
+create_syntax_table ($1);
+
+define_syntax ("{","}",'%', $1); % comments
+define_syntax ("#","",'%', $1); % comments
+define_syntax ("%","",'%', $1); % comments
+define_syntax ("([<", ")]>", '(', $1); % brackets
+define_syntax ('"', '"', $1); % strings
+define_syntax ("a-zA-Z_0-9`'", 'w', $1); % words
+define_syntax (":+-=*@~,;.?", '+', $1); % operators
+
+
+() = define_keywords_n ($1, "EBPN_E", 2, 0);
+() = define_keywords_n ($1, "'_E''eb''pn'PRIMPROPTYPE", 4, 0);
+() = define_keywords_n ($1, "'prim''prop''type'", 6, 0);
+
+define Automath_mode ()
+{
+ variable kmap = "Automath";
+
+ set_mode(kmap, 0x04);
+ use_syntax_table (kmap);
+ runhooks("Automath_mode_hook");
+}
+
+add_mode_for_extension ("Automath", "aut");
--- /dev/null
+$1 = "Helena";
+
+create_syntax_table ($1);
+
+define_syntax ("\\*","*\\",'%', $1); % comments
+define_syntax ("([{<", ")]}>", '(', $1); % brackets
+define_syntax ('"', '"', $1); % strings
+define_syntax ("\\a-zA-Z_0-9", 'w', $1); % words
+
+set_syntax_flags ($1, 4);
+
+() = define_keywords_n ($1, "\\ax\\th", 3, 0);
+() = define_keywords_n ($1, "\\def", 4, 0);
+() = define_keywords_n ($1, "\\cong\\decl\\open", 5, 0);
+() = define_keywords_n ($1, "\\close\\graph\\sorts", 6, 0);
+() = define_keywords_n ($1, "\\require", 8, 0);
+() = define_keywords_n ($1, "\\generate", 9, 0);
+
+define helena_mode ()
+{
+ variable kmap = "Helena";
+
+ set_mode(kmap, 0x04);
+ use_syntax_table (kmap);
+ runhooks("helena_mode_hook");
+}
+
+add_mode_for_extension ("helena", "hln");
--- /dev/null
+@incollection{lambdadelta7,
+ author="F. {Guidi}",
+ title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
+ publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores",
+ address="Ponta Delgada, Portugal",
+ editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
+ booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)",
+ pages="204-213",
+ year="2010",
+ month="July"
+}
+
+@techreport{lambdadelta6,
+ author="F. {Guidi}",
+ title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}",
+ type="Technical Report",
+ institution="University of Bologna",
+ address="Bologna, Italy",
+ number="UBLCS 2009-16",
+ year="2009",
+ month="September"
+}
+
+@article{lambdadelta5,
+ author="F. {Guidi}",
+ title="{The Formal System $\lambda\delta$}",
+ publisher="ACM",
+ address="New York, NY, USA",
+ journal="Transactions on Computational Logic",
+ volume="11",
+ number="1",
+ year="2009",
+ month="October",
+ pages="Article No. 5"
+}
+
+@incollection{lambdadelta4,
+ author="F. {Guidi}",
+ title="{Lambda Types on the Lambda Calculus with Abbreviations}",
+ publisher="Universit\`a di Siena",
+ address="Siena, Italy",
+ editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
+ booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487",
+ pages="387-387",
+ year="2007",
+ month="June"
+}
+
+@techreport{lambdadelta3,
+ author="F. {Guidi}",
+ title="{Lambda-Types on the Lambda-Calculus with Abbreviations}",
+ type="Technical Report",
+ institution="University of Bologna",
+ address="Bologna, Italy",
+ number="UBLCS 2006-25",
+ year="2006",
+ month="November"
+}
+
+@techreport{lambdadelta2,
+ author="F. {Guidi}",
+ title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}",
+ type="Technical Report",
+ institution="University of Bologna",
+ address="Bologna, Italy",
+ number="UBLCS 2006-01",
+ year="2006",
+ month="January"
+}
+
+@misc{lambdadelta1,
+ author="F. {Guidi}",
+ title="{lambda\_delta\_1}",
+ howpublished="Formal specification with the proof assistant Coq 7.3.1",
+ year="2007",
+ month="January",
+ note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}"
+}
--- /dev/null
+@incollection{lambdadelta7,
+ author="F. {Guidi}",
+ title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
+ publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores",
+ address="Ponta Delgada, Portugal",
+ editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
+ booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)",
+ pages="204-213",
+ year="2010",
+ month="July"
+}
+
+@techreport{lambdadelta6,
+ author="F. {Guidi}",
+ title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}",
+ type="Technical Report",
+ institution="University of Bologna",
+ address="Bologna, Italy",
+ number="UBLCS 2009-16",
+ year="2009",
+ month="September"
+}
+
+@article{lambdadelta5,
+ author="F. {Guidi}",
+ title="{The Formal System $\lambda\delta$}",
+ publisher="ACM",
+ address="New York, NY, USA",
+ journal="Transactions on Computational Logic",
+ volume="11",
+ number="1",
+ year="2009",
+ month="October",
+ pages="Article No. 5"
+}
+
+@incollection{lambdadelta4,
+ author="F. {Guidi}",
+ title="{Lambda Types on the Lambda Calculus with Abbreviations}",
+ publisher="Universit\`a di Siena",
+ address="Siena, Italy",
+ editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
+ booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487",
+ pages="387-387",
+ year="2007",
+ month="June"
+}
+
+@techreport{lambdadelta3,
+ author="F. {Guidi}",
+ title="{Lambda-Types on the Lambda-Calculus with Abbreviations}",
+ type="Technical Report",
+ institution="University of Bologna",
+ address="Bologna, Italy",
+ number="UBLCS 2006-25",
+ year="2006",
+ month="November"
+}
+
+@techreport{lambdadelta2,
+ author="F. {Guidi}",
+ title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}",
+ type="Technical Report",
+ institution="University of Bologna",
+ address="Bologna, Italy",
+ number="UBLCS 2006-01",
+ year="2006",
+ month="January"
+}
+
+@misc{lambdadelta1,
+ author="F. {Guidi}",
+ title="{lambda\_delta\_1}",
+ howpublished="Formal specification with the proof assistant Coq 7.3.1",
+ year="2007",
+ month="January",
+ note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}"
+}
--- /dev/null
+<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html>
+ <head>
+ <meta content="text/html; charset=UTF-8" http-equiv="content-type">
+ <title>lambdadelta home page</title>
+ <meta content="Ferruccio Guidi" name="author">
+ <meta content="The formal system lambdadelta" name="description">
+ <link rel="shortcut icon" href="download/crux_16.ico">
+ </head>
+ <body>
+ <div style="text-align: center;">
+ <br>
+ <a href="http://lambdadelta.info"><img alt="[Crux Logo]"
+ title="The Crux" src="download/crux_32.png" style="border: 0px
+ solid ; width: 32px; height: 32px;"></a>
+ <h1>The Formal System λδ (lambdadelta)<br>
+ </h1>
+ <h2>Towards the unification of terms, types, environments and
+ contexts</h2>
+ <img style="width: 95%; height: 4px;" alt="[Separator]"
+ title="Separator" src="download/rainbow.png"><br>
+ <table style="text-align: left; width: 95%; margin-left: auto;
+ margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
+ <tbody>
+ <tr>
+ <td style="vertical-align: top;">
+ <ul>
+ <li><a href="index.html">Foreword</a></li>
+ </ul>
+ <ul>
+ <li><a href="news.html">News</a></li>
+ </ul>
+ <ul>
+ <li><a href="documentation.html">Papers</a></li>
+ </ul>
+ <ul>
+ <li>Resources<br>
+ </li>
+ </ul>
+ </td>
+ <td style="vertical-align: top; text-align: left;">
+ <h3 style="text-align: right;">Computer-checked formal
+ specifications <img style="width: 37px; height: 37px;"
+ alt="[Butterfly]" title="Butterfly"
+ src="download/b9.png"></h3>
+ <span style="font-weight: bold;">Resource
+ 1</span> below provides for the statically generated <span
+ style="font-weight: bold;">natural language
+ representation</span> of
+ λδ meta-theory (faster rendering w.r.t. resource 2 below).<br>
+ <span style="font-weight: bold;">Resource 2</span> below
+ provides
+ for the dynamically generated <span style="font-weight:
+ bold;">natural
+ language representation</span> of
+ λδ meta-theory (powered by the <a
+ href="http://helm.cs.unibo.it/">HELM</a>
+ rendering engine).<br>
+ Remarkably, λδ was born and developed in the digital
+ format of <span style="font-weight: bold;">resource 3</span>
+ below, which is not the
+ formal counterpart of some informal material previously
+ written on
+ paper (as it happens for most currently digitalized
+ Mathematics).<br>
+ <ol>
+ <li><a name="static"></a>F. Guidi: <a
+ style="font-style: italic;"
+ href="static/matita/lambdadelta/">lambdadelta</a>
+ (revised <span style="font-weight: bold;">2011-09</span>).
+ Formal
+ specification for <a
+ href="http://matita.cs.unibo.it/">Matita</a> 0.5
+ (HTML pages generated
+ by the <a href="http://helm.cs.unibo.it/">HELM</a>
+ rendering engine)<br>
+ Here are the most relevant theorems proved in the
+ formal specification:
+ <ul>
+ <li><a
+href="static/matita/lambdadelta/Basic_1/pr3/pr3/pr3_confluence.con.html">Confluence
+ of
+ reduction</a> (Church-Rosser property).</li>
+ <li><a
+ href="static/matita/lambdadelta/Basic_1/ty3/props/ty3_correct.con.html">Correctness
+ of
+ types</a>.</li>
+ <li><a
+ href="static/matita/lambdadelta/Basic_1/ty3/props/ty3_unique.con.html">Uniqueness
+ of
+ types
+ up
+ to
+ conversion</a>.<br>
+ </li>
+ <li><a
+ href="static/matita/lambdadelta/Basic_1/ty3/pr3/ty3_sred_pr3.con.html">Subject
+ reduction
+ of
+ the
+ type
+ assignment</a>.</li>
+ <li><a
+href="static/matita/lambdadelta/Basic_1/ty3/arity_props/ty3_sn3.con.html">Strong
+ normalization
+ of
+ the
+ typed
+ terms</a>.</li>
+ <li><a
+ href="static/matita/lambdadelta/Basic_1/ty3/dec/ty3_inference.con.html">Decidability
+ of
+ the
+ type
+ inference
+ problem</a>.<br>
+ <br>
+ </li>
+ </ul>
+ </li>
+ <li><a name="dynamic"></a>F. Guidi: <a
+ style="font-style: italic;"
+href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html&param.thmedia-type=text/html&param.thkeys=T1%2CT2%2CL%2CE&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&param.encoding=UTF-8&param.media-type=text/html&param.keys=d_c%2CC1%2CHC2%2CL&profile=default&param.profile=default&param.CICURI=theory:/matita/lambdadelta/">lambdadelta</a>
+ (revised <span style="font-weight: bold;">2011-09</span>).
+ Formal
+ specification for <a
+ href="http://matita.cs.unibo.it/">Matita</a> 0.5 (<a
+ href="http://helm.cs.unibo.it/">HELM</a> directory).<br>
+ <br>
+ </li>
+ <li><a name="ldp1"></a>F. Guidi: <a
+ href="download/lambdadelta_1.tar.gz"><span
+ style="font-style: italic;">lambdadelta_1</span></a>
+ (revised <span style="font-weight: bold;">2011-09</span>).
+Formal
+ specification for <span style="font-weight: bold;">Coq
+ 7.3.1</span>
+ (source
+ proof scripts). <a href="#bibtex">BibTeX entry</a>.<br>
+ </li>
+ </ol>
+ <h3 style="text-align: right;">Tools <img style="width:
+ 37px; height: 37px;" alt="[Butterfly]"
+ title="Butterfly" src="download/b5.png"></h3>
+ <a name="lddl"></a><img style="width: 32px; height: 32px;"
+ alt="[Crux Logo]" title="The Crux"
+ src="download/crux_32.png"><span style="font-weight:
+ bold;"> </span>The <span style="font-weight: bold;"><span
+ style="text-decoration: underline;">λδ
+ Digital
+ Library
+ (LDDL)</span></span> is part of <a
+ href="http://helm.cs.unibo.it/">HELM</a>
+ and contains a set of
+ resources expressed in λδ.<br>
+ <ul>
+ <li><span style="font-weight: bold;">Contents:</span>
+ Landau's "<span style="font-style: italic;">Grundlagen
+ der Analysis</span>" (from
+ Jutting's specification in <a
+ href="http://www.win.tue.nl/automath/">Automath</a>).<br>
+ <span style="font-weight: bold;"></span></li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">Access:</span> <a
+ href="static/lddl/">static pages</a> (updated <span
+ style="font-weight: bold;">2011-09</span>), <a
+ href="download/lddl.tar.bz2">data set</a> (updated <span
+ style="font-weight: bold;">2011-09</span>), <a
+ href="http://lambdadelta.info/xml">HELM server URL</a>
+ (updated <span style="font-weight: bold;">2011-09</span>).</li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">Examples:</span> <a
+href="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
+ definition
+ "t234"</a> (in "basic_rg" λδ), <a
+href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
+ definition
+ "t234"</a> (in "complete_rg" λδ).<br>
+ </li>
+ </ul>
+ <br>
+ <a name="helena"></a><span style="font-weight: bold;"><img
+ style="width: 32px; height: 32px;" alt="[Helena Logo]"
+ title="Helena" src="download/helena_32.png"> <span
+ style="text-decoration: underline;">Helena</span></span>
+ is a λδ
+ processor,
+ implemented in <a href="http://caml.inria.fr/">Caml</a>
+ as a part of
+ the <a href="http://helm.cs.unibo.it/">HELM</a> software,
+ meant for
+ testing the stable features of the calculus as well as the
+ unstable
+ ones.<br>
+ The processor source code is available in the directory <a
+href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&rev=0&sc=0">/trunk/helm/software/helena/</a>
+ of the <a
+ href="http://helm.cs.unibo.it/software/index.html">HELM
+ Svn
+ repository</a>. The Svn revisions containing the stable
+ versions
+ of Helena are indicated below. <br>
+ <ul>
+ <li><span style="font-weight: bold;">Version 0.8.2.</span>
+ In
+ progress.<br>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">Version 0.8.1
+ (2010-11).</span>
+ Exploits a subset of "complete_rg" λδ as the
+ intermediate language.
+ Features importation from ".hln" files containing λδ
+ textual syntax.
+ The overall validation speed of the "<span
+ style="font-style: italic;">Grundlagen
+ der
+ Analysis</span>" increases of 22% with respect to
+ version 0.8.0. [Svn
+ revision: 11032] (<a
+ href="download/helena_0.8.1.tar.gz">archived
+ source code</a>)
+ <ul>
+ <li><span style="font-weight: bold;">2009-12.</span>
+ Helena
+ appears in F. Wiedijk's <a
+ href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">index
+of
+computer
+ math systems</a>.</li>
+ </ul>
+ </li>
+ </ul>
+ <ul>
+ <li><a style=" font-weight: bold;"
+ href="documentation.html#ldp6">Version 0.8.0</a><span
+ style="font-weight: bold;"> (2009-09).</span>
+ Supports
+ "basic_rg" λδ with naive implementation of
+ impredicative sort
+ inclusion. Features
+ importation from <a
+ href="http://www.win.tue.nl/automath/">Automath</a>
+ and exportation to <a href="http://www.w3.org/XML/">XML</a>.
+ [Svn
+ revision: 10304] (<a
+ href="download/helena_0.8.0.tar.gz">archived
+ source code</a>)<br>
+ <ul>
+ <li><span style="font-weight: bold;">2009-09.</span>
+ Jutting's specification of Landau's "<span
+ style="font-style: italic;">Grundlagen
+ der
+ Analysis</span>" enters λδ Digital Library.<br>
+ <span style="font-weight: bold;"></span></li>
+ <li><span style="font-weight: bold;">2009-06.</span>
+ Jutting's specification of Landau's "<span
+ style="font-style: italic;">Grundlagen
+ der
+ Analysis</span>" is
+ successfully processed, enabling sort inclusion<span
+ style="font-weight: bold;"></span>.</li>
+ </ul>
+ </li>
+ </ul>
+ <h3 style="text-align: right;">Other resources <img
+ style="width: 37px; height: 37px;" alt="[Butterfly]"
+ title="Butterfly" src="download/b4.png"></h3>
+ <ul>
+ <li><a name="bibtex"></a>A
+ BibTeX database of λδ documentation: <a
+ href="download/lambdadelta.bib"><span
+ style="font-style: italic;">lambdadelta.bib</span></a>,
+ <a style="font-style: italic;"
+ href="download/lambdadelta.txt">lambdadelta.txt</a>
+ (revised <span style="font-weight: bold;">2011-09</span>).</li>
+ </ul>
+ <ul>
+ <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
+ for
+ editing ".hln" files (containing λδ textual syntax): <a
+ style="font-style: italic;"
+ href="download/helena.sl">helena.sl</a>
+ (revised <span style="font-weight: bold;">2010-11</span>).</li>
+ </ul>
+ <ul>
+ <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
+ for
+ editing ".aut" files (containing <a
+ href="http://www.win.tue.nl/automath/">Automath</a>
+ textual syntax): <a style="font-style: italic;"
+ href="download/automath.sl">automath.sl</a>
+ (revised <span style="font-weight: bold;">2008-07</span>).</li>
+ </ul>
+ <ul>
+ <li>A logo for λδ: <a href="images/crux_177.png"><span
+ style="font-style: italic;">crux_177.png</span></a>
+ (revised <span style="font-weight: bold;">2012-09</span>).<br>
+ </li>
+ </ul>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ <br>
+ <a href="http://validator.w3.org/check?uri=referer"><img
+ alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
+ Transitional" src="http://www.w3.org/Icons/valid-html401"
+ style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
+ href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
+ Browser Here]" title="Use Any Browser Here"
+ src="download/globe_trans.png" style="border: 0px solid ;
+ width: 147px; height: 42px;"></a> <img style="width: 88px;
+ height: 31px;" alt="[PNG Used Here]" title="PNG Used Here"
+ src="download/PNGnow2.png"><br>
+ <br>
+ Last update 2012-12-01 by <a
+ href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+ Guidi</a><br>
+ </div>
+ </body>
+</html>
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html>
+<head>
+ <meta content="text/html; charset=UTF-8" http-equiv="content-type">
+ <title>lambdadelta home page</title>
+ <meta content="Ferruccio Guidi" name="author">
+ <meta content="The formal system lambdadelta" name="description">
+ <link rel="shortcut icon" href="download/crux_16.ico">
+</head>
+<body>
+<div style="text-align: center;">
+<br>
+<a href="http://lambdadelta.info"><img alt="[Crux Logo]"
+ title="The Crux" src="download/crux_32.png"
+ style="border: 0px solid ; width: 32px; height: 32px;"></a>
+<h1>The Formal System λδ (lambdadelta)<br>
+</h1>
+<h2>Towards the unification of terms, types, environments and contexts</h2>
+<img style="width: 95%; height: 4px;" alt="[Separator]"
+ title="Separator" src="download/rainbow.png"><br>
+<table
+ style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;"
+ border="0" cellpadding="2" cellspacing="20">
+ <tbody>
+ <tr>
+ <td style="vertical-align: top;">
+ <ul>
+ <li>Foreword</li>
+ </ul>
+ <ul>
+ <li><a href="news.html">News</a></li>
+ </ul>
+ <ul>
+ <li><a href="documentation.html">Papers</a></li>
+ </ul>
+ <ul>
+ <li><a href="implementation.html">Resources</a><br>
+ </li>
+ </ul>
+ </td>
+ <td style="vertical-align: top; text-align: left;">
+ <h3 style="text-align: right;">Foreword <img
+ style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
+ src="download/b9.png"></h3>
+The formal system λδ
+(lambdadelta) is a typed lambda calculus that pursues the static and
+dynamic unification of terms, types, environments and contexts while
+enjoying a well-conceived meta-theory, which includes the commonly
+desired properties.<br>
+ <br>
+λδ takes some features from the calculi of the Automath family and
+some from the pure type systems, but it differs from both in that it
+does not include the Π construction while it provides for an
+abbreviation mechanism at the level of terms.<br>
+ <br>
+λδ features explicit type annotations, which are borrowed from
+realistic type checker implementations and with which type checking is
+reduced to type inference.<br>
+ <br>
+The reduction steps of λδ include β-contraction, δ-expansion,
+ζ-contraction and θ-swap. On the other hand,
+η-contraction is not included.<br>
+ <br>
+The meta-theory of λδ includes important properties such as the
+confluence of reduction, the correctness of types, the
+uniqueness of types up to conversion, the subject reduction of the type
+assignment, the strong normalization of the typed terms. The
+decidability of type inference and of type checking come as corollaries.<br>
+ <br>
+λδ features uniformly dependent types and a predicative abstraction
+mechanism, so the calculus can serve as a formal specification language
+for the type theories that need a predicative foundation. λδ is
+expected to have the expressive power of λ→.<br>
+ <br>
+λδ comes in several versions listed in the following table, which
+includes the major milestones:<br>
+ <br>
+ <table style="text-align: left; width: 100%;" border="1"
+ cellpadding="2" cellspacing="0">
+ <tbody>
+ <tr>
+ <td
+ style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Version<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Name<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Started<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Released<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(223, 223, 223); text-align: center;">Dismissed<br>
+ </td>
+ </tr>
+ <tr>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 223, 191);">2<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 223, 191);">basic_2<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 223, 191);">April
+2011<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
+in
+2013<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 223, 191);">not
+planned yet<br>
+ </td>
+ </tr>
+ <tr>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 191, 191);">1<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 191, 191);">basic_1<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 191, 191);">May
+2004<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 191, 191);">November
+2006<br>
+ </td>
+ <td
+ style="vertical-align: top; background-color: rgb(255, 191, 191);">May
+2008<br>
+ </td>
+ </tr>
+ </tbody>
+ </table>
+ <br>
+ <h3 style="text-align: right;">Notice
+for
+the
+Internet
+Explorer
+user <img style="width: 37px; height: 37px;" alt="[Butterfly]"
+ title="Butterfly" src="download/b3.png"></h3>
+To view this site
+correctly, please select a font with <a href="http://www.unicode.org/">Unicode</a>
+support.
+For example <span style="font-weight: bold;">Lucida Sans Unicode</span>
+(it should be already installed on your system).
+To change the current font follow: <span style="font-weight: bold;">"Tools"
+menu
+→ "Internet
+Options" entry → "General" tab → "Fonts" button.</span><br>
+ </td>
+ </tr>
+ </tbody>
+</table>
+<br>
+<a href="http://validator.w3.org/check?uri=referer"><img
+ alt="[Valid HTML 4.01 Transitional]"
+ title="Valid HTML 4.01 Transitional"
+ src="http://www.w3.org/Icons/valid-html401"
+ style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
+ href="http://www.anybrowser.org/campaign/"><img
+ alt="[Use Any Browser Here]" title="Use Any Browser Here"
+ src="download/globe_trans.png"
+ style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
+ style="width: 88px; height: 31px;" alt="[PNG Used Here]"
+ title="PNG Used Here" src="download/PNGnow2.png"><br>
+<br>
+Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+Guidi</a><br>
+</div>
+</body>
+</html>
--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<html>
+<head>
+ <meta content="text/html; charset=UTF-8" http-equiv="content-type">
+ <title>lambdadelta home page</title>
+ <meta content="Ferruccio Guidi" name="author">
+ <meta content="The formal system lambdadelta" name="description">
+ <link rel="shortcut icon" href="download/crux_16.ico">
+</head>
+<body>
+<div style="text-align: center;"> <br>
+<a href="http://lambdadelta.info"><img alt="[Crux Logo]"
+ title="The Crux" src="download/crux_32.png"
+ style="border: 0px solid ; width: 32px; height: 32px;"></a>
+<h1>The Formal System λδ (lambdadelta)<br>
+</h1>
+<h2>Towards the unification of terms, types, environments and contexts</h2>
+<img style="width: 95%; height: 4px;" alt="[Separator]"
+ title="Separator" src="download/rainbow.png"><br>
+<table
+ style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;"
+ border="0" cellpadding="2" cellspacing="20">
+ <tbody>
+ <tr>
+ <td style="vertical-align: top;">
+ <ul>
+ <li><a href="index.html">Foreword</a></li>
+ </ul>
+ <ul>
+ <li>News</li>
+ </ul>
+ <ul>
+ <li><a href="documentation.html">Papers</a></li>
+ </ul>
+ <ul>
+ <li><a href="implementation.html">Resources</a><br>
+ </li>
+ </ul>
+ </td>
+ <td style="vertical-align: top; text-align: left;">
+ <h3 style="text-align: right;">News <img
+ style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
+ src="download/b5.png"></h3>
+ <ul>
+ <li><span style="font-weight: bold;">September 2011.</span> The
+denomination "lambdadelta" changes to "lambdadelta".
+ <ul>
+ <li>The character "-" is reserved in λδ textual syntax
+(recognized by <span style="font-style: italic;">Helena 0.8.1</span>).
+ </li>
+ <li>Eventually, the occurrences of the character "-" will
+be replaced by "_" in all λδ-related identifiers.</li>
+ <li>In particular, this refactoring involves file names and
+path names.</li>
+ <li>The permanent λδ URL is sheduled to become <span
+ style="font-style: italic;">http://lambdadelta.info</span> on
+December 2012.<br>
+ </li>
+ </ul>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">April 2011.</span> The
+specification of λδ version 2 and related topics is restarted in <a
+ href="http://matita.cs.unibo.it/">Matita 0.5</a>.
+ <ul>
+ <li><a href="apps_2.html">Here</a> is a page about the
+topics related to the specification (Applications).</li>
+ <li><a href="basic_2.html">Here</a> is a page about the
+specification (Core). </li>
+ </ul>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">December 2010.</span>
+Permanent λδ URL acquired: <a href="http://lambdadelta.info">http://lambdadelta.info</a>
+(pointing at this site). <br>
+ <span style="font-weight: bold;"></span></li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">November 2010.</span> <span
+ style="font-style: italic;">Helena 0.8.1</span> is released. <br>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">September 2009.</span> <span
+ style="font-style: italic;">Helena 0.8.0</span> is released and the <a
+ href="implementation.html#lddl">λδ Digital Library</a> is started.<br>
+ <span style="font-weight: bold;"></span></li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">June 2009.</span> <span
+ style="font-style: italic;">Helena</span>, a <a
+ href="implementation.html#helena">validator for λδ version 2</a>, is
+available as a part of the <a href="http://helm.cs.unibo.it/">HELM</a>
+software. <br>
+ </li>
+ </ul>
+ <span style="font-weight: bold;"></span>
+ <ul>
+ <li><span style="font-weight: bold;">September 2008.</span>
+This site is online.<br>
+ </li>
+ </ul>
+ <span style="font-weight: bold;"></span>
+ <ul>
+ <li><span style="font-weight: bold;">July 2008.</span> <a
+ href="documentation.html#ldp5">First journal paper on λδ</a> accepted
+for publication.</li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">July 2008.</span> First <a
+ href="http://helm.cs.unibo.it/procedural/">procedural reconstruction</a>
+for <a href="http://matita.cs.unibo.it/">Matita 0.5</a> of the <a
+ href="implementation.html#ldp1">λδ proof scripts for Coq 7.3.1</a>.<br>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">June 2008.</span> The <a
+ href="implementation.html#static">HTML pages of the specification of
+λδ version 1 for Matita 0.5</a> are online.<br>
+ <span style="font-weight: bold;"></span></li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">May 2008.</span> The
+specification of λδ version 1 is closed.<br>
+ <span style="font-weight: bold;"></span></li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">March 2008.</span> The
+specification of λδ version 2 is started with Coq 7.3.1 (false start). </li>
+ </ul>
+<!-- <ul>
+ <li>native type assignment with new rules for application: <span
+ style="font-style: italic;">nty</span> (it replaces <span
+ style="font-style: italic;">ty3</span>);<br>
+ </li>
+ <li>parallel conversion on focalized terms: <span
+ style="font-style: italic;">fpcs</span> (it replaces <span
+ style="font-style: italic;"></span><span style="font-style: italic;">pc3</span>);
+ <br>
+ </li>
+ <li>new weak parallel reduction on environments: <span
+ style="font-style: italic;">wcpr</span> <span
+ style="font-style: italic;"></span>(it is based on <span
+ style="font-style: italic;">fpr</span> and replaces <span
+ style="font-style: italic;">wcpr0</span>); <br>
+ </li>
+ <li>parallel reduction on focalized terms: <span
+ style="font-style: italic;">fpr</span> and <span
+ style="font-style: italic;">fprs</span> (they replace <span
+ style="font-style: italic;"></span><span style="font-style: italic;"></span><span
+ style="font-style: italic;">pr2</span>, <span
+ style="font-style: italic;">pr3</span>); <br>
+ </li>
+ </ul>
+ <ul>
+ <li>new thinning relation: <span
+ style="font-style: italic;">drop</span>
+(it replaces the old <span style="font-style: italic;">drop</span>, <span
+ style="font-style: italic;">clear</span>, <span
+ style="font-style: italic;">getl</span>, <span
+ style="font-style: italic;">cimp</span>, <span
+ style="font-style: italic;">drop1</span>);</li>
+ <li>new shift function: <span style="font-style: italic;">shift</span>:
+(it
+replaces
+
+ <span style="font-style: italic;">app1</span>);</li>
+ <li>new length function for environments: <span
+ style="font-style: italic;">clen</span>;<br>
+ </li>
+ <li>new relocation function: <span
+ style="font-style: italic;">lift</span> (it replaces old <span
+ style="font-style: italic;">lift</span>, <span
+ style="font-style: italic;">lift1</span>);<br>
+ </li>
+ <li>new term structure with polarity indicators and no
+distinction between binding and flat items;</li>
+ <li>new general theory of relocation (comprises new
+relocation functions: <span style="font-style: italic;">s</span>, <span
+ style="font-style: italic;">r</span>);</li>
+ <li>we removed context-free reduction and conversion (<span
+ style="font-style: italic;">pr0</span>, <span
+ style="font-style: italic;">pr1</span>, <span
+ style="font-style: italic;">pc1</span>);<br>
+ </li>
+ <li>we removed greedy substitution (<span
+ style="font-style: italic;"></span><span style="font-style: italic;">csubst0</span>,
+ <span style="font-style: italic;">csubst1</span>, <span
+ style="font-style: italic;">fsubst0</span>, <span
+ style="font-style: italic;">subst0</span>, <span
+ style="font-style: italic;">subst1</span>);<br>
+ </li>
+ <li>we removed level indicators on environments (<span
+ style="font-style: italic;">cbk</span>).</li>
+ </ul>
+-->
+ <ul>
+ <li><span style="font-weight: bold;">September 2007.</span> The
+ <a href="implementation.html#dynamic">specification of λδ
+version 1 for Matita 0.4</a> is online.</li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">November 2006.</span> <a
+ href="documentation.html#ldp3">λδ version 1</a> is released.</li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">December 2005.</span> <a
+ href="documentation.html#ldt1">First communication on λδ</a>.<br>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">May 2004.</span> The <a
+ href="implementation.html#ldp1">specification of λδ version 1</a> is
+started with Coq 7.3.1.<br>
+ </li>
+ </ul>
+ <h3 style="text-align: right;">Visibility <img
+ style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly"
+ src="download/b4.png"></h3>
+ <ul>
+ <li><span style="font-weight: bold;">February 2012.</span> The <a
+ href="http://www.google.com/">Google</a> search for <span
+ style="color: rgb(255, 0, 0);">formal system lambda delta</span> gives
+5 resources about λδ in the first 6 results.<br>
+ </li>
+ </ul>
+ <ul>
+ <li><span style="font-weight: bold;">February 2012.</span> The <a
+ href="http://www.yahoo.com/">Yahoo</a> search <span
+ style="color: rgb(255, 0, 0);">formal system lambda delta</span> gives
+this site as the first result.</li>
+ </ul>
+ </td>
+ </tr>
+ </tbody>
+</table>
+<br>
+<a href="http://validator.w3.org/check?uri=referer"><img
+ alt="[Valid HTML 4.01 Transitional]"
+ title="Valid HTML 4.01
+ Transitional"
+ src="http://www.w3.org/Icons/valid-html401"
+ style="border: 0px solid ; width: 88px; height: 31px;"></a> <a
+ href="http://www.anybrowser.org/campaign/"><img
+ alt="[Use Any
+ Browser Here]" title="Use Any Browser Here"
+ src="download/globe_trans.png"
+ style="border: 0px solid ; width: 147px; height: 42px;"></a> <img
+ style="width: 88px; height: 31px;" alt="[PNG Used Here]"
+ title="PNG Used Here" src="download/PNGnow2.png"><br>
+<br>
+Last update 2012-12-01 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+
+Guidi</a><br>
+</div>
+</body>
+</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info"
+ description = "BTM"
+ title = "BTM"
+ head = "cic:/matita/BTM/"
+>
+ <section>Character classes</section>
+ <body>This table shows how the first 45 positive integers
+ are distributed in the four classes.
+ </body>
+ <table name="chc_45"/>
+
+ <footer/>
+</page>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info"
+ description = "applications of lambdadelta version 2"
+ title = "applications of lambdadelta version 2"
+ head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
+>
+ <section>Contents of the Specification</section>
+ <body>This specification comprises a collection of checked
+ applications of λδ version 2.
+ In particular it contains the components below.
+ </body>
+ <news date="MLTT1.">
+ Martin-Löf's Type Theory with one universe
+ using λδ as theory of expressions.
+ </news>
+ <news date="Functional.">
+ The validation algorithm for λδ as implemented in
+ <rlink to="implementation.html#helena">Helena 0.8</rlink>.
+ </news>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="apps_2_sum"/>
+ <news date="2012 February 24.">
+ The Applications directory is started.
+ </news>
+ <news date="2011 December 20.">
+ The Functional component is started
+ inside the specification of λδ version 2.
+ </news>
+ <news date="2011 December 12.">
+ The MLTT1 component is started.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>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).
+ </body>
+ <table name="apps_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
--- /dev/null
+name "apps_2_src"
+
+table {
+ class "grey"
+ [ { "component" * } {
+ [ { "plane" * } {
+ [ "files" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "MLTT1" * } {
+ [ { "" * } {
+ [ "genv_primitive" "judgement" * ]
+ }
+ ]
+ }
+ ]
+ class "red"
+ [ { "functional" * } {
+ [ { "reduction and type machine" * } {
+ [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ }
+ ]
+ [ { "unfold" * } {
+ [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
+ }
+ ]
+ }
+ ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info"
+ description = "lambdadelta version 2"
+ title = "lambdadelta version 2"
+ head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
+>
+ <section>System's Syntax and Behavior</section>
+ <body>This is a summary of the "block structure"
+ of the System's syntactic items and reductions.
+ </body>
+ <table name="basic_2_blk"/>
+ <body>* In terms only.
+ ** In terms and local environments only.
+ *** In global environments only.
+ **** Sort level k in terms only.
+ </body>
+
+ <section>Summary of the Specification</section>
+ <body>Here is a numerical acount of the specification's contents
+ and its timeline.
+ </body>
+ <table name="basic_2_sum"/>
+ <news date="In progress.">
+ Context-sensitive subject equivalence
+ for native type assignment.
+ </news>
+ <news date="In progress.">
+ Closure of extended context-sensitive computation
+ for native validity.
+ </news>
+ <news date="In progress.">
+ Extended context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news date="2012 October 16.">
+ Confluence for context-free parallel reduction on closures.
+ </news>
+ <news date="2012 July 26.">
+ Term binders polarized to control ζ reduction.
+ </news>
+ <news date="2012 April 16.">
+ Context-sensitive subject equivalence
+ for atomic arity assignment
+ (anniversary milestone).
+ </news>
+ <news date="2012 March 15.">
+ Context-sensitive strong normalization
+ for simply typed terms.
+ </news>
+ <news date="2012 January 27.">
+ Support for abstract candidates of reducibility.
+ </news>
+ <news date="2011 September 21.">
+ Confluence for context-sensitive parallel reduction on terms.
+ </news>
+ <news date="2011 September 6.">
+ Confluence for context-free parallel reduction on terms.
+ </news>
+ <news date="2011 April 17.">
+ Specification starts.
+ </news>
+
+ <section>Logical Structure of the Specification</section>
+ <body>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).
+ </body>
+ <table name="basic_2_src"/>
+
+ <section>Physical Structure of the Specification</section>
+ <body>The source files are grouped in directories,
+ one for each component.
+ </body>
+ <footer/>
+</page>
--- /dev/null
+name "basic_2_blk"
+
+table {
+ class "grey" [ { "domain" * } {
+ [
+ [ "block" ] [ "leader" ]
+ [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
+ ]
+ } ]
+ [ { "{X | Γ ⊢ X : W}" * } {
+ class "wine" [
+ [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ]
+ [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
+ ]
+ class "magenta" [
+ [ "local typed declaration **" ] [ "Γ ⊢ -λW" ]
+ [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
+ ]
+ class "prune" [
+ [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+ ]
+ class "blue" [
+ [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ]
+ [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
+ ]
+ } ]
+ [ { "{X | Γ ⊢ X = V}" * } {
+ class "sky" [
+ [ "local abbreviation *" ] [ "Γ ⊢ +δV" ]
+ [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
+ ]
+ class "cyan" [
+ [ "local definition **" ] [ "Γ ⊢ -δV" ]
+ [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ]
+ ]
+ class "water" [
+ [ "global definition ***" ] [ "Γ ⊢ pδV" ]
+ [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
+ ]
+ } ]
+ [ { "no" * } {
+ class "green" [
+ [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "no" ]
+ ]
+ } ]
+}
+
+class "text" { 0 } { 2 * }
+
+class "plane" { 1 }
--- /dev/null
+name "basic_2_src"
+
+table {
+ class "grey"
+ [ { "component" * } {
+ [ { "plane" * } {
+ [ "files" * ]
+ }
+ ]
+ }
+ ]
+(*
+ class "wine"
+ [ { "examples" * } {
+ [ { "" * } {
+ [ "" * ]
+ }
+ ]
+ }
+ ]
+ class "magenta"
+ [ { "higher order dynamic typing" * } {
+ [ { "higher order native type assignment" * } {
+ [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
+ }
+ ]
+ }
+ ]
+*)
+ class "prune"
+ [ { "dynamic typing" * } {
+(*
+ [ { "local env. ref. for native type assignment" * } {
+ [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ]
+ }
+ ]
+ [ { "native type assignment" * } {
+ [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
+ }
+ ]
+*)
+ [ { "stratified native validity" * } {
+ [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" + "snv_ssta" * ]
+ }
+ ]
+ }
+ ]
+ class "blue"
+ [ { "equivalence" * } {
+ [ { "focalized equivalence" * } {
+ [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "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" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ]
+ }
+ ]
+ }
+ ]
+ class "sky"
+ [ { "conversion" * } {
+ [ { "focalized conversion" * } {
+ [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
+ [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ]
+ }
+ ]
+ [ { "context-sensitive conversion" * } {
+ [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
+ }
+ ]
+ }
+ ]
+ class "cyan"
+ [ { "computation" * } {
+(*
+ [ { "hyper computation" * } {
+ [ "ysteps ( ? ⊢ ⦃?,?⦄ •⭃*[g] ⦃?,?⦄ )" "ysteps_csups" * ]
+ [ "yprs ( ? ⊢ ⦃?,?⦄ •⥸*[g] ⦃?,?⦄ )" "yprs_csups" + "yprs_xprs" + "yprs_yprs" * ]
+ }
+ ]
+*)
+ [ { "extended computation" * } {
+ [ "xprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )" "xprs_lift" + "xprs_aaa" + "xpr_lsubss" + "xprs_cprs" + "xprs_xprs" * ]
+ }
+ ]
+ [ { "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" * ]
+ }
+ ]
+ [ { "focalized computation" * } {
+ [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_cprs" + "lfprs_lfprs" * ]
+ [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
+ }
+ ]
+ [ { "context-sensitive computation" * } {
+ [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "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" * ]
+ }
+ ]
+ }
+ ]
+ class "water"
+ [ { "reducibility" * } {
+(*
+ [ { "hyper reduction" * } {
+ [ "ypr ( ? ⊢ ⦃?,?⦄ •⥸[g] ⦃?,?⦄ )" * ]
+ }
+ ]
+*)
+ [ { "extended reduction" * } {
+ [ "xpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )" "xpr_lift" + "xpr_aaa" + "xpr_lsubss" * ]
+ }
+ ]
+ [ { "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" * ]
+ }
+ ]
+ [ { "context-sensitive normal forms" * } {
+ [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
+ }
+ ]
+ [ { "context-sensitive reduction" * } {
+ [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss" + "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" * ]
+ }
+ ]
+ }
+ ]
+ class "green"
+ [ { "unwind" * } {
+ [ { "" * } {
+ [ "" * ]
+ }
+ ]
+ }
+ ]
+(*
+ [ { "stratified unwind" * } {
+ [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" "sstas_ltpss" "sstas_sstas" * ]
+ }
+ ]
+*)
+ class "grass"
+ [ { "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" * ]
+ }
+ ]
+ }
+ ]
+ class "yellow"
+ [ { "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" * ]
+ }
+ ]
+ }
+ ]
+ class "orange"
+ [ { "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" * ]
+ }
+ ]
+ }
+ ]
+ class "red"
+ [ { "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" * ]
+ }
+ ]
+ }
+ ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for persistent lambdadelta logical data -->
+
+<!-- TERMS -->
+
+<!ENTITY % leaf '(Sort|LRef|GRef)'>
+
+<!ENTITY % node '(Cast|Appl|Abst|Abbr|Void)'>
+
+<!ENTITY % term '(%node;*,%leaf;)'>
+
+<!ENTITY % terms '(%term;*)'>
+
+<!ELEMENT Sort EMPTY>
+<!ATTLIST Sort
+ position NMTOKEN #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT LRef EMPTY>
+<!ATTLIST LRef
+ position NMTOKEN #REQUIRED
+ offset NMTOKEN #IMPLIED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT GRef EMPTY>
+<!ATTLIST GRef
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Cast %term;>
+<!ATTLIST Cast
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Appl %terms;>
+<!ATTLIST Appl
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Abst %terms;>
+<!ATTLIST Abst
+ level NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Abbr %terms;>
+<!ATTLIST Abbr
+ name NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!ELEMENT Void EMPTY>
+<!ATTLIST Void
+ name NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
+>
+
+<!-- ENVIRONMENT ENTRIES -->
+
+<!ENTITY % entity '(ABST|ABBR)'>
+
+<!ELEMENT ABST %term;>
+<!ATTLIST ABST
+ uri CDATA #REQUIRED
+ level NMTOKEN #IMPLIED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta NMTOKENS #IMPLIED
+ lang NMTOKEN "en-US"
+ info CDATA #IMPLIED
+>
+
+<!ELEMENT ABBR %term;>
+<!ATTLIST ABBR
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta NMTOKENS #IMPLIED
+ lang NMTOKEN "en-US"
+ info CDATA #IMPLIED
+>
+
+<!ELEMENT ENTITY %entity;>
+<!ATTLIST ENTITY
+ xmlns CDATA #FIXED "http://lambdadelta.info"
+ hierarchy NMTOKEN #REQUIRED
+ options NMTOKENS #IMPLIED
+>
+
+<!-- CONVERSION CONSTRAINT SYSTEM -->
+
+<!ENTITY % cc '(ToPositive|ToOne|ToNext)'>
+
+<!ENTITY % ccs '(%cc;*)'>
+
+<!ELEMENT ToPositive EMPTY>
+<!ATTLIST ToPositive
+ arity NMTOKEN #IMPLIED
+ mark NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToOne EMPTY>
+<!ATTLIST ToOne
+ arity NMTOKEN #IMPLIED
+ mark NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToNext EMPTY>
+<!ATTLIST ToNext
+ arity NMTOKEN #IMPLIED
+ prec NMTOKENS #IMPLIED
+ next NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+ xmlns CDATA #FIXED "http://lambdadelta.info"
+ uri CDATA #REQUIRED
+>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+>
+
+<xsl:param name="baseurl"/>
+
+<xsl:include href="xhtbl.xsl"/>
+<xsl:include href="ld_web_library.xsl"/>
+<xsl:include href="ld_web_root.xsl"/>
+
+<xsl:output
+ method="xml"
+ doctype-public="-//W3C//DTD XHTML 1.1//EN"
+ doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"
+ encoding="UTF-8"
+ indent="yes"
+/>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:template name="home">
+ <div class="spacer">
+ <a href="{$baseurl}">
+ <img class="icon32"
+ alt="[lambdadelta home]"
+ title="lambdadelta home"
+ src="{$baseurl}images/crux_32.png"
+ />
+ </a>
+ </div>
+</xsl:template>
+
+<xsl:template name="rule">
+ <div class="spacer">
+ <img class="rule"
+ alt="[Spacer]"
+ title="lambdadelta rainbow rule"
+ src="{$baseurl}images/rainbow.png"
+ />
+ </div>
+</xsl:template>
+
+<xsl:template name="xhtml">
+ <a href="http://validator.w3.org/check?uri=referer">
+ <img class="w3c"
+ alt="[Valid XHTML 1.1]"
+ title="Valid XHTML 1.1"
+ src="http://www.w3.org/Icons/valid-xhtml11-blue"
+ />
+ </a>
+</xsl:template>
+
+<xsl:template name="css">
+ <a href="http://jigsaw.w3.org/css-validator/check/referer">
+ <img class="w3c"
+ alt="[Valid CSS level 2]"
+ title="Valid CSS level 2"
+ src="http://www.w3.org/Icons/valid-css2-blue"
+ />
+ </a>
+</xsl:template>
+
+<xsl:template name="xslt">
+ <a href="http://www.w3.org/XML/">
+ <img class="w3c"
+ alt="[Generated from XML via XSL]"
+ title="Generated from XML via XSL"
+ src="{$baseurl}images/xml_xsl2.png"
+ />
+ </a>
+</xsl:template>
+
+<xsl:template name="png">
+ <a href="http://www.w3.org/Graphics/PNG/">
+ <img class="w3c"
+ alt="[PNG used here]"
+ title="PNG used here"
+ src="{$baseurl}images/PNGnow2.png"
+ />
+ </a>
+</xsl:template>
+
+<xsl:template name="browser">
+ <a href="http://www.anybrowser.org/campaign/">
+ <img class="w3c"
+ alt="[Viewable with any browser]"
+ title="Viewable with any browser"
+ src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"
+ />
+ </a>
+</xsl:template>
+
+<xsl:template name="helena">
+ <a href="{$baseurl}implementation.html#helena">
+ <img class="w3c"
+ alt="[Powered by Helena lambdadelta processor]"
+ title="Powered by Helena lambdadelta processor"
+ src="{$baseurl}images/helena_label.png"
+ />
+ </a>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0"
+ xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:date="http://exslt.org/dates-and-times"
+ xmlns:ld="http://lambdadelta.info"
+ xmlns="http://www.w3.org/1999/xhtml"
+ extension-element-prefixes="date"
+>
+
+<xsl:template match="ld:section">
+ <div class="head2">
+ <xsl:apply-templates/>
+ </div>
+</xsl:template>
+
+<xsl:template match="ld:body">
+ <div class="text">
+ <xsl:apply-templates/>
+ </div>
+</xsl:template>
+
+<xsl:template match="ld:rlink">
+ <a href="{$baseurl}{@to}">
+ <xsl:apply-templates/>
+ </a>
+</xsl:template>
+
+<xsl:template match="ld:news">
+ <ul><li>
+ <span class="date"><xsl:value-of select="@date"/></span>
+ <xsl:apply-templates/>
+ </li></ul>
+</xsl:template>
+
+<xsl:template match="ld:table">
+ <div class="text">
+ <xsl:call-template name="xhtbl"/>
+ </div>
+</xsl:template>
+
+<xsl:template match="ld:footer">
+ <xsl:call-template name="rule"/>
+ <div class="spacer"><br/></div>
+ <div class="spacer">
+ <xsl:call-template name="xhtml"/>
+ <xsl:call-template name="css"/>
+ <xsl:call-template name="xslt"/>
+ <xsl:apply-templates/>
+ <xsl:call-template name="png"/>
+ <xsl:call-template name="browser"/>
+ </div>
+ <div class="spacer"><br/></div>
+ <div class="spacer">
+ <xsl:value-of select="'Last update: '"/>
+ <xsl:value-of select="date:date-time()"/>
+ </div>
+</xsl:template>
+
+<xsl:template match="ld:helena-label">
+ <xsl:call-template name="helena"/>
+</xsl:template>
+
+<xsl:template match="ld:page">
+ <html xmlns="http://www.w3.org/1999/xhtml"><head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="{@description}"/>
+ <title><xsl:value-of select="@title"/></title>
+ <link rel="stylesheet" type="text/css"
+ href="{$baseurl}css/ld_web.css"
+ />
+ <link rel="stylesheet" type="text/css"
+ href="{$baseurl}css/lddl.css"
+ />
+ <link rel="stylesheet" type="text/css"
+ href="{$baseurl}css/xhtbl.css"
+ />
+ <link rel="shortcut icon"
+ href="{$baseurl}images/crux_16.ico"
+ />
+ </head><body lang="en-US">
+ <xsl:call-template name="home"/>
+ <div class="head1"><xsl:value-of select="@head"/></div>
+ <xsl:call-template name="rule"/>
+ <xsl:apply-templates/>
+ </body></html>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:param name="baseurl"/>
+
+<xsl:include href="lddl_library.xsl"/>
+<xsl:include href="lddl_term.xsl"/>
+<xsl:include href="lddl_entity.xsl"/>
+<xsl:include href="lddl_root.xsl"/>
+
+<xsl:output
+ method="xml"
+ doctype-public="-//W3C//DTD XHTML 1.1//EN"
+ doctype-system="http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd"
+ encoding="UTF-8"
+ indent="no"
+/>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ld="http://lambdadelta.info"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="ABST ABBR"/>
+
+<xsl:template name="ENTITY">
+ <xsl:param name="kind"/>
+ <div class="head2">
+ <span class="global">
+ <xsl:value-of select="$kind"/>
+ <xsl:call-template name="cn"/>
+ <xsl:call-template name="sp"/>
+ <span class="gref">
+ <xsl:call-template name="global"/>
+ </span>
+ <xsl:call-template name="sp"/>
+ <xsl:call-template name="op"/>
+ <span class="gref">
+ <xsl:call-template name="mk_path"/>
+ </span>
+ <xsl:call-template name="cp"/>
+ </span>
+ </div>
+ <div class="text">
+ <xsl:call-template name="idescr"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@meta"/>
+ <xsl:call-template name="qt"/>
+ </div>
+ <div class="text">
+ <xsl:apply-templates/>
+ </div>
+</xsl:template>
+
+<xsl:template match="ld:ABST">
+ <xsl:call-template name="ENTITY">
+ <xsl:with-param name="kind">Declaration</xsl:with-param>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template match="ld:ABBR">
+ <xsl:call-template name="ENTITY">
+ <xsl:with-param name="kind">Definition</xsl:with-param>
+ </xsl:call-template>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ld="http://lambdadelta.info"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:template name="sp">
+ <xsl:text> </xsl:text>
+</xsl:template>
+
+<xsl:template name="cm">
+ <xsl:text>, </xsl:text>
+</xsl:template>
+
+<xsl:template name="sl">
+ <xsl:text>/</xsl:text>
+</xsl:template>
+
+<xsl:template name="plus">
+ <xsl:text>+</xsl:text>
+</xsl:template>
+
+<xsl:template name="fs">
+ <xsl:text>.​</xsl:text>
+</xsl:template>
+
+<xsl:template name="op">
+ <xsl:text>(</xsl:text>
+</xsl:template>
+
+<xsl:template name="cp">
+ <xsl:text>)</xsl:text>
+</xsl:template>
+
+<xsl:template name="ob">
+ <xsl:text>[</xsl:text>
+</xsl:template>
+
+<xsl:template name="cb">
+ <xsl:text>]</xsl:text>
+</xsl:template>
+
+<xsl:template name="oa">
+ <xsl:text><</xsl:text>
+</xsl:template>
+
+<xsl:template name="ca">
+ <xsl:text>></xsl:text>
+</xsl:template>
+
+<xsl:template name="cn">
+ <xsl:text>:</xsl:text>
+</xsl:template>
+
+<xsl:template name="eq">
+ <xsl:text>=</xsl:text>
+</xsl:template>
+
+<xsl:template name="qt">
+ <xsl:text>"</xsl:text>
+</xsl:template>
+
+<xsl:template name="idescr">
+ <xsl:text>Informal description: </xsl:text>
+</xsl:template>
+
+<xsl:template name="vpars">
+ <xsl:text>Validation parameters: </xsl:text>
+</xsl:template>
+
+<xsl:template name="shier">
+ <xsl:text>sort hierarchy = </xsl:text>
+</xsl:template>
+
+<xsl:template name="kopts">
+ <xsl:text>kernel options = </xsl:text>
+</xsl:template>
+
+<xsl:template name="multiple">
+ <span class="separator">
+ <xsl:call-template name="cm"/>
+ </span>
+</xsl:template>
+
+<xsl:template name="lambda">
+ <a title="{@mark}">
+ <xsl:choose>
+ <xsl:when test="@level=0">
+ <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
+ <sup><xsl:value-of select="@level"/></sup>
+ </xsl:when>
+ <xsl:when test="@level=1">
+ <xsl:text disable-output-escaping="yes">&Pi;</xsl:text>
+ </xsl:when>
+ <xsl:when test="@level=2">
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ </xsl:when>
+ <xsl:when test="not(@level)">
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <sup><xsl:text disable-output-escaping="yes">&infin;</xsl:text></sup>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text disable-output-escaping="yes">&lambda;</xsl:text>
+ <sup><xsl:value-of select="@level"/></sup>
+ </xsl:otherwise>
+ </xsl:choose>
+ </a>
+</xsl:template>
+
+<xsl:template name="delta">
+ <a title="{@mark}">
+ <xsl:text disable-output-escaping="yes">&delta;</xsl:text>
+ </a>
+</xsl:template>
+
+<xsl:template name="chi">
+ <a title="{@mark}">
+ <xsl:text disable-output-escaping="yes">&chi;</xsl:text>
+ </a>
+</xsl:template>
+
+<xsl:template name="position">
+ <xsl:variable name="index">
+ <xsl:value-of select="@position"/>
+ <xsl:if test="@offset != 0">
+ <xsl:call-template name="plus"/>
+ <xsl:value-of select="@offset"/>
+ </xsl:if>
+ </xsl:variable>
+ <a title="{$index}">
+ <xsl:value-of select="@name"/>
+ </a>
+</xsl:template>
+
+<xsl:template name="uri">
+ <xsl:variable name="url">
+ <xsl:value-of select="$baseurl"/>
+ <xsl:value-of select="substring-after(@uri,'ld:')"/>
+ <xsl:text>.html</xsl:text>
+ </xsl:variable>
+ <a href="{$url}" title="{@uri}"><xsl:value-of select="@name"/></a>
+</xsl:template>
+
+<xsl:template name="global">
+ <a title="{@mark}">
+ <xsl:value-of select="@name"/>
+ </a>
+</xsl:template>
+
+<xsl:template name="mk_names">
+ <xsl:param name="names">
+ <xsl:value-of select="normalize-space(@name)"/>
+ <xsl:call-template name="sp"/>
+ </xsl:param>
+ <xsl:param name="sep" select="false()"/>
+ <xsl:if test="$names and $sep">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ <xsl:if test="$names">
+ <span class="lref">
+ <xsl:value-of select="substring-before($names, ' ')"/>
+ </span>
+ <xsl:call-template name="mk_names">
+ <xsl:with-param name="names" select="substring-after($names, ' ')"/>
+ <xsl:with-param name="sep" select="true()"/>
+ </xsl:call-template>
+ </xsl:if>
+</xsl:template>
+
+<xsl:template name="mk_terms">
+ <xsl:for-each select="*">
+ <xsl:apply-templates select="."/>
+ <xsl:if test="(name()='Sort' or name()='LRef' or name()='GRef') and position()!=last()">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ </xsl:for-each>
+</xsl:template>
+
+<xsl:template name="mk_binder">
+ <xsl:param name="sep-seq"/>
+ <xsl:call-template name="ob"/>
+ <xsl:call-template name="mk_binder_rec1">
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ </xsl:call-template>
+ <xsl:call-template name="cb"/>
+</xsl:template>
+
+<xsl:template name="mk_binder_rec1">
+ <xsl:param name="sep-seq"/>
+ <xsl:param name="names">
+ <xsl:value-of select="normalize-space(@name)"/>
+ <xsl:call-template name="sp"/>
+ </xsl:param>
+ <xsl:param name="sep" select="false()"/>
+ <xsl:param name="start" select="true()"/>
+ <xsl:param name="pos" select="1"/>
+ <xsl:choose>
+ <xsl:when test="$start and $pos <= count(*)">
+ <xsl:if test="$names and $sep">
+ <xsl:call-template name="multiple"/>
+ </xsl:if>
+ <span class="lref">
+ <xsl:value-of select="substring-before($names, ' ')"/>
+ </span>
+ <xsl:copy-of select="$sep-seq"/>
+ <xsl:call-template name="mk_binder_rec2">
+ <xsl:with-param name="names" select="substring-after($names, ' ')"/>
+ <xsl:with-param name="pos" select="$pos"/>
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:when test="not($start) and $pos <= count(*)">
+ <xsl:call-template name="mk_binder_rec2">
+ <xsl:with-param name="names" select="$names"/>
+ <xsl:with-param name="pos" select="$pos"/>
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ </xsl:call-template>
+ </xsl:when>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="mk_binder_rec2">
+ <xsl:param name="sep-seq"/>
+ <xsl:param name="names"/>
+ <xsl:param name="pos"/>
+ <xsl:apply-templates select="*[$pos]"/>
+ <xsl:call-template name="mk_binder_rec1">
+ <xsl:with-param name="sep-seq" select="$sep-seq"/>
+ <xsl:with-param name="names" select="$names"/>
+ <xsl:with-param name="sep" select="true()"/>
+ <xsl:with-param name="start" select="name(*[$pos])='Sort' or name(*[$pos])='LRef' or name(*[$pos])='GRef'"/>
+ <xsl:with-param name="pos" select="$pos+1"/>
+ </xsl:call-template>
+</xsl:template>
+
+<xsl:template name="mk_segment">
+ <xsl:param name="path"/>
+ <xsl:param name="name"/>
+ <xsl:variable name="url">
+ <xsl:value-of select="$baseurl"/>
+ <xsl:value-of select="substring-after($path,'ld:')"/>
+ </xsl:variable>
+ <a href="{$url}"><xsl:value-of select="$name"/></a>
+ <xsl:call-template name="sl"/>
+</xsl:template>
+
+<xsl:template name="mk_path">
+ <xsl:param name="rpath" select="@uri"/>
+ <xsl:variable name="newrpath" select="substring-after($rpath,'/')"/>
+ <xsl:choose>
+ <xsl:when test="$newrpath">
+ <xsl:variable name="segment" select="substring-before($rpath,$newrpath)"/>
+ <xsl:call-template name="mk_segment">
+ <xsl:with-param name="path" select="substring-before(@uri,$newrpath)"/>
+ <xsl:with-param name="name" select="substring-before($segment,'/')"/>
+ </xsl:call-template>
+ <xsl:call-template name="mk_path">
+ <xsl:with-param name="rpath" select="$newrpath"/>
+ </xsl:call-template>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:variable name="path" select="substring-before(@uri,$rpath)"/>
+ <xsl:value-of select="substring-after(@uri,$path)"/>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template name="lddl">
+ <xsl:text disable-output-escaping="yes">&lambda;&delta; Digital Library (LDDL)</xsl:text>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ld="http://lambdadelta.info"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="ENTITY"/>
+
+<xsl:template match="/">
+ <html xmlns="http://www.w3.org/1999/xhtml"><head>
+ <meta http-equiv="Content-Language" content="en-us"/>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+ <meta http-equiv="Content-Style-Type" content="text/css"/>
+ <meta name="author" content="Ferruccio Guidi"/>
+ <meta name="description" content="lambdadelta digital library"/>
+ <title>lambdadelta digital library (LDDL)</title>
+ <link rel="stylesheet" type="text/css"
+ href="http://lambdadelta.info/css/ld.css"
+ />
+ <link rel="stylesheet" type="text/css"
+ href="http://lambdadelta.info/css/lddl.css"
+ />
+ <link rel="shortcut icon"
+ href="http://lambdadelta.info/download/crux_16.ico"
+ />
+ </head><body>
+ <div class="spacer">
+ <a href="http://lambdadelta.info/">
+ <img class="icon32"
+ alt="[lambdadelta home]" title="lambdadelta home"
+ src="http://lambdadelta.info/download/crux_32.png"
+ /></a>
+ </div>
+ <div class="head1">
+ <xsl:call-template name="lddl"/>
+ </div>
+ <div class="spacer">
+ <img class="rule"
+ alt="[Spacer]" title="lambdadelta rainbow rule"
+ src="http://lambdadelta.info/download/rainbow.png"
+ />
+ </div>
+ <xsl:apply-templates/>
+ <div class="spacer">
+ <a href="http://validator.w3.org/check?uri=referer">
+ <img class="w3c"
+ alt="[Valid XHTML 1.1]"
+ title="Valid XHTML 1.1"
+ src="http://www.w3.org/Icons/valid-xhtml11-blue"
+ /></a>
+ <a href="http://jigsaw.w3.org/css-validator/check/referer">
+ <img class="w3c"
+ alt="[Valid CSS level 2]"
+ title="Valid CSS level 2"
+ src="http://www.w3.org/Icons/valid-css2-blue"
+ /></a>
+ <a href="http://www.w3.org/XML/">
+ <img class="w3c"
+ alt="[Generated from XML via XSL]"
+ title="Generated from XML via XSL"
+ src="http://lambdadelta.info/download/xml_xsl2.png"
+ /></a>
+ <a href="http://lambdadelta.info/implementation.html#helena">
+ <img class="w3c"
+ alt="[Powered by Helena lambdadelta processor]"
+ title="Powered by Helena lambdadelta processor"
+ src="http://lambdadelta.info/download/helena_label.png"
+ /></a>
+ <a href="http://www.w3.org/Graphics/PNG/">
+ <img class="w3c"
+ alt="[PNG used here]"
+ title="PNG used here"
+ src="http://lambdadelta.info/download/PNGnow2.png"
+ /></a>
+ <a href="http://www.anybrowser.org/campaign/">
+ <img class="w3c"
+ alt="[Viewable with any browser]"
+ title="Viewable with any browser"
+ src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"
+ /></a>
+ </div>
+ </body></html>
+</xsl:template>
+
+<xsl:template match="ld:ENTITY">
+ <xsl:apply-templates/>
+ <div class="text">
+ <xsl:call-template name="vpars"/>
+ <xsl:call-template name="shier"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@hierarchy"/>
+ <xsl:call-template name="qt"/>
+ <xsl:call-template name="cm"/>
+ <xsl:call-template name="sp"/>
+ <xsl:call-template name="kopts"/>
+ <xsl:call-template name="qt"/>
+ <xsl:value-of select="@options"/>
+ <xsl:call-template name="qt"/>
+ </div>
+</xsl:template>
+
+</xsl:stylesheet>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+ xmlns:ld="http://lambdadelta.info"
+ xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:strip-space elements="Sort LRef GRef Cast Appl Abst Abbr Void"/>
+
+<xsl:template name="separator">
+ <span class="separator">
+ <xsl:call-template name="fs"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="ld:Sort">
+ <span class="sort">
+ <xsl:call-template name="position"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="ld:LRef">
+ <span class="lref">
+ <xsl:call-template name="position"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="ld:GRef">
+ <span class="gref">
+ <xsl:call-template name="uri"/>
+ </span>
+</xsl:template>
+
+<xsl:template match="ld:Cast">
+ <span class="cast">
+ <xsl:call-template name="oa"/>
+ <xsl:apply-templates/>
+ <xsl:call-template name="ca"/>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="ld:Appl">
+ <span class="appl">
+ <xsl:call-template name="op"/>
+ <xsl:call-template name="mk_terms"/>
+ <xsl:call-template name="cp"/>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="ld:Abst">
+ <span class="local">
+ <xsl:call-template name="lambda"/>
+ <xsl:call-template name="mk_binder">
+ <xsl:with-param name="sep-seq">
+ <xsl:call-template name="cn"/>
+ </xsl:with-param>
+ </xsl:call-template>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="ld:Abbr">
+ <span class="local">
+ <xsl:call-template name="delta"/>
+ <xsl:call-template name="mk_binder">
+ <xsl:with-param name="sep-seq">
+ <xsl:call-template name="eq"/>
+ </xsl:with-param>
+ </xsl:call-template>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+<xsl:template match="ld:Void">
+ <span class="local">
+ <xsl:call-template name="chi"/>
+ <xsl:call-template name="ob"/>
+ <xsl:call-template name="mk_names"/>
+ <xsl:call-template name="cb"/>
+ </span>
+ <xsl:call-template name="separator"/>
+</xsl:template>
+
+</xsl:stylesheet>
projects / helm.git / commitdiff
