FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:     | 1 |   ...   | 11 | 12 || 14 | 15 |   ...   | 22 |

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

-- [ Page 13 ] --

◦ We have used= to define resource and rmap, indicating that they are opaque to the rest of the proof. The rest of the Coq development does not know that the underlying model uses dependent types. When the rest of the soundness proof wishes to use resource and rmap, it must use the axioms exposed by the module, such as NO and YES as defined in section 7.2.6. Therefore the rest of the proof can be blissfully unaware of the stratification going on under the hood.

In contrast, we have used = to define world and predicate, indicating that those definitions are fully exposed to the rest of the proof.

7.2.3 Relating the models The definitions in the third section of figure 7.2 are used only under the hood. However, as we shall see in section 7.2.6 they are critical to defining some parts of the interface that the rest of the proof does use, such as the YES pseudoconstructor.

Within the model, often it is useful to know the amount of stratication in a given rmap. The function level allows just that, taking a rmap and returning the value of its first component.

Another thing the model must be able to do is take an external view of the model (i.e., a predicate) and translate it into the stratified construction (i.e., a predicaten ). A predicate in some sense is infinitely


 stratified; accordingly, it is important to be able to project a predicate down into the finitely stratified model.

This is the job of the stratify operator4. The stratify operator takes a natural n and a predicate P, and produces a predicaten Pn, which is P stratified to level n. It does this by using the recursion operator fix in the Calculus of Constructions to recursively define the nested structure of the stratified predicate.

As explained above, a stratified predicate at level 0 is has type unit;

the value tt has the unit type. A stratified predicate at level n + 1 is a pair of a stratified predicate at level n and a function from a pair of rmap at level n and mem to Prop. The first component of this pair is defined by the recursive call to the stratify operator. The second component is

more interesting, since it is the essential point of the stratification:

–  –  –

By the definition of predicaten, this must have type worldn−1 → Prop, and accordingly the parameter v has type worldn−1. Recall that worldn−1 = locals × rmapn−1 × mem. The result type must be Prop, which is simple enough to satisfy on its own (e.g., with true), but the goal is to build the stratified Pn from P.

Given that we have a stratified rmapn−1 as the second component of v, we can build an rmap with the dependent pair {n − 1, v.1}. By Appel et al. [AMRV07] write this operator as ⌊·⌋n, and is define it in a more mathematical style as definition 29.

7.2. A SUBSTRUCTURAL MODAL MODEL  projecting out the first and third components of v as well we are able to build a world, to which we can apply the predicate P.

Since P is being applied to a rmapn−1 of level n − 1, it will only be able to judge properties involving the rmap that are no more than n − 1 levels of stratification deep. As an example, consider the value

–  –  –

Simplifying the definition yields (tt, λv : (locals × rmap0 × mem). P (v.1, {0, v.2}, v.3)).

Unfolding the definition of rmap0 yields (tt, λv : (locals×(address → resource0 )×mem). P (v.1, {0, v.2}, v.3)).

A resource0 is either NO0 or YES0 (k, π, P0). However, predicate0 is equal to unit, so the list P0 is a list of elements of type unit. Of course, one unit is much like another; this means that stratify 1 P cannot distinguish two YES0 resources by examining their predicates.

The inability to fully distinguish YESn resources by examining their predicates has significant implications for inversion. Suppose we have two predicates P and Q, and we know that for a given k

–  –  –

What can we conclude? Certainly not P = Q, since perhaps at some greater level of stratification k ′ k the two predicates will differ. In fact, in the worst case k = 0, and we have the horrible-looking fact that

–  –  –

In other words, stratify k P = stratify k Q if and only if P and Q are equivalent for all rmaps with stratification level strictly less than k.

7.2.4 Characterizing Increasing Approximation The problem with (C1) is that it both exposes the inner workings of the stratified model by universally quantifying over φj and exposes the inner workings of the dependent model by explicitly constructing

–  –  –

Since the idea behind (C1) is that P and Q are equivalent for all rmaps with stratification level strictly less than k, it seems reasonable to characterize this property in a way that does not expose the underlying model.

In figure 7.3 we build the machinery to do just that. First we define three operators, age1 predicaten+1, age1 resourcen+1, and age1 rmapn+1 that remove one level of stratification from predicaten+1, resourcen+1, and rmapn+1, respectively, by “forgetting” some stratification. A point to note is that age1 predicaten+1, which causes the actual information loss, has a very simple definition due to the pair structure of predicaten.

All three of these operators are undefined on stratification level 0, and, since all of the operators expose the underlying stratification, we wish to completely hide them from the rest of the proof.

Now that we have defined aging on the stratified model, we extend it to the dependent model with the age1 operator, which simply unpacks the dependent pair and then uses the age1 rmapn+1 operator. Since we would like age1 to be defined for all rmaps, we have it return None if j = 0. Since age1 is actually removing structure, it is irreflexive, i.e.,

–  –  –

The age1 operator is opaque; the rest of the proof can see that it exists, but is only allowed to use it via axioms defined in the module type.

Finally, we define the age operator, which is just the nth composition

7.2. A SUBSTRUCTURAL MODAL MODEL  of age1. For all n 0, age is irreflexive5.

Now that we have defined age, we can use it to characterize the stratify operator by observing that

–  –  –

This is a much better characterization of stratify because it does not expose the stratified construction. However, it is not ideal, since it requires exposing the private level function. We will see a still more elegant way of expressing this property in section 7.3.

7.2.5 Stratified separation algebras for the model In section 4.4 we defined a stratified separation algebra by building on the ideas of Calcagno et al. [COY07]. In section 4.5 we explained that shares are such an algebra. Here we will show how to lift the separation algebra on share to resource, rmap, and world.

For comparison with previous work [AMRV07], the relation R(φ, φ′ ) = ∃n. (age (n + 1) φ = Some φ′ ) is irreflexive, transitive, and Noetherian, and moves between the worlds in the underlying Kripke model.


 Join relations for the stratified model We define the join relation ⊕n of resourcen as follows. Two YESn resources join YESn (k, Some π1, Pn ) ⊕n YESn (k, Some π2, Pn ) = YESn (k, Some π3, Pn )

–  –  –

In other words, for two YESn resources to join, they must be the same kind, have shares that join, and have identical predicate lists. NOn is the identity element for level n. Two resourcen at different levels never join.

–  –  –

As with resourcen, two rmapn at different levels do not join.

From the join relation on rmapn, we define the join relation on worldn by requiring the rmapn to join and all other members of the tuple to be In the presentation we “overload” the ⊕n and ⊕ symbols, using the same symbol for resource, rmap, etc.


–  –  –

Join relations for the dependent model

Once we have defined the join relation ⊕n on elements ξa ξb ξc :

resourcen, we can define the join relation ⊕ on resource by saying that

–  –  –

Finally, we can define the join relation on world by requiring the



rmaps to join and all other members of the tuple to be equal:

–  –  –

Stratified separation algebras When the join relation is defined in this way, resourcen, resource, rmapn, rmap, worldn, and world become stratified separation algebras as defined in section 4.4; proved in Coq7.

The join relations for resourcen, rmapn, and worldn and the proof that they form stratified separation algebras are completely hidden from the rest of the proof. However, the join relations for resource, rmap, and world and the fact that they form stratified separation algebras are exposed to the rest of the proof and are used to reason about the substructural elements in the model.

7.2.6 The public interface The rest of the CSL soundness proof should never see the internals of the stratification. Instead, the rest of the proof should treat the definitions of resource and rmap as opaque and handle elements of type resource and rmap by using a carefully designed interface.

In the actual Coq development, a special kind of function constructor, called a Joinmap, was used to lift the separation algebra properties from resource to rmap.

7.2. A SUBSTRUCTURAL MODAL MODEL  That interface consists of three parts. The first is a number of functions whose existence and type signature are exported to the rest of the proof but whose internals are hidden by the module type. The second is a series of helper definitions which are defined in terms of the opaque functions and are fully visible to the rest of the proof. We have already discussed the age1 and age operators, which were given in figure 7.3.

The first of these is an opaque definition; the second is a helper definition. The third part of the interface is a long series of axioms which show how the opaque functions behave. For example, one exported axiom involving age1 is

–  –  –

In other words, age1 is irreflexive.

Figure 7.4 gives some of the most important opaque functions, with the definitions of resource at and the pseudoconstructors NO and YES.

These have the types given in figure 6.3 and explained in section 6.2.2.

In that section we also explained how to build up the other pseudoconstructors such as LK from YES.

The join relation ⊕ was discussed in section 7.2.5. To reason about the join relation we export all of the axioms of a stratified separation algebra given in section 4.4, as well as property 8 from section 4.5.

The resource at function takes an rmap and an address and returns the resource associated with that address. As mentioned in section 6.2.2,



–  –  –

resource at is usually written infix using the @ symbol, a convention we will follow in this presentation as well.

The NO pseudoconstructor takes an rmap φ; out of this it extracts the level n and constructs the dependent pair {n, NOn }, which has type resource. The YES pseudoconstructor takes an rmap φ, a kind k, a pshare π, and a list of predicates P, extracts the level n from φ, maps the stratify function at level n over P to get Pn, and constructs the dependent pair {n, YESn (k, π, Pn )}, which also has type resource.

We are now in a position to understand the ramifications for inverting the YES pseudoconstructor, as promised in section 6.2.2. By examining the definitions and understanding the results of inverting the stratify function, it is clear that

–  –  –

if and only if level φ = level φ′, k = k ′, π = π ′, and the predicates in P and P ′ are equivalent up to stratification level φ.

Unfortunately this characterization of YES inversion exposes the underlying model. When we define our modal substructural logic it will be possible to express this property in a very elegant way (see section 7.3.10).

We also give the helper definitions ⊥ and same age. ⊥ is defined exactly as explained in section 4.3. The same age relation, which is defined in terms of the join relation, states that two resource maps are


 in the same equivalence class, as explained in section 4.4. There is a convenient connection between the public same age relation and the

private level function:

same age(φ, φ′)

–  –  –

We have now given an explanation of the underlying stratified separation algebra, and have explained how one can use dependent types to hide the stratification from the rest of the proof. However, even reasoning about the dependently typed model can be laborious.

The second major insight of the modal model of Appel et al. [AMRV07] was that one can define a modal logic for reasoning about the model.

Various operators in the modal logic will reason about different aspects of the model. The modal logic then becomes a clean interface to the opaque dependent model, which itself is a clean interface for the ugly details of the stratification.

In the Coq development we take this idea a step further [DAH08].

In general we have found that when we get to a point in the Coq development where the way forward is difficult or unclear, the solution


SUBSTRUCTURAL LOGIC  is to redefine the problem in terms of our modal substructural logic, frequently with the aid of a new operator. Since our logic has an underlying semantics, adding a new operator is quite easy. Reformulating a problem in the modal logic often allows the correct solution to become more apparent.

Pages:     | 1 |   ...   | 11 | 12 || 14 | 15 |   ...   | 22 |

Similar works:


«Fugitive Pleasure and the Meaningful Life: Nietzsche on Nihilism and Higher Values Paul Katsafanas Forthcoming in Journal of the American Philosophical Association Penultimate draft In an early text, Nietzsche tells us that philosophers have a distinctive and undeniably exalted role: their “proper task” is “to be lawgivers as to the measure, stamp and weight of things” (UM III.3).1 Not particular things, though: Nietzsche does not imagine philosophers assessing the value of apples and...»

«Characterization of the Roles of TopoIIIα-RMI1 in Maintaining Genome Integrity by Jay Tun-Chieh Yang A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Graduate Department of Biochemistry University of Toronto © Copyright by Jay Tun-Chieh Yang (2012) Characterization of the roles of TopoIIIα-RMI1 in maintaining genome integrity Doctor of Philosophy, 2012; Jay Tun-Chieh Yang; Department of Biochemistry, University of Toronto Abstract Bloom syndrome...»

«LOCAL UNDERSTANDING AND PRACTICES RELATED TO IMCI INTERVENTIONS IN EASTERN TANZANIA INAUGURALDISSERTATION Zur Erlangung der Würde eines Doktor der Philosophie Vorgelegt der Philosophisch-Naturwissenschaflichen Fakultät Der Universtät Basel von Charles Chrisostom Mayombana aus Ngara, Tanzania Basel, September 2004 Genehmigt von der Philosophish-Naturwissenschaftlichen Fakultät der Universität Basel auf Antrag von Herrn Prof. Dr. Marcel Tanner, PD Dr. Brigit Oberist und Dr. Don de Savigny...»

«Journal of Philosophy of Life Vol.3, No.1 (January 2013):44-67 A Coleridgean Account of Meditative Experience Peter Cheyne* Abstract This paper presents an exploratory account of contemplation and meditative experience as found in Coleridge’s ‘Meditative Poems’ and in the nature writing recorded in his notebooks. In these writings, we see the importance of meditative thinking as an exercise concerned with spiritual transformation towards the true, the good, and the beautiful. Sometimes...»

«Body and Soul in Ancient Philosophy Edited by Dorothea Frede and Burkhard Reis Walter de Gruyter · Berlin · New York Contents Introduction....................................... 1 I. Presocratics Carl Huffman The Pythagorean conception of the soul from Pythagoras to Philolaus.......................................... 21 Christian Schäfer Das Pythagorasfragment des Xenophanes und die Frage nach der Kritik der...»

«Laboratory of Polymer Chemistry Department of Chemistry University of Helsinki Helsinki, Finland POLYMERIC AND HYBRID MATERIALS: POLYMERS ON PARTICLE SURFACES AND AIR-WATER INTERFACES Jukka Niskanen ACADEMIC DISSERTATION FOR THE DEGREE OF DOCTOR OF PHILOSOPHY To be presented, with the permission of the Faculty of Science of the University of Helsinki, for public criticism in Auditorium A129 of the Department of Chemistry, on April 5th 2013, at 12 o’clock noon. Helsinki 2013 Supervisor...»

«Kensington Gardens Pre-School.a place where children play, learn and laugh. 430 The Parade Kensington Gardens SA 5068 Phone : 08 8331 8068 Fax : 08 8364 6874 Email : admin@kensingtonpre.sa.edu.au Website: www. kensingtonpre.sa.edu.a POLICIES & PROCEDURES  Philosophy Statement  Leadership and Service Management Education & Care Services National Regulations Chapter 4 – Operational requirements Part 4.7: Division 2 – Policies and Procedures  Enrolment and Orientation Policy ...»

«School Travel Mode Choice Behaviour in Toronto, Canada by Raktim Mitra A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Program in Planning, Department of Geography University of Toronto © Copyright by Raktim Mitra 2011 School Travel Mode Choice Behaviour in Toronto, Canada Raktim Mitra Doctor of Philosophy Program in Planning, Department of Geography University of Toronto Abstract Interest in school transportation has emerged in response to concern...»

«Structure in Ontology – 15/11/2007 The Structure of Material Objects The theory of substrata and properties and its problems 1.2. The bundle theory and its problems 3. The theory of tropes and its problems 4. The theory of substance and its problems 5. The stuff theory and its problems The structure of the lecture on structure –This lecture on structure has a structure, and its structure completely piggy-backs (with minor modifications) on Varzi [2007], which is the best introductory...»

«Ryerson University Digital Commons @ Ryerson Theses and dissertations 1-1-2012 Sound as Signifier: Communication and Expression Through the Sound of Clothing Tala Kamea Berkes Ryerson University Follow this and additional works at: http://digitalcommons.ryerson.ca/dissertations Part of the Fashion Design Commons, and the Philosophy Commons Recommended Citation Berkes, Tala Kamea, Sound as Signifier: Communication and Expression Through the Sound of Clothing (2012). Theses and dissertations....»

«Amphiphilic Polymers: Crystallization-assisted Self-assembly and Applications in Pharmaceutical Formulation A DISSERTATION SUBMITTED TO THE FACULTY OF UNIVERSITY OF MINNESOTA BY Ligeng Yin IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Marc A. Hillmyer, Advisor April, 2013 © Ligeng Yin 2013 i Acknowledgements First and foremost, I would like to thank my advisor Prof. Marc Hillmyer. His guidance and continuous support not only helped me improve scientific...»

<<  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.