Design And Implementation Of Practical Constraint Logic .

Transcription

Design and Implementation ofPracticalConstraint Logic Programming SystemsSpiro MichaylovAugust 24, 1992CMU-CS-92-168School of Computer ScienceCarnegie Mellon University5000 Forbes AvenuePittsburgh, PA 15213-3891Submitted in partial fulfillment of the requirementsfor the degree of Doctor of Philosophy.c 1992by Spiro MichaylovThis research was sponsored partly by IBM through a graduate fellowship and a joint study agreement, and partly by the Avionics Laboratory, Wright Research and Development Center, AeronauticalSystems Division (AFSC), U. S. Air Force, Wright-Patterson AFB, OH 45433-6543 under ContractF33615-90-C-1465, ARPA Order No. 7597.The views and conclusions contained in this document are those of the author and should not beinterpreted as representing the official policies, either expressed or implied, of the U.S. Government.

Keywords: programming languages, declarative programming, logic programming, constraints, programming methodology, efficient implementation

AbstractThe Constraint Logic Programming (CLP) scheme, developed by Jaffar and Lassez,defines a class of rule–based constraint programming languages. These generalize traditional logic programming languages (like Prolog) by replacing the basic operationalstep, unification, with constraint solving. While CLP languages have a tremendousadvantage in terms of expressive power, they must be shown to be amenable to practical implementations. This thesis describes a systematic approach to the design andimplementation of practical CLP systems. The approach is evaluated with respect totwo major objectives. First, the Prolog subset of the languages must be executed withessentially the efficiency of an equivalent Prolog system. Second, the cost of constraintsolving must be commensurate with the complexity of the constraints arising.The language CLP(R), whose domain is uninterpreted functors over real numbers,is the central case study. First, the design of CLP(R) is discussed in relation to programming methodology. The discussion of implementation begins with an interpreterthat achieves the efficiency of equivalent Prolog interpreters, and meets many of thebasic efficiency requirements for constraint solving. Many of the principles applied inthe interpreter are then used to develop an abstract machine for CLP(R), leading to acompiler-based system achieving performance comparable to modern Prolog compilers.Furthermore, it is shown how this technology can be extended so that the efficiencyof CLP(R) approaches that of imperative programming languages. Finally, to demonstrate the wider applicability of the techniques developed, it is shown how they canbe used to design and implement a version of Elf, a language with equality constraintsover λ-expressions with dependent types.iii

ContentsIBackground11 Introduction22 Constraints and Logic Programming2.1 Logic Programming and Prolog . . . . . . . . . . . . . . . . .2.1.1 The Prolog Operational Model . . . . . . . . . . . . .2.1.2 Implementation Techniques . . . . . . . . . . . . . . .2.1.3 Programming Methodology and Practical Experience .2.2 Constraints and Constraint Programming . . . . . . . . . . .2.2.1 Constraint Solving . . . . . . . . . . . . . . . . . . . .2.2.2 Classification of Constraint Languages . . . . . . . . .2.2.3 Review of Systems . . . . . . . . . . . . . . . . . . . .2.3 Constraint Logic Programming . . . . . . . . . . . . . . . . .2.3.1 Examples . . . . . . . . . . . . . . . . . . . . . . . . .2.3.2 Review of Languages and Systems . . . . . . . . . . .2.3.3 Applications . . . . . . . . . . . . . . . . . . . . . . .II.Languages and Programming77711121213151618191925263 Language Design3.1 CLP Operational Model . . . . . . . . . . . . .3.2 Complications Related to Deciding Constraints3.3 Effect on Language Design . . . . . . . . . . . .3.3.1 Syntactic Restrictions . . . . . . . . . .3.3.2 Dynamic Restrictions . . . . . . . . . .3.4 Looking Ahead . . . . . . . . . . . . . . . . . .4 CLP(R)4.1 The Language and Operational Model4.1.1 The Structure R . . . . . . . .4.1.2 CLP(R) Constraints . . . . . .4.1.3 CLP(R) Programs . . . . . . .4.1.4 The Operational Model . . . .iv.27272930313135.36. . . . . 36. . . . . 36. . . . . 37. . . . . 37. . . . . 39

4.24.34.44.5Basic Programming Techniques . . . . .Major Examples: Electrical Engineering4.3.1 Analysis and Synthesis of Analog4.3.2 Digital Signal Flow . . . . . . . .4.3.3 Electro-Magnetic Field AnalysisSurvey of Other Applications . . . . . .Empirics . . . . . . . . . . . . . . . . . .5 λProlog and Elf5.1 The Domain . . . . . . . . . . . . .5.2 The Languages . . . . . . . . . . .5.3 Higher-Order Abstract Syntax . .5.4 Manipulating Proofs . . . . . . . .5.5 Programming Methodology . . . .5.6 Empirical Study . . . . . . . . . .5.6.1 Properties of Programs . .5.6.2 The Measurements . . . . .5.6.3 The Programs and ResultsIII. . . . . . . . .Circuits. . . . . . . . . . . . . . . . .43474757596162.70707276818284848687Implementation Techniques946 Implementation Strategy956.1 Run-Time Strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 966.2 Compile-Time Strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . 976.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 997 Organization of Solvers7.1 Adding Delay to The Implementation Model7.2 Multiple Constraint Solvers . . . . . . . . . .7.3 Interpreting CLP(R) . . . . . . . . . . . . . .7.3.1 Unification . . . . . . . . . . . . . . .7.3.2 The Interface . . . . . . . . . . . . . .7.3.3 Linear Equations and Inequalities . .7.3.4 Some Examples of Constraint Flow . .7.4 Summary . . . . . . . . . . . . . . . . . . . .1001001021041051101101131148 Managing Hard Constraints8.1 Delay Mechanisms . . . . . . . . . . . . . . .8.2 Wakeup Systems . . . . . . . . . . . . . . . .8.3 Structural Requirements of a Wakeup System8.4 Example Wakeup Systems . . . . . . . . . . .8.5 The Runtime Structure . . . . . . . . . . . .8.5.1 Delaying a new hard constraint . . . .8.5.2 Responding to Changes in Σ . . . . .115116116119121122125126v

8.5.38.5.4Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126Summary of the Access Structure . . . . . . . . . . . . . . . . . . 1279 Incremental Constraint Solvers9.1 Practical Implications of Incrementality . .9.2 Incrementality and Prolog . . . . . . . . . .9.3 Strategy for Incremental Solvers . . . . . .9.4 Incrementality in Four Modules of CLP(R)9.4.1 Unification . . . . . . . . . . . . . .9.4.2 Linear Equations . . . . . . . . . . .9.4.3 Linear Inequalities . . . . . . . . . .9.4.4 The Delay Pool . . . . . . . . . . . .9.5 Summary . . . . . . . . . . . . . . . . . . .12912913113213313313313613613810 Compilation10.1 Prolog Compilation and the WAM . . . . . . .10.2 The Core CLAM . . . . . . . . . . . . . . . . .10.2.1 Instructions for Arithmetic Constraints10.2.2 Runtime Issues . . . . . . . . . . . . . .10.3 Basic Code Generation . . . . . . . . . . . . . .10.4 Global Optimization of CLP(R) . . . . . . . .10.4.1 Modes and Types . . . . . . . . . . . . .10.4.2 Redundancy . . . . . . . . . . . . . . . .10.5 The Extended CLAM . . . . . . . . . . . . . .10.6 Summary of Main CLAM Instructions . . . . .10.7 Empirics . . . . . . . . . . . . . . . . . . . . . .10.8 Extended Examples . . . . . . . . . . . . . . .13914014214214414615215215215415715715911 Efficient Implementation of Elf11.1 Higher-Order Unification . . . .11.2 Hard Constraints . . . . . . . .11.3 Easy Cases of Constraints . . .11.4 Other Implementation Issues .168168170172175IV.Conclusions.17712 Conclusions178A Electrical Engineering Programs180A.1 Circuit Solver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180A.2 Transistor Circuit Analysis and Design . . . . . . . . . . . . . . . . . . . 183A.3 Signal Flow Graph Simulation . . . . . . . . . . . . . . . . . . . . . . . . 190vi

B Natural Semantics ProgramsB.1 Expressions of Mini-ML . . . . . . . . .B.2 Natural Operational Semantics . . . . .B.3 The Value Property and Evaluation . .B.3.1 The Value Property . . . . . . .B.3.2 Transformation of Evaluations tovii. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Value Deductions .194194195196196197

List of Figures1.1Requirements of a Programming Language . . . . . . . . . . . . . . . . .32.1Simple Prolog example . . . . . . . . . . . . . . . . . . . . . . . . . . . .154.164.17Successful derivation sequence for ohm query . . . . . . .SEND MORE MONEY . . . . . . . . . . . . . . .Piecewise linear diode model . . . . . . . . . . . . . . .Resistive circuit with diode . . . . . . . . . . . . . . . .Use of the general package to solve a DC circuit . . . . .RLC Circuit . . . . . . . . . . . . . . . . . . . . . . . . .DC model of NPN transistor . . . . . . . . . . . . . . .An NPN type transistor . . . . . . . . . . . . . . . . . .Biasing Circuit for NPN transistor . . . . . . . . . . . .High frequency filter . . . . . . . . . . . . . . . . . . . .Input and output for filter . . . . . . . . . . . . . . . . .Liebmann’s 5-point approximation to Laplace’s equationSolving Laplace’s equation . . . . . . . . . . . . . . . . .Small Programs: Resolution and Unification . . . . . . .Small Programs: Arithmetic . . . . . . . . . . . . . . . .Large Programs: Resolution and Unification . . . . . . .Large Programs: Arithmetic . . . . . . . . . . . . . . . .5.15.25.35.45.5Elf program to convert propositional formula toSummary of Elf syntax . . . . . . . . . . . . . .Basic Computation . . . . . . . . . . . . . . . .Proof Manipulation . . . . . . . . . . . . . . . .Mini-ML comparison . . . . . . . . . . . . . . .4146484951525454555858596067686869negation normal form. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .73758889906.1Basic Implementation Model . . . . . . . . . . . . . . . . . . . . . . . .967.17.27.37.4Generic Implementation Model with Delay .Delay/Wakeup Mechanism . . . . . . . . . .CLP(R) Solver Organization . . . . . . . .Unification Table for CLP(R) Interpreter .viii.101101106107

8.18.28.38.48.58.68.7Wakeup degrees for pow/3 . . . . . . .Wakeup degrees for mult/3 . . . . . .Wakeup degrees for array/4 . . . . . .Wakeup degrees for conc/3 . . . . . .Wakeup degrees for clos/2, conc/3 andThe access structure . . . . . . . . . .The new access structure . . . . . . . . . . . . . . .or/3. . . . . . . . . . . . . . . . . . . . . . . . . . . . .in CLP(Σ ). . . . . . . . . . . . .1211221231231241261279.19.29.3Solver state after two equations . . . . . . . . . . . . . . . . . . . . . . . 135Solver state after choice point and third equation . . . . . . . . . . . . . 135Delay stack and access structure . . . . . . . . . . . . . . . . . . . . . . 13710.1 Unification Table for CLAM Execution . . . . . . . . . . . . . .10.2 Summary of Main CLAM Instructions . . . . . . . . . . . . . .10.3 Prolog benchmarks . . . . . . . . . . . . . . . . . . . . . . . . .10.4 Program for reasoning about mortgage repayments . . . . . . .10.5 Four queries for the mortgage program . . . . . . . . . . . . . .10.6 C function for Q1 . . . . . . . . . . . . . . . . . . . . . . . . . .10.7 C function for Q2 . . . . . . . . . . . . . . . . . . . . . . . . . .10.8 Timings for Mortgage program . . . . . . . . . . . . . . . . . .10.9 High-level pseudocode: mortgage specialized for Q1 . . . . . . .10.10High-level pseudocode: mortgage specialized for Q2 . . . . . . .10.11High-level pseudocode: mortgage specialized for Q3 . . . . . . .10.12High-level pseudocode: mortgage specialized for Q4 . . . . . . .10.13Core CLAM code for general mortgage program . . . . . . . . .10.14Extended CLAM code for mortgage program, specialized for Q110.15Extended CLAM code for mortgage program, specialized for Q210.16Extended CLAM code for mortgage program, specialized for Q310.17Extended CLAM code for mortgage program, specialized for 616711.111.211.311.411.5.170171173174174Comparison of solutions in Huet’s and Miller’s algorithmsCore unification table for Elf . . . . . . . . . . . . . . . .Wakeup system for Elf . . . . . . . . . . . . . . . . . . . .Conventional term representation for Elf . . . . . . . . . .Functor/Arguments term representation for Elf . . . . . .ix. pag

Constraint Logic Programming Systems Spiro Michaylov August 24, 1992 CMU-CS-92-168 School of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213-3891 Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy. c 1992 by Spiro Michaylov This research was sponsored partly by IBM through a graduate fellowship and a joint