OpenRaiser/Intern-Atlas huggingface dataset:
Data Definitions in the ACL2 Sedan
Venue: arXiv cs.PL 2014
Year: 2014

We present a data definition framework that enables the convenient specification of data types in ACL2s, the ACL2 Sedan. Our primary motivation for developing the data definition framework was pedagogical. We were teaching undergraduate students how to reason about programs using ACL2s and wanted to provide them with an effective method for defining, testing, and reasoning about data types in the context of an untyped theorem prover. Our framework is now routinely used not only for pedagogical purposes, but also by advanced users. Our framework concisely supports common data definition patterns, e.g. list types, map types, and record types. It also provides support for polymorphic functions. A distinguishing feature of our approach is that we maintain both a predicative and an enumerative characterization of data definitions. In this paper we present our data definition framework via a sequence of examples. We give a complete characterization in terms of tau rules of the inclusion/exclusion relations a data definition induces, under suitable restrictions. The data definition framework is a key component of counterexample generation support in ACL2s, but can be independently used in ACL2, and is available as a community book.
Polymorphic Types in ACL2
Venue: arXiv cs.LO 2014
Year: 2014

This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the Hindley-Milner paradigm of functional programming (as exemplified in popular languages like ML and Haskell), including a "typed" style of programming with the ability to define polymorphic types. These ideas are introduced via macros into the language of ACL2, taking advantage of ACL2's guard-checking mechanism to perform type checking on both function definitions and theorems. Finally, we discuss how these macros were used to implement features of Specware, a software specification and implementation system.
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
Venue: arXiv cs.LO 2014
Year: 2014

Behavioral synthesis involves compiling an Electronic System-Level (ESL) design into its Register-Transfer Level (RTL) implementation. Loop pipelining is one of the most critical and complex transformations employed in behavioral synthesis. Certifying the loop pipelining algorithm is challenging because there is a huge semantic gap between the input sequential design and the output pipelined implementation making it infeasible to verify their equivalence with automated sequential equivalence checking techniques. We discuss our ongoing effort using ACL2 to certify loop pipelining transformation. The completion of the proof is work in progress. However, some of the insights developed so far may already be of value to the ACL2 community. In particular, we discuss the key invariant we formalized, which is very different from that used in most pipeline proofs. We discuss the needs for this invariant, its formalization in ACL2, and our envisioned proof using the invariant. We also discuss some trade-offs, challenges, and insights developed in course of the project.
Deciding the On-line Chromatic Number of a Graph with Pre-Coloring is PSPACE-Complete
Venue: arXiv cs.CC 2014
Year: 2014

The problem of determining if the on-line chromatic number of a graph is less than or equal to k, given a pre-coloring, is shown to be PSPACE-complete.
Towards a Better Understanding of the Local Attractor in Particle Swarm Optimization: Speed and Solution Quality
Venue: arXiv cs.NE 2014
Year: 2014

Particle Swarm Optimization (PSO) is a popular nature-inspired meta-heuristic for solving continuous optimization problems. Although this technique is widely used, the understanding of the mechanisms that make swarms so successful is still limited. We present the first substantial experimental investigation of the influence of the local attractor on the quality of exploration and exploitation. We compare in detail classical PSO with the social-only variant where local attractors are ignored. To measure the exploration capabilities, we determine how frequently both variants return results in the neighborhood of the global optimum. We measure the quality of exploitation by considering only function values from runs that reached a search point sufficiently close to the global optimum and then comparing in how many digits such values still deviate from the global minimum value. It turns out that the local attractor significantly improves the exploration, but sometimes reduces the quality of the exploitation. As a compromise, we propose and evaluate a hybrid PSO which switches off its local attractors at a certain point in time. The effects mentioned can also be observed by measuring the potential of the swarm.
A computational study of the effects of remodelled electrophysiology and mechanics on initiation of ventricular fibrillation in human heart failure
Venue: arXiv cs.CE 2014
Year: 2014

The study of pathological cardiac conditions such as arrhythmias, a major cause of mortality in heart failure, is becoming increasingly informed by computational simulation, numerically modelling the governing equations. This can provide insight where experimental work is constrained by technical limitations and/or ethical issues. As the models become more realistic, the construction of efficient and accurate computational models becomes increasingly challenging. In particular, recent developments have started to couple the electrophysiology models with mechanical models in order to investigate the effect of tissue deformation on arrhythmogenesis, thus introducing an element of nonlinearity into the mathematical representation. This paper outlines a biophysically-detailed computational model of coupled electromechanical cardiac activity which uses the finite element method to approximate both electrical and mechanical systems on unstructured, deforming, meshes. An ILU preconditioner is applied to improve performance of the solver. This software is used to examine the role of electrophysiology, fibrosis and mechanical deformation on the stability of spiral wave dynamics in human ventricular tissue by applying it to models of both healthy and failing tissue. The latter was simulated by modifying (i) cellular electrophysiological properties, to generate an increased action potential duration and altered intracellular calcium handling, and (ii) tissue-level properties, to simulate the gap junction remodelling, fibrosis and increased tissue stiffness seen in heart failure. The resulting numerical experiments suggest that, for the chosen mathematical models of electrophysiology and mechanical response, introducing tissue level fibrosis can have a destabilising effect on the dynamics, while the net effect of the electrophysiological remodelling stabilises the system.
Explicit Reference Governor for Continuous Time Nonlinear Systems Subject to Convex Constraints
Venue: arXiv cs.SY 2014
Year: 2014

This paper introduces a novel closed-form strategy that dynamically modifies the reference of a pre-compensated nonlinear system to ensure the satisfaction of a set of convex constraints. The main idea consists of translating constraints in the state space into constraints on the Lyapunov function and then modulating the reference velocity so as to limit the value of the Lyapunov function. The theory is introduced for general nonlinear systems subject to convex constraints. In the case of polyhedric constraints, an explicit solution is provided for the large and highly relevant class of nonlinear systems whose Lyapunov function is lower-bounded by a quadratic form. In view of improving performances, further specializations are provided for the relevant cases of linear systems and robotic manipulators.
Changing the Environment Based on Empowerment as Intrinsic Motivation
Venue: arXiv cs.AI 2014
Year: 2014

One aspect of intelligence is the ability to restructure your own environment so that the world you live in becomes more beneficial to you. In this paper we investigate how the information-theoretic measure of agent empowerment can provide a task-independent, intrinsic motivation to restructure the world. We show how changes in embodiment and in the environment change the resulting behaviour of the agent and the artefacts left in the world. For this purpose, we introduce an approximation of the established empowerment formalism based on sparse sampling, which is simpler and significantly faster to compute for deterministic dynamics. Sparse sampling also introduces a degree of randomness into the decision making process, which turns out to beneficial for some cases. We then utilize the measure to generate agent behaviour for different agent embodiments in a Minecraft-inspired three dimensional block world. The paradigmatic results demonstrate that empowerment can be used as a suitable generic intrinsic motivation to not only generate actions in given static environments, as shown in the past, but also to modify existing environmental conditions. In doing so, the emerging strategies to modify an agent's environment turn out to be meaningful to the specific agent capabilities, i.e., de facto to its embodiment.
Unsupervised Feature Learning through Divergent Discriminative Feature Accumulation
Venue: arXiv cs.NE 2014
Year: 2014

Unlike unsupervised approaches such as autoencoders that learn to reconstruct their inputs, this paper introduces an alternative approach to unsupervised feature learning called divergent discriminative feature accumulation (DDFA) that instead continually accumulates features that make novel discriminations among the training set. Thus DDFA features are inherently discriminative from the start even though they are trained without knowledge of the ultimate classification problem. Interestingly, DDFA also continues to add new features indefinitely (so it does not depend on a hidden layer size), is not based on minimizing error, and is inherently divergent instead of convergent, thereby providing a unique direction of research for unsupervised feature learning. In this paper the quality of its learned features is demonstrated on the MNIST dataset, where its performance confirms that indeed DDFA is a viable technique for learning useful features.
Broadcasting in Networks of Unknown Topology in the Presence of Swamping
Venue: arXiv cs.DC 2014
Year: 2014

In this paper, we address the problem of broadcasting in a wireless network under a novel communication model: the {\em swamping} communication model. In this model, nodes communicate only with those nodes at geometric distance greater than $s$ and at most $r$ from them. Communication between nearby nodes under this model can be very time consuming, as the length of the path between two nodes within distance $s$ is only bounded above by the diameter $D$, in many cases. For the $n$-node lattice networks, we present algorithms of optimal time complexity, respectively $O(n/r + r/(r-s))$ for the lattice line and $O(\sqrt{n}/r + r/(r-s))$ for the two-dimensional lattice. We also consider networks of unknown topology of diameter $D$ and of a parameter $g$ ({\em granularity}). More specifically, we consider networks with $γ$ the minimum distance between any two nodes and $g = 1/γ$. We present broadcast algorithms for networks of nodes placed on the line and on the plane with respective time complexities $O(D/l + g^2)$ and $O(Dg/l + g^4)$, where $l \in Θ(\max\{(1-s),γ\})$.
Structured Dictionary Learning for Classification
Venue: arXiv cs.CV 2014
Year: 2014

Sparsity driven signal processing has gained tremendous popularity in the last decade. At its core, the assumption is that the signal of interest is sparse with respect to either a fixed transformation or a signal dependent dictionary. To better capture the data characteristics, various dictionary learning methods have been proposed for both reconstruction and classification tasks. For classification particularly, most approaches proposed so far have focused on designing explicit constraints on the sparse code to improve classification accuracy while simply adopting $l_0$-norm or $l_1$-norm for sparsity regularization. Motivated by the success of structured sparsity in the area of Compressed Sensing, we propose a structured dictionary learning framework (StructDL) that incorporates the structure information on both group and task levels in the learning process. Its benefits are two-fold: (i) the label consistency between dictionary atoms and training data are implicitly enforced; and (ii) the classification performance is more robust in the cases of a small dictionary size or limited training data than other techniques. Using the subspace model, we derive the conditions for StructDL to guarantee the performance and show theoretically that StructDL is superior to $l_0$-norm or $l_1$-norm regularized dictionary learning for classification. Extensive experiments have been performed on both synthetic simulations and real world applications, such as face recognition and object classification, to demonstrate the validity of the proposed DL framework.
Learning Word Representations with Hierarchical Sparse Coding
Venue: arXiv cs.CL 2014
Year: 2014

We propose a new method for learning word representations using hierarchical regularization in sparse coding inspired by the linguistic study of word meanings. We show an efficient learning algorithm based on stochastic proximal methods that is significantly faster than previous approaches, making it possible to perform hierarchical sparse coding on a corpus of billions of word tokens. Experiments on various benchmark tasks---word similarity ranking, analogies, sentence completion, and sentiment analysis---demonstrate that the method outperforms or is competitive with state-of-the-art methods. Our word representations are available at \url{http://www.ark.cs.cmu.edu/dyogatam/wordvecs/}.
Categorical Semantics for Functional Reactive Programming with Temporal Recursion and Corecursion
Venue: arXiv cs.PL 2014
Year: 2014

Functional reactive programming (FRP) makes it possible to express temporal aspects of computations in a declarative way. Recently we developed two kinds of categorical models of FRP: abstract process categories (APCs) and concrete process categories (CPCs). Furthermore we showed that APCs generalize CPCs. In this paper, we extend APCs with additional structure. This structure models recursion and corecursion operators that are related to time. We show that the resulting categorical models generalize those CPCs that impose an additional constraint on time scales. This constraint boils down to ruling out $ω$-supertasks, which are closely related to Zeno's paradox of Achilles and the tortoise.
Program Verification of Numerical Computation - Part 2
Venue: arXiv cs.LO 2014
Year: 2014

These notes present some extensions of a formal method introduced in an earlier paper. The formal method is designed as a tool for program verification of numerical computation and forms the basis of the software package VPC. Included in the extensions that are presented here are disjunctions and methods for detecting non-computable programs. A more comprehensive list of the construction rules as higher order constructs is also presented.
Local degree blocking model for link prediction in complex networks
Venue: arXiv cs.SI 2014
Year: 2014

Recovering and reconstructing networks by accurately identifying missing and unreliable links is a vital task in the domain of network analysis and mining. In this article, by studying a specific local structure, namely a degree block having a node and its all immediate neighbors, we find it contains important statistical features of link formation for complex networks. We therefore propose a parameter-free local blocking (LB) predictor to quantitatively detect link formation in given networks via local link density calculations. The promising experimental results performed on six real-world networks suggest that the new index can outperform other traditional local similarity-based methods on most of tested networks. After further analyzing the scores' correlations between LB and two other methods, we find that the features of LB index are analogous to those of both PA index and short-path-based index, which empirically verify that large degree principle and short path principle simultaneously captured by the LB index are jointly driving link formation in complex networks.
ARC Sort: Enhanced and Time Efficient Sorting Algorithm
Venue: arXiv cs.DS 2014
Year: 2014

This paper discusses about a sorting algorithm which uses the concept of buckets where each bucket represents a certain number of digits. A two dimensional data structure is used where one dimension represents buckets i. e; number of digits and each bucket's corresponding dimensions represents the input numbers that belong to that bucket. Each bucket is then individually sorted. Since every preceding bucket elements will always be smaller than the succeeding buckets no comparison between them is required. By doing this we can significantly reduced the time complexity of any sorting algorithm used to sort the given set of inputs.
A Piggybank Protocol for Quantum Cryptography
Venue: arXiv cs.CR 2014
Year: 2014

This paper presents a quantum mechanical version of the piggy-bank cryptography protocol. The basic piggybank cryptography idea is to use two communications: one with the encrypted message, and the other regarding the encryption transformation which the receiver must decipher first. In the quantum mechanical version of the protocol, the encrypting unitary transformation information is sent separately but just deciphering it is not enough to break the system. The proposed quantum protocol consists of two stages.
Context management strategies in wireless network
Venue: arXiv cs.NI 2014
Year: 2014

Context management strategies in wireless technology are dependent upon the collection of accurate information from the individual nodes. This information (called context information) can be exploited by administrators or automated systems in order to decide on specific management concerns. While traditional approaches for fixed networks are more or less centralized, more complex management strategies have been proposed for wireless networks, such as hierarchical, fully distributed and hybrid ones. The reason for the introduction of new strategies is based on the dynamic and unpredictable nature of wireless networks and their (usually) limited resources, which do not support centralized management solutions. In this work, efforts is being made to uncovered some specific strategies that can be used to managed context information that reaches the centre of decision making, the work is concluded with a detail comparison of the strategies to enable context application developers make right choice of strategy to be employed in a specific situation.
Subsidization Competition: Vitalizing the Neutral Internet
Venue: arXiv cs.NI 2014
Year: 2014

Unlike telephone operators, which pay termination fees to reach the users of another network, Internet Content Providers (CPs) do not pay the Internet Service Providers (ISPs) of users they reach. While the consequent cross subsidization to CPs has nurtured content innovations at the edge of the Internet, it reduces the investment incentives for the access ISPs to expand capacity. As potential charges for terminating CPs' traffic are criticized under the net neutrality debate, we propose to allow CPs to voluntarily subsidize the usagebased fees induced by their content traffic for end-users. We model the regulated subsidization competition among CPs under a neutral network and show how deregulation of subsidization could increase an access ISP's utilization and revenue, strengthening its investment incentives. Although the competition might harm certain CPs, we find that the main cause comes from high access prices rather than the existence of subsidization. Our results suggest that subsidization competition will increase the competitiveness and welfare of the Internet content market; however, regulators might need to regulate access prices if the access ISP market is not competitive enough. We envision that subsidization competition could become a viable model for the future Internet.
A Generalized and Adaptive Method for Community Detection
Venue: arXiv cs.SI 2014
Year: 2014

Complex networks represent interactions between entities. They appear in various contexts such as sociology, biology, etc., and they generally contain highly connected subgroups called communities. Community detection is a well-studied problem and most of the algorithms aim to maximize the Newman-Girvan modularity function, the most popular being the Louvain method (it is well-suited on very large graphs). However, the classical modularity has many drawbacks: we can find partitions of high quality in graphs without community structure, e.g., on random graphs; it promotes large communities. Then, we have adapted the Louvain method to other quality functions. In this paper, we describe a generic version of the Louvain method. In particular, we give a sufficient condition to plug a quality function into it. We also show that global performance of this new version is similar to the classical Louvain algorithm, that promotes it to the best rank of the community detection algorithms.
Maximum Likelihood-based Online Adaptation of Hyper-parameters in CMA-ES
Venue: arXiv cs.NE 2014
Year: 2014

The Covariance Matrix Adaptation Evolution Strategy (CMA-ES) is widely accepted as a robust derivative-free continuous optimization algorithm for non-linear and non-convex optimization problems. CMA-ES is well known to be almost parameterless, meaning that only one hyper-parameter, the population size, is proposed to be tuned by the user. In this paper, we propose a principled approach called self-CMA-ES to achieve the online adaptation of CMA-ES hyper-parameters in order to improve its overall performance. Experimental results show that for larger-than-default population size, the default settings of hyper-parameters of CMA-ES are far from being optimal, and that self-CMA-ES allows for dynamically approaching optimal settings.
A Utility Proportional Fairness Radio Resource Block Allocation in Cellular Networks
Venue: arXiv cs.NI 2014
Year: 2014

This paper presents a radio resource block allocation optimization problem for cellular communications systems with users running delay-tolerant and real-time applications, generating elastic and inelastic traffic on the network and being modelled as logarithmic and sigmoidal utilities respectively. The optimization is cast under a utility proportional fairness framework aiming at maximizing the cellular systems utility whilst allocating users the resource blocks with an eye on application quality of service requirements and on the procedural temporal and computational efficiency. Ultimately, the sensitivity of the proposed modus operandi to the resource variations is investigated.
Intersection graphs of segments and $\exists\mathbb{R}$
Venue: arXiv cs.CG 2014
Year: 2014

A graph $G$ with vertex set $\{v_1,v_2,\ldots,v_n\}$ is an intersection graph of segments if there are segments $s_1,\ldots,s_n$ in the plane such that $s_i$ and $s_j$ have a common point if and only if $\{v_i,v_j\}$ is an edge of~$G$. In this expository paper, we consider the algorithmic problem of testing whether a given abstract graph is an intersection graph of segments. It turned out that this problem is complete for an interesting recently introduced class of computational problems, denoted by $\exists\mathbb{R}$. This class consists of problems that can be reduced, in polynomial time, to solvability of a system of polynomial inequalities in several variables over the reals. We discuss some subtleties in the definition of $\exists\mathbb{R}$, and we provide a complete and streamlined account of a proof of the $\exists\mathbb{R}$-completeness of the recognition problem for segment intersection graphs. Along the way, we establish $\exists\mathbb{R}$-completeness of several other problems. We also present a decision algorithm, due to Muchnik, for the first-order theory of the reals.