Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userRanking and Unranking of Hereditarily Finite Functions and Permutations
93
0
0.0
(
0
)
Added by
Paul Tarau
Publication date
2008
fields
Informatics Engineering
and research's language is
English
Authors
Paul Tarau
Ask ChatGPT about the research
No Arabic abstract
Prologs ability to return multiple answers on backtracking provides an elegant mechanism to derive reversible encodings of combinatorial objects as Natural Numbers i.e. {em ranking} and {em unranking} functions. Starting from a generalization of Ackermans encoding of Hereditarily Finite Sets with Urelements and a novel tupling/untupling operation, we derive encodings for Finite Functions and use them as building blocks for an executable theory of {em Hereditarily Finite Functions}. The more difficult problem of {em ranking} and {em unranking} {em Hereditarily Finite Permutations} is then tackled using Lehmer codes and factoradics. The paper is organized as a self-contained literate Prolog program available at url{http://logic.csci.unt.edu/tarau/research/2008/pHFF.zip}
rate research
Read More
The paper is organized as a self-contained literate Haskell program that implements elements of an executable finite set theory with focus on combinatorial generation and arithmetic encodings. The code, tested under GHC 6.6.1, is available at http://logic.csci.unt.edu/tarau/research/2008/fSET.zip . We introduce ranking and unranking functions generalizing Ackermanns encoding to the universe of Hereditarily Finite Sets with Urelements. Then we build a lazy enumerator for Hereditarily Finite Sets with Urelements that matches the unranking function provided by the inverse of Ackermanns encoding and we describe functors between them resulting in arithmetic encodings for powersets, hypergraphs, ordinals and choice functions. After implementing a digraph representation of Hereditarily Finite Sets we define {em decoration functions} that can recover well-founded sets from encodings of their associated acyclic digraphs. We conclude with an encoding of arbitrary digraphs and discuss a concept of duality induced by the set membership relation. Keywords: hereditarily finite sets, ranking and unranking functions, executable set theory, arithmetic encodings, Haskell data representations, functional programming and computational mathematics
Inspired by a width invariant defined on permutations by Guillemot and Marx, the twin-width invariant has been recently introduced by Bonnet, Kim, Thomasse, and Watrigant. We prove that a class of binary relational structures (that is: edge-colored partially directed graphs) has bounded twin-width if and only if it is a first-order transduction of a~proper permutation class. As a by-product, it shows that every class with bounded twin-width contains at most $2^{O(n)}$ pairwise non-isomorphic $n$-vertex graphs.
For which sets A does there exist a mapping, computed by a total or partial recursive function, such that the mapping, when its domain is restricted to A, is a 1-to-1, onto mapping to $Sigma^*$? And for which sets A does there exist such a mapping that respects the lexicographical ordering within A? Both cases are types of perfect, minimal hash functions. The complexity-theoret
We introduce a method for proving almost sure termination in the context of lambda calculus with continuous random sampling and explicit recursion, based on ranking supermartingales. This result is extended in three ways. Antitone ranking functions have weaker restrictions on how fast they must decrease, and are applicable to a wider range of programs. Sparse ranking functions take values only at a subset of the programs reachable states, so they are simpler to define and more flexible. Ranking functions with respect to alternative reduction strategies give yet more flexibility, and significantly increase the applicability of the ranking supermartingale approach to proving almost sure termination, thanks to a novel (restricted) confluence result which is of independent interest. The notion of antitone ranking function was inspired by similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language, but adapted to a higher-order functional language. The sparse ranking function and confluent semantics extensions are unique to the higher-order setting. Our methods can be used to prove almost sure termination of programs that are beyond the reach of methods in the literature, including higher-order and non-affine recursion.
The verification of many algorithms for calculating transcendental functions is based on polynomial approximations to these functions, often Taylor series approximations. However, computing and verifying approximations to the arctangent function are very challenging problems, in large part because the Taylor series converges very slowly to arctangent-a 57th-degree polynomial is needed to get three decimal places for arctan(0.95). Medina proposed a series of polynomials that approximate arctangent with far faster convergence-a 7th-degree polynomial is all that is needed to get three decimal places for arctan(0.95). We present in this paper a proof in ACL2(r) of the correctness and convergence rate of this sequence of polynomials. The proof is particularly beautiful, in that it uses many results from real analysis. Some of these necessary results were proven in prior work, but some were proven as part of this effort.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
