The proceedings contain 5 papers. The topics discussed include: hereditary substitutions for simple types, formalized;hereditarily finite representations of natural numbers and self-delimiting codes;foundational progr...
ISBN:
(纸本)9781450302555
The proceedings contain 5 papers. The topics discussed include: hereditary substitutions for simple types, formalized;hereditarily finite representations of natural numbers and self-delimiting codes;foundational program verification in Coq with automated proofs;type inference in context;and arrows are strong monads.
Using a bijection between natural numbers and hereditarily finite functions we derive a new reversible variable length self-delimiting code through a bitstring representation in a balanced parenthesis language. The co...
详细信息
ISBN:
(纸本)9781450302555
Using a bijection between natural numbers and hereditarily finite functions we derive a new reversible variable length self-delimiting code through a bitstring representation in a balanced parenthesis language. The code features the ability to encode arbitrarily nested data types, can represent huge (low "complexity") numbers, and is decodable from its beginning or its end. Besides its possible practical applications to media stream encodings, a comparison with the well-known Elias omega code and a conjecture about its asymptotic: behavior under the Kraft inequality suggest it as an interesting object of study for experimental mathematicians. The paper is organized as a self-contained literate Haskell program inviting the reader to explore its content independently. Its code is available at http://***/tarau/research/2010/***.
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functionalprogramming l...
详细信息
ISBN:
(纸本)9781450302555
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functionalprogramming language Haskell, which (1) optimally plays sequential games, (2) implements a computational version of the Tychonoff Theorem from topology, and (3) realizes the Double-Negation Shift from logic and proof theory. The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad. In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).
暂无评论