Name
Abstract | ||
|---|---|---|
predecessor. A typical example for a prim. rec. algorithm is the natural definition of the factorial function. It is common belief that prim. rec. cannot be reduced to it- eration in a computationally faithful manner. This is because no encoding of natural numbers in the polymorphic lambda-calculus (System F) seems possible which supports a constant-time predecessor operation (see Sp lawski and Urzy- czyn (SU99)). Mendler extended System F by a scheme of prim. rec. for rank-1 datatypes and proved strong normalization (Men87). Mendler's formulation does not follow the usual category-theoretic approach with initial recursive algebras (see Geuvers (Geu92)). For rank-2 datatypes there are also examples of functions which can most naturally be implemented with prim. rec. One is redecoration for triangular ma- trices which is presented below. These examples are not instances of generalized foldsa la Bird et al., which remain within the realm of iteration but hardwire Kan extensions into the recursion scheme. Rank-2 prim. rec., which we propose in this work, seeks to extend rank-2 iteration in the same way that prim. rec. extends rank-1 iteration. We achieve this by lifting Mendler's scheme of prim. rec. to rank 2. The decision for Mendler-style and against the traditional way roots in the following observation: Experiments with formulations according to the traditional style showed unnecessary but unavoidable traversals of the whole data structures in our examples. Mendler's style, however, yielded precisely the ? The first author is supported by the Graduiertenkolleg "Logik in der Informatik" of |
Year | Venue | DocType |
|---|---|---|
2003 | FICS | Conference |
Citations | PageRank | References |
0 | 0.34 | 5 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Abel | 1 | 131 | 9.57 |
| Ralph Matthes | 2 | 201 | 21.67 |