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 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.     

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 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.     

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.     

An Algebraic Characterization of Inductive Soundness in Proof by Consistency

Kapur and Musser studied the theoretical basis for proof by consistency and obtained an inductive completeness result:p=q if and only if p=q is true in every inductive model.However,there is a loophole in their proof for the soundness part:p=q implies p=q is true in every inductive model.The aim of this paper is to give a correct characterization of inductive soundness from an algebraic view by introducing strong inductive models.     

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.     

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.     

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.     

Formal Ontology: Foundation of Domain Knowledge Sharing and Reusing

Domain analysis is the activity of identifying and representing the relevant information in a domain,so that the information can be shared and reused in similar systems.But until now,no efficient approaches are available for capturing and representing the results of domain analysis and then for sharing and reusing the domain knowledge.This paper proposes an ontology-oriented approach for formalizing the domain models.The architecture for the multiple-layer structure of the domain knowledge base is also discussed.And finally,some genetic algorithm-based methods have been given for supporting the knowledge sharing and reusing.     

The multivoicedness of game play: Exploring the unfolding of a student’s learning trajectory in a gaming context at school

The purpose of this article is to gain knowledge about how interactions in a gaming context become constituted as effective resources for a student’s learning trajectory. In addition, this detailed study of a learning trajectory documents how a computer game becomes a learning resource for working on a specific topic in school. The article reports on a qualitative study of students at an upper secondary school who have played the computer game Global Conflicts: Palestine to learn about the complexity of the Israeli-Palestinian conflict. A sociocultural and dialogic approach to learning and meaning-making is employed as an analytical framework. Analyzing different interactional episodes, in which important orientations and reorientations are located, documents how the student’s learning trajectory developed and changed during the project. When engaged in game play in educational settings, experiences with playing computer games outside of school can relevantly be invoked and become part of the collaborative project of finding out how to play the game. However, these ways of engaging with a computer game might not necessarily facilitate a subtle understanding of the specific topic that is addressed in the game. The findings suggest that the constitution of a computer game as a learning resource is a collaborative project, in which multiple resources for meaning-making are in play, and for which the teacher has an important role in facilitating student’s adoption of a multiperspective on the conflict. Furthermore, the findings shed light on what characterizes student-teacher interactions that contribute to a subtle understanding, and offer a framework for important issues upon which to reflect in game-based learning (GBL).     

Predicting customer behavior in the market-space: a study of Rayport and Sviokla’s framework

The rapidly evolving phenomenon of the World Wide Web and the creation of a new international arena for electronic commerce have expanded the possibilities for the marketing of products and services. The role played by customer behavior in the market-space is still not entirely understood and calls for investigations into the significance of customer attitudes and loyalty. In this article, a model is developed; it examines the significance of content, context, and infrastructure in determining customer loyalty. An empirical study involving 145 subjects was conducted to test this model and to gain a better understanding of the relationship between customer belief about a Web site (specifically, an e-publishing site) and customer behavior (such as attitudes toward brand and customer loyalty).The results indicate that customer attitude is influenced by belief about brand equity (value), which is affected by the content, context, and infrastructure. Customer loyalty is determined by attitude and belief about the context in which the products or services are offered. These findings provide a better understanding of customer behavior associated with Web sites in the market-space, also confirm the proposition of Rayport and Sviokla that ‘customer loyalty is developed at the context level’.     

Detection of error-related negativity in complex visual stimuli: a new neuroergonomic arrow in the practitioner’s quiver

Abstract

Brain processes responsible for the error-related negativity (ERN) evoked response potential (ERP) have historically been studied in highly controlled laboratory experiments through presentation of simple visual stimuli. The present work describes the first time the ERN has been evoked and successfully detected in visual search of complex stimuli. A letter flanker task and a motorcycle conspicuity task were presented to participants during electroencephalographic (EEG) recording. Direct visual inspection and subsequent statistical analysis of the resultant time-locked ERP data clearly indicated that the ERN was detectable in both groups. Further, the ERN pattern did not differ between groups. Such results show that the ERN can be successfully elicited and detected in visual search of complex static images, opening the door to applied neuroergonomic use. Harnessing the brain’s error detection system presents significant opportunities and complex challenges, and implication of such are discussed in the context of human-machine systems.

Practitioner Summary: For the first time, error-related negativity (ERN) has been successfully elicited and detected in a visually complex applied search task. Brain-process-based error detection in human-machine systems presents unique challenges, but promises broad neuroergonomic applications.     

Technique of Monitoring a Human Operator’s Behavior in Man-Machine Systems

Monitoring a human operator’s behavior in man-machine systems is aimed at detecting and diagnosing unwanted behavioral deviations of a human operator from the preset sequence of actions, taking into account their possible response to the current state of the system. The human operator’s behavior is described using the nondeterministic finite-state machine (FSM) model. Techniques for constructing and determinizating this model are proposed to ensure the minimal possible loss of information. The solution of the task is illustrated by the example of working IT system operators.     

A Syntactic Proof of the Conservativity ofλ_ω overλ_2

In this paper,the relationship between the second order typed λ－calculus λ2 and its higher order version λω is discussed.A purely syntactic proof of the conservativity of λωover λ2 is given.