WWW.THESIS.DISLIB.INFO
FREE ELECTRONIC LIBRARY - Online materials, documents
 
<< HOME
CONTACTS



Pages:   || 2 |

«Abstract. A method ~sg~ven for dec~dlng formulas in combinations of unquantified first-order theories. Rather than couphng separate decision ...»

-- [ Page 1 ] --

Deciding Combinations of Theories

ROBERT E. SHOSTAK

SRI International, Menlo Park, Cahforma

Abstract. A method ~sg~ven for dec~dlng formulas in combinations of unquantified first-order theories.

Rather than couphng separate decision procedures for the contributing theories, the method makes use

of a single, uniform procedure that minimizes the code needed to accommodate each additional theory.

It ~s apphcable to theories whose semantics can be encoded within a certain class of purely equational canonical form theories that ~s closed under combination. Examples are given from the equational theories of integer and real anthmeUc, a subtheory of monadic set theory, the theory of cons, car, and cdr, and others. A discussion of the speed performance of the procedure and a proof of the theorem that underhes ~ts completeness are also g~ven.The procedure has been used extensivelyas the deductive core of a system for program specificaUonand verifcation.

Categories and Subject Descriptors- D.2.4 [Software Engineering]: Program Verificationmcorrectness proofs; verification; F 3 1 [Logics and Meanings of Programs]' Specifyingand Verifyingand Reasoning about Programs--mechamcal verification; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Loglcmmechamcal theorem proving General Terms: Algonthms, Verification AddlUonal Key Words and Phrases: Decision procedures

1. Introduction M u c h attention has been given in the last few years to the problem o f developing decision procedures for applications in program verification and mechanical p r o o f o f theorems in mathematics. It often happens, in these applications, that the formulas to be proved involve diverse semantic constructs. Verification conditions for programs, for example, often mix arithmetic with data structure semantics.

Accordingly, a n u m b e r o f procedures have been developed (such as those o f Jefferson [2] and the author [7]) for particular m i x e s o f theories. One o f the m o s t general results along these lines is given by Nelson and O p p e n [4] in their work on simplification using cooperating decision procedures. Th¢~ central idea, here, is that procedures for diverse unquantified theories in a certain class can be hooked together so as collectively to decide a formula involving constructs f r o m each. T h e coupled procedures c o m m u n i c a t e by passing back and forth information they individually derive a b o u t equality a m o n g terms.

The m e t h o d described in this paper also addresses the p r o b l e m o f deciding c o m b i n a t i o n s o f theories. Rather than connecting separate procedures for the constituent theories, however, it is based on a single, u n i f o r m procedure that This research was supported m part by the National Science Foundation under Grant No. MCS 79and by the Air Force Office of Scientific Research under Contract No. F49620-79-C-0099.

Author's addless" Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025 Permission to~..o~y without fee all or part of th~s material ~s granted provided that the copies are not made or distributed for d~rect commercial advantage, the ACM copyright notice and the title of the pubhcation and its date appear, and notice is given that copying is by permission of the AssoclaUon for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

© 1984 ACM 0004-5411/84/0100-0001 $00.75 Journal of the Asu~ctaUonfor ComputingMachinery,Vo| 31, No 1,January 1984,pp 1-12 2 ROBERT E. SHOSTAK localizes the mechanism particular to each constituent to a relatively small amount of code. As a result, new semantic constructs can be incorporated quite easily. The method also obviates the explicit computation of entailed equality information required by the distributed approach, and the redundant representation of this information in the separate procedures.

The method is applicable to theories whose semantics can be expressed inside a certain class of purely equational canonical form theories. The class has the property that the canonizing functions of arbitrary members can be combined to obtain a canonizing function for their union. The decision procedure extends the congruence closure methods [1, 5, 6] that have been used for the pure theory of equality. The extension depends upon a notion of semantic signature that generalizes the earlier concept of signature to accommodate the semantics of the canonical form theories.

The method is useful for a surprisingly rich class of constructs. We give examples from integer and real arithmetic, the theory ofrecursive data structures, a subtheory of monadic set theory, and the first-order theory of equality. The procedure has been used intensively in a major verification effort [8] over the course of several months, and has been found to give good speed performance.

The next two sections characterize the class of theories to which the method is applicable, and prove that it is closed under combination. Section 4 gives the decision procedure and exemplifies its operation. Sections 5 and 6 discuss performance issues and an extension of the method that treats nonconvex theories. The last section gives a proof of the theorem on which the procedure is based.

2. o-Theories a n d Algebraic Solvability The procedure described in this paper operates over a subclass of certain unquantiffed first-order equational theories called o-theories. Such theories have both interpreted and uninterpreted function symbols. Terms whose outermost function symbol is interpreted are themselves said to be interpreted, and all other terms (including variables) are said to be uninterpreted. The distinguishing feature of otheories is that each has an effective canonizer, i.e., a computable function o from terms to terms such that a purely interpreted (i.e., containing no uninterpreted function symbols) equation t = u is valid in the theory iff o(t) --- o(u). The canonizer o must act as an identity on uninterpreted terms, must be idempotent (i.e., o(o(t)) = o(t)), and must have the property that the arguments of each interpreted canonical term must themselves be canonical.





The semantics of o-theories are defined with respect to o-interpretations, i.e., Herbrand interpretations that respect o in the sense that for each interpreted term t = f(t~...., tn), v(t) = o(f(v(tO..... v(tn))), where v(t) is the value of t in the interpretation. Note that these semantics say more than that two terms must be equal in all interpretations if they have identical canonical forms; they also say that certain terms (for example, distinct canonical constants) must be unequal in all interpretations.

A simple example of a o-theory is the equational theory of addition and multiplication by constants over the reals. Each term in this theory can, of course, be reduced to a linear expression of the form a~x~ + a2x2 +... + a,,x, + c (n _0), where each a, is a nonzero real constant, each x, is a variable, and c is a real constant. By specifying some criterion for ordering the xi's (alphabetic ordering, for example), removing unity coefficients, and discarding c if c -- 0, a suitable o can be defined. Note that the theory can trivially be enriched with uninterpreted function symbols.

Deciding Combinations o f Theortes 3 The decision procedure we will describe operates on a-theories with a s~eial property we call algebraic solvabihty Such theories have a solverma computable function that takes a purely interpreted equation (no uninterpreted symbols other than variables) e(say t = u) as input, and returns either true, false, or a conjunction of equations. The returned formula must be equivalent to e and must be either true or false if e has no variables. Moreover, the equations (if any) in the returned formula must all be of the form x, = t,, where the x,'s are distinct variables of t (or u if t has none) that do not occur in any of the t,'s.

Returning to the example of real linear arithmetic, a suitable solver is trivially provided by conventional algebraic manipulation; solving 3x + 2y -- 2x + 4, for example, gives x = - 2 y + 4.

At first glance, one might expect that algebraic solvability is such a strong criterion that there are no nontrivial theories other than, say, theories over fields, that satisfy it. Surprisingly, this is not so. As the following examples suggest, algebraic solvability is characteristic of many constructs one encounters in practice.

Example 1. The convex theory o f cons, car, and cdr.

First consider the theory

of cons, car, and cdr with the following axiomitization:

car(cons(x, y)) -- x, cdr(cons(x, y)) = y, cons(car(x), cdr(x)) -- x.

Using the first two of these axioms as rewrite rules, one can always reduce a term in the theory to a canonical form in which cons is not an argument of either car or cdr.

A solve function for this theory is given by the algorithm shown in Figure 1.

Note that the algorithm introduces new (existentially quantified) variables. The chief function of the main routine solve is to grind the left side of the given equation (represented as an ordered pair) down to a variable; the auxiliary function solvel (which takes two terms and returns a term) takes over from there, and attempts to eliminate that variable from the right side. The routine resolve, called by solve, sees to it that no equations in the returned conjunction have the same left side.

Consider, for example, the action of the algorithm on the equation cons(car(x), cdr(car( y))) = cdr(cons( y, x)).

The two sides are first canonized to obtain cons(car(x), cdr(car( y))) -- x.

This equation is then reduced to the two equations car(x) = car(x), cdr(car( y)) = cdr(x).

The first of these reduces to true and is, in effect, discarded. The second becomes car(y) = cons(a, cdr(x)), where a is a new variable, and then (recursing again) y = cons(cons(a, cdr(x)), d), which is then returned.

It is not difficult to show that the algorithm satisfies the criteria for a solver. The reader might find it amusing to prove that it always terminates.

4 ROBERT E. SHOSTAK

–  –  –

Similarly, A _CB becomes s~ + s5 -- (I,.

It is easy to see that terms in the encoding theory can be canonized simply by ordering the set variables in some way and eliminating redundancies.

A solver for the encoding theory is also easy to construct. One simply replaces each side of an equation with its a-form and cancels variables occurring on both sides. If the two sides thereby become identical, true is returned; otherwise, the conjunction A v, =,I,.

is returned, where the v,'s are the remaining variables. [] Example 4. The unquantified first-order theory of equality. This theory has no interpreted function symbols at all. a is therefore just the identity function. The solve function merely returns true if the given equation is an identity, and acts as an identity otherwise. [] Until now we have been concerned with solve functions for equations with only purely interpreted terms. In the next section and in the procedure itself it will be necessary to deal with equations that may have uninterpreted terms other than variables. The notion of solver is extended to deal with such equations in the following way.

We will say that a solver for a a-theory T is a computable function that takes an arbitrary equation e(say t --- u) over T as input and returns either true, false, or a conjunction of equations. The returned formula must be equivalent to e and must be one of true or false if e contains no uninterpreted terms. Moreover, the equations (if any) in the returned formula must all be of the form u, = t,, where the ui's are distinct uninterpreted subterms of t(or u if t has none) that do not occur in the t,'s except possibly as proper subterms of uninterpreted terms.

Note that all the solvers we have talked about so far can be trivially extended to satisfy the new definition simply by treating the maximally uninterpreted subterms of a submitted equation as if they were distinct variables. For example, the equation f(x) -- g(x + 2, f(x)) = O, when solved in linear arithmetic, produces f(x) = - l × g(x + 2,f(x)).

6 ROBERT E. SHOSTAK Note that although fix) occurs on the right-hand side of the result, it occurs only as a proper subterm of an uninterpreted term.

3. Combining Theories Algebraically solvable a-theories have the elegant and useful property that they can be combined (provided they are compatible in a certain sense) without giving up algebraic solvability.

One needs to be careful, of course, about what it means to combine theories.

Simply to say that the interpreted symbols of the combined theory are the union of those of the constituents does not suffice. The semantics of mixed terms (terms with symbols from different constituents) must be explicated, and conflicts that may arise when the constituents share interpreted symbols must be resolved.

The most natural resolution (and the one we espouse) of the issue of mixed terms is simply to assume that interpreted symbols from different theories have no semantic interaction in the combined theory; if a function interpreted in T~ but not in T2 is given an argument that is interpreted in T2 but not in TI, the effect is to treat the argument as if it were uninterpreted. For example, in the combination of real linear arithmetic with the theory of cons, car, and cdr, we will have a(car(cons(l + 1, nil)))= 1 + I.

We will consider that + is uninterpreted with respect to cons, car, and cdr, (and vice versa) in the combined theory, and that 1 + 1 is therefore an uninterpreted subterm of car(cons(l + 1, nil)).

It still remains to resolve the question of what happens if the constituent theories share interpreted symbols. Here we will take the conservative stand of requiring that the shared symbols have exactly the same semantics. More precisely, we will say that T~ and T2 are compatible if for each term t in their combination whose function symbol is interpreted in both, a~(t) = a2(t). We will consider only combinations of compatible theories.

Note that as a consequence of the view that uninterpretedness is relative, the purely interpreted terms of the combined theory are exactly the union of those from the constituent theories; the action of the combined a on each such term is the action of the a of the appropriate constituent. It is easy to check that the combined o thus defined satisfies the requirements for a canonizer.



Pages:   || 2 |


Similar works:

«2012 Mid-Continent transportation researCh ForuM September 6-7, 2012 Madison, Wisconsin Madison Concourse Hotel & Governor's Club 2012 Mid-continent transportation research ForuM F e at u r e d S p e a k e r S tereSa adamS Teresa Adams is a Professor of Transportation Engineering and City Planning in the Department of Civil and Environmental Engineering at the University of Wisconsin–Madison, and is Director and Principal Investigator of the National Center for Freight and Infrastructure...»

«TREDEGAR & DISTRICT CANINE SOCIETY Chairman: Mr. Clive Evans Vice Chairman: Mr. Trevor Jones Treasurer: Mrs. Lilian Evans Committee: Mrs. Cynthia. Crossley, Mr. Jon Crossley, Mrs. Linda David, Mrs. Jane Humphries, Mrs. Janet Saunders SCHEDULE OF UNBENCHED 73 CLASS MEMBERS LIMITED SHOW (Held under Kennel Club Rules & Show Regulation) Not judged on the Group System At TREDEGAR LEISURE CENTRE, STABLE LANE TREDEGAR, GWENT, NP22 4BH On SATURDAY 2nd APRIL 2016 Show Opens 9.30 a.m. Judging in both...»

«ChAPTER FoUR chargeS and PenalTieS I. the NatUre of charges A provisions of the Civil Service Reform Act, 5 USC 7513, requires “at least 30 days’ advance written notice, unless there is reasonable cause to believe the employee has committed a crime for which a sentence of imprisonment may be imposed, stating the specific reasons for the proposed action.” The statute also provides the right to appeal for individuals whose cases are within the jurisdiction of MSPB, and a determination by...»

«Revenue Operational Manual 12.01.02 [12.01.02] Income tax loss relief Restrictions to the amount of relief available Contents 1. Introduction 2. What relief is available for trading losses? 2.1. Current year trading losses (section 381) 2.2. Carry forward of unused trading losses (section 382) 2.3. Terminal loss relief (section 385) 3. How relief is given under section 381 4. Claiming relief under section 381 5. Restrictions on relief available under section 381 5.1. Land losses (section 381A)...»

«THIS DOCUMENT IS IMPORTANT AND REQUIRES YOUR IMMEDIATE ATTENTION. If you are in any doubt as to the action you should take, you are recommended to seek your own financial advice from your stockbroker, bank manager, solicitor, accountant or other independent financial adviser duly authorised under the Financial Services and Markets Act 2000, as amended, (“FSMA”) who specialises in advising on the acquisition of shares and other securities. This document, which has been drawn up in accordance...»

«In the Matter of the Tenure Hearing of Mark C. Bringhurst, School District of the City of Vineland, Cumberland County, Agency Dkt. No. 236-8/12 DECISION Before Robert C. Gifford, Esq. Arbitrator Appearances: For the Vineland Board of Education: Robert A. De Santo, Esq. Gruccio Pepper De Santo & Ruth For Mark C. Bringhurst: Robert J. Bowman, Esq. Schroll & Bowman Vineland City Board of Education [“Board” or “Petitioner”], pursuant to N.J.S.A. 18A:6-10 et. seq., certified tenure charges...»

«Minutes of the 2009 Spring Metropolitan Council Meeting Wednesday, Feb. 18 Friday, Feb. 20, 2009 East Norwich Inn, East Norwich, NY A. Agenda The 2009 Spring Session of the Metropolitan Council began with a retreat on the evening of Wednesday, February 18, 2009, lead by Metropolitan Jonah in Chancery's St. Sergius of Radonezh Chapel. In his talk, which was titled The Spiritual Process, His Beatitude said that the essence of the spiritual process is to overcome one's ego. The teaching of the...»

«WHAT CAN ELIZABETHAN PAMPHLETS AND BALLADS TELL US ABOUT ELIZABETHAN MILITARY CULTURE? DONG-HA SEO In the early part of the sixteenth century, print culture in England was dominated by the publication of religious texts. In 1588, however, after the defeat of the Spanish Armada, England saw a proliferation of both religious and secular print. Some of the secular pamphlets were war-oriented ballads and some newsbooks. This explosion of interest in contemporary war-oriented ballads and news...»

«Managerial Optimism and Earnings Smoothing Christa H.S. Bouwman* Case Western Reserve University and Wharton Financial Institutions Center August 2012 This paper empirically examines how CEO optimism affects earnings smoothing and earnings surprises. It is documented that optimistic managers smooth earnings more than rational managers and are associated with smaller (in absolute value) earnings surprises. A possible theoretical explanation is offered for these results based on a combination of...»

«Religion, State & Society, Vo!. 23, No. 3, 1995 Impressions of the Contemporary Russian Orthodox Church: Its Problems and Its Theological Education DIMITRY POSPIELOVSKY The Russian Orthodox Church has failed to find in itself the living force to lead Russian society morally or spiritually, as was hoped by both believers and nonbelievers when the collapse of the Soviet state had become obvious. The 1988 Millennial Council (Sobor) of the Church adopted a statute which is close in essence and...»

«Conference on Trends in the Management of Human Resources in Higher Education ANNOUNCEMENT AND PROGRAMME 25 and 26 August 2005 at the OECD Headquarters in Paris The Aim Higher education institutions, whether public or private, and regardless of national structures of finance and governance, are facing a number of challenges related to strategies for and management of human resources. HEI leaders, academics and other staff often find themselves in situations, where financial pressure,...»

«Colonel Frank CFS NEWS Seely School Issue : 34 June A Specialist College for Excellence in Mathematics & Computing 2011 ECO GREEN FLAG AWARD! CALVERTON SCHOOL GETS IT’S SECOND TOP ECO-SCHOOL AWARD Colonel Frank Seely School in Calverton received its second top environmental award – which is uncommon for secondary schools, especially in this region. The school was assessed on 1st July and has now been awarded the top Eco-Schools Green Flag Award for the second time in three years by the...»





 
<<  HOME   |    CONTACTS
2017 www.thesis.dislib.info - Online materials, documents

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.