916 papers · page 45 of 46
Abstract Let ψ be a partial recursive function (of one argument) with λ-defining term F ∈Λ°. This means There are several proposals for what F ⌜ n ⌝ should be in case ψ( n ) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy …
At the recent TC2 working conference on constructing programs from specifications (Moeller, 1991), I presented the derivation of a functional program for solving a problem posed by Knuth (1990). Slightly simplified, the problem was to construct a shortest decimal fraction represe…
In my previous Functional Pearls article (Bird, 1992), I proved a theorem giving conditions under which an optimization problem could be implemented by a greedy algorithm. A greedy algorithm is one that picks a ‘best’ element at each stage. Here, we return to this theorem and ext…
Abstract The essential part of abstract interpretation is to build a machine-representable abstract domain expressing interesting properties about the possible states reached by a program at runtime. Many techniques have been developed which assume that one knows in advance the c…
Abstract One can have all the advantages of functional programming – correctness, clarity, simplicity, and flexibility – without any sacrifice in performance, even for a scientifically significant computation on a supercomputer. Therefore, why use Fortran? We demonstrate parity –…
Abstract Some extensions of the basic formalism of stream processing functions are useful to specify complex structures such as operating systems. In this paper we give the foundations of higher order stream processing functions. These are functions which send and accept not only…
Abstract MetaMorph is a software tool that supports transformation and proof for an equational non-strict functional language. It was developed as a vehicle for research into the synthesis of digital logic, but is equally suitable for reasoning about functional programs. The theo…
Abstract In a functional program, a simple random number generator may generate a lazy list of random numbers. This is fine when the random numbers are consumed sequentially at a single point in the program. However, things are more complicated in a program where random numbers a…
In this paper we show that it is possible to implement a symmetric set of finite-list operations efficiently; the set is symmetric in the sense that lists can be manipulated at either end. We derive the definitions of these operations from their specifications by calculation. The…
Abstract In combinator parsing , the text of parsers resembles BNF notation. We present the basic method, and a number of extensions. We address the special problems presented by white-space, and parsers with separate lexical and syntactic phases. In particular, a combining form …
Abstract The G-machine (Johnsson, 1987; Peyton Jones, 1987) is a compiled graph reduction machine for lazy functional languages. The G-machine compiler contains many optimizations to improve performance. One set of such optimizations is designed to improve the performance of tail…
Abstract The Spineless Tagless G-machine is an abstract machine designed to support non-strict higher-order functional languages. This presentation of the machine falls into three parts. Firstly, we give a general discussion of the design issues involved in implementing non-stric…
Abstract This paper presents a simple framework for performing calculations with the elements of (finite) lattices. A particular feature of this work is the use of type classes to enable the use of overloaded function symbols within a strongly typed language. Previous application…
Abstract We present a simple and easy-to-understand explanation of ML type inference and parametric polymorphism within the framework of type monomorphism, as in the first order typed lambda calculus. We prove the equivalence of this system with the standard interpretation using …
Abstract We start by giving a compact representation schema for λ-terms, and show how this leads to an exceedingly small and elegant self-interpreter. We then define the notion of a self-reducer , and show how this too can be written as a small λ-term. Both the self-interpreter a…
Abstract The integration of functional and logic programming languages has been a topic of great interest in the last decade. Many proposals have been made, yet none is completely satisfactory especially in the context of higher order functions and lazy evaluation. This paper add…
Abstract We present a new static system which reconstructs the types, regions and effects of expressions in an implicitly typed functional language that supports imperative operations on reference values. Just as types structurally abstract collections of concrete values, regions…
Abstract This paper compares three different sparse matrix representations in Miranda for solving linear systems of equations: quadtrees, binary trees and run-length encoding. It compares the three data structures in each of two common linear system solvers, Conjugate Gradient an…
Abstract The λσ-calculus is a refinement of the λ-calculus where substitutions are manipulated explicitly. The λσ-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical λ-calcul…
Abstract Programming languages often come with type systems. Some of these are simple, others are sophisticated. As a stylistic representation of types in programming languages several versions of typed lambda calculus are studied. During the last 20 years many of these systems h…