| author | blanchet |
| Fri, 08 Mar 2013 14:15:39 +0100 | |
| changeset 51380 | cac8c9a636b6 |
| parent 49510 | ba50d204095e |
| child 52794 | aae782070611 |
| permissions | -rw-r--r-- |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
<html> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
<head> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
7 |
<title>BNF Package</title> |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
</head> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
<body> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
|
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
12 |
<h3><i>BNF</i>: A (co)datatype package based on bounded natural functors |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
(BNFs)</h3> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
<p> |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
16 |
The <i>BNF</i> package provides a fully modular framework for constructing |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
17 |
inductive and coinductive datatypes in HOL, with support for mixed mutual and |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
18 |
nested (co)recursion. Mixed (co)recursion enables type definitions involving |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
19 |
both datatypes and codatatypes, such as the type of finitely branching trees of |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
20 |
possibly infinite depth. The framework draws heavily from category theory. |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
<p> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
The package is described in the following paper: |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
<ul> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
<li><a href="http://www21.in.tum.de/~traytel/papers/codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
<i>Logic in Computer Science (LICS 2012)</i>, 2012. |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
</ul> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
<p> |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
32 |
The main entry point for applications is <tt>BNF.thy</tt>. The <tt>Examples</tt> |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
33 |
directory contains various examples of (co)datatypes, including the examples |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
34 |
from the paper. |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
<p> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
The key notion underlying the package is that of a <i>bounded natural functor</i> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
(<i>BNF</i>)—an enriched type constructor satisfying specific properties |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
preserved by interesting categorical operations (composition, least fixed point, |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
40 |
and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt> |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
41 |
files register various basic types, notably for sums, products, function spaces, |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
42 |
finite sets, multisets, and countable sets. Custom BNFs can be registered as well. |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
<p> |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
45 |
<b>Warning:</b> The package is under development. Please contact any nonempty |
|
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49159
diff
changeset
|
46 |
subset of |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
<a href="mailto:traytel@in.tum.de">the</a> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
<a href="mailto:popescua@in.tum.de">above</a> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
<a href="mailto:blanchette@in.tum.de">authors</a> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
if you have questions or comments. |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
</body> |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
</html> |