OpenRaiser/Intern-Atlas huggingface dataset:
A Lambda-Calculus with letrec, case, constructors and non-determinism
Venue: arXiv cs.PL 2000
Year: 2000

A non-deterministic call-by-need lambda-calculus \calc with case, constructors, letrec and a (non-deterministic) erratic choice, based on rewriting rules is investigated. A standard reduction is defined as a variant of left-most outermost reduction. The semantics is defined by contextual equivalence of expressions instead of using $αβ(η)$-equivalence. It is shown that several program transformations are correct, for example all (deterministic) rules of the calculus, and in addition the rules for garbage collection, removing indirections and unique copy. This shows that the combination of a context lemma and a meta-rewriting on reductions using complete sets of commuting (forking, resp.) diagrams is a useful and successful method for providing a semantics of a functional programming language and proving correctness of program transformations.
Chip-level CMP Modeling and Smart Dummy for HDP and Conformal CVD Films
Venue: arXiv cs.CE 2000
Year: 2000

Chip-level CMP modeling is investigated to obtain the post-CMP film profile thickness across a die from its design layout file and a few film deposition and CMP parameters. The work covers both HDP and conformal CVD film. The experimental CMP results agree well with the modeled results. Different algorithms for filling of dummy structure are compared. A smart algorithm for dummy filling is presented, which achieves maximal pattern-density uniformity and CMP planarity.
A Decomposition Theorem for Maximum Weight Bipartite Matchings
Venue: arXiv cs.DS 2000
Year: 2000

Let G be a bipartite graph with positive integer weights on the edges and without isolated nodes. Let n, N and W be the node count, the largest edge weight and the total weight of G. Let k(x,y) be log(x)/log(x^2/y). We present a new decomposition theorem for maximum weight bipartite matchings and use it to design an O(sqrt(n)W/k(n,W/N))-time algorithm for computing a maximum weight matching of G. This algorithm bridges a long-standing gap between the best known time complexity of computing a maximum weight matching and that of computing a maximum cardinality matching. Given G and a maximum weight matching of G, we can further compute the weight of a maximum weight matching of G-{u} for all nodes u in O(W) time.
Automatic Debugging Support for UML Designs
Venue: arXiv cs.SE 2000
Year: 2000

Design of large software systems requires rigorous application of software engineering methods covering all phases of the software process. Debugging during the early design phases is extremely important, because late bug-fixes are expensive. In this paper, we describe an approach which facilitates debugging of UML requirements and designs. The Unified Modeling Language (UML) is a set of notations for object-orient design of a software system. We have developed an algorithm which translates requirement specifications in the form of annotated sequence diagrams into structured statecharts. This algorithm detects conflicts between sequence diagrams and inconsistencies in the domain knowledge. After synthesizing statecharts from sequence diagrams, these statecharts usually are subject to manual modification and refinement. By using the ``backward'' direction of our synthesis algorithm, we are able to map modifications made to the statechart back into the requirements (sequence diagrams) and check for conflicts there. Fed back to the user conflicts detected by our algorithm are the basis for deductive-based debugging of requirements and domain theory in very early development stages. Our approach allows to generate explanations on why there is a conflict and which parts of the specifications are affected.
Retrieval from Captioned Image Databases Using Natural Language Processing
Venue: arXiv cs.CL 2000
Year: 2000

It might appear that natural language processing should improve the accuracy of information retrieval systems, by making available a more detailed analysis of queries and documents. Although past results appear to show that this is not so, if the focus is shifted to short phrases rather than full documents, the situation becomes somewhat different. The ANVIL system uses a natural language technique to obtain high accuracy retrieval of images which have been annotated with a descriptive textual caption. The natural language techniques also allow additional contextual information to be derived from the relation between the query and the caption, which can help users to understand the overall collection of retrieval results. The techniques have been successfully used in a information retrieval system which forms both a testbed for research and the basis of a commercial system.
Systematic Debugging of Attribute Grammars
Venue: arXiv cs.SE 2000
Year: 2000

Although attribute grammars are commonly used for compiler construction, little investigation has been conducted on debugging attribute grammars. The paper proposes two types of systematic debugging methods, an algorithmic debugging and slice-based debugging, both tailored for attribute grammars. By means of query-based interaction with the developer, our debugging methods effectively narrow the potential bug space in the attribute grammar description and eventually identify the incorrect attribution rule. We have incorporated this technology in our visual debugging tool called Aki.
SimLab 1.1, Software for Sensitivity and Uncertainty Analysis, tool for sound modelling
Venue: arXiv cs.DM 2000
Year: 2000

The aim of this paper is to present and describe SimLab 1.1 (Simulation Laboratory for Uncertainty and Sensitivity Analysis) software designed for Monte Carlo analysis that is based on performing multiple model evaluations with probabilistically selected model input. The results of these evaluations are used to determine both the uncertainty in model predictions and the input variables that drive this uncertainty. This methodology is essential in situations where a decision has to be taken based on the model results; typical examples include risk and emergency management systems, financial analysis and many others. It is also highly recommended as part of model validation, even where the models are used for diagnostic purposes, as an element of sound model building. SimLab allows an exploration of the space of possible alternative model assumptions and structure on the prediction of the model, thereby testing both the quality of the model and the robustness of the model based inference.
Top-down induction of clustering trees
Venue: arXiv cs.LG 2000
Year: 2000

An approach to clustering is presented that adapts the basic top-down induction of decision trees method towards clustering. To this aim, it employs the principles of instance based learning. The resulting methodology is implemented in the TIC (Top down Induction of Clustering trees) system for first order clustering. The TIC system employs the first order logical decision tree representation of the inductive logic programming system Tilde. Various experiments with TIC are presented, in both propositional and relational domains.
Dancing links
Venue: arXiv cs.DS 2000
Year: 2000

The author presents two tricks to accelerate depth-first search algorithms for a class of combinatorial puzzle problems, such as tiling a tray by a fixed set of polyominoes. The first trick is to implement each assumption of the search with reversible local operations on doubly linked lists. By this trick, every step of the search affects the data incrementally. The second trick is to add a ghost square that represents the identity of each polyomino. Thus puts the rule that each polyomino be used once on the same footing as the rule that each square be covered once. The coding simplifies to a more abstract form which is equivalent to 0-1 integer programming. More significantly for the total computation time, the search can naturally switch between placing a fixed polyomino or covering a fixed square at different stages, according to a combined heuristic. Finally the author reports excellent performance for his algorithm for some familiar puzzles. These include tiling a hexagon by 19 hexiamonds and the N queens problem for N up to 18.
Proving Termination of Normalization Functions for Conditional Expressions
Venue: arXiv cs.LO 2000
Year: 2000

Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure function, (2) in domain theory using LCF, (3) showing that its recursion relation, defined by the pattern of recursive calls, is well-founded. The last two proofs are essentially the same though conducted in markedly different logical frameworks. An obviously total variant of the normalize function is presented as the `computational meaning' of those two proofs. A related function makes nested recursive calls. The three termination proofs become more complex: termination and correctness must be proved simultaneously. The recursion relation approach seems flexible enough to handle subtle termination proofs where previously domain theory seemed essential.
Mechanizing Coinduction and Corecursion in Higher-order Logic
Venue: arXiv cs.LO 2000
Year: 2000

A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists; greatest fixedpoints express coinductive data types, such as lazy lists. Well-founded recursion expresses recursive functions over inductive data types; corecursion expresses functions that yield elements of coinductive data types. The theory rests on a traditional formalization of infinite trees. The theory is intended for use in specification and verification. It supports reasoning about a wide range of computable functions, but it does not formalize their operational semantics and can express noncomputable functions also. The theory is illustrated using finite and infinite lists. Corecursion expresses functions over infinite lists; coinduction reasons about such functions.
Reasoning with Higher-Order Abstract Syntax in a Logical Framework
Venue: arXiv cs.LO 2001
Year: 2001

Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and inference systems. Given such specifications, it is natural to consider proving properties about the specified systems in the framework: for example, given the specification of evaluation for a functional programming language, prove that the language is deterministic or that evaluation preserves types. One challenge in developing a framework for such reasoning is that higher-order abstract syntax (HOAS), an elegant and declarative treatment of object-level abstraction and substitution, is difficult to treat in proofs involving induction. In this paper, we present a meta-logic that can be used to reason about judgments coded using HOAS; this meta-logic is an extension of a simple intuitionistic logic that admits higher-order quantification over simply typed lambda-terms (key ingredients for HOAS) as well as induction and a notion of definition. We explore the difficulties of formal meta-theoretic analysis of HOAS encodings by considering encodings of intuitionistic and linear logics, and formally derive the admissibility of cut for important subsets of these logics. We then propose an approach to avoid the apparent tradeoff between the benefits of higher-order abstract syntax and the ability to analyze the resulting encodings. We illustrate this approach through examples involving the simple functional and imperative programming languages PCF and PCF:=. We formally derive such properties as unicity of typing, subject reduction, determinacy of evaluation, and the equivalence of transition semantics and natural semantics presentations of evaluation.
Constraint Programming viewed as Rule-based Programming
Venue: arXiv cs.AI 2001
Year: 2001

We study here a natural situation when constraint programming can be entirely reduced to rule-based programming. To this end we explain first how one can compute on constraint satisfaction problems using rules represented by simple first-order formulas. Then we consider constraint satisfaction problems that are based on predefined, explicitly given constraints. To solve them we first derive rules from these explicitly given constraints and limit the computation process to a repeated application of these rules, combined with labeling.We consider here two types of rules. The first type, that we call equality rules, leads to a new notion of local consistency, called {\em rule consistency} that turns out to be weaker than arc consistency for constraints of arbitrary arity (called hyper-arc consistency in \cite{MS98b}). For Boolean constraints rule consistency coincides with the closure under the well-known propagation rules for Boolean constraints. The second type of rules, that we call membership rules, yields a rule-based characterization of arc consistency. To show feasibility of this rule-based approach to constraint programming we show how both types of rules can be automatically generated, as {\tt CHR} rules of \cite{fruhwirth-constraint-95}. This yields an implementation of this approach to programming by means of constraint logic programming. We illustrate the usefulness of this approach to constraint programming by discussing various examples, including Boolean constraints, two typical examples of many valued logics, constraints dealing with Waltz's language for describing polyhedral scenes, and Allen's qualitative approach to temporal logic.
Cluster Computing White Paper
Venue: arXiv cs.DC 2001
Year: 2001

Cluster computing is not a new area of computing. It is, however, evident that there is a growing interest in its usage in all areas where applications have traditionally used parallel or distributed computing platforms. The growing interest has been fuelled in part by the availability of powerful microprocessors and high-speed networks as off-the-shelf commodity components as well as in part by the rapidly maturing software components available to support high performance and high availability applications. This White Paper has been broken down into eleven sections, each of which has been put together by academics and industrial researchers who are both experts in their fields and where willing to volunteer their time and effort to put together this White Paper. The status of this paper is draft and we are at the stage of publicizing its presence and making a Request For Comments (RFC).
Managing Periodically Updated Data in Relational Databases: A Stochastic Modeling Approach
Venue: arXiv cs.DB 2001
Year: 2001

Recent trends in information management involve the periodic transcription of data onto secondary devices in a networked environment, and the proper scheduling of these transcriptions is critical for efficient data management. To assist in the scheduling process, we are interested in modeling the reduction of consistency over time between a relation and its replica, termed obsolescence of data. The modeling is based on techniques from the field of stochastic processes, and provides several stochastic models for content evolution in the base relations of a database, taking referential integrity constraints into account. These models are general enough to accommodate most of the common scenarios in databases, including batch insertions and life spans both with and without memory. As an initial "proof of concept" of the applicability of our approach, we validate the insertion portion of our model framework via experiments with real data feeds. We also discuss a set of transcription protocols which make use of the proposed stochastic model.
Phutball Endgames are Hard
Venue: arXiv cs.CC 2001
Year: 2001

We show that, in John Conway's board game Phutball (or Philosopher's Football), it is NP-complete to determine whether the current player has a move that immediately wins the game. In contrast, the similar problems of determining whether there is an immediately winning move in checkers, or a move that kings a man, are both solvable in polynomial time.
A Classification of Symbolic Transition Systems
Venue: arXiv cs.LO 2001
Year: 2001

We define five increasingly comprehensive classes of infinite-state systems, called STS1--5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.
Checking Properties within Fairness and Behavior Abstractions
Venue: arXiv cs.LO 2001
Year: 2001

This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used. It shows that using a more abstract notion than truth under fairness, specifically the concept of a property being satisfied within fairness can lead to interesting possibilities. Technically, it is first established that deciding satisfaction within fairness is a PSPACE-complete problem and it is shown that properties satisfied within fairness can always be satisfied by some fair implementation. Thereafter, the interaction between behavior abstraction and satisfaction within fairness is studied and it is proved that satisfaction of properties within fairness can be verified on behavior abstractions, if the abstraction homomorphism is weakly continuation-closed.
Tree Contractions and Evolutionary Trees
Venue: arXiv cs.CE 2001
Year: 2001

An evolutionary tree is a rooted tree where each internal vertex has at least two children and where the leaves are labeled with distinct symbols representing species. Evolutionary trees are useful for modeling the evolutionary history of species. An agreement subtree of two evolutionary trees is an evolutionary tree which is also a topological subtree of the two given trees. We give an algorithm to determine the largest possible number of leaves in any agreement subtree of two trees T_1 and T_2 with n leaves each. If the maximum degree d of these trees is bounded by a constant, the time complexity is O(n log^2(n)) and is within a log(n) factor of optimal. For general d, this algorithm runs in O(n d^2 log(d) log^2(n)) time or alternatively in O(n d sqrt(d) log^3(n)) time.
Linear-Time Succinct Encodings of Planar Graphs via Canonical Orderings
Venue: arXiv cs.DS 2001
Year: 2001

Let G be an embedded planar undirected graph that has n vertices, m edges, and f faces but has no self-loop or multiple edge. If G is triangulated, we can encode it using {4/3}m-1 bits, improving on the best previous bound of about 1.53m bits. In case exponential time is acceptable, roughly 1.08m bits have been known to suffice. If G is triconnected, we use at most (2.5+2\log{3})\min\{n,f\}-7 bits, which is at most 2.835m bits and smaller than the best previous bound of 3m bits. Both of our schemes take O(n) time for encoding and decoding.
Data Security Equals Graph Connectivity
Venue: arXiv cs.CR 2001
Year: 2001

To protect sensitive information in a cross tabulated table, it is a common practice to suppress some of the cells in the table. This paper investigates four levels of data security of a two-dimensional table concerning the effectiveness of this practice. These four levels of data security protect the information contained in, respectively, individual cells, individual rows and columns, several rows or columns as a whole, and a table as a whole. The paper presents efficient algorithms and NP-completeness results for testing and achieving these four levels of data security. All these complexity results are obtained by means of fundamental equivalences between the four levels of data security of a table and four types of connectivity of a graph constructed from that table.
On the Automated Classification of Web Sites
Venue: arXiv cs.IR 2001
Year: 2001

In this paper we discuss several issues related to automated text classification of web sites. We analyze the nature of web content and metadata in relation to requirements for text features. We find that HTML metatags are a good source of text features, but are not in wide use despite their role in search engine rankings. We present an approach for targeted spidering including metadata extraction and opportunistic crawling of specific semantic hyperlinks. We describe a system for automatically classifying web sites into industry categories and present performance results based on different combinations of text features and training data. This system can serve as the basis for a generalized framework for automated metadata creation.
Fast Pricing of European Asian Options with Provable Accuracy: Single-stock and Basket Options
Venue: arXiv cs.CE 2001
Year: 2001

This paper develops three polynomial-time pricing techniques for European Asian options with provably small errors, where the stock prices follow binomial trees or trees of higher-degree. The first technique is the first known Monte Carlo algorithm with analytical error bounds suitable for pricing single-stock options with meaningful confidence and speed. The second technique is a general recursive bucketing-based scheme that can use the Aingworth-Motwani-Oldham aggregation algorithm, Monte-Carlo simulation and possibly others as the base-case subroutine. This scheme enables robust trade-offs between accuracy and time over subtrees of different sizes. For long-term options or high frequency price averaging, it can price single-stock options with smaller errors in less time than the base-case algorithms themselves. The third technique combines Fast Fourier Transform with bucketing-based schemes for pricing basket options. This technique takes polynomial time in the number of days and the number of stocks, and does not add any errors to those already incurred in the companion bucketing scheme. This technique assumes that the price of each underlying stock moves independently.
Compact Encodings of Planar Graphs via Canonical Orderings and Multiple Parentheses
Venue: arXiv cs.DS 2001
Year: 2001

Let G be a plane graph of n nodes, m edges, f faces, and no self-loop. G need not be connected or simple (i.e., free of multiple edges). We give three sets of coding schemes for G which all take O(m+n) time for encoding and decoding. Our schemes employ new properties of canonical orderings for planar graphs and new techniques of processing strings of multiple types of parentheses. For applications that need to determine in O(1) time the adjacency of two nodes and the degree of a node, we use 2m+(5+1/k)n + o(m+n) bits for any constant k > 0 while the best previous bound by Munro and Raman is 2m+8n + o(m+n). If G is triconnected or triangulated, our bit count decreases to 2m+3n + o(m+n) or 2m+2n + o(m+n), respectively. If G is simple, our bit count is (5/3)m+(5+1/k)n + o(n) for any constant k > 0. Thus, if a simple G is also triconnected or triangulated, then 2m+2n + o(n) or 2m+n + o(n) bits suffice, respectively. If only adjacency queries are supported, the bit counts for a general G and a simple G become 2m+(14/3)n + o(m+n) and (4/3)m+5n + o(n), respectively. If we only need to reconstruct G from its code, a simple and triconnected G uses roughly 2.38m + O(1) bits while the best previous bound by He, Kao, and Lu is 2.84m.
Chaos for Stream Cipher
Venue: arXiv cs.CR 2001
Year: 2001

This paper discusses mixing of chaotic systems as a dependable method for secure communication. Distribution of the entropy function for steady state as well as plaintext input sequences are analyzed. It is shown that the mixing of chaotic sequences results in a sequence that does not have any state dependence on the information encrypted by them. The generated output states of such a cipher approach the theoretical maximum for both complexity measures and cycle length. These features are then compared with some popular ciphers.