OpenRaiser/Intern-Atlas huggingface dataset:
Order-consistent programs are cautiously monotonic
Venue: arXiv cs.LO 2000
Year: 2000

Some normal logic programs under the answer set (stable model) semantics lack the appealing property of "cautious monotonicity." That is, augmenting a program with one of its consequences may cause it to lose another of its consequences. The syntactic condition of "order-consistency" was shown by Fages to guarantee existence of an answer set. This note establishes that order-consistent programs are not only consistent, but cautiously monotonic. From this it follows that they are also "cumulative." That is, augmenting an order-consistent with some of its consequences does not alter its consequences. In fact, as we show, its answer sets remain unchanged.
Towards a Universal Theory of Artificial Intelligence based on Algorithmic Probability and Sequential Decision Theory
Venue: arXiv cs.AI 2000
Year: 2000

Decision theory formally solves the problem of rational agents in uncertain worlds if the true environmental probability distribution is known. Solomonoff's theory of universal induction formally solves the problem of sequence prediction for unknown distribution. We unify both theories and give strong arguments that the resulting universal AIXI model behaves optimal in any computable environment. The major drawback of the AIXI model is that it is uncomputable. To overcome this problem, we construct a modified algorithm AIXI^tl, which is still superior to any other time t and space l bounded agent. The computation time of AIXI^tl is of the order t x 2^l.
Resource-distribution via Boolean constraints
Venue: arXiv cs.LO 2000
Year: 2000

We consider the problem of searching for proofs in sequential presentations of logics with multiplicative (or intensional) connectives. Specifically, we start with the multiplicative fragment of linear logic and extend, on the one hand, to linear logic with its additives and, on the other, to the additives of the logic of bunched implications, BI. We give an algebraic method for calculating the distribution of the side-formulae in multiplicative rules which allows the occurrence or non-occurrence of a formula on a branch of a proof to be determined once sufficient information is available. Each formula in the conclusion of such a rule is assigned a Boolean expression. As a search proceeds, a set of Boolean constraint equations is generated. We show that a solution to such a set of equations determines a proof corresponding to the given search. We explain a range of strategies, from the lazy to the eager, for solving sets of constraint equations. We indicate how to apply our methods systematically to large family of relevant systems.
Verifying the Unification Algorithm in LCF
Venue: arXiv cs.LO 2000
Year: 2000

Manna and Waldinger's theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented in detail, as an example of interaction with LCF. Translating the theory into LCF's domain-theoretic logic is largely straightforward. Well-founded induction on a complex ordering is translated into nested structural inductions. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. The verification is presented as a series of lemmas. The LCF proofs are compared with the original ones, and with other approaches. It appears difficult to find a logic that is both simple and flexible, especially for proving termination.
Set Theory for Verification: I. From Foundations to Functions
Venue: arXiv cs.LO 2000
Year: 2000

A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the flexibility to adapt to variants of set theory. Its higher-order syntax supports the definition of new binding operators. Unknowns in subgoals can be instantiated incrementally. The paper describes the derivation of rules for descriptions, relations and functions, and discusses interactive proofs of Cantor's Theorem, the Composition of Homomorphisms challenge [9], and Ramsey's Theorem [5]. A generic proof assistant can stand up against provers dedicated to particular logics.
A Structured Language Model
Venue: arXiv cs.CL 2000
Year: 2000

The paper presents a language model that develops syntactic structure and uses it to extract meaningful information from the word history, thus enabling the use of long distance dependencies. The model assigns probability to every joint sequence of words - binary-parse-structure with headword annotation. The model, its probabilistic parametrization, and a set of experiments meant to evaluate its predictive power are presented.
On Reconfiguring Tree Linkages: Trees can Lock
Venue: arXiv cs.CG 2000
Year: 2000

It has recently been shown that any simple (i.e. nonintersecting) polygonal chain in the plane can be reconfigured to lie on a straight line, and any simple polygon can be reconfigured to be convex. This result cannot be extended to tree linkages: we show that there are trees with two simple configurations that are not connected by a motion that preserves simplicity throughout the motion. Indeed, we prove that an $N$-link tree can have $2^{Ω(N)}$ equivalence classes of configurations.
Well-Typed Logic Programs Are not Wrong
Venue: arXiv cs.LO 2001
Year: 2001

We consider prescriptive type systems for logic programs (as in Goedel or Mercury). In such systems, the typing is static, but it guarantees an operational property: if a program is "well-typed", then all derivations starting in a "well-typed" query are again "well-typed". This property has been called subject reduction. We show that this property can also be phrased as a property of the proof-theoretic semantics of logic programs, thus abstracting from the usual operational (top-down) semantics. This proof-theoretic view leads us to questioning a condition which is usually considered necessary for subject reduction, namely the head condition. It states that the head of each clause must have a type which is a variant (and not a proper instance) of the declared type. We provide a more general condition, thus reestablishing a certain symmetry between heads and body atoms. The condition ensures that in a derivation, the types of two unified terms are themselves unifiable. We discuss possible implications of this result. We also discuss the relationship between the head condition and polymorphic recursion, a concept known in functional programming.
Automatic Differentiation Tools in Optimization Software
Venue: arXiv cs.MS 2001
Year: 2001

We discuss the role of automatic differentiation tools in optimization software. We emphasize issues that are important to large-scale optimization and that have proved useful in the installation of nonlinear solvers in the NEOS Server. Our discussion centers on the computation of the gradient and Hessian matrix for partially separable functions and shows that the gradient and Hessian matrix can be computed with guaranteed bounds in time and memory requirements
Slicing Event Traces of Large Software Systems
Venue: arXiv cs.SE 2001
Year: 2001

Debugging of large software systems consisting of many processes accessing shared resources is a very difficult task. Many commercial systems record essential events during system execution for post-mortem analysis. However, the event traces of large and long-running systems can be quite voluminous. Analysis of such event traces to identify sources of incorrect behavior can be very tedious, error-prone, and inefficient. In this paper, we propose a novel technique of slicing event traces as a means of reducing the number of events for analysis. This technique identifies events that may have influenced observed incorrect system behavior. In order to recognize influencing events several types of dependencies between events are identified. These dependencies are determined automatically from an event trace. In order to improve the precision of slicing we propose to use additional dependencies, referred to as cause-effect dependencies, which can further reduce the size of sliced event traces. Our initial experience has shown that this slicing technique can significantly reduce the size of event traces for analysis.
An Even Faster and More Unifying Algorithm for Comparing Trees via Unbalanced Bipartite Matchings
Venue: arXiv cs.CV 2001
Year: 2001

A widely used method for determining the similarity of two labeled trees is to compute a maximum agreement subtree of the two trees. Previous work on this similarity measure is only concerned with the comparison of labeled trees of two special kinds, namely, uniformly labeled trees (i.e., trees with all their nodes labeled by the same symbol) and evolutionary trees (i.e., leaf-labeled trees with distinct symbols for distinct leaves). This paper presents an algorithm for comparing trees that are labeled in an arbitrary manner. In addition to this generality, this algorithm is faster than the previous algorithms. Another contribution of this paper is on maximum weight bipartite matchings. We show how to speed up the best known matching algorithms when the input graphs are node-unbalanced or weight-unbalanced. Based on these enhancements, we obtain an efficient algorithm for a new matching problem called the hierarchical bipartite matching problem, which is at the core of our maximum agreement subtree algorithm.
A Dynamic Programming Approach to De Novo Peptide Sequencing via Tandem Mass Spectrometry
Venue: arXiv cs.CE 2001
Year: 2001

The tandem mass spectrometry fragments a large number of molecules of the same peptide sequence into charged prefix and suffix subsequences, and then measures mass/charge ratios of these ions. The de novo peptide sequencing problem is to reconstruct the peptide sequence from a given tandem mass spectral data of k ions. By implicitly transforming the spectral data into an NC-spectrum graph G=(V,E) where |V|=2k+2, we can solve this problem in O(|V|+|E|) time and O(|V|) space using dynamic programming. Our approach can be further used to discover a modified amino acid in O(|V||E|) time and to analyze data with other types of noise in O(|V||E|) time. Our algorithms have been implemented and tested on actual experimental data.
The Enhanced Double Digest Problem for DNA Physical Mapping
Venue: arXiv cs.CE 2001
Year: 2001

The double digest problem is a common NP-hard approach to constructing physical maps of DNA sequences. This paper presents a new approach called the enhanced double digest problem. Although this new problem is also NP-hard, it can be solved in linear time in certain theoretically interesting cases.
Non-convex cost functionals in boosting algorithms and methods for panel selection
Venue: arXiv cs.NE 2001
Year: 2001

In this document we propose a new improvement for boosting techniques as proposed in Friedman '99 by the use of non-convex cost functional. The idea is to introduce a correlation term to better deal with forecasting of additive time series. The problem is discussed in a theoretical way to prove the existence of minimizing sequence, and in a numerical way to propose a new "ArgMin" algorithm. The model has been used to perform the touristic presence forecast for the winter season 1999/2000 in Trentino (italian Alps).
Components and Interfaces of a Process Management System for Parallel Programs
Venue: arXiv cs.DC 2001
Year: 2001

Parallel jobs are different from sequential jobs and require a different type of process management. We present here a process management system for parallel programs such as those written using MPI. A primary goal of the system, which we call MPD (for multipurpose daemon), is to be scalable. By this we mean that startup of interactive parallel jobs comprising thousands of processes is quick, that signals can be quickly delivered to processes, and that stdin, stdout, and stderr are managed intuitively. Our primary target is parallel machines made up of clusters of SMPs, but the system is also useful in more tightly integrated environments. We describe how MPD enables much faster startup and better runtime management of parallel jobs. We show how close control of stdio can support the easy implementation of a number of convenient system utilities, even a parallel debugger. We describe a simple but general interface that can be used to separate any process manager from a parallel library, which we use to keep MPD separate from MPICH.
Easy and Hard Constraint Ranking in OT: Algorithms and Complexity
Venue: arXiv cs.CL 2001
Year: 2001

We consider the problem of ranking a set of OT constraints in a manner consistent with data. We speed up Tesar and Smolensky's RCD algorithm to be linear on the number of constraints. This finds a ranking so each attested form x_i beats or ties a particular competitor y_i. We also generalize RCD so each x_i beats or ties all possible competitors. Alas, this more realistic version of learning has no polynomial algorithm unless P=NP! Indeed, not even generation does. So one cannot improve qualitatively upon brute force: Merely checking that a single (given) ranking is consistent with given forms is coNP-complete if the surface forms are fully observed and Delta_2^p-complete if not. Indeed, OT generation is OptP-complete. As for ranking, determining whether any consistent ranking exists is coNP-hard (but in Delta_2^p) if the forms are fully observed, and Sigma_2^p-complete if not. Finally, we show that generation and ranking are easier in derivational theories: in P, and NP-complete.
Mathematical Model of Word Length on the Basis of the Cebanov-Fucks Distribution with Uniform Parameter Distribution
Venue: arXiv cs.CL 2001
Year: 2001

The data on 13 typologically different languages have been processed using a two-parameter word length model, based on 1-displaced uniform Poisson distribution. Statistical dependencies of the 2nd parameter on the 1st one are revealed for the German texts and genre of letters.
Gene Expression Programming: a New Adaptive Algorithm for Solving Problems
Venue: arXiv cs.AI 2001
Year: 2001

Gene expression programming, a genotype/phenotype genetic algorithm (linear and ramified), is presented here for the first time as a new technique for the creation of computer programs. Gene expression programming uses character linear chromosomes composed of genes structurally organized in a head and a tail. The chromosomes function as a genome and are subjected to modification by means of mutation, transposition, root transposition, gene transposition, gene recombination, and one- and two-point recombination. The chromosomes encode expression trees which are the object of selection. The creation of these separate entities (genome and expression tree) with distinct functions allows the algorithm to perform with high efficiency that greatly surpasses existing adaptive techniques. The suite of problems chosen to illustrate the power and versatility of gene expression programming includes symbolic regression, sequence induction with and without constant creation, block stacking, cellular automata rules for the density-classification problem, and two problems of boolean concept learning: the 11-multiplexer and the GP rule problem.
Soundness, Idempotence and Commutativity of Set-Sharing
Venue: arXiv cs.PL 2001
Year: 2001

It is important that practical data-flow analyzers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary generic properties for an abstract domain to be well-defined and sound with respect to the concrete semantics. In logic programming, the abstract domain Sharing is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there were no satisfactory proofs for the key properties of commutativity and idempotence that are essential for Sharing to be well-defined and that published statements of the soundness of Sharing assume the occurs-check. This paper provides a generalization of the abstraction function for Sharing that can be applied to any language, with or without the occurs-check. Results for soundness, idempotence and commutativity for abstract unification using this abstraction function are proven.
Magical Number Seven Plus or Minus Two: Syntactic Structure Recognition in Japanese and English Sentences
Venue: arXiv cs.CL 2001
Year: 2001

George A. Miller said that human beings have only seven chunks in short-term memory, plus or minus two. We counted the number of bunsetsus (phrases) whose modifiees are undetermined in each step of an analysis of the dependency structure of Japanese sentences, and which therefore must be stored in short-term memory. The number was roughly less than nine, the upper bound of seven plus or minus two. We also obtained similar results with English sentences under the assumption that human beings recognize a series of words, such as a noun phrase (NP), as a unit. This indicates that if we assume that the human cognitive units in Japanese and English are bunsetsu and NP respectively, analysis will support Miller's $7 \pm 2$ theory.
Faster-than-light effects and negative group delays in optics and electronics, and their applications
Venue: arXiv cs.PF 2001
Year: 2001

Recent manifestations of apparently faster-than-light effects confirmed our predictions that the group velocity in transparent optical media can exceed c. Special relativity is not violated by these phenomena. Moreover, in the electronic domain, the causality principle does not forbid negative group delays of analytic signals in electronic circuits, in which the peak of an output pulse leaves the exit port of a circuit before the peak of the input pulse enters the input port. Furthermore, pulse distortion for these superluminal analytic signals can be negligible in both the optical and electronic domains. Here we suggest an extension of these ideas to the microelectronic domain. The underlying principle is that negative feedback can be used to produce negative group delays. Such negative group delays can be used to cancel out the positive group delays due to transistor latency (e.g., the finite RC rise time of MOSFETS caused by their intrinsic gate capacitance), as well as the propagation delays due to the interconnects between transistors. Using this principle, it is possible to speed up computer systems.
A Dualheap Selection Algorithm - A Call for Analysis
Venue: arXiv cs.DS 2001
Year: 2001

An algorithm is presented that efficiently solves the selection problem: finding the k-th smallest member of a set. Relevant to a divide-and-conquer strategy, the algorithm also partitions a set into small and large valued subsets. Applied recursively, this partitioning results in a sorted set. The algorithm's applicability is therefore much broader than just the selection problem. The presented algorithm is based upon R.W. Floyd's 1964 algorithm that constructs a heap from the bottom-up. Empirically, the presented algorithm's performance appears competitive with the popular quickselect algorithm, a variant of C.A.R. Hoare's 1962 quicksort algorithm. Furthermore, constructing a heap from the bottom-up is an inherently parallel process (processors can work independently and simultaneously on subheap construction), suggesting a performance advantage with parallel implementations. Given the presented algorithm's broad applicability, simplicity, serial performance, and parallel nature, further study is warranted. Specifically, worst-case analysis is an important but still unsolved problem.
Replica Selection in the Globus Data Grid
Venue: arXiv cs.DC 2001
Year: 2001

The Globus Data Grid architecture provides a scalable infrastructure for the management of storage resources and data that are distributed across Grid environments. These services are designed to support a variety of scientific applications, ranging from high-energy physics to computational genomics, that require access to large amounts of data (terabytes or even petabytes) with varied quality of service requirements. By layering on a set of core services, such as data transport, security, and replica cataloging, one can construct various higher-level services. In this paper, we discuss the design and implementation of a high-level replica selection service that uses information regarding replica location and user preferences to guide selection from among storage replica alternatives. We first present a basic replica selection service design, then show how dynamic information collected using Globus information service capabilities concerning storage system properties can help improve and optimize the selection process. We demonstrate the use of Condor's ClassAds resource description and matchmaking mechanism as an efficient tool for representing and matching storage resource capabilities and policies against application requirements.
Chain Programs for Writing Deterministic Metainterpreters
Venue: arXiv cs.LO 2001
Year: 2001

Many metainterpreters found in the logic programming literature are nondeterministic in the sense that the selection of program clauses is not determined. Examples are the familiar "demo" and "vanilla" metainterpreters. For some applications this nondeterminism is convenient. In some cases, however, a deterministic metainterpreter, having an explicit selection of clauses, is needed. Such cases include (1) conversion of OR parallelism into AND parallelism for "committed-choice" processors, (2) logic-based, imperative-language implementation of search strategies, and (3) simulation of bounded-resource reasoning. Deterministic metainterpreters are difficult to write because the programmer must be concerned about the set of unifiers of the children of a node in the derivation tree. We argue that it is both possible and advantageous to write these metainterpreters by reasoning in terms of object programs converted into a syntactically restricted form that we call "chain" form, where we can forget about unification, except for unit clauses. We give two transformations converting logic programs into chain form, one for "moded" programs (implicit in two existing exhaustive-traversal methods for committed-choice execution), and one for arbitrary definite programs. As illustrations of our approach we show examples of the three applications mentioned above.
System Support for Bandwidth Management and Content Adaptation in Internet Applications
Venue: arXiv cs.NI 2001
Year: 2001

This paper describes the implementation and evaluation of an operating system module, the Congestion Manager (CM), which provides integrated network flow management and exports a convenient programming interface that allows applications to be notified of, and adapt to, changing network conditions. We describe the API by which applications interface with the CM, and the architectural considerations that factored into the design. To evaluate the architecture and API, we describe our implementations of TCP; a streaming layered audio/video application; and an interactive audio application using the CM, and show that they achieve adaptive behavior without incurring much end-system overhead. All flows including TCP benefit from the sharing of congestion information, and applications are able to incorporate new functionality such as congestion control and adaptive behavior.