8816413
Uses of Higher-Order Unification for Implementing Program Transformers
Source-to-source program transformers belong to the class of meta-programs that manipulate programs as objects. It has previously been argued that a higher-order extension of Prolog, such as λProlog, makes a suitable implementation language for such meta-programs. In this paper, we consider this claim in more detail. In λProlog, object-level programs and program schemata can be represented using simply typed λ-terms and higher-order (functional) variables. Unification of these λ-terms, called higher-order unification, can elegantly describe several important meta-level operations on programs. We detail some properties of higher-order unification that make it suitable for analyzing program structures. We then present (in λProlog) the specification of several simple program transformers together with a more involved partial evaluator. With the depth-first control strategy of λProlog for both clause selection and unifier selection all the above mentioned specifications can be and have been executed and tested. Comments University of Pennsylvania Department of Computer and Information Science Technical Report No. MSCIS-88-46. This technical report is available at ScholarlyCommons: http://repository.upenn.edu/cis_reports/698 USES OF HIGHER-ORDER UNIFICATION FOR IMPLEMENTING PROGRAM TRANSFORMERS JohnHannan Dale Miller MS-CIS-88-46 LlNC LAB 118 Department of Computer and Information Science School of Engineering and Applied Science University of Pennsylvania Philadelphia, PA 19104
3264852
Reasoning with higher-order abstract syntax in a logical framework
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 article, 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 λ-terms (key ingredients for HOAS) as well as induction and a notion of definition. The latter concept of definition is a proof-theoretic device that allows certain theories to be treated as "closed" or as defining fixed points. 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 trade-off 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.
14782174
Uniform Proofs as a Foundation for Logic Programming
Abstract Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 (1991) 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. The operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed.
10134130
A Congruence Format for Name-passing Calculi
We define and use a SOS-based framework to specify the transition systems of calculi with name-passing properties. This setting uses proof-theoretic tools to take care of some of the difficulties specific to name-binding and make them easier to handle in proofs. The contribution of this paper is the presentation of a format that ensures that open bisimilarity is a congruence for calculi specified within this framework, extending the well-known tyft/tyxt format to the case of name-binding and name-passing. We apply this result to the @p-calculus in both its late and early semantics.
100764
Foundational aspects of syntax
A large variety of computing systems, such as compilers, interpreters, static analyzers, and theorem provers, need to manipulate syntactic objects like programs, types, formulas, and proofs. A common characteristic of these syntactic objects is that they contain variable binders, such as quantifiers, scoping operators, and parameters. The presence of binders complicates formal specifications and symbolic processing. Consider, for example, a function definition of the form
5278164
A Logic Programming Approach to Manipulating Formulas and Programs
By permitting function and predicate symbols to be variables and by replacing first-order terms by simply typed $lambda$-terms, a higher-order extension to first-order Horn clauses can be described. To be complete in principle, a logic programming language based on this extension must incorporate higher-order unification. Although this is a more complex operation than first-order unification, its availability as a primitive makes certain kinds of programming tasks easier. We illustrate this aspect in the paper by presenting some programs in a higher-order version of Prolog called $\lambda$Prolog that manipulate objects, such as formulas and programs, whose representation requires structures containing abstractions or bound variables. Specifically, we show (a) how a simple natural deduction theorem prover may be implemented in $\lambda$Prolog, and (b) how some simple program transformers for a functional programming language may be written in this language. These programs exploit the availability of $\lambda$-conversion and higher-order unification in $\lambda$Prolog to provide elegant solutions to several awkward problems inherent in these tasks. We contend that programs which perform similar tasks but which are written in languages without these features would, at least, be much less perspicuous.
34355186
Achromatic numbers and graph operations
Abstract In this paper we investigate the achromatic number of the disjoint union ofgraphs and the achromatic number of the categorical product of graphs. We obtain the best possible upper and lower bounds for the union of graphs and the best possible lower bound for the product of graphs. Finally we show that the achromatic number of the product of graphs is bounded above.
5486748
Scaling internet routers using optics
Routers built around a single-stage crossbar and a centralized scheduler do not scale, and (in practice) do not provide the throughput guarantees that network operators need to make efficient use of their expensive long-haul links. In this paper we consider how optics can be used to scale capacity and reduce power in a router. We start with the promising load-balanced switch architecture proposed by C-S. Chang. This approach eliminates the scheduler, is scalable, and guarantees 100% throughput for a broad class of traffic. But several problems need to be solved to make this architecture practical: (1) Packets can be mis-sequenced, (2) Pathological periodic traffic patterns can make throughput arbitrarily small, (3) The architecture requires a rapidly configuring switch fabric, and (4) It does not work when linecards are missing or have failed. In this paper we solve each problem in turn, and describe new architectures that include our solutions. We motivate our work by designing a 100Tb/s packet-switched router arranged as 640 linecards, each operating at 160Gb/s. We describe two different implementations based on technology available within the next three years.
21145709
A Hybrid Genetic Algorithm for the Single Machine Scheduling Problem
A hybrid genetic algorithm (HGA) is proposed for the single machine, single stage, scheduling problem in a sequence dependent setup time environment within a fixed planning horizon (SSSDP). It incorporates the elitist ranking method, genetic operators, and a hill-climbing technique in each searching area. To improve the performance and efficiency, hill climbing is performed by uniting the Wagner-Whitin Algorithm with the problem-specific knowledge. The objective of the HGA is to minimize the sum of setup cost, inventory cost, and backlog cost. The HGA is able to obtain a superior solution, if it is not optimal, in a reasonable time. The computational results of this algorithm on real life SSSDP problems are promising. In our test cases, the HGA performed up to 50% better than the Just-In-Time heuristics and 30% better than the complete batching heuristics.
13298925
Collection analysis for Horn clause programs
We consider approximating data structures with collections of the items that they contain. For examples, lists, binary trees, tuples, etc, can be approximated by sets or multisets of the items within them. Such approximations can be used to provide partial correctness properties of logic programs. For example, one might wish to specify than whenever the atom sort(t,s) is proved then the two lists t and s contain the same multiset of items (that is, s is a permutation of t). If sorting removes duplicates, then one would like to infer that the sets of items underlying t and s are the same. Such results could be useful to have if they can be determined statically and automatically. We present a scheme by which such collection analysis can be structured and automated. Central to this scheme is the use of linear logic as a computational logic underlying the logic of Horn clauses
9952136
Using a distributed single address space operating system to support modern cluster computing
Recent 64-bit microprocessors have made a huge 18.4 quintillion byte address space potentially available to programs. This has led to the design of operating systems that provide a single virtual address space in which all code and data reside in and across all levels of storage and all nodes of a distributed system. These operating systems, called single address space operating systems (SASOSs), have characteristics that can be used to support modern cluster computing in a distributed system in ways that provide an improved program development environment and higher performance than is available from conventional operating systems. Sombrero, our SASOS design, makes use of its hardware support for object-grained protection, separate thread-related protection domains and implicit protection domain crossing to provide support for modern cluster computing which is not available in SASOSs built on stock processors. Its design, which provides direct system-level support for object-oriented programming, includes a number of features targeted specifically at modern cluster computing.