Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 4 of 4
Full-Text Articles in Entire DC Network
Proving Non-Deterministic Computations In Agda, Sergio Antoy, Michael Hanus, Steven Libby
Proving Non-Deterministic Computations In Agda, Sergio Antoy, Michael Hanus, Steven Libby
Computer Science Faculty Publications and Presentations
We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. The first approach eliminates non-determinism by considering the set of all non-deterministic values produced by an application. The second approach encodes every non-deterministic choice that the application could perform. We consider our initial experiment a success. Although proving properties of programs is a notoriously difficult task, the functional logic …
From Boolean Equalities To Constraints, Sergio Antoy, Michael Hanus
From Boolean Equalities To Constraints, Sergio Antoy, Michael Hanus
Computer Science Faculty Publications and Presentations
Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction …
Compiling Collapsing Rules In Certain Constructor Systems, Sergio Antoy, Andy Jost
Compiling Collapsing Rules In Certain Constructor Systems, Sergio Antoy, Andy Jost
Computer Science Faculty Publications and Presentations
The implementation of functional logic languages by means of graph rewriting requires a special handling of collapsing rules. Recent advances about the notion of a needed step in some constructor systems offer a new approach to this problem. We present two results: a transformation of a certain class of constructor-based rewrite systems that eliminates collapsing rules, and a rewrite-like relation that takes advantage of the absence of collapsing rules. We formally state and prove the correctness of these results. When used together, these results simplify without any loss of efficiency an implementation of graph rewriting and consequently of functional logic …
A Comparative Study Of Reservoir Computing For Temporal Signal Processing, Alireza Goudarzi, Peter Banda, Matthew R. Lakin, Christof Teuscher, Darko Stefanovic
A Comparative Study Of Reservoir Computing For Temporal Signal Processing, Alireza Goudarzi, Peter Banda, Matthew R. Lakin, Christof Teuscher, Darko Stefanovic
Computer Science Faculty Publications and Presentations
Reservoir computing (RC) is a novel approach to time series prediction using recurrent neural networks. In RC, an input signal perturbs the intrinsic dynamics of a medium called a reservoir. A readout layer is then trained to reconstruct a target output from the reservoir's state. The multitude of RC architectures and evaluation metrics poses a challenge to both practitioners and theorists who study the task-solving performance and computational power of RC. In addition, in contrast to traditional computation models, the reservoir is a dynamical system in which computation and memory are inseparable, and therefore hard to analyze. Here, we compare …