Abstracts

The following is a list of abstracts of and references to my papers, followed by addresses where they can be obtained.

10.

Tom Costello and Anna Patterson

January 1998

Quantifiers over Contexts We can reason about theories, as well as in them. Many natural phenomena can be captured by theories, often by introducing a modality, true just of the theory. Rather than treat these phenomena as the sentences true in this modality, we can treat the entire theory or modality as an object. This point of view was proposed by McCarthy, who proposed calling these reified modalities contexts.

Contexts, viewed as theories or modalities, have structural properties, and associated natural structural operations, such as union and intersection. These structural properties are most naturally captured by an algebra, reminiscent of relation or dynamic algebra , a set of operations that can be applied to contexts to form new contexts.

Thus we can have a larger space of modalities than just those that are explicitly named. We add quantifiers that range over modalities, so that we can state propositions like, ``no context with the property P exists'', or ``all contexts obey Q''. We give an axiomatization of these quantifiers which we show is complete with respect to a natural semantics.


9. Implicit programming and the Logic of Constructible Duality

Anna Patterson, PhD Thesis

January 1998

We present an investigation of duality in the traditional logical manner. We extend Nelson's symmetrization of intuitionistic logic, constructible falsity, to a self-dual logic --- constructible duality. We develop a self-dual model by considering an interval of worlds in an intuitionistic Kripke model. The duality arises through how we judge truth and falsity. Truth is judged forward in the Kripke model, as in intuitionistic logic, while falsity is judged backwards.

We develop a self-dual algebra such that every point in the algebra is representable by some formula in the logic. This algebra arises as an instantiation of a Heyting algebra into several categorical constructions. In particular, we show that this algebra is an instantiation of the Chu construction applied to a Heyting algebra, the second Dialectica construction applied to a Heyting algebra, and as an algebra for the study of recursion and corecursion. Thus the algebra provides a common base for these constructions, and suggests itself as an important part of any constructive logical treatment of duality.

Implicit programming is suggested as a new paradigm for computing with constructible duality as its formal system. We show that all the operators that have computable least fixed points are definable explicitly and all operators with computable optimal fixed points are definable implicitly within constructible duality.

Implicit programming adds a novel definitional mechanism that allows functions to be defined implicitly. This new programming feature is especially useful for programming with co-recursively defined data-types such as circular lists.


8. Implicit programming and computable optimal fixed points

Anna Patterson and Tom Costello (Stanford University)

July 1997

If a program has a unique solution then programming semantics should return that solution. Optimal fixed points represent this unique solution; that is, if the only choice is between undefined and a specific defined value then we choose the defined value. However, optimal fixed points can be uncomputable. For this reason they have been relatively underutilized.

Here we provide a method which computes the optimal fixed point when it is computable. To do this we use proofs of uniqueness in an extension of intuitionistic logic together with its associated Curry-Howard-De Bruijn isomorphism. Using this correspondence, we extract programs in a confluent strongly normalizable lambda calculus that computes the optimal fixed point of a recursively defined function. When this uniqueness proof exists, the optimal fixed point is computable.

We give several examples of where this fixed point gives intuitive answers. This new semantics is especially natural for functions on co-recursively defined data-types, like streams or circular lists.


7. A Logical Treatment of Constructible Duality

Anna Patterson (Stanford University)

March 1997

We present an investigation of duality in the traditional logical manner. We extend Nelson's symmetrization of intuitionistic logic, constructible falsity, to a self-dual logic; constructible duality. We develop a self-dual model by considering an interval of worlds in an intuitionistic Kripke model. The duality arises through how we judge truth and falsity. Truth is judged forward in the Kripke model, as in intuitionistic logic, while falsity is judged backwards, that is forward in the dual model.

We define a symmetrization of the Beth-Fitting construction which transforms an interval Kripke model in a self-dual algebra for the logic of constructible duality and back. We then show that every point in the algebra is representable by some formula in the logic.

This algebra arises as an instantiation of a pseudo-Boolean algebra into several categorical constructions. In particular, we show that this algebra is an instantiation of the $\Chu$ construction applied to a pseudo-Boolean algebra, the second Dialectica construction applied to a pseudo-Boolean algebra, and as posetal case of a suggestion by Pitts for the study of recursion and corecursion. Thus the algebra provides a common base for these constructions, and suggests itself as a necessary part of any logical treatment of constructive duality.


6. Bisimulation and Propositional Intuitionistic Logic (extended version)

Anna Patterson (Stanford University)

April 1997

The Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic suggests that $p$ implies $q$ can be interpreted as a computation that given a proof of $p$ constructs a proof of $q$. Dually, we show that every finite canonical model of $q$ contains a finite canonical model of $p$. If $q$ and $p$ are interderivable, their canonical models contain each other.

Using this insight, we are able to characterize validity in a Kripke structure in terms of {\em bisimilarity}.

Theorem 1 Let $K$ be a {\em finite} Kripke structure for propositional intuitionistic logic, then two worlds in $K$ are bisimilar if and only if they satisfy the same set of formulas.

This theorem lifts to structures in the following manner.

Theorem 2 Two finite Kripke structures $K$ and $K'$ are bisimilar if and only if they have the same set of valid formulas.

We then generalize these results to a variety of infinite structures; finite principal filter structures and saturated structures.


5. Exponentials as Projections from Paraconsistent Logics

Anna Patterson and Tom Costello (Stanford University)

February 1997

Classical or intuitionistic logic can be recaptured from a paraconsistent logic. We consider operations that map a part of $N^-$, a paraconsistent logic, to intuitionistic logic.

Girard \cite{Gir87} introduces an operator !$_l$ called an exponential, to add structural rules to linear logic\footnote{We use subscript $l$ to denote operators from linear logic.}. A formula !$_l A $ can be replicated or discarded. Thus the exponential removes the ``linearity'', the notion that assumptions should only be used once, from linear logic.

We show that a Girard exponential, that is a co-monad where ! distributes through the additive conjunction, can be added as a new operator to the logic of constructible falsity $N^-$; a conservative extension of intuitionistic logic.

This shows that we can naturally divide the exponential construction of Girard into two parts, one that deals with ``linearity'' or counting the occurrences of assumptions, and a second that captures the embedding of a intuitionistic logic in a paraconsistent logic.


4. Guilt-Free Exponentials

Anna Patterson and Tom Costello (Stanford University)

January 1997

Girard introduces an operator ! called an exponential, to add structural rules to linear logic A formula ! A can be replicated or discarded. Thus the exponential removes the ``linear'' property of linear logic.

The exponential is also used to embed intuitionistic logic in linear logic. Girard suggests that intuitionistic implication $A \iimp B$ can be represented as ! A --o B.

We suggest that these two uses can be separated. We look at how the second transformation can be carried out in $N-$ a logic which already contains all the structural rules of intuitionistic logic.

We show how exponentials arise from adding constants to the logic of constructible falsity $N-$. These two new units complete $N-$, in the sense that there is a representation theorem for $N-$ with these additional units onto $H \times H^{op}$ where $H$ is a Heyting algebra.


3. Bisimulation and Propositional Intuitionistic Logic

Anna Patterson (Stanford University)

June 1996

Brouwer suggests that $p \iimp q$ can be interpreted as a computation that given a proof of $p$ constructs a proof of $q$. Dually we can see this as saying that every counter model of $q$ contains a counter model of $p$. However, what does it mean to contain another Kripke structure? We read this as: every counter model of $q$ contains a substructure that is bisimilar to a counter model of $p$.

If $q$ and $p$ are interderivable, then the counter models contain each other. Thus we study {\em bisimulation} as a way of studying interderivability. Using bisimulation, we are able to characterize validity in a Kripke structure.

Theorem 1: Let $K$ be a finite Kripke structure for propositional intuitionistic logic, then two worlds in $K$ are bisimilar if and only if they satisfy the same set of formulas.

This theorem lifts to structures in the following manner.

Theorem 2: Two finite Kripke structures $K$ and $K'$ are bisimilar if and only if they have the same set of valid formulas.

This correspondence exists also for finite principal filter structures and saturated structures.


2. A new semantics for constructible falsity

Anna Patterson (Stanford University)

March 1996

Constructive mathematics preserves the symmetry of Boolean logic's two truth values when it allows a proposition to be undecided: ``could be either true or false''. Intuitionistic logic destroys this symmetry by focusing on truth and offering only a nonconstructive ``negation as failure'', $\sim \! p = p \iimp \bot$. Nelson's system $N$[1] of constructible falsity restores symmetry to intuitionistic logic with an involutory {\em strong} negation $\lnot p$ asserting the actual falsity of $p$. (cf. Zaslavski\v{\i}[3] for another symmetrization.) Thomason[2] proposes a Kripke structure interpretation with three truth values for which he shows that $N$ is sound and complete.

We give a Kripke model having only two truth values for which we show that $N$ is sound and complete. Truth is defined on intervals $(w_t, w_f)$ in the Kripke structure such that $w_f$ is accessible from $w_t$. Truth is judged from one end $w_t$, falsity from the other $w_f$. A formula $\varphi$ holds at an interval if and only if it holds at all non-trivial subintervals. We interpret strong negation as dualizing the Kripke structure with respect to both truth and accessibility.

1. Abstraction and Modularity Mechanisms for Concurrent Computing,

G. Agha and S. Fr\olund and W. Kim and R. Panwar A. Patterson and D. Sturman

March 1993


0. An Actor formalism for open concurrent systems

R.K.Shyamasundar and A. Patterson and G. Agha (University of Illinois Champaign-Urbana)

November 1991

This paper describes a universal model of concurrent computation based on an Actor formalism. Apart from the usual actor primitives, namely, branching, message send, actor creation, and local state change, we introduce a hierarchical structuring operator called {\it hibernate}. We formally describe the transitional semantics of a kernel actor language extended with the hibernate operator. The hibernate operator provides structuring capabilities for an asynchronous formalism which are similar to those provided by restriction (or hiding) in port-based synchronous communication formalisms. The operator also provides a way to realize multi-party interactions such as broadcasts. Our formalism uses the distributed name generation scheme of actors; it thus avoids problems of scope intrusion and extrusion which occur in other models of concurrency. The formalism is illustrated by means of some examples including two embeddings of the call-by-name $\lambda$-calculus, respectively, lazy and with futures, and an example of multi-party interaction in a group of cooperating robots. Finally, we compare the proposed model with the chemical abstract machine model and discuss some open problems.