WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:     | 1 |   ...   | 12 | 13 || 15 | 16 |   ...   | 22 |

«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»

-- [ Page 14 ] --

7.3.1 Assertions in the modal substructural logic An assertion in the modal substructural logic is just a predicate. Accordingly one defines it by giving a function from world to Prop. We say that a world w forces a predicate P, written

–  –  –

Since our assertions are just functions from world to Prop, we have what is called a shallow embedding of our modal substructural logic in Coq. This would not be the case if we defined our own proposition language (calling it, e.g., nuProp) and used it instead of Coq’s Prop.

The shallow embedding significantly simplifies the process of creating the machine-checked proofs. We are able to use tactics developed for Prop with our predicates; for example, we can use the destruct tactic to break apart the conjunction in our modal logic. Also, we are able to use Coq’s native variable-binding mechanisms, thereby avoiding the binder issues raised in the POPLmark quagmire [ABF+ 05].

Almost all of our assertions are public in the sense that the remainder of the proof can see and use the definitions to reason about the underlying model. One exception is the definition of higher-order recursion operator µHO, which is opaque; the rest of the proof is given fold-unfold rules to reason about that operator as explained in section 7.3.9.

In the rest of this chapter we will give a selection of operators in our logic, explain their use, and provide their models.

7.3.2 Logical operators In figure 7.5 we give some basic logical operators and their models.

–  –  –

that we avoid variable capture.

[·]Coq useful because it ensures that the entire expressive power of Coq is available in the logic. The simplest use of [·]Coq is to define the predicates true and false8. We will see a more powerful use of [·]Coq when we define the precisely operator in section 7.3.8.

One of the advantages of our approach is that it is easy to define new operators in terms of old ones; we have done this in the definitions of true and false. Although both are predicates—that is, functions from world to Prop—their definition does not contain a λ; instead they utilize the λ in [·]Coq.

To avoid “symbol explosion” in the presentation, we overload many symbols to operate both at the Prop and predicate levels. Since the two have different types in Coq, only one will be possible in any given context.

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

 Conjunction ∧ and disjunction ∨ are defined by lifting the operations defined on Prop. We also lift the universal and existential quantifiers ∀ and ∃. Since we use the quantifiers at the Prop level in the definitions of universal and existential quantification in our logic, we have full impredicative quantification: v can thus range over values, predicates, worlds, shares, and any other types definable in Coq.

We define the operator exactly so that we can precisely specify the resource map if we wish; exactly is not particularly useful in the CSL correctness proofs of programs, but is used in both the soundness proofs and in defining the concurrent operational semantics in chapter 8.

7.3.3 Modal operators In figure 7.6 we give some modal operators and their models9. Recall that a world is a tuple of locals ρ, resource map φ, and memory m. The modal operators enable us to reason cleanly and orthogonally about these elements.

The simplest modal operator is close, which is used to remove the effect of the locals ρ on a predicate’s behavior by universally quantifying over them. Thus, for any predicate P, close P ignores the locals ρ. If P already ignores ρ, then close P = P and we say that P is closed.

–  –  –

fashionably P, written P. In previous work [AMRV07] approximately was called later, and for this reason the Coq development refers to this operator as later. Each quantifies over the resource map φ in a different way. Unlike with the locals ρ, we cannot simply use universal quantification over all possible φ, since the underlying model does not allow a stratified resource map φn to say anything meaningful about stratified resource maps φn+m+1 of higher stratification.

While a stratified resource map φn cannot say anything meaningful about resource maps of higher stratification, it can describe properties of resource maps of lesser stratification φn−m−1. This was the underlying

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

 idea behind the approximation operator agen defined in section 7.2.4.

The ⊲ P operator models the central idea of that section as a modal operator. If (ρ, φ, m) |= ⊲ P, then P may or may not hold on (ρ, φ, m), but will hold on all φ′ strictly more approximate than φ: (ρ, φ′, m) |= P.

Since all that is required for close P = P is that P not depend on local variables, it is natural to wonder which P have the property that ⊲ P = P. Due to the irreflexivity of age (n + 1), ⊲ P = P is a very strong requirement; in fact

–  –  –

This makes sense, since the most approximate predicate—that is, the one that gives the least information—is true. The essentially irreflexive nature of the ⊲ operator was a key technical insight of the modal model of Appel et al. [AMRV07], and we will see its expressive power when we see how to invert YES in section 7.3.10.





In the modal logic, ⊲ serves two purposes. The first is to give a compact characterization of approximation, which it does very well.

The second is somewhat different; it is to restrict the “wildness” of terms in the underlying stratified model. There is a natural idea that if w |= P, and if w ′ is a more approximate version of w, then w ′ |= P.

In informal terms, if w is “good enough” to guarantee P, then if w

7.3. REASONING ABOUT THE MODEL WITH A MODAL

SUBSTRUCTURAL LOGIC  becomes a little more approximate, it should be even easier for it to guarantee P. Reformulated in the modal logic, we would very much like our P to have the property that

–  –  –

This will be true as long as φ has level greater than 5, but false as φ nears level 0.

The modal operator necessarily P, written P, forces predicates to be necessary. In figure 7.6 we give two equivalent defintions for P.

–  –  –

The second definition of in figure 7.6 shows that it is very similar to a reflexive version of ⊲, and leads naturally to the proof that for all P,

–  –  –

is not particularly restrictive; P is necessary as long as it does not try to expose the underlying stratified construction. In fact, almost all of the operators presented here are necessary automatically, or become necessary when applied to necessary predicates. Therefore, as long as we build our CSL proofs using the operators presented here, we can ignore the existence of unnecessary predicates. One major exception is that implication is not automatically necessary even when applied to necessary predicates; this is discussed in section 7.3.7.

The modal operator fashionably P, written P, quantifies over the φ in the world in a different way. While ⊲ P and P were primarily concerned with reasoning about the underlying stratified construction, P is used to force P to ignore φ, similar to the way that close P is used to force P to ignore ρ.

Unlike in close P, where we quantify over all possible ρ, in P we cannot quantify over all possible φ, since resource maps of level n are not able to say anything meaningful about resource maps of level n+ m+ 1.

7.3. REASONING ABOUT THE MODEL WITH A MODAL

SUBSTRUCTURAL LOGIC  Accordingly, we quantify over all resource maps of the same level; this is the strongest meaningful quantification possible. Put another way, P is only allowed to utilize one fact about the resource map φ, which is its level. If we want to quantify over all resource maps at this level of

–  –  –

We use the modal operator everywhere P, written !P, to quantify over the memory m. The definitions of !P and close P are similar, since the memory m is similar to the locals ρ in the sense that neither has a particularly complicated structure that interferes with the model. If a predicate P ignores the memory, then

–  –  –

and we say that P is ubiquitous. Just as there are many closed predicates, there are many ubiquitous ones.

7.3.4 Substructural operators In figure 7.7 we give three basic substructural operators and their models. The assertion emp holds if the resource map φ only contains NO resources. Recall from section 7.2.6 that NO takes a resource map φ as a parameter and creates a resource stratified to the same level as φ, which it packages up into a dependent pair. Since a predicate is a function from world, we can use the resource map contained in the world.

–  –  –

Figure 7.7: Models of substructural assertions YES φ k π P at location l and NO elsewhere.

YES then creates a list of predicates stratified to level φ; we will take advantage of this in section 7.3.10 when we express what can be concluded from

–  –  –

The requirement that all other locations are NO is standard for separation logic; larger structures are built with the separating conjunction.

Since we have defined our join relations as a stratified separation algebra, we model the separating conjunction P ∗ Q in a way similar to Calcagno et al. [COY07]. When

–  –  –

Using the separating conjunction it is possible to describe complex substructural properties of the underlying model in an elegant way.

7.3.5 Reasoning in the modal substructural logic The motivation for defining the modal substructural logic is that we have found it much easier to reason about the model using the logic than to reason on the underlying model directly. The proofs of the soundness of CSL can become very complicated, and it is not unusual to have 50 or more premises leading to a goal. In that context, it is vital to be able to express properties concisely in order to reason about them with minimal mental overhead.

One advantage of using our logic is that we can prove a large number of lemmas describing how the logic behaves; a small subset of them are pictured in figure 7.8. Most of the lemmas take the form of equalities in the logic, which is quite convenient since we can use powerful rewrite tactics in Coq.

A very useful strategy we used while developing the soundness proof was to express the premises and goal of a lemma in the logic, and then use the kinds of rules given in figure 7.8 to prove the goal from the hypothesis. Sometimes it was not possible complete the proof entirely in the logic, in which case we had two choices: to define a new logic

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC



–  –  –

Figure 7.8: Rules for reasoning in the modal substructural logic

7.

3. REASONING ABOUT THE MODEL WITH A MODAL

SUBSTRUCTURAL LOGIC  operator to express the property and then continue to reason in the logic, or to dip briefly out of the logic and reason instead directly on the underlying model. The choice made depended on the difficulty of proving the underlying fact and a guess as to the amount of use the new operator would have. Dockins et al. [DAH08] discuss this in more detail.

To give an example of reasoning in the modal logic, we prove that

–  –  –

Of course, this can be proved directly on the underlying model, but the details and multiple quantifiers can quickly overwhelm an understanding of what is going on, particularly in the context of a larger proof, leading to a considerably longer and more frusterating proving experience.

7.3. REASONING ABOUT THE MODEL WITH A MODAL

SUBSTRUCTURAL LOGIC  7.3.6 Modelling the assertions of Concurrent

–  –  –

is kLK. The share π is projected into the right half of the full share in the style of the isomorphism noted by Parkinson [Par05]. In our share models there is an isomorphism between any two nonempty shares, and project uses that isomorphism to squeeze π into ◭⊲. For example,

–  –  –

Finally, we put the lock invariant R into the predicate list.

The hold l R assertion is defined quite similarly to the lock assertion,

CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC



–  –  –

resource map contains a YES at location f whose kind is kFUN. The share is ◭◮, and the predicate list contains the pre- and postconditions P and Q.

7.3.7 Logical Implication Almost all of our operators are suitable for use in a CSL proof about programs. However, there are a few operators that we do recommend avoiding in that context, particularly full logical implication, which

7.3. REASONING ABOUT THE MODEL WITH A MODAL

SUBSTRUCTURAL LOGIC  interacts complexly with the underlying stratified model, and which was conspicuously missing from the basic logical operators defined in figure 7.5. We define four related implication operators in figure 7.10;

the first two are dangerous in the sense that if not used carefully they will expose wild predicates in the underlying model.

Of course nothing prevents the use of the dangerous forms of implication; since the system is semantic instead of syntactic, an end-user can utilize any operator he wishes. However, full implication can be more difficult to use than expected, and so we recommend that CSL proofs avoid it. Full implication is largely used in the soundness proofs of the model itself, indicating that it can be useful in carefully controlled situations. For most situations, however, we reccomend the use of the safer, more restricted forms of implication given in the second part of figure 7.10.



Pages:     | 1 |   ...   | 12 | 13 || 15 | 16 |   ...   | 22 |


Similar works:

«An Iterative Approach to Examining the Effectiveness of Data Sanitization By ANHAD PREET SINGH B.Tech. (Punjabi University) 2007 M.S. (University of California, Davis) 2012 DISSERTATION Submitted in partial satisfaction of the requirements for the degree of DOCTOR OF PHILOSOPHY in COMPUTER SCIENCE in the OFFICE OF GRADUATE STUDIES of the UNIVERSITY OF CALIFORNIA DAVIS Approved: Matthew Bishop (Co-Chair) Sean Peisert (Co-Chair) Raquel Loran Hill Committee in Charge [2015] i c Anhad Preet Singh,...»

«The Diverse Geographies of Jewishness: Exploring the Intersections between Race, Religion, and Citizenship among Israeli Migrants in Toronto by Tamir Arviv A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Department of Geography and Planning University of Toronto © Copyright by Tamir Arviv 2016 ii The Diverse Geographies of Jewishness: Exploring the Intersections between Race, Religion, and Citizenship among Israeli Migrants in Toronto Tamir Arviv...»

«NORTHWESTERN UNIVERSITY Toward Rotational Cooling of Trapped SiO+ by Optical Pumping A DISSERTATION SUBMITTED TO THE GRADUATE SCHOOL IN PARTIAL FULFILLMENT OF THE REQUIREMENTS for the degree DOCTOR OF PHILOSOPHY Field of Physics and Astronomy By David Tabor EVANSTON, ILLINOIS June 2014 UMI Number: 3627205 All rights reserved INFORMATION TO ALL USERS The quality of this reproduction is dependent upon the quality of the copy submitted. In the unlikely event that the author did not send a complete...»

«EVOLVING THE REAL-TIME GRAPHICS PIPELINE FOR MICROPOLYGON RENDERING A DISSERTATION SUBMITTED TO THE DEPARTMENT OF COMPUTER SCIENCE AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Kayvon Fatahalian December 2010 © 2011 by Kayvon Fatahalian. All Rights Reserved. Re-distributed by Stanford University under license with the author. This work is licensed under a Creative Commons AttributionNoncommercial...»

«Introduction: Thomas Mann and Gnosticism in the Cultural Matrix of His Time Kirsten J. Grimstad The last decades of the twentieth century witnessed a far-reaching revival of interest in the ancient and radical philosophy of religion known as Gnosticism. In 1945 a cache of original Gnostic texts buried in the desert at Nag Hammadi in Upper Egypt around 400 C.E. came to light by accident when a camel-driver struck upon a large clay jar while digging for fertilizer. The jar contained papyrus...»

«Chapter Two Man and Superman Shaw’s Non-Dramatic Writings haw was a failed novelist, and a successful journalist and critic before he became a playwright. His criticism for newspapers, although interesting and voluminous, frequently deals with subjects that are not relevant to the central issue of his relations to contemporary philosophical ideas. His three extended attempts at criticism, The Quintessence of Ibsenism, The Perfect Wagnerite, and The Sanity of Art, are of more immediate...»

«UNIVERSITY OF NAIROBI DEPARTMENT OF LINGUISTICS AND LANGUAGES CURRICULUM VITAE PERSONAL DETAILS NAME: Dr. Isaiah Ndung'u Mwaniki SI (Kenyatta College), DIP Ed, Certificate in Language in Education U.K, MED University of Exeter (UK), PHD University of Nairobi. MOBILE PHONE NO: +254729 506 888/ +254720565271 E-MAIL: drmwanikindung'u45@yahoo.com drmwaniki@uonbi.ac.ke DATE OF BIRTH: 9th September, 1946 PLACE OF BIRTH: Tetu Location, Nyeri District MARITAL STATUS: Married with Four Children...»

«PATTERNING OF CONJUGATED POLYMERS FOR ELECTROCHROMIC DEVICES By AVNI ANIL ARGUN A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA Copyright 2004 by Avni A. Argun To Evrim ACKNOWLEDGMENTS As I look back upon the years that have led to this dissertation, I have been fortunate to have been surrounded by the help and influence of numerous exceptional people. First, I...»

«Why assertion and practical reasoning are possibly not governed by the same epistemic norm Robin McKenna University of Geneva rbnmckenna@gmail.com Penultimate draft. Final version forthcoming in Logos & Episteme. Abstract This paper focuses on Martin Montminy’s recent attempt to show that assertion and practical reasoning are necessarily governed by the same epistemic norm (“Why assertion and practical reasoning must be governed by the same epistemic norm”, Pacific Philosophical Quarterly...»

«Stony Brook University The official electronic file of this thesis or dissertation is maintained by the University Libraries on behalf of The Graduate School at Stony Brook University. © Allll Riightts Reserved by Autthor. © A R gh s Reserved by Au hor Translating Contemporary Japanese Culture: Novels and Animation A Dissertation Presented by Tadahiko Haga to The Graduate School in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy in Comparative Literature Stony...»

«EFFICIENTLY ACQUIRING REFLECTANCE FIELDS USING PATTERNED ILLUMINATION A DISSERTATION SUBMITTED TO THE DEPARTMENT OF ELECTRICAL ENGINEERING AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Gaurav Garg September 2006 ii c Copyright by Gaurav Garg 2006 All Rights Reserved iii iv I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a...»

«ALUMINUM NITRIDE-ON-SILICON TEMPERATURE-STABLE RESONATORS AND FILTERS FOR TIMING APPLICATIONS by Vikram Atul Thakar A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Mechanical Engineering) in The University of Michigan 2014 Doctoral Committee: Assistant Professor Mina Rais-Zadeh, Chair Professor Yogesh Gianchandani Professor Karl Grosh Professor Khalil Najafi © Vikram Thakar All rights reserved 2014 DEDICATION To Friends and Family ii...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

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.