+++ /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://lambda_delta.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://lambda-delta.info/css/ld_web.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
- <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
- </head>
- <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/BTM/</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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-11-22T16:07:02+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://lambda-delta.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/lambda_delta
-RXMLDIR = $(REMOTE):$(RDIR)/xml
-RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl
-
-SLS = helena.sl automath.sl
-BIB = lambda_delta.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://lambda_delta.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 lambda_delta version 2"/>
- <title>applications of lambda_delta version 2</title>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
- <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
- </head>
- <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/apps_2/ (applications of λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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-11-22T16:07:02+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://lambda_delta.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="lambda_delta version 2"/>
- <title>lambda_delta version 2</title>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/ld_web.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/lddl.css"/>
- <link rel="stylesheet" type="text/css" href="http://lambda-delta.info/css/xhtbl.css"/>
- <link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
- </head>
- <body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/basic_2/ (λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.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="lambda_delta rainbow rule" src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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-11-22T16:07:02+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://lambda-delta.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>lambda_delta home page</title>
- <meta content="Ferruccio Guidi" name="author">
- <meta content="The formal system lambda_delta" name="description">
- <link rel="shortcut icon" href="download/crux_16.ico">
- </head>
- <body>
- <div style="text-align: center;">
- <br>
- <a href="http://lambda-delta.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 λδ (lambda_delta)<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
- lambda_delta Logo]" title="Basic lambda_delta"
- 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
- lambda-delta</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
- lambda_delta Logo]" title="Basic lambda_delta"
- 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 lambda-delta</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-02-24 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>lambda_delta home page</title>
- <meta content="Ferruccio Guidi" name="author">
- <meta content="The formal system lambda_delta" name="description">
- <link rel="shortcut icon" href="download/crux_16.ico">
- </head>
- <body>
- <div style="text-align: center;">
- <br>
- <a href="http://lambda-delta.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 λδ (lambda_delta)<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/lambda_delta/">lambda_delta</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/lambda_delta/Basic_1/pr3/pr3/pr3_confluence.con.html">Confluence
- of
- reduction</a> (Church-Rosser property).</li>
- <li><a
- href="static/matita/lambda_delta/Basic_1/ty3/props/ty3_correct.con.html">Correctness
- of
- types</a>.</li>
- <li><a
- href="static/matita/lambda_delta/Basic_1/ty3/props/ty3_unique.con.html">Uniqueness
- of
- types
- up
- to
- conversion</a>.<br>
- </li>
- <li><a
- href="static/matita/lambda_delta/Basic_1/ty3/pr3/ty3_sred_pr3.con.html">Subject
- reduction
- of
- the
- type
- assignment</a>.</li>
- <li><a
-href="static/matita/lambda_delta/Basic_1/ty3/arity_props/ty3_sn3.con.html">Strong
- normalization
- of
- the
- typed
- terms</a>.</li>
- <li><a
- href="static/matita/lambda_delta/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/lambda_delta/">lambda_delta</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/lambda_delta_1.tar.gz"><span
- style="font-style: italic;">lambda_delta_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://lambda-delta.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/lambda_delta.bib"><span
- style="font-style: italic;">lambda_delta.bib</span></a>,
- <a style="font-style: italic;"
- href="download/lambda_delta.txt">lambda_delta.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-10-16 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>lambda_delta home page</title>
- <meta content="Ferruccio Guidi" name="author">
- <meta content="The formal system lambda_delta" name="description">
- <link rel="shortcut icon" href="download/crux_16.ico">
-</head>
-<body>
-<div style="text-align: center;">
-<br>
-<a href="http://lambda-delta.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 λδ (lambda_delta)<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 λδ
-(lambda_delta) 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-11-20 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>lambda_delta home page</title>
- <meta content="Ferruccio Guidi" name="author">
- <meta content="The formal system lambda_delta" name="description">
- <link rel="shortcut icon" href="download/crux_16.ico">
-</head>
-<body>
-<div style="text-align: center;"> <br>
-<a href="http://lambda-delta.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 λδ (lambda_delta)<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 "lambda-delta" changes to "lambda_delta".
- <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://lambda_delta.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://lambda-delta.info">http://lambda-delta.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-11-20 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://lambda_delta.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://lambda_delta.info"
- description = "applications of lambda_delta version 2"
- title = "applications of lambda_delta version 2"
- head = "cic:/matita/lambda_delta/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://lambda_delta.info"
- description = "lambda_delta version 2"
- title = "lambda_delta version 2"
- head = "cic:/matita/lambda_delta/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 lambda_delta 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://lambda-delta.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://lambda-delta.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="[lambda_delta home]"
- title="lambda_delta home"
- src="{$baseurl}images/crux_32.png"
- />
- </a>
- </div>
-</xsl:template>
-
-<xsl:template name="rule">
- <div class="spacer">
- <img class="rule"
- alt="[Spacer]"
- title="lambda_delta 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 lambda_delta processor]"
- title="Powered by Helena lambda_delta 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://lambda_delta.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://lambda-delta.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://lambda-delta.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://lambda-delta.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="lambda_delta digital library"/>
- <title>lambda_delta digital library (LDDL)</title>
- <link rel="stylesheet" type="text/css"
- href="http://lambda-delta.info/css/ld.css"
- />
- <link rel="stylesheet" type="text/css"
- href="http://lambda-delta.info/css/lddl.css"
- />
- <link rel="shortcut icon"
- href="http://lambda-delta.info/download/crux_16.ico"
- />
- </head><body>
- <div class="spacer">
- <a href="http://lambda-delta.info/">
- <img class="icon32"
- alt="[lambda_delta home]" title="lambda_delta home"
- src="http://lambda-delta.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="lambda_delta rainbow rule"
- src="http://lambda-delta.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://lambda-delta.info/download/xml_xsl2.png"
- /></a>
- <a href="http://lambda-delta.info/implementation.html#helena">
- <img class="w3c"
- alt="[Powered by Helena lambda_delta processor]"
- title="Powered by Helena lambda_delta processor"
- src="http://lambda-delta.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://lambda-delta.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://lambda-delta.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
