Venanzio Capretta, Graham Hutton, Mauro Jaskelioff · Repository@Nottingham (University of Nottingham) · 2016
Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they actually generate a productive infinite object? A standard means to achieve productivity is to use Banach's fixed-point theorem, which guarantees the unique existence of solutions to recursive equations on metric spaces under certain conditions. Functions satisfying these conditions are called contractions. In this article, we give a new characterization of contractions on streams in the form of a sound and complete representation theorem, and generalize this result to a wide class of non-well-founded structures, first to infinite binary trees, then to final coalgebras of container functors.
Cited by 1Open access
Venanzio Capretta, Graham Hutton, Mauro Jaskelioff · Greater South Information System · 2016
Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they actually generate a productive infinite object? A standard means to achieve productivity is to use Banach's fixed-point theorem, which guarantees the unique existence of solutions to recursive equations on metric spaces under certain conditions. Functions satisfying these conditions are called contractions. In this article, we give a new characterization of contractions on streams in the form of a sound and complete representation theorem, and generalize this result to a wide class of non-well-founded structures, first to infinite binary trees, then to final coalgebras of container functors.
Cited by 0Open access
Hans Zantema, Matthias Raffelsieper · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2010
For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate the notion of productivity. This generalizes stream productivity. We develop a general technique to prove productivity based on proving context-sensitive termination, by which the power of present termination tools can be exploited. In order to treat cases where the approach does not apply directly, we develop transformations extending the power of the basic approach. We present a tool combining these ingredients that can prove productivity of a wide range of examples fully automatically.
Cited by 14Open access
Arthur G. Duncan · 1998
Cited by 1
César Domínguez, Julio Rubio · 2010
Cited by 5
César Domínguez, Julio Rubio · Lecture notes in computer science · 2010
Cited by 2Open access
C. Titus Brown · Figshare · 2016
A talk I gave at the Integrative Genetics and Genomics Graduate Group Seminar Series, UC Davis, April 11th, 2016. Essentially: MinHash to quickly compute Jaccard distances between raw mRNAseq data sets.
Cited by 0Open access
Brown, C. Titus · Figshare · 2016
A talk I gave at the Integrative Genetics and Genomics Graduate Group Seminar Series, UC Davis, April 11th, 2016. Essentially: MinHash to quickly compute Jaccard distances between raw mRNAseq data sets.
Cited by 0Open access
Manfred Schmidt-Schauss, David Sabel, Marko Schütz · Springer Link (Chiba Institute of Technology)
Various static analyses of functional programming languages that permit infinite data structures make use of set constants like <ns0:monospace>Top</ns0:monospace>, <ns0:monospace>Inf</ns0:monospace>, and <ns0:monospace>Bot</ns0:monospace>, denoting all terms, all lists not eventually ending in Nil, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics in the set of all, also infinite, computable trees, where all term constructors are non-strict. This paper proves decidability, in particular DEXPTIME-completeness, of inclusion of co-inductively defined sets by using algorithms and results from tree automata and set constraints. The test for set inclusion is required by certain strictness analysis algorithms in lazy functional programming languages and could also be the basis for further set-based analyses.
Cited by 0
Thomas Schwentick · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2008
Finite or infinite strings or trees with labels from a finite alphabet play an important role in computer science. They can be used to model many interesting objects including system runs in Automated Verification and XML documents in Database Theory. They allow the application of formal tools like logical formulas to specify properties and automata for their implementation. In this framework, many reasoning tasks that are undecidable for general computational models can be solved algorithmically, sometimes even efficiently. Nevertheless, the use of finitely labelled structures usually requires an early abstraction from the real data. For example, theoretical research on XML processing very often con- centrates on the document structure (including labels) but ignores attribute or text values. While this abstraction has led to many interesting results, some aspects like key or other integrity constraints can not be adequately handled. In Automated Verification of software systems or communication protocols, infinite domains occur even more naturally, e.g., induced by program data, recursion, time, com- munication or by unbounded numbers of concurrent processes. Usually one approximates infinite domains by finite ones in a very early abstraction step. An alternative approach that has been investigated in recent years is to extend strings and trees by (a limited amount of) data and to use logical languages with a restricted ex- pressive power concerning this data. As an example, in the most simple setting, formulas can only test equality of data values. The driving goal is to identify logical languages and corresponding automata models which are strong enough to describe interesting proper- ties of data-enhanced structures while keeping decidability or even feasibility of automatic reasoning. The talk gives a basic introduction into data-enhanced finitely labelled structures, presents examples of their use, and highlights recent decidability and complexity results.
Cited by 3Open access
Franklyn Turbak · 2001
Cyclic data structures can be tricky to create and manipulate in declarative programming languages. In a declarative setting, a natural way to view cyclic structures is as denoting regular trees, those trees which may be infinite but have only a finite number of distinct subtrees. This paper shows how to implement the unfold (anamorphism) operator in both eager and lazy languages so as to create cyclic structures when the result is a regular tree as opposed to merely infinite lazy structures. The usual fold (catamorphism) operator when used with a strict combining function on any infinite tree yields an undefined result. As an alternative, this paper defines and show how to implement a cycfold operator with more useful semantics when used with a strict function on cyclic structures representing regular trees. This paper also introduces an abstract data type (cycamores) to simplify the use of cyclic structures representing regular trees in both eager and lazy languages. Implementions of cycamores in both SML and Haskell are presented. 1.
Cited by 0
Franklyn Turbak, J. B. Wells · 2001
Cyclic data structures can be tricky to create and manipulate in declarative programming languages. In a declarative setting, a natural way to view cyclic structures is as denoting regular trees, those trees which may be infinite but have only a finite number of distinct subtrees. This paper shows how to implement the unfold (anamorphism) operator in both eager and lazy languages so as to create cyclic structures when the result is a regular tree as opposed to merely infinite lazy structures. The usual fold (catamorphism) operator when used with a strict combining function on any infinite tree yields an undefined result. As an alternative, this paper defines and show how to implement a cycfold operator with more useful semantics when used with a strict function on cyclic structures representing regular trees. This paper also introduces an abstract data type (cycamores) to simplify the use of cyclic structures representing regular trees in both eager and lazy languages. Implementions of cycamores in both SML and Haskell are presented.
Cited by 0
VBN Forskningsportal (Aalborg Universitet) · 2005
The aim of the workshop is, to provide a forum for researchers interested in the development of mathematical techniques for the analysis and verification of systems with infinitely many states. Topics: Techniques for modeling and analysis of infinite-state systems; Equivalence-checking and model-checking with infinite-state systems; Parameterized systems; Probabilistic and timed systems; Calculi for mobility and security; Finite-state abstractions of infinite-state systems; Data structures for infinite state spaces;
Cited by 0
Thibodeau, David · eScholarship@McGill (McGill) · 2016
Infinite structures are an integral part of computer science as they serve as representations for concepts such as constantly running devices and processes or data communication streams.Due to their importance, it is crucial that programming languages are equipped with adequate means to encode and reason about infinite structures.This thesis investigates the recent idea of copatterns, a device to represent infinite structures in a fashion dual to usual definitions of finite data, by integrating it to Levy's Call-by-Push Value language.We define a coverage algorithm for copattern matching definitions.We prove that evaluation preserves types and that well-typed terms do not get stuck.We define a translation from our language to Levy's and prove that this translation preserves evaluation.
Cited by 0Open access
2012
The principles and techniques of programming with functions. Purely functional programming languages; recursion; higher-order functions; reduction models; strictness; type systems; list operations; infinite data structures; program synthesis and transformation.
Cited by 0
Alastair J. Telford, David A. Turner · Kent Academic Repository (University of Kent) · 1997
It is our aim to develop an elementary strong functional programming (ESFP) system. To be useful, ESFP should include structures such as streams which can be computationally unwound infinitely often. We describe a syntactic analysis to ensure that infinitely proceeding structures, which we shall term codata, are productive. This analysis is an extension of the check for guardedness that has been used with definitions over coinductive types in Martin-Lof&apos;s type theory and in the calculus of constructions. Our analysis is presented as a form of abstract interpretation that allows a wider syntactic class of corecursive definitions to be recognised as productive than in previous work. Thus programmers will have fewer restrictions on their use of infinite streams within a strongly normalizing functional language. Contents 1 Introduction 1 2 Infinite Objects 2 2.1 Functional Programming and Infinite Data . . . . . . . . . . . . 3 2.2 Guarded Infinite Objects . . . . . . . . . . . . . ....
Cited by 6Open access
L. Cnend, P. Flajolet, J. Francdn et al. · 1980
Abstract Dynamic data structures for priority queues, dictionaries.., are izfl under sequences of arbitrary insert, delete and query operations in various contexts when the universe of keys is finite both exact and asymptotic estimates are provided; when the universe of keys is infinite, a new asymptotic formula is given which makes it possible to analyze rather complex data structures including binomial queues. We conclude by further showing how to derive variance estimates for simple structures.
Cited by 0
Ulrich Berger, Vasco Brattka, Victor Selivanov et al. · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2012
There is a large gap between mathematical structures and the structures computer implementations are based on. To stimulate research to overcome this---especially for infinitary structures---highly non-trivial problem the Dagstuhl Seminar 11411 ``Computing with Infinite Data: Topological and Logical Foundations'' was held. This report collects the ideas that were presented and discussed during the course of the seminar.
Cited by 0Open access
F. Lockwood Morris · Syracuse University Libraries (Syracuse University) · 1978
The notion of list structure is discussed, and a new construct is introduced into LISP which permits the computation of list structures containing cycles without recourse to operations which alter existing structures. It is shown that list structures can be used to represent both finite and “rational” infinite terms. Substitutions (generalized for a term algebra which includes infinite terms) are discussed, “tables” are introduced as an abstract data type, and two methods of representing substitutions by tables, together with their interrelation, are considered. Concise programs are given for a succession of forms of Robinson’s unification algorithm, including one which operates in almost linear time, and for the application of substitutions to terms.
Cited by 6Open access
Andreas Abel, Brigitte Pientka · 2014
In this paper, we study strong normalization of a core language based on System Fω which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard’s reducibility candidates. As such, our system allows for non-determinism and does not rely on coverage. Since System Fω is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda. 1
Cited by 0