Harry G. Mairson

CSL Conference 2002 Conference Paper

Proofnets and Context Semantics for the Additives

• Harry G. Mairson
• Xavier Rival

Abstract We provide a context semantics for Multiplicative-Additive Linear Logic (MALL), together with proofnets whose reduction preserves semantics, where proofnet reduction is equated with cut-elimination on MALL sequents. The results extend the program of Gonthier, Abadi, and Lévy, who provided a “geometry of optimal λ-reduction” (context semantics) for λ-calculus and Multiplicative-Exponential Linear Logic (MELL). We integrate three features: a semantics that uses buses to implement slicing; a proofnet technology that allows multidimensional boxes and generalized garbage, preserving the linearity of additive reduction; and finally, a read-back procedure that computes a cut-free proof from the semantics, a constructive companion to full abstraction theorems.

I&C Journal 2001 Journal Article

Parallel Beta Reduction Is Not Elementary Recursive

• Andrea Asperti
• Harry G. Mairson

We analyze the inherent complexity of implementing Lévy's notion of optimal evaluation for the λ-calculus, where similar redexes are contracted in one step via so-called parallel β-reduction. Optimal evaluation was finally realized by Lamping, who introduced a beautiful graph reduction technology for sharing evaluation contexts dual to the sharing of values. His pioneering insights have been modified and improved in subsequent implementations of optimal reduction. We prove that the cost of parallel β-reduction is not bounded by any Kalmár-elementary recursive function. Not only do we establish that the parallel β-step cannot be a unit-cost operation, we demonstrate that the time complexity of implementing a sequence of n parallel β-steps is not bounded as O(2 n ), O(22 n ), O(222 n ), or in general, O(K l (n)), where K l (n) is a fixed stack of l 2's with an n on top. A key insight, essential to the establishment of this non-elementary lower bound, is that any simply typed λ-term can be reduced to normal form in a number of parallel β-steps that is only polynomial in the length of the explicitly typed term. The result follows from Statman's theorem that deciding equivalence of typed λ-terms is not elementary recursive. The main theorem gives a lower bound on the work that must be done by any technology that implements Lévy's notion of optimal reduction. However, in the significant case of Lamping's solution, we make some important remarks addressing how work done by β-reduction is translated into equivalent work carried out by his bookkeeping nodes. In particular, we identify the computational paradigms of superposition of values and of higher-order sharing, appealing to compelling analogies with quantum mechanics and SIMD-parallelism.

I&C Journal 1996 Journal Article

Database Query Languages Embedded in the Typed Lambda Calculus

• Gerd G. Hillebrand
• Paris C. Kanellakis
• Harry G. Mairson

We investigate the expressive power of the typedλ-calculus when expressing computations over finite structures, i. e. , databases. We show that the simply typedλ-calculus can express various database query languages such as the relational algebra, fixpoint logic, and the complex object algebra. In our embeddings, inputs and outputs areλ-terms encoding databases, and a program expressing a query is aλ-term which types when applied to an input and reduces to an output. Our embeddings have the additional property that PTIME computable queries are expressible by programs that, when applied to an input, reduce to an output in a PTIME sequence of reduction steps. Under our database input-output conventions, all elementary queries are expressible in the typedλ-calculus and the PTIME queries are expressible in the order-5 (order-4) fragment of the typedλ-calculus (with equality).

TCS Journal 1992 Journal Article

A simple proof of a theorem of Statman

• Harry G. Mairson

In this note, we reprove a theorem of Statman that deciding the βη-equality of two first-order typable λ-terms is not elementary recursive (Statman, 1982). The basic idea of our proof, like that of Statman's is the Henkin quantifier elimination procedure (Henkin, 1963). However, our coding is much simpler, and easy to understand.

FOCS Conference 1985 Conference Paper

Average Case Lower Bounds on the Construction and Searching of Partial Orders

• Harry G. Mairson

It is very well known in computer science that partially ordered files are easier to search. In the worst case, for example, a totally unordered file requires no preprocessing, but Ω(n) time to search, while a totally ordered file requires Ω(n log n) preprocessing time to sort, but can be searched in O(log n) time. Behind the casual observation, then, lurks the notion of a computational tradeoff between sorting and searching. We analyze this tradeoff in the average case, using the decision tree model. Let P be a preprocessing algorithm that produces partial orders given a set U of n elements, and let S be a searching algorithm for these partial orders. Assuming any of the n! permutations of the elements of U are equally likely, and that we search for any y isin; U with equal probability (in unsuccessful search, all "gaps" are considered equally likely), the average costs P(n) of preprocessing and S(n) of searching may be computed. We demonstrate a tradeoff of the form P(n) + n log S(n) = Ω(n log n), for both successful and unsuccessful search. The bound is tight up to a constant factor. In proving this tradeoff, we show a lower bound on the average case of searching a partial order. Let A be a partial order on n elements consistent with Π permutations. We show S(n) = Ω(Π3/n/n2) for successful search of A, and S(n) = Ω(Π2/n/n) for unsuccessful search. These lower bounds show, for example, that heaps require linear time to search on the average.

STOC Conference 1984 Conference Paper

Correcting Faults in Write-Once Memory

• Danny Dolev
• David Maier 0001
• Harry G. Mairson
• Jeffrey D. Ullman

FOCS Conference 1983 Conference Paper

The Program Complexity of Searching a Table

• Harry G. Mairson

Given a fixed set S of n keys, we would like to store them so that queries of the form "Is x ∈ S? " can be answered quickly. A commonly employed scheme to solve this problem uses a table to store the keys, and a special purpose program depending on S which probes the table. We analyze the tradeoff between the maximum number of probes allowable to answer a query, and the information-theoretic complexity of the program to do so. Perfect hashing (where the query must be answered in one probe) has a program complexity of nlog2 e(1 + o(1)) bits, and this lower bound can be achieved. Under a model combining perfect hashing and binary search methods, it is shown that for k probes to the table, nk/2k+1(1 + o(1)) bits are necessary and sufficient to describe a table searching algorithm. This model gives some information-theoretic bounds on the complexity of searching an external memory. We examine some schemes where pointers are allowed in the table, and show that for k probes to the table, about nlog2e/e(k+1)! (1+o(1)) bits are necessary and sufficient to describe the search. Finally, we prove some lower bounds on the worst case performance of hash functions described by bounded Boolean circuits, and worst case performance of universal classes of hash functions.