Bushes are considered as the first example of a truly nested datatype, i. e., a family of datatypes indexed over all types where a constructor argument not only calls this family with a changing index but even with an index that involves the family itself. For tho time being, no induction principles for these datatypes are known. However, the author has introduced with Abel and Uustalu (TCS 333(1-2), pp. 3-66, 2005) iteration schemes that guarantee to define only terminating functions on those datatypes. The article uses a generalization of Bushes to n-fold self-application and shows how to define elements of these types that have a number of data entries that is obtained by iterated raising to the power of n. Moreover, the data entries are just all the n-branching trees up to a certain height. The real question is how to extract this list of trees from that complicated data structure and to prove this extraction correct. Here, we use the "refined conventional iteration" from the cited article for the extraction and describe a verification that has been formally verified inside Coq with its predicative notion of set. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Matthes, R. (2006). A datastructure for iterated powers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4014 LNCS, pp. 299–315). Springer Verlag. https://doi.org/10.1007/11783596_18
Mendeley helps you to discover research relevant for your work.