Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm

Huffman’s algorithm is a procedure for constructing a binary tree with minimum weighted path length. Our Isabelle/HOL proof closely follows the sketches found in standard algorithms textbooks, uncovering a few snags in the process. Another distinguishing feature of our formalization is the use of custom induction rules to help Isabelle’s automatic tactics, leading to very short proofs for most of the lemmas. This work was supported by the DFG grant NI 491/11-1.     

Proof Pearl—A Mechanized Proof of GHC’s Mergesort

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art proof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.     

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Avoiding deadlock is crucial to interconnection networks. In ’87, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel dependency graph is acyclic. We formally define and prove a slightly different condition from which the original condition of Dally and Seitz can be derived. Dally and Seitz prove that a deadlock situation induces cyclic dependencies by reductio ad absurdum. In contrast we introduce the notion of a waiting graph from which we explicitly construct a cyclic dependency from a deadlock situation. Moreover, our proof is structured in such a way that it only depends on a small set of proof obligations associated to arbitrary routing functions and switching policies. Discharging these proof obligations is sufficient to instantiate our condition for deadlock-free routing on particular networks. Our condition and its proof have been formalized using the ACL2 theorem proving system.     

Weak Derandomization of Weak Algorithms: Explicit Versions of Yao��s Lemma

A simple averaging argument shows that given a randomized algorithm A and a function f such that for every input x, Pr[A(x) = f(x)] ≥ 1 − ρ (where the probability is over the coin tosses of A), there exists a non-uniform deterministic algorithm B “of roughly the same complexity” such that Pr[B(x) = f(x)] ≥ 1 − ρ (where the probability is over a uniformly chosen input x). This implication is often referred to as “the easy direction of Yao’s lemma” and can be thought of as “weak derandomization” in the sense that B is deterministic but only succeeds on most inputs. The implication follows as there exists a fixed value r′ for the random coins of A such that “hardwiring r′ into A” produces a deterministic algorithm B. However, this argument does not give a way to explicitly construct B.     

On the Black-Box Complexity of Sperner’s Lemma

We present several results on the complexity of various forms of Sperner’s Lemma in the black-box model of computing. We give a deterministic algorithm for Sperner problems over pseudo-manifolds of arbitrary dimension. The query complexity of our algorithm is linear in the separation number of the skeleton graph of the manifold and the size of its boundary. As a corollary we get an deterministic query algorithm for the black-box version of the problem 2D-SPERNER, a well studied member of Papadimitriou’s complexity class PPAD. This upper bound matches the deterministic lower bound of Crescenzi and Silvestri. The tightness of this bound was not known before. In another result we prove for the same problem an lower bound for its probabilistic, and an lower bound for its quantum query complexity, showing that all these measures are polynomially related. Research supported by the European Commission IST Integrated Project Qubit Application (QAP) 015848, the OTKA grants T42559 and T46234, and by the ANR Blanc AlgoQP grant of the French Research Ministry.     

Interpolation in Valiant��s Theory

We investigate the following question: if a polynomial can be evaluated at rational points by a polynomial-time boolean algorithm, does it have a polynomial-size arithmetic circuit? We argue that this question is certainly difficult. Answering it negatively would indeed imply that the constant-free versions of the algebraic complexity classes VP and VNP defined by Valiant are different. Answering this question positively would imply a transfer theorem from boolean to algebraic complexity.     

On �� 2 ? �� 2-products of automata

Two equivalent sufficient conditions are given for the completeness of classes of finite automata with respect to the isomorphic simulation under the ?? ₂ ? ?? ₂-product. It is conjectured that these conditions are also necessary with respect to the isomorphic or homomorphic simulation too.     

The Concept of ��Work�� in CSCW

The scope of CSCW, its focus on work, has been a topic of sporadic debate for many years ?? indeed, from the very beginning in the late 1980s. But in recent years the issue has become one of general concern. Most of this debate has been taking place in closed fora such as program committees, editorial boards, and email discussion groups, but over the last few years the debate has been brought out in the open in a few publications, in particular in a programmatic article from 2005 by three esteemed CSCW researchers: Andy Crabtree, Tom Rodden, and Steve Benford. They argue that CSCW should ??move its focus away from work??. Other researchers argue along the same lines. Taking this open challenge as a welcome cue, the present article addresses CSCW??s scope: the rationale for its focus on ordinary work. After an initial discussion of the arguments put forward by Crabtree et al. and by others, the article focuses on an analysis of the concept of ??work??, drawing on the methods and insights of ??ordinary language philosophy??, and, flowing from this, a critique of the notion of ??work?? in conversation analysis. After a critical appraisal of prevailing myths about the realities of work in the contemporary world, the article ends in an attempt to position CSCW in the context of technological development more broadly. The underlying premise of the article is that it is time to reconsider CSCW: to rethink what it is and why it might be important.     

Geometric Tools in Juan De ��lava��s Stonecutting Workshop

Stonemasonry of the Gothic vault in its totality is based upon geometry of the line, whereas classic stereotomy relies on the comprehensive knowledge of the surface and the highly sophisticated sides of the voussoirs necessary for its vaults. It is obvious that this leap in the art of construction was paralleled and accompanied by an extension of the horizons of geometry. In Spain, it was made possible thanks to the centuries-old tradition of stone building begun in the most remote medieval times and to the presence of outstanding architects or stonemasons such as Juan de álava, whose professional work surpassed the established limits and provided the art of building with new instruments.     

Optimal navigation in planar time-varying flow: Zermelo��s problem revisited

This paper is concerned with time-optimal navigation for flight vehicles in a planar, time-varying flow-field, where the objective is to find the fastest trajectory between initial and final points. The primary contribution of the paper is the observation that in a point-symmetric flow, such as inside vortices or regions of eddie-driven upwelling/downwelling, the rate of the steering angle has to be equal to one-half of the instantaneous vertical vorticity. Consequently, if the vorticity is zero, then the steering angle is constant. The result can be applied to find the time-optimal trajectories in practical control problems, by reducing the infinite-dimensional continuous problem to numerical optimization involving at most two unknown scalar parameters.     

Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM

Distributed algorithms are subtle and error-prone. Still, very few of them have been formally verified, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms.We consider formal verification of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal verification of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.     

Simulation of a mannequin’s thermal plume in a small room

Simulation results are presented for the buoyancy-driven flow in a small room containing a seated mannequin that is maintained at a constant temperature. The study was motivated, in part, by a published experimental study of the thermal plume around a human subject. The results presented are a step toward the goal of using DNS to develop a more detailed understanding of the nature of the flow in the thermal plume created by humans modeled here as heated mannequins. The results were obtained without using sub-grid scale modeling and are helpful in establishing the resolution requirements for accurate simulations. It is seen that the results for the highest resolution grid are in reasonable quantitative agreement with a published experimental study of a human subject’s thermal plume. The results for the velocity field are used to compute the trajectories of small particles in the room. Results are presented for the trajectories of five-micrometer solid particles that are initially dispersed near the floor in front of the mannequin. The simulation results show that the buoyancy-driven flow around the mannequin is effective at dispersing the particles over a large portion of the room.     

An analysis of a firm’s capacity in Mazda’s Keiretsu

Capacity is defined as the power resulting from the specific position of a company in a network organization. This article extends the theory of network organizations to examine Mazda’s Yokokai Keiretsu, and proposes a new approach to calculating a firm’s capacity in a network. Capacity is divided into two categories, take-in capacity and take-out capacity, and the gap between them is called the capacity difference. We analyze the impact of capacity difference as a determinant of corporate performance in network organizations, thus providing a new perspective for successful corporate management.     

Jeffrey’s rule of conditioning in a possibilistic framework

Conditioning, belief update and revision are important tasks for designing intelligent systems. Possibility theory is among the powerful uncertainty theories particularly suitable for representing and reasoning with uncertain and incomplete information. This paper addresses an important issue related to the possibilistic counterparts of Jeffrey’s rule of conditioning. More precisely, it addresses the existence and uniqueness of the solutions computed using the possibilistic counterparts of the so-called kinematics properties underlying Jeffrey’s rule of conditioning. We first point out that like the probabilistic framework, in the quantitative possibilistic setting, there exists a unique solution for revising a possibility distribution given the uncertainty bearing on a set of exhaustive and mutually exclusive events. However, in the qualitative possibilistic framework, the situation is different. In particular, the application of Jeffrey’s rule of conditioning does not guarantee the existence of a solution. We provide precise conditions where the uniqueness of the revised possibility distribution exists.     

Motion of a disk in contact with a parametric 2D curve and Painlevé’s paradox

Multibody System Dynamics - This paper addresses the modeling and simulation of a homogeneous disk that undergoes plane motion constrained to be in permanent contact with and in the same plane as a...     

A Rejoinder to Notes on a ‘Constructive Proof of the Existence of a Collateral Equilibrium’

This rejoinder contains a few remarks on my paper published in this journal with the title ‘A Constructive Proof of the Existence of Collateral Equilibrium for a Two-Period Exchange Economy Based on a Smooth Interior-Point Path’ and Ragupathy and Velupillai’s notes on a ‘Constructive Proof of the Existence of Collateral Equilibrium’ published recently in the same journal.