A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.     

A decision procedure for common Lisp''sSUBTYPEP predicate

Common Lisp [25],[26] includes a dynamic datatype system of moderate complexity, as well as predicates for checking the types of language objects. Additionally, an interesting predicate of two type specifiers—SUBTYPEP—is included in the language. Thissubtypep predicate provides a mechanism with which to query the Common Lisp type system regarding containment relations among the various built-in and user-defined types. Whilesubtypep is rarely needed by an applications programmer, the efficiency of a Common Lisp implementation can depend critically upon the quality of itssubtypep predicate: the run-time system typically calls uponsubtypep to decide what sort of representations to use when making arrays; the compiler calls uponsubtypep to interpret userdeclarations, on which efficient data representation and code generation decisions are based.As might be expected due to the complexity of the Common Lisp type system, there may be type containment questions which cannot be decided. In these casessubtypep is expected to return can't determine, in order to avoid giving an incorrect answer. Unfortunately, most Common Lisp implementations have abused this license by answering can't determine in all but the most trivial cases.In particular, most Common Lisp implementations of SUBTYPEP fail on the basic axioms of the Common Lisp type system itself [25][26]. This situation is particularly embarrassing for Lisp-the premier symbol processing language—in which the implementation of complex symbolic logical operations should be relatively easy. Sincesubtypep was presumably included in Common Lisp to answer thehard cases of type containment, this lazy evaluation limits the usefulness of an important language feature.     

CLP(ℜ) and some electrical engineering problems

The Constraint Logic Programming Scheme defines a class of languages designed for programming with constraints using a logic programming approach. These languages are soundly based on a unified framework of formal semantics. In particular, as an instance of this scheme with real arithmetic constraints, the CLP() language facilitates and encourages a concise and declarative style of programming for problems involving a mix of numeric and non-numeric computation.In this paper we illustrate the practical applicability of CLP() with examples of programs to solve electrical engineering problems. This field is particularly rich in problems that are complex and largely numeric, enabling us to demonstrate a number of the unique features of CLP(). A detailed look at some of the more important programming techniques highlights the ability of CLP() to support well-known, powerful techniques from constraint programming. Our thesis is that CLP() is an embodiment of these techniques in a language that is more general, elegant and versatile than the earlier languages, and yet is practical.An earlier version of this paper appeared in the proceedings of the 4th International Conference on Logic Programming, Melbourne, May 1987. Much of this work was carried out while the authors were at Monash University, Melbourne, Australia.     

Flexible manufacturing system (FMS) scheduling using filtered beam search

This paper reports our effort to develop a knowledge based system for scheduling jobs in a flexible manufacturing system (FMS). We view FMS scheduling as a two-stage process: static scheduling, followed by real-time rescheduling if unanticipated events were to occur. This paper deals with the static scheduling stage. The system uses a frame-based knowledge representation scheme and a problem-solving strategy based on filtered beam search. Filtered beam search views a scheduling problem as a state space search and generates a good schedule quickly by controlling the amount of search required. Evaluation functions are used to decide which branches are the most promising. An important feature of this system, in our view, is the explicit manner in which environmental, procedural and structural knowledge, (stored in the knowledge base using a frame-based scheme) can be used to improve the quality of the generated schedule. The system has been implemented and tested using Common Lisp on a Macintosh system with a 3MB main memory and a 40MB hard disk. Computational experience with our system is reported.     

Overview: The common lisp object system

The Common Lisp Object System is an object-oriented system that is based on the concepts of generic functions, multiple inheritance, and method combination. All objects in the Object System are instances of classes that form an extension to the Common Lisp type system. The Common Lisp Object System is based on a meta-object protocol that renders it possible to alter the fundamental structure of the Object System itself.     

Endpaper: Technical issues of separation in function cells and value cells

Summary The bulk of arguments that focus on clean semantics and notational simplicity tend to favor uniting the function and value namespaces. In spite of this, there are those who hold strongly to a belief that a two-namespace system affords useful expressive power that they are unwilling to do without. In the end, practical considerations favor the status quo for Common Lisp. There are a large number of improvements beyond a single namespace that could be made to Common Lisp that would clean it up and simplify it. We feel that the time for such radical changes to Common Lisp has passed, and it is the job of future Lisp designers to take the lessons from Common Lisp and Scheme to produce an improved Lisp.This paper is an adaptation of a report produced for X3J13 by the authors, a technical working group engaged in standardizing Common Lisp for ANSI.     

Qlisp: parallel processing in Lisp

The authors describe a version of Common Lisp for multiprocessing, called Qlisp. It supports medium-grained parallelism for artificial-intelligence and symbolic programs. Qlisp supports the futures data type. It also introduces partially, multiply invoked functions that let program components be synchronized. An implementation of Qlisp on an Alliant FX/8, based on Lucid Common Lisp, a commercial system, is described     

EuLisp in education

We present our experience withEuLisp as a teaching language, focussing on the level of the language which was specifically designed for this purpose (level-0).EuLisp has been used in undergraduate and postgraduate teaching since 1990, in lectures and laboratories, where in many cases it has replaced Scheme or Common Lisp. It has been used extensively in programming courses, parallelism courses, as a vehicle for advanced courses in symbolic computing and programming language design; it has also been used as a platform for final year undergraduate projects. This experience has demonstrated thatEuLisp is well suited to teaching and far reaching in its capabilities: it supports the relevant concepts in a consistent and versatile framework, so that the language serves to facilitate the educational process. The discussion is illustrated with examples, and where appropriate we draw a comparison with the Lisp dialects used previously in these courses.     

Intelligent backtracking in CLP(ℜ)

CLP() is a constraint logic programming language in which constraints can be expressed in the domain of real numbers. Computation in this specialized domain gives access to information useful in intelligent backtracking. In this paper, we present an efficient constraint satisfaction algorithm for linear constraints in the real number domain and show that our algorithm directly generates minimal sets of conflicting constraints when failures occur. We demonstrate how information gleaned during constraint satisfaction can be integrated with unification failure analysis. The resulting intelligent backtracking method works in the context of a two-sorted domain, where variables can be bound to either structured terms or real number expressions. We discuss the implementation of backtracking and show examples where the benefit of pruning the search tree outweights the overhead of failure analysis.     

智能对象语言CLOS的分布实现

ＣＬＯＳ系统是一个嵌入Ｃｏｍｍｏｎ Ｌｉｓｐ的面向对象标准语言。文中结合所提出的类分方法，通过引入同步或异步通信协议和ＲＰＣ并发控制，详细介绍了一个新的分布ＣＬＯＳ系统ＰａｒＣＬＯＳ。     

A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View

We describe a mechanically checked correctness proof for a system of n processes, each running a simple, non-blocking counter algorithm. We prove that if the system runs longer than 5n steps, the counter is increased. The theorem is formalized in applicative Common Lisp and proved with the ACL2 theorem prover. The value of this paper lies not so much in the trivial algorithm addressed as in the method used to prove it correct. The method allows one to reason accurately about the behavior of a concurrent, multiprocess system by reasoning about the sequential computation carried out by a selected process, against a memory that is changed externally. Indeed, we prove general lemmas that allow shifting between the multiprocess and uniprocess views. We prove a safety property using a multiprocess view, project the property to a uniprocess view, and then prove a global progress property via a local, sequential computation argument. Our uniprocessor view is a formal compositional semantics for a shared memory system.     

Some Remarks on the Semantics of FIPA's Agent Communication Language

The Foundation for Intelligent Physical Agents (FIPA) standardisation body has produced a set of specifications outlining a generic model for the architecture and operation of agent-based systems. The FIPA'97 Specification Part 2 is the normative specification of an Agent Communication Language (ACL) which agents use to talk to each other. The FIPA ACL is based on speech act theory. Its syntax is defined by performatives parameterised by attribute value pairs, while its semantics is given in terms of the mental states of the communicating agents (i.e. intentionality). However, it is not clear if the formal semantics is meant as a normative or informative specification. The primary purpose of this paper is then to give an expository analysis of the FIPA ACL semantics to clarify this situation. We also offer some guidelines motivated from our own analysis, experience and understanding of how the semantic definitions and logical axioms should be interpreted and applied. However, our conclusion is that while the FIPA ACL specification offers significant potential to a developer using it for guidance, there are limitations on using an agent's mental state to specify the meaning of a performative as part of a normative standard. We consider some possibilities for making improvements in this direction.     

UCL+P—Defining and Implementing Persistent Common Lisp

The Persistent Lisp language was defined and an implementation, UCL+P, 1 was designed and constructed. Persistent Lisp is a superset of Common Lisp which fully supports the development of programs manipulating persistent data while maintaining Lisp semantics across the storage/retrieval of values. Persistence features provided are concurrent atomic transactions, demand loading of values, and transparent load and store of persistent values. All Common Lisp data types (with the exception of streams) can be made persistent. Nonsymbolic values are initially created as transient values on the runtime heap. When a transaction completes, transient values which are reachable from a persistent symbol become persistent. The package mechanism has been extended to add a persistence attribute to packages. When symbols are interned in a package with the persistence attribute, they become persistent, as do values reachable from them. UCL+P was created to support these features, by making extensive low-level modifications to the UCL compiler and runtime system. A new runtime data structure, the indirection vector, was created to support the relocation of newly persistent values from the runtime heap to the persistent heap.     

CLOS的分布实现技术

ＣＬＯＳ系统是一个嵌入ＣｏｍｍｏｎＬｉｓｐ的面向对象标准语言，本文结合我们提出的类划分方法，通过引入同步或异步通信协议和ＲＰＣ并发控制，详细介绍了一个新的分布ＣＬＯＳ系统ＰａｒＣＬＯＳ。测试结果表明：若结点较均匀，运行效率大于８０％。     

An industrial strength theorem prover for a logic based on CommonLisp

ACL2 is a reimplemented extended version of R.S. Boyer and J.S. Moore's (1979; 1988) Nqthm and M. Kaufmann's (1988) Pc-Nqthm, intended for large scale verification projects. The paper deals primarily with how we scaled up Nqthm's logic to an industrial strength” programming language-namely, a large applicative subset of Common Lisp-while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola CAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on the AMD5_K 86 microprocessor by Advanced Micro Devices, Inc     

Programming with dual numbers and its applications in mechanisms design

Dual numbers are expressed in the form x+y where ². Dual metanumbers are defined in this paper as DualZero, DualInf and DualNaN. The extended dual plane and the extended finite dual plane are introduced to describe dual numbers and dual metanumbers. Handling of dual numbers in the C^H programming language is presented. The I/O, arithmetic and relational operations, and built-in mathematical functions are defined for both dual numbers and dual metanumbers. As a result of polymorphism, the syntaxes of dual arithmetic and relational operations, and built-in dual functions are the same as those for real and complex numbers in the C^H programming language. The valid lvalues related to dual numbers in C^H are defined. The computation of the motion screw for a rigid-body displacement is used as an example to illustrate the creation of user's dual functions. The efficacy of C^H programming with dual numbers is demonstrated by displacement analysis of an RCCC mechanism. For the first time, dual data is handled as a built-in data type in a general-purpose computer programming language. Programming with dual numbers in C^H is simpler than in any other computer programming language.     

Mechanical verification of strategies

This paper presents a method of representing planning domains in the Boyer-Moore logic so that we can prove mechanically whether a strategy solves a problem. Current approaches require explicit frame axioms and state constraints to be included as part of a domain specification and use a programming language for expressing strategies. These make it difficult to specify domains and verify plans efficiently. Our method avoids explicit frame axioms, since domains are specified by programming an interpreter for sequences of actions in the Boyer-Moore logic. Strategies are represented as planners, Lisp programs that take an initial state and other arguments as input and return a sequence of actions that, when executed in the given initial state, will bring about a goal state. Mechanical verification of a strategy is accomplished by proving that the corresponding planner solves all instances of the given problem. We illustrate our approach by verifying strategies in some variations of the blocks world.The work described here was supported in part by NSF Grant MIP-9017499.     

Neural and fuzzy methods in handwriting recognition

Handwriting recognition requires tools and techniques that recognize complex character patterns and represent imprecise, common-sense knowledge about the general appearance of characters, words and phrases. Neural networks and fuzzy logic are complementary tools for solving such problems. Neural networks, which are highly nonlinear and highly interconnected for processing imprecise information, can finely approximate complicated decision boundaries. Fuzzy set methods can represent degrees of truth or belonging. Fuzzy logic encodes imprecise knowledge and naturally maintains multiple hypotheses that result from the uncertainty and vagueness inherent in real problems. By combining the complementary strengths of neural and fuzzy approaches into a hybrid system, we can attain an increased recognition capability for solving handwriting recognition problems. This article describes the application of neural and fuzzy methods to three problems: recognition of handwritten words; recognition of numeric fields; and location of handwritten street numbers in address images