2 |
2 |
3 <html> |
3 <html> |
4 |
4 |
5 <head> |
5 <head> |
6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
7 <title>Codatatype Package</title> |
7 <title>BNF Package</title> |
8 </head> |
8 </head> |
9 |
9 |
10 <body> |
10 <body> |
11 |
11 |
12 <h3><i>Codatatype</i>: A (co)datatype package based on bounded natural functors |
12 <h3><i>BNF</i>: A (co)datatype package based on bounded natural functors |
13 (BNFs)</h3> |
13 (BNFs)</h3> |
14 |
14 |
15 <p> |
15 <p> |
16 The <i>Codatatype</i> package provides a fully modular framework for |
16 The <i>BNF</i> package provides a fully modular framework for constructing |
17 constructing inductive and coinductive datatypes in HOL, with support for mixed |
17 inductive and coinductive datatypes in HOL, with support for mixed mutual and |
18 mutual and nested (co)recursion. Mixed (co)recursion enables type definitions |
18 nested (co)recursion. Mixed (co)recursion enables type definitions involving |
19 involving both datatypes and codatatypes, such as the type of finitely branching |
19 both datatypes and codatatypes, such as the type of finitely branching trees of |
20 trees of possibly infinite depth. The framework draws heavily from category |
20 possibly infinite depth. The framework draws heavily from category theory. |
21 theory. |
|
22 |
21 |
23 <p> |
22 <p> |
24 The package is described in the following paper: |
23 The package is described in the following paper: |
25 |
24 |
26 <ul> |
25 <ul> |
28 Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br> |
27 Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br> |
29 <i>Logic in Computer Science (LICS 2012)</i>, 2012. |
28 <i>Logic in Computer Science (LICS 2012)</i>, 2012. |
30 </ul> |
29 </ul> |
31 |
30 |
32 <p> |
31 <p> |
33 The main entry point for applications is <tt>Codatatype.thy</tt>. |
32 The main entry point for applications is <tt>BNF.thy</tt>. The <tt>Examples</tt> |
34 The <tt>Examples</tt> directory contains various examples of (co)datatypes, |
33 directory contains various examples of (co)datatypes, including the examples |
35 including the examples from the paper. |
34 from the paper. |
36 |
35 |
37 <p> |
36 <p> |
38 The key notion underlying the package is that of a <i>bounded natural functor</i> |
37 The key notion underlying the package is that of a <i>bounded natural functor</i> |
39 (<i>BNF</i>)—an enriched type constructor satisfying specific properties |
38 (<i>BNF</i>)—an enriched type constructor satisfying specific properties |
40 preserved by interesting categorical operations (composition, least fixed point, |
39 preserved by interesting categorical operations (composition, least fixed point, |
41 and greatest fixed point). The <tt>Basic_BNFs.thy</tt> file registers |
40 and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt> |
42 various basic types, notably for sums, products, function spaces, finite sets, |
41 files register various basic types, notably for sums, products, function spaces, |
43 multisets, and countable sets. Custom BNFs can be registered as well. |
42 finite sets, multisets, and countable sets. Custom BNFs can be registered as well. |
44 |
43 |
45 <p> |
44 <p> |
46 <b>Warning:</b> The package is under development. Future versions are expected |
45 <b>Warning:</b> The package is under development. Please contact any nonempty |
47 to support multiple constructors and selectors per (co)datatype (instead of a |
46 subset of |
48 single <i>fld</i> or <i>unf</i> constant) and provide a nicer syntax for |
|
49 (co)induction and (co)recursive function definitions. Please contact |
|
50 any nonempty subset of |
|
51 <a href="mailto:traytel@in.tum.de">the</a> |
47 <a href="mailto:traytel@in.tum.de">the</a> |
52 <a href="mailto:popescua@in.tum.de">above</a> |
48 <a href="mailto:popescua@in.tum.de">above</a> |
53 <a href="mailto:blanchette@in.tum.de">authors</a> |
49 <a href="mailto:blanchette@in.tum.de">authors</a> |
54 if you have questions or comments. |
50 if you have questions or comments. |
55 |
51 |